2-Pointer Logic

For reasoning about properties of pointers, we consider conjunctions of equalities and dis-equalities between terms built up from address constants by addition of offsets and dereferencing. We call the resulting class of formulas 2-pointer logic. We introduce a quantitative version of congruence closure to provide polynomial time algorithms for deciding satisfiability as well as implication between formulas. By generalizing quantitative congruence closure to quantitative finite automata, we succeed in constructing canonical normal forms so that checking of equivalence between conjunctions reduces to syntactic equality. We apply our techniques to realize abstract transformers for dedicated forms of assignments via pointers, in particular, indefinite, definite and locally invertible assignments. Quantitative finite automata here allow us to restrict formulas to properties expressible by some subterm-closed subset of terms only.