Domaines numériques abstraits faiblement relationnels - PDF

Description
THÈSE présentée à l ÉCOLE POLYTECHNIQUE pour l obtention du titre de DOCTEUR DE L ÉCOLE POLYTECHNIQUE EN INFORMATIQUE Antoine MINÉ 6 décembre 2004 Domaines numériques abstraits faiblement relationnels

Please download to get full document.

View again

of 242
All materials on our website are shared by users. If you have any questions about copyright issues, please report us to resolve them. We are always happy to assist you.
Information
Category:

Religion & Spirituality

Publish on:

Views: 25 | Pages: 242

Extension: PDF | Download: 0

Share
Transcript
THÈSE présentée à l ÉCOLE POLYTECHNIQUE pour l obtention du titre de DOCTEUR DE L ÉCOLE POLYTECHNIQUE EN INFORMATIQUE Antoine MINÉ 6 décembre 2004 Domaines numériques abstraits faiblement relationnels Weakly Relational Numerical Abstract Domains Président: Rapporteurs: Examinateur: Directeur de thèse: Chris Hankin Professeur, Imperial College, Londres Roberto Giacobazzi Professeur, Università degli Studi di Verona Helmut Seidl Professeur, Technische Universität München Nicolas Halbwachs Directeur de recherche CNRS, VERIMAG, Grenoble Patrick Cousot Professeur, École Normale Supérieure, Paris École Normale Supérieure Département d Informatique c, Cette recherche a été conduite à l École Normale Supérieure de Paris durant un contrat d allocation couplée (normalien) de l Université Paris IX Dauphine. Cette recherche a été financée en partie par les projets Daedalus (projet européen IST du programme FP5) et Astrée (projet français RNTL). Les opinions présentées dans ce document sont celles propres de son auteur et ne reflètent en aucun cas celles de l École Polytechnique, de l Université Parix IX Dauphine, ou de l École Normale Supérieure de Paris. RÉSUMÉ iii Résumé Le sujet de cette thèse est le développement de méthodes pour l analyse automatique des programmes informatiques. Une des applications majeures est la conception d outils pour découvrir les erreurs de programmation avant qu elles ne se produisent, ce qui est crucial à l heure où des tâches critiques mais complexes sont confiées à des ordinateurs. Nous nous plaçons dans le cadre de l interprétation abstraite, qui est une théorie de l approximation sûre des sémantiques de programmes, et nous nous intéressons en particulier aux domaines numérique abstraits spécialisés dans la découverte automatique des propriétés des variables numérique d un programme. Dans cette thèse, nous introduisons plusieurs nouveaux domaines numériques abstraits et, en particulier, le domaine des zones (permettant de découvrir des invariants de la forme X Y c), des zones de congruence (X Y +a [b]) et des octogones (±X ±Y c). Ces domaines sont basés sur les concepts existants de graphe de potentiel, de matrice de différences bornées et sur l algorithmique des plus courts chemins. Ils sont intermédiaires, en terme de précision et de coût, entre les domaines non relationnels (tel celui des intervalles), très peu précis, et les domaines relationnels classiques (tel celui des polyèdres), très coûteux. Nous les nommons «faiblement relationnels». Nous présentons également des méthodes permettant d appliquer les domaines relationnels à l analyse de nombres à virgule flottante, jusqu à présent uniquement réalisable par des domaines non relationnels donc peu précis. Enfin, nous présentons des méthodes génériques dites de «linéarisation» et de «propagation de constantes symboliques» permettant d améliorer la précision de tout domaine numérique, pour un surcoût réduit. Les méthodes introduites dans cette thèse ont été intégrées à Astrée, un analyseur spécialisé dans la vérification de logiciels embarqués critiques et se sont révélées indispensable pour prouver l absence d erreurs à l exécution de logiciels de commande de vol électrique pour les avions Airbus A340 et A380. Ces résultats expérimentaux viennent justifier l intérêt de nos méthodes pour des cadres d applications réelles. Ph. D. Weakly Relational Numerical Abstract Domains iv RÉSUMÉ Thèse Domaines numériques abstraits faiblement relationnels ASTRACT v Abstract The goal of this thesis is to design techniques related to the automatic analysis of computer programs. One major application is the creation of tools to discover bugs before they actually happen, an important goal in a time when critical yet complex tasks are performed by computers. We will work in the Abstract Interpretation framework, a theory of sound approximation of program semantics. We will focus, in particular, on numerical abstract domains that specialise in the automatic discovery of properties of the numerical variables of programs. In this thesis, we introduce new numerical abstract domains: the zone abstract domain (that can discover invariants of the form X Y c), the zone congruence domain (X Y + a [b]), and the octagon domain (±X ± Y c), among others. These domains rely on the classical notions of potential graphs, difference bound matrices, and algorithms for the shortest-path closure computation. They are in-between, in terms of cost and precision, between non-relational domains (such as the interval domain), that are very imprecise, and classical relational domains (such as the polyhedron domain), that are very costly. We will call them weakly relational. We also introduce some methods to apply relational domains to the analysis of floating-point numbers, which was previously only possible using imprecise, non-relational domains. Finally, we introduce so-called linearisation and symbolic constant propagation generic methods to enhance the precision of any numerical domain, for only a slight increase in cost. The techniques presented in this thesis have been integrated within Astrée, an analyser for critical embedded software, and were instrumental in proving the absence of run-time errors in fly-by-wire softwares used in Airbus A340 and A380 planes. Experimental results show the usability of our methods in the context of real-life applications. Ph. D. Weakly Relational Numerical Abstract Domains vi ASTRACT Thèse Domaines numériques abstraits faiblement relationnels ACKNOWLEDGMENTS vii Acknowledgments First of all, I would like to thank deeply my Professor and Ph. D. adviser, Patrick Cousot. He introduced me to the field of program semantics through the rewarding and enlightening way of Abstract Interpretation, and then, allowed me to join him in the search for better abstractions. He managed to protect my autonomy while supporting my work. Patrick has always had the most respect for his students, considering them as his peer researchers During my thesis, I had the rare opportunity to work on a thrilling group project: Astrée was at the same time a practical experiment and a theorystressing challenge. It funnelled my passion for programming in a way supplementing my theoretical research. Its astounding and repeated successes strengthened my faith in times of disillusionment. I would like to thank all the members of the magic team for sharing with me this experience: runo lanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, David Monniaux, and Xavier Rival An additional acknowledgment goes to runo and Patrick for their proof-reading of this thesis. The Astrée project would not have been possible without the support and the trust from Famantanantsoa Randimbivololona and Jean Souyris at Airbus. I am glad they actually did buy us the promised dinner I also thank the bakers at the oulange Vème, the official sandwich supplier for the magic team I shall not forget to thank my estimated collegues and friends from Radhia s sister team : Charles Hymans, Francesco Logozzo, Damien Massé, and Élodie-Jane Sims A well-balanced live cannot include only work and I found also much support during my off-line time. This is why I would like to thank my parents and all my sisters: Judith, Garance, and Manuèle. Last but not least, I wish to thank Cécile; she was always supporting and never resented my days and nights spent in front of the computer... Ph. D. Weakly Relational Numerical Abstract Domains viii ACKNOWLEDGMENTS Thèse Domaines numériques abstraits faiblement relationnels CONTENTS ix Contents Title Page i Résumé iii Abstract v Acknowledgments vii Table of Contents ix 1 Introduction Motivation Key Concepts Overview of the Thesis Our Contribution Abstract Interpretation of Numerical Properties General Definitions Abstract Interpretation Primer Galois Connection ased Abstract Interpretation Concretisation-ased Abstract Interpretation Partial Galois Connections Fixpoint Computation Chaotic Iterations Reduced Product Related Work in Abstract Interpretation Theory The Simple Language Language Syntax Concrete Semantics A Note on Missing Features Discovering Properties of Numerical Variables Numerical Abstract Domains Abstract Interpretor Fall-ack Transfer Functions Non-Relational Abstract Domains Overview of Existing Numerical Abstract Domains The Interval Abstract Domain Ph. D. Weakly Relational Numerical Abstract Domains x CONTENTS The Polyhedron Abstract Domain The Need for Relational Domains Other Applications of Numerical Abstract Domains The Zone Abstract Domain Introduction Constraints and Their Representation Constraints Representations Lattice Structure Canonical Representation Emptiness Testing Closure Operator Closure Algorithms Incremental Closure Set-Theoretic Operators Equality Testing Inclusion Testing Union Abstraction Intersection Abstraction Conversion Operators Conversion etween Zones and Intervals Conversion etween Zones and Polyhedra Transfer Functions Forget Operator Assignment Transfer Function Test Transfer Functions ackwards Assignment Transfer Function Extrapolation Operators Widenings Interaction between the Closure and our Widenings Narrowings Cost Considerations Ways to close Hollow Representation Conclusion The Octagon Abstract Domain Introduction Modified Representation Octagonal Constraints Encoding Coherence Lattice Structure Thèse Domaines numériques abstraits faiblement relationnels CONTENTS xi 4.3 Modified Closure Algorithms Emptiness Testing Strong Closure Floyd Warshall Algorithm for Strong Closure Incremental Strong Closure Algorithm Integer Case Operators and Transfer Functions Adapted Set-Theoretic Operators Adapted Forget Operator Adapted Conversion Operators Adapted Transfer Functions Adapted Extrapolation Operators Alternate Octagon Encodings Efficient Representation Adapted Hollow Form Analysis Examples Decreasing Loop Absolute Value Rate Limiter Related Works and Extensions Conclusion A Family of Zone-Like Abstract Domains Introduction Constraint Matrices Representing Constraints Previous Work on Closed Half-Rings Acceptable ases Adapted Closure Algorithm Galois Connection Operators and Transfer Functions Set-Theoretic Operators Forget and Projection Operators Transfer Functions Extrapolation Operators Instance Examples Translated Equality Retrieving the Zone Domain Zones With Strict Constraints Integer Congruences Rational Congruences Unacceptable ases Ph. D. Weakly Relational Numerical Abstract Domains xii CONTENTS 5.5 Conclusion Symbolic Enhancement Methods Introduction Linearisation Interval Linear Forms Interval Linear Form Operators From Expressions to Interval Linear Forms Multiplication Strategies From Expressions to Quasi-Linear Forms Extending Numerical Expressions Symbolic Constant Propagation Motivation Symbolic Constant Propagation Domain Interaction With a Numerical Abstract Domain Substitution Strategies Cost Considerations Interval Linear Form Propagation Domain Comparison with Relational Abstract Domains Conclusion Analysis of Machine-Integer and Floating-Point Variables Introduction Modeling Machine-Integers Modified Syntax and Concrete Semantics Adapted Abstract Semantics Analysis Example Using Machine-Integers in the Abstract Using Regular Arithmetics Using Saturated Arithmetics Modeling IEEE 754 Floating-Point Numbers IEEE 754 Representation IEEE 754 Computation Model Linearising Floating-Point Expressions Analysis Example Using Floating-Point Numbers in the Abstract Floating-Point Interval Analysis Floating-Point Linearisation Floating-Point Zone and Octagon Domains Convergence Acceleration Conclusion Thèse Domaines numériques abstraits faiblement relationnels CONTENTS xiii 8 Application to the Astrée Static Analyser Introduction Presentation of Astrée Scope of the Analyser History of the Analyser Design by Refinement rief Description Implementation Analysis Steps Abstract Domains Partitioning Techniques Integrating the Octagon Abstract Domain Implementation Choices Octagon Packing Analysis Results Integrating the Symbolic Constant Propagation Implementation Choices Analysis Results Extrapolation Operators Conclusion Conclusion 249 A Lengthy Proofs 253 A.1 Proof of Thm : Strong Closure Algorithm for Octagons A.2 Proof of Thm : Closure Algorithm for Constraint Matrices ibliography List of Figures List of Definitions List of Theorems List of Examples Index Index of Symbols Ph. D. Weakly Relational Numerical Abstract Domains xiv CONTENTS Thèse Domaines numériques abstraits faiblement relationnels Chapter 1: Introduction 1 Chapter 1 Introduction 1.1 Motivation Since the birth of computer science, writing correct programs has always been considered a great challenge. Generally, much more time and effort is needed to hunt down and eliminate bugs, that is, unintentional programming errors, than to actually write programs. As we rely more and more on software, the consequences of a bug are more and more dramatic, causing great financial and even human losses. Moreover, software complexity seems to follow Moore s law and grow exponentially with time, making them harder and harder to debug. Two extreme examples are the overflow bug that caused the failure of the Ariane 5 launcher in 1996 [ea96] and the cumulated imprecision errors in a Patriot missile ense that caused it to miss its Scud missile target, resulting in 28 people being killed in 1992 [Ske92]. In order to ensure the correctness of programs, one massively used technique is testing. As only a few sample program behaviors can actually be observed, testing methods easily leave bugs. Also, testing does not seem to catch up with the software complexity explosion: it becomes more and more costly while giving worse and worse results. Formal methods, on the other hand, try to address these problems by providing mathematically sound techniques that guarantee a full coverage of all program behaviors while relying on symbolic as opposed to explicit representations to achieve efficiency. In this thesis, we wish to contribute to the field of formal methods used in the verification of the correctness of programs. 1.2 Key Concepts Program Semantics. Semantics is the branch of computer science devoted to associating a mathematical meaning to computer programs, thus allowing formal reasoning about programs and their properties. Such formal methods grounded on program semantics should be distinguished from purely empirical or statistical methods. Ph. D. Weakly Relational Numerical Abstract Domains 2 Chapter 1: Introduction Static Analysis. Static Analysis is devoted to the conception of analysers, that is, programs able to discover properties of programs at compile-time. Unlike testing, debugging, or profiling, static analysers do not need to actually run the analysed program; they can reason about infinite sets of unbounded computations in arbitrary contexts at once. Moreover, a static analyser should preferably always terminate and its computation time should be more or less predictable. y Rice s theorem [Ric53], any property on the outcome of a program that is not always true for all programs or false for all programs which includes every single interesting property is undecidable, so, a perfect static analyser cannot exist. All static analysers will thus make approximations, one way or another. A sound static analyser is one for which approximations do not compromise the truth of its result: it can output either a inite yes meaning that the property is indeed true regardless of approximations or I don t know meaning that the approximations prevent the analyser from issuing a inite answer. Abstract Interpretation. Abstract Interpretation [CC77, CC92b] is a general theory of the approximations of program semantics. It allows, among other applications, designing static analyses that are sound by construction. A core concept is that of abstract domain, that is, a class of properties together with a set of operators to manipulate them allowing, in conjunction with the abstract interpretation framework, the design of a static analyser for this class of properties. Each abstract domain embeds some sort of approximation. There does not exist a single, all-purpose, abstract domain: abstract domains must be chosen depending on the properties that need to be inferred, but also the language constructs that are used in the analysed program and the amount of computing resources available for the static analysis. However, an abstract domain is not tied to one particular program but to a whole class of programs as it generally embeds an infinite set of properties. Advantages over Other Formal Methods. Unlike other formal methods for reasoning on programs, once an abstract domain is designed, the static analysis performs fully automatically and directly on the source code. This is to be compared to model-checking that requires the user to construct by hand a generally finite model for each new program to be analysed and theorem-proving that often requires much user assistance during the proof generation. Numerical Properties. The focus of this thesis is the numerical properties of the variables of a program. Such properties allow answering questions of the form: Can there be a division by zero?, Can this computation exceed the digit capacity of the computer?, Can this array index exceed the array bounds?. They have quite a lot of applications in program verification and optimisation. All numerical properties, except the simplest ones, are undecidable. Weakly Relational Numerical Abstract Domains. Numerical abstract domains focus on the properties of the numerical program variables. Relational domains are able to Thèse Domaines numériques abstraits faiblement relationnels 1.3 Overview of the Thesis 3 express relationships between variables, that is, arithmetic properties involving several variables at a time, such as X=Y+Z. Classical relational domains are more precise but also much more costly than non-relational ones. The subject of this thesis is the introduction of new relational numerical abstract domains that are in-between, in terms of precision and cost, between existing non-relational and relational domains. As each introduced domain can be seen as the restriction, with respect to the properties expressed, of an existing relational domain, we call them weakly relational. The algorithms underlying these new domains are, however, quite different and allow a reduced time and memory consumption. 1.3 Overview of the Thesis This thesis is organised as follows. Chap. 2 recalls the formal framework of Abstract Interpretation and its application to the design of static analyses for the numerical properties of programs. The construction of a generic static analyser, parametrised by a numerical abstract domain, for a simple programming language called Simple is presented. It will serve throughout the thesis to illustrate our newly introduced abstract domains. Chap. 3 then introduces our first weakly relational abstract domain: the domain of zones that allows discovering invariants of the form ±X c and X Y c, where X and Y are program variables and c is a constant in Z, Q, or R. Then, Chap. 4 presents the octagon abstract domain that extends the zone abstract domain in order to discover invariants of the form ±X ± Y c. Chap. 5 proposes another generalisation of the zone abstract domain that allows representing invariants of the form X Y S where S lives in a non-relational abstraction. We will present several instances of this abstract domain family. One of particular interest is the zone congruence domain that can infer invariants of the form X Y + c [d]. Another example is the strict zone domain that can infer invariants of the form X Y c. Chap. 6 presents two generic techniques that can be applied to improve the pr
Related Search
Similar documents
View more...
We Need Your Support
Thank you for visiting our website and your interest in our free products and services. We are nonprofit website to share and download documents. To the running of this website, we need your help to support us.

Thanks to everyone for your continued support.

No, Thanks