Improving the results of static analyses of programs by local decreasing iterations

Abstract

We present a new technique conceived for improving the accuracy of the results of static analyses of programs (such as constant propagation, range analysis, etc.). It relies on and complements the classical lattice-theoretic model for abstract interpretation [4], and is therefore defined at a very general level, although it applies only to analyses on numbers in this paper. The idea consists in embedding local decreasing iterations in the (global) iteration stage of the analysis; by local iterations, we mean that they correspond to some special control points of the program and not to the whole program to be analyzed. Special techniques dedicated to static analyses on numbers are developed to take full advantage of the method, which allows, in practice, to handle more efficiently conditional branches, assignments in backwards analysis, combinations of static analysis frameworks, and to combine abstract interpretation and symbolic evaluation. Several examples show that it may significantly improve the analysis results.