Verimag

bibtex

@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. },
}

URL

PDF

Publication Sections


Contact | Site Map | Site powered by SPIP 3.0.25 + AHUNTSIC [CC License]

info visites 777236