Pointer Logic / Shape Analysis

Origin. Reynolds (1970s), Sagiv-Reps-Wilhelm. Heap reasoning. Points-to analysis. Shape graphs. Foundation for heap verification.

Models. Heap cells and pointers. Reachability predicates. Shape invariants. Alias analysis. Memory safety.

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. Abstract interpretation.

Summary nodes: Represent multiple concrete nodes. Abstraction for unbounded structures. Materialization/folding. Finite abstraction.

Symbols.

Metatheory. Heap abstraction. Shape analysis. Pointer tracking. Three-valued.

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

Limitations. Precision-scalability tradeoff. Complexity. Approximation. Specific structures.