Parametric Shape Analysis via 3-Valued Logic

Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm

We present a family of abstract-interpretation algorithms that are capable of determining ``shape invariants'' of programs that perform destructive updating on dynamically allocated storage. The main idea is to represent the stores that can possibly arise during execution using three-valued logical structures.

Questions about properties of stores can be answered by evaluating predicate-logic formulae using Kleene's semantics of three-valued logic:

If a formula evaluates to true, then the formula holds in every store represented by the three-valued structure.

If a formula evaluates to false, then the formula does not hold in any store represented by the three-valued structure.

If a formula evaluates to unknown, then we do not know if this formula always holds, never holds, or sometimes holds and sometimes does not hold in the stores represented by the three-valued structure.

Three-valued logical structures are thus a conservative representation of memory stores.

The approach described is a parametric framework: It provides the basis for generating a family of shape-analysis algorithms by varying the vocabulary used in the three-valued logic.

(Click here to access the paper: PostScript, PDF.)