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.