An Abstract Domain for Analyzing Heap-Manipulating Low-Level Software

We describe an abstract domain for representing useful invariants of heap-manipulating programs (in presence of recursive data structures and pointer arithmetic) written in languages like C or low-level code. This abstract domain allows representation of must and may equalities among pointer expressions. The integer variables used in pointer expressions can be quantified existentially or universally and can have constraints over some base domain. We allow quantification of a special form, namely $\exists \forall$ quantification. This choice was made to balance expressiveness with efficient automated deduction. The existential quantification is over some dummy non-program variables, which are automatically made explicit by our analysis to express useful program invariants. The universal quantifier is used to express properties of collections of memory locations. Our abstract interpreter automatically computes invariants about programs over this abstract domain. We present initial experimental results demonstrating the effectiveness of this abstract domain on some common coding patterns.