*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