Analysis of programs using arrays

L’analyse statique de programmes est un domaine crucial en compilation, en optimisation, et en validation de logiciels. Les structures de données complexes (tableaux, listes, graphes...), omniprésentes dans les programmes, posent des problèmes difficiles, du fait qu’elles représentent des ensembles de données de taille importante ou inconnue, et que l’adressage des données dans ces ensembles est calculé (indexation, indirection). La plupart des travaux sur l’analyse des structures de données concernent la vérification de la correction des accès aux données (vérification que les indices d’un tableau sont dans les bornes, que les pointeurs ne sont pas nuls, “shape analysis”). L’analyse du contenu des structures de données est encore peu abordée. A Verimag, ce domaine a été abordé récemment, et a donné lieu à de premiers résultats sur l’analyse de tableaux unidimensionnels. Une méthode d’analyse de programmes simples a été proposée [1], qui permet de découvrir des propriétés des contenus de tableaux, comme par exemple que le résultat d’un programme de tri est bien un tableau trié. Un autre type de propriétés, dites “non positionnelles” a aussi été considéré [2], qui concerne le contenu global d’un tableau, indépendamment de son rangement: par exemple, on montre que le résultat d’un tri est une permutation du tableau initial. Ces premiers résultats sont très encourageants, mais encore embryonnaires. L’objectif du travail de thèse proposé est de les étendre dans plusieurs directions. Notre analyse de propriétés positionnelles est capable de découvrir des relations point- à-point entre des “tranches” de tableaux (ensembles de cellules consécutives). Les extensions envisagées concernent les tableaux multidimensionnels, les ensembles de cellules non nécessairement consécutives, et les structures de données plus générales. Concernant les propriétés non positionnelles, les premiers résultats sont limités aux égalités de contenus de tableaux. Ils doivent être étendus à des relations plus complexes (inclusions, sommes disjointes...) et à d’autres structures de données. Ce travail prend place dans le projet ASOPT (“Analyse statique et optimisation”), accepté dans le programme Arpège de l’ANR en 2008. Références : [1] N. Halbwachs, M. Péron. Discovering properties about arrays in simple programs. ACM Conference on Programming Language Design and Implementation, PLDI 2008. Tucson (Az.), juin 2008. [2] V. Perrelle. Analyse statique du contenu de tableaux, propriétés non positionnelles. Rapport de M2R, Master Parisien de Recherche en Informatique, septembre 2008.Static analysis is key area in compilation, optimization and software validation. The complex data structures (arrays, dynamic lists, graphs...) are ubiquitous in programs, and can be challenging, because they can be large or of unbounded size and accesses are computed. (through indexing or indirections). Whereas the verification of the validity of the array accesses was one of the initial motivations of abstract interpretation, the discovery of properties about array contents was only adressed recently. Most of the analyses of array contents are based on a partitioning of the arrays. Then, they try to discover properties about each fragment of this partition. The choice of this partition is a difficult problem and each method have its flaw. Moreover, classical representations of array partitions induce an exponential complexity for these analyzes. In this thesis, we generalize the concept of array partitioning into the concept of "fragmentation" which allow overlapping fragments, handling potentially empty fragments and selecting specialized relations. On the other hand, we propose an abstraction of these fragmentations in terms of graphs called "slices diagrams" as well as the operations to manipulate them and ensuring a polynomial complexity. Finally, we propose a new criterion to compute a semantic fragmentation inspired by the existing ones which attempt to correct their flaws. These methods have been implemented in a static analyzer. Experimentations shows that the analyzer can efficiently and precisly prove some challenging exemples in the field of static analysis of programs manipulating arrays