Set Based Analysis of Arithmetic

Set based analysis is an approach to compile-time program analysis that is based on a simple approximation: all dependencies between variables are ignored. In effect, program variables are treated as sets of values. Thus far, set based analysis techniques have focussed on dataconstructor languages. The main reason for this is algorithmic: the equality for data-constructor values is structural (that is, two values f (v 1 ; . . . ; v n ) and f 0 (v 0 1 ; . . . ; v 0 n ) are equal if and only if f and f 0 are identical constructors and v i = v 0 i , i = 1::n). This has important implications for how sets of such values can be represented during the computation of a set based analysis. In contrast, the equality theory of arithmetic is much richer. Two terms with very different structure can be equal. Correspondingly, the manipulationand representation of sets of arithmetic values is significantly more complex. In this paper we extend the ideas of set based analysis to arithmeti..