Viktor Kuncak and Martin Rinard. On the boolean algebra of shape analysis constraints. Technical report, MIT CSAIL, August 2003.

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.

[ bib ] Back