Pointer Logic / Shape Analysis

Origin. Burstall's 1972 treatment of "distinct nonrepeating tree systems" is the first attempt to reason about programs that alter linked structures. Jones and Muchnick (1979, 1981) introduced the flow-analytic version, abstracting the heap by k-limiting; Chase, Wegman and Zadeck (1990) added storage shape graphs. Sagiv, Reps and Wilhelm gave the theory its general form in "Solving shape-analysis problems in languages with destructive updating" (1998) and "Parametric shape analysis via 3-valued logic" (2002), implemented as TVLA. Reynolds's separation logic (2002), developed with O'Hearn and Yang, is the deductive counterpart.

Models. The heap is a finite partial map from locations to records of fields, and the difficulty is that it is unbounded and that two syntactically distinct expressions may name the same cell. Aliasing defeats the substitution-based reasoning that works for variables, and the shape of a structure — list, tree, dag, cyclic — is a property of an unbounded graph rather than of any fixed number of cells. Shape analysis answers by abstracting the concrete heap to a finite graph in which one summary node stands for many concrete cells, and by admitting a third truth value where the abstraction cannot decide.

Formalism.

Heap model: Heap H: Loc →_fin (Field → Val). Locations with fields. Pointers as field values. Partial function.

Points-to: x ↦ y: x points to y. Basic heap fact. Field variant: x.f ↦ y.

Reachability: reach(x, y): y reachable from x. Transitive closure. Shape characterization. Path existence.

Shape predicates: list(x): x points to acyclic list. tree(x): x points to tree. dag(x): directed acyclic graph. Recursive definitions.

Separation: x ⊛ y: x and y have disjoint reachable sets. Non-aliasing. Critical for modular reasoning. Separation logic connection.

Three-valued logic: 0: definitely no. 1: definitely yes. 1/2: maybe. Information order: 0 ⊑ 1/2 and 1 ⊑ 1/2, with 0 and 1 incomparable. The definite values carry more information than the indefinite one.

Two-valued structures as stores: A concrete store is a logical structure: individuals are heap cells, unary predicates record which variable points where, binary predicates record fields. Program statements are predicate-update formulas.

Canonical abstraction: Choose a finite set of unary abstraction predicates. Merge all individuals agreeing on their values into one summary node. Predicates that disagree among the merged individuals take the value 1/2. The result is a three-valued structure of bounded size.

Instrumentation predicates: Derived predicates recorded explicitly rather than recomputed — reach, cyclicity, sharing. Needed because abstraction does not commute with definition: reach cannot be recovered from the abstracted fields.

Focus and coercion: Focus refines a structure so a chosen formula is definite, materializing a summary node into individuals. Coercion discards structures violating the integrity constraints. Together they restore precision lost by merging.

Symbols.

Metatheory. Sagiv, Reps and Wilhelm (2002) put shape analysis on a uniform footing by treating a concrete store as a two-valued logical structure and abstraction as canonical abstraction. The Embedding Theorem is the soundness result: if a first-order formula with transitive closure evaluates to a definite value in the abstract structure, it has that value in every concrete structure the abstraction embeds. Soundness therefore comes automatically for every property expressible in the language, with no separate argument per predicate — this is what makes the framework parametric. The abstract domain is finite, its size doubly exponential in the number of abstraction predicates, which yields termination of the fixpoint computation. Precision lost by merging is partly recovered by focus and coercion. Reachability is not first-order definable, so it cannot be recomputed from the abstraction and must be carried as an instrumentation predicate.

Applies to. Program analysis. Memory safety. Shape verification. Alias analysis.

Limitations. Approximation is forced, not chosen: Landi (1992) proved precise may-alias analysis undecidable for programs with dynamic allocation, and Horwitz (1997) showed the flow-insensitive version NP-hard. Canonical abstraction is finite only relative to a chosen vocabulary of abstraction predicates, and that choice decides what the analysis can prove; the theory supplies no way to find them, and a distinction the predicates cannot express is invisible to the analysis. The domain is doubly exponential in that vocabulary. Shape predicates are written per data structure, so lists, trees and dags each need their own definitions and materialization rules, and a structure outside the catalogue gets no invariant. On the deductive side, quantifier-free propositional separation logic is PSPACE-complete, and adding first-order quantification makes validity undecidable.

© 2026 Lingenic LLC