Weakly Relational Numerical Abstract Domains

`THESE pr´esent´ee a` ´l’ECOLE POLYTECHNIQUE pour l’obtention du titre de ´DOCTEUR DE L’ECOLE POLYTECHNIQUE EN INFORMATIQUE ´Antoine MINE 6 d´ecembre 2004 Domaines num´eriques abstraits faiblement relationnels Weakly Relational Numerical Abstract Domains Pr´esident: Chris Hankin Professeur, Imperial College, Londres Rapporteurs: Roberto Giacobazzi Professeur, Universita` degli Studi di Verona Helmut Seidl Professeur, Technische Universitat Munchen¨ ¨ Examinateur: Nicolas Halbwachs Directeur de recherche CNRS, VERIMAG, Grenoble Directeur de th`ese: Patrick Cousot ´Professeur, Ecole Normale Sup´erieure, Paris ´Ecole Normale Sup´erieure D´epartement d’InformatiquecAntoine Min´e, 2004. ´Cette recherche a ´et´e conduite `a l’Ecole Normale Sup´erieure de Paris durant un contrat d’allocationcoupl´ee(normalien)del’Universit´eParisIXDauphine. Cetterecherchea´et´efi- nanc´eeenpartieparlesprojetsDaedalus(projeteurop´eenIST-1999-20527duprogramme ´FP5) et Astree (projet franc¸ais RNTL). Lesopinionspr´esent´eesdanscedocumentsontcellespropresdesonauteuretnerefl`etenten ´ ´aucun cas celles de l’Ecole Polytechnique, de l’Universit´e Parix IX Dauphine, ou de l’Ecole Normale Sup´erieure de Paris.´ ´RESUME iii R´esum´e Le sujet de cette th`ese est le d´eveloppement de m´ethodes pour l’ana- lyse automatique des programmes informatiques. Une des applications majeures est la conception d’outils pour d´ecouvrir les erreurs de pro- grammation avant qu’elles ne se produisent, ce qui est crucial `a l’heure ou` des tˆaches critiques mais complexes sont confi´ees `a des ordinateurs. Nous nous pla¸cons dans le cadre de l’interpr´etation abstraite, qui est une th´eorie de l’approximation surˆ e des s´emantiques de programmes, et nous nous int´eressons en particulier aux domaines num´erique abstraits sp´ecialis´es dans la d´ecouverte automatique des propri´et´es des variables num´erique d’un programme. Danscetteth`ese,nousintroduisonsplusieursnouveauxdomainesnum´e- riques abstraits et, en particulier, le domaine des zones (permettant de d´ecouvrirdesinvariantsdelaformeX−Y ≤c),deszonesdecongruence (X ≡Y +a[b])etdesoctogones(±X±Y ≤c).Cesdomainessontbas´es sur les concepts existants de graphe de potentiel, de matrice de diff´e- rences born´ees et sur l’algorithmique des plus courts chemins. Ils sont interm´ediaires, en terme de pr´ecision et de coutˆ , entre les domaines non relationnels (tel celui des intervalles), tr`es peu pr´ecis, et les domaines relationnels classiques (tel celui des poly`edres), tr`es coutˆ eux. Nous les nommons « faiblement relationnels ». Nous pr´esentons ´egalement des m´ethodes permettant d’appliquer les domaines relationnels `a l’analyse denombres`avirguleflottante,jusqu’a`pr´esentuniquementr´ealisablepar des domaines non relationnels donc peu pr´ecis. Enfin, nous pr´esentons des m´ethodes g´en´eriques dites de « lin´earisation » et de « propagation de constantes symboliques » permettant d’am´eliorer la pr´ecision de tout domaine num´erique, pour un surcouˆt r´eduit. ´Lesm´ethodesintroduitesdanscetteth`eseont´et´eint´egr´ees`aAstree,un analyseur sp´ecialis´e dans la v´erification de logiciels embarqu´es critiques etsesontr´ev´el´eesindispensablepourprouverl’absenced’erreurs`al’ex´e- cutiondelogicielsdecommandede vol´electriquepourlesavionsAirbus A340etA380.Cesr´esultatsexp´erimentauxviennentjustifierl’int´erˆetde nos m´ethodes pour des cadres d’applications r´eelles. Antoine Mine´ Ph. D. – Weakly Relational Numerical Abstract Domains´ ´iv RESUME Th`ese – Domaines num´eriques abstraits faiblement relationnels Antoine Mine´ABSTRACT v Abstract The goal of this thesis is to design techniques related to the automatic analysisofcomputerprograms. Onemajorapplicationisthecreationof 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 no- tions 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 in- terval domain), that are very imprecise, and classical relational domains (suchasthepolyhedrondomain),thatareverycostly. Wewillcallthem “weaklyrelational”. Wealsointroducesomemethodstoapplyrelational domains to the analysis of floating-point numbers, which was previously only possible using imprecise, non-relational domains. Finally, we in- troduce 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 As- ´tree,ananalyserforcriticalembeddedsoftware,andwereinstrumental inprovingtheabsenceofrun-timeerrorsinfly-by-wiresoftwaresusedin Airbus A340 and A380 planes. Experimental results show the usability of our methods in the context of real-life applications. Antoine Mine´ Ph. D. – Weakly Relational Numerical Abstract Domainsvi ABSTRACT Th`ese – Domaines num´eriques abstraits faiblement relationnels Antoine Mine´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 en- lightening way of Abstract Interpretation, and then, allowed me to join him in the search for better abstractions. He man- aged 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: Astree was at the same time a practical experiment and a theory- stressing challenge. It funnelled my passion for programming in a way supple- menting my theoretical research. Its astounding and repeated successes strength- ened my faith in times of disillusionment. I would like to thank all the members of the“magic team”for sharing with me this experience: Bruno Blanchet, Patrick Cousot, Radhia Cousot, J´erˆome Feret, Laurent Mauborgne, David Monniaux, and Xavier Rival An additional acknowledgment goes to Bruno and Patrick for their ´proof-reading of this thesis. The Astree project would not have been possible without the support and the trust from Famantanantsoa Randimbivololona and JeanSouyrisatAirbus. Iamgladtheyactuallydidbuyusthepromiseddinner I `emealso thank the bakers at the“Boulange V ”, the official sandwich supplier for the “magicteam” Ishallnotforgettothankmyestimatedcolleguesandfriendsfrom Radhia’s“sister team”: Charles Hymans, Francesco Logozzo, Damien Mass´e, ´and Elodie-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`ele. Last but not least, I wish to thank C´ecile; she was always supporting and never resented my days and nights spent in front of the computer... Antoine Mine´ Ph. D. – Weakly Relational Numerical Abstract Domainsviii ACKNOWLEDGMENTS Th`ese – Domaines num´eriques abstraits faiblement relationnels Antoine Mine´CONTENTS ix Contents Title Page . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . i R´esum´e . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . iii Abstract . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . v Acknowledgments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . vii Table of Contents . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ix 1 Introduction 1 1.1 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.2 Key Concepts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.3 Overview of the Thesis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.4 Our Contribution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 2 Abstract Interpretation of Numerical Properties 5 2.1 General Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.2 Abstract Interpretation Primer . . . . . . . . . . . . . . . . . . . . . . . . . 8 2.2.1 Galois Connection Based Abstract Interpretation . . . . . . . . . . . 8 2.2.2 Concretisation-Based Abstract Interpretation . . . . . . . . . . . . . 11 2.2.3 Partial Galois Connections . . . . . . . . . . . . . . . . . . . . . . . 11 2.2.4 Fixpoint Computation . . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.2.5 Chaotic Iterations . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 2.2.6 Reduced Product . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 2.2.7 Related Work in Abstract Interpretation Theory . . . . . . . . . . . 20 2.3 The Simple Language . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 2.3.1 Language Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 2.3.2 Concrete Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 2.3.3 A Note on Missing Features . . . . . . . . . . . . . . . . . . . . . . . 26 2.4 Discovering Properties of Numerical Variables . . . . . . . . . . . . . . . . . 26 2.4.1 Numerical Abstract Domains . . . . . . . . . . . . . . . . . . . . . . 27 2.4.2 Abstract Interpretor . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2.4.3 Fall-Back Transfer Functions . . .