Maison Jean Kuntzmann
22 septembre 2010 - 15h00
Contributions à l’analyse statique de programmes manipulant des tableaux (Phd Defense)
par Mathias Péron de UJF / VERIMAG
Résumé : Si l'analyse automatique des accès aux tableaux a été largement
étudiée, on trouve très peu de résultats convaincants sur l'analyse
du contenu des tableaux.
Pour une telle analyse, les analyses numériques sont centrales.
Notamment, si l'on découvre l'invariant i <> j, on évite d'affaiblir
la connaissance sur a[j] lors d'une affectation à a[i]. Nous proposons
une nouvelle analyse numérique faiblement relationnelle, combinant des
contraintes de zones (x - y ≤ c ou ±x ≤ c) à des contraintes de
non-égalités (x <> y ou x <> 0). Cette analyse a une complexité en O(n4),
si les variables prennent leur valeurs dans un ensemble dense. Dans le
cas arithmétique, décider de la satisfaisabilité d'une conjonction de
telles contraintes est un problème NP-complet. Nous proposons une
analyse en O(n4) également pour ce cas.
Au cœur des analyses du contenu des tableaux on trouve aussi des
analyses de partitionnement symbolique. Pour une boucle « for i = 1 to
n », où un tableau est accédé à la cellule i, il est nécessaire de
considérer le contenu des tableaux sur les tranches [1, i - 1], [i, i]
et [i + 1, n] pour être précis. Nous définissons une analyse de
partitionnement sémantique, puis une analyse du contenu des tableaux
basée sur ses résultats. Cette dernière associe à chaque tranche T une
propriété P dont les variables représentent le contenu des tableaux
sur cette tranche. La propriété P est interprétée cellule-par-cellule,
ainsi pour T = [1, i - 1] et P = (a = b + 1) il est exprimé que
pour tout k dans [1, i - 1], a[k] = b[k] + 1.
Les résultats expérimentaux montrent que notre analyse automatique est
efficace et précise, sur une classe de programmes simples : tableaux
unidimensionnels, indexés par une variable au plus (x + c ou c),
traversés par des boucles, imbriquées ou non, avec des compteurs
suivant une progression arithmétique. Elle découvre par exemple que le
résultat d'un tri par insertion est un tableau trié, ou que durant le
parcours d'un tableau gardé par une sentinelle, tous les accès à ce
tableau sont corrects.
Jury :
Jean-Claude FERNANDEZ Université Joseph Fourier Président pressenti
Patrick COUSOT École Normale Supérieure Rapporteur
Reinhard WILHELM Universität des Saarlandes Rapporteur
Francesco LOGOZZO Microsoft Research Examinateur
Gaël MULAT MathWorks Examinateur
Mihaela SIGHIREANU Université Paris Diderot Examinateur
Nicolas HALBWACHS Centre National de la Recherche Scientifique Directeur de thèse
