@phdthesis{P\'10,
title = { Contributions \`a l'analyse statique de programmes manipulant des tableaux },
author = {P\'eron, Mathias},
month = {septembre},
year = {2010},
school = {Universit\'e de Grenoble},
team = {SYNC},
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 a property
whose variables stand for the arrays contents of the slice. The properties are interpreted pointwise
on the slice. So for = [1, i - 1] and = (a = b + 1), it means that [1, i - 1], a[ ] = b[ ] + 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. },
}
