A Generic Framework for Interprocedural Analysis of Numerical Properties

Abstract. Relations among program variables like 1 + 3 · x1 + 5 · x2 ≡ 0 [224] have been called linear congruence relations. Such a relation is valid at a program point iff it is satisfied by all reaching program states. Knowledge about non-trivial valid congruence relations is crucial for var-ious aggressive program transformations. It can also form the backbone of a program correctness proof. In his seminal paper [1], Philippe Granger presents an intraprocedural analysis which is able to infer linear congruence relations between integer variables. For affine programs, i.e., programs where all assignments are affine expressions and branching is non-deterministic, Granger’s analysis is complete, i.e., infers all valid congruence relations between variables. No upper bound, though, has been proven for Granger’s algorithm. Here, we present a variation of Granger’s analysis which runs in polynomial time. Moreover, we provide an interprocedural extension of this algo-rithm. The polynomial algorithm as well as its interprocedural exten