Maison Jean Kuntzmann
22 September 2010 - 15h00
Contributions to the Static Analysis of Programs Handling Arrays (Phd Defense)
by Mathias Péron from UJF / VERIMAG
Abstract: Array bound checking has been widely studied. However, there are very
few convincing results about array contents analysis.
For such an analysis, numerical analyses are fundamental. In
particular, when assigning a[i], knowledge about a[j] is kept
unchanged if the invariant i <> j is discovered. We propose a new
weakly relational numerical analysis, combining potential constraints
(x - y ≤ c or ±x ≤ c) with disequalities (x <> y or x <> 0). If the
variables are valued in a dense set, the analysis runs in O(n4). In
the arithmetic case, the satisfiability problem of the conjunction of
such constraints is NP-complete. We propose an analysis with
complexity O(n4) for this case too.
In the core of array contents analyses we also find symbolic
partitioning analyses. To precisely analyze a loop “for i = 1 to n”,
in which an array is accessed at index i, slices [1, i - 1], [i, i]
and [i + 1, n] of arrays contents must be considered. We define a
semantic partitioning analysis and then an array contents analysis
based on its results. This later analysis binds to each slice S a
property P whose variables stand for the arrays contents of the
slice. The properties P are interpreted pointwise on the slice. So for
S = [1, i - 1] and P = (a = b + 1), it means that for all k in
[1, i - 1], a[k] = b[k] + 1.
Experimental results show that our automatic analysis is efficient and
precise on simple programs: one-dimensional arrays, indexed by one
variable at most (x + c or c), traversed by possibly nested “for”
loops, the counters of which follow an arithmetic progression. The
analysis is able, for instance, to discover that the result of an
insertion sort is a sorted array, or that, in an array traversal
guarded by a “sentinel”, the index stays within the bounds.
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
