||On The Boolean Algebra of Shape Analysis Constraints
|LCS Document Number:
|Shape analysis is a promising technique for statically verifying
and extracting properties of programs that manipulate
complex data structures. We introduce a new characterization
of constraints that arise in parametric shape
analysis based on manipulation of three-valued structures
as dataflow facts.
We identify an interesting syntactic class of first-order
logic formulas that captures the meaning of three-valued
structures under concretization. This class is broader than
previously introduced classes, allowing for a greater flexibility
in the formulation of shape analysis constraints in
program annotations and internal analysis representations.
Three-valued structures can be viewed as one possible normal
form of the formulas in our class.
Moreover, we characterize the meaning of three-valued
structures under “tight concretization”. We show that the
seemingly minor change from concretization to tight concretization
increases the expressive power of three-valued
structures in such a way that the resulting constraints are
closed under all boolean operations. We call the resulting
constraints boolean shape analysis constraints.
The main technical contribution of this paper is a natural
syntactic characterization of boolean shape analysis constraints
as arbitrary boolean combinations of first-order sentences
of certain form, and an algorithm for transforming
such boolean combinations into the normal form that corresponds
directly to three-valued structures.
Our result holds in the presence of arbitrary shape analysis
instrumentation predicates. The result enables the reduction
(without any approximation) of the entailment and
the equivalence of shape analysis constraints to the satisfiability
of shape analysis constraints. When the satisfiability
of the constraints is decidable, our result implies that the
entailment and the equivalence of the constraints are also
decidable, which enables the use of constraints in a compositional
shape analysis with a predictable behavior.
|To obtain this publication:
To purchase a printed copy of this publication please contact