Symbolically Computing Most-Precise Abstract Operations for Shape Analysis
Greta Yorsh, Thomas Reps and Mooly Sagiv
Shape analysis concerns the problem of determining ``shape invariants''
for programs that perform destructive updating on dynamically
allocated storage.
This paper presents a new algorithm that takes as input
an abstract value
(a 3-valued logical structure describing some set of concrete stores X)
and a precondition p, and computes the most-precise abstract value
for the stores in X that satisfy p.
This algorithm solves several open problems in shape analysis:
(i) computing the most-precise abstract value of a set of concrete
stores specified by a logical formula;
(ii) computing best transformers for atomic program statements and
conditions;
(iii) computing best transformers for loop-free code fragments (i.e.,
blocks of atomic program statements and conditions);
(iv) performing interprocedural shape analysis using procedure
specifications and assume-guarantee reasoning; and
(v) computing the most-precise overapproximation of the meet of two
abstract values.
The algorithm employs a decision procedure for the logic used to
express properties of data structures. A decidable logic for
expressing such properties is described in [5]. The algorithm can
also be used with an undecidable logic and a theorem prover;
termination can be assured by using standard techniques (e.g., having
the theorem prover return a safe answer if a time-out threshold is
exceeded) at the cost of losing the ability to guarantee that a
most-precise result is obtained. A prototype has been implemented in
TVLA, using the SPASS theorem prover.
(Click here to access the paper:
[PostScript;
PDF;
(c) Springer-Verlag]