Parametric Shape Analysis via 3-Valued Logic
Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm
Shape analysis concerns the problem of determining ``shape
invariants'' for programs that perform destructive updating on
dynamically allocated storage.
This paper presents a parametric framework for shape analysis
that can be instantiated in different ways to create different
shape-analysis algorithms that provide varying degrees of efficiency
and precision.
A key innovation of the work is that the stores that can possibly
arise during execution are represented (conservatively) using
3-valued logical structures.
The framework is instantiated in different ways by varying the
predicates used in the 3-valued logic.
The class of programs to which a given instantiation of the framework
can be applied is not limited a priori (i.e., as in some work
on shape analysis, to programs that manipulate only lists, trees,
dags, etc.);
each instantiation of the framework can be applied to any program,
but may produce imprecise results (albeit conservative ones)
due to the set of predicates employed.
[paper:
PostScript,
PDF;
talk: Powerpoint]