A Relational Approach to Interprocedural Shape Analysis
Bertrand Jeannet, Alexey Loginov, Thomas Reps, and Mooly Sagiv
This paper addresses the verification of properties of
imperative programs with recursive procedure calls,
heap-allocated storage, and destructive updating
of pointer-valued fields -- i.e., interprocedural shape analysis.
The paper makes three contributions:
-
It introduces a new method for abstracting relations
over memory configurations for use in abstract interpretation.
-
It shows how this method furnishes the elements needed for
a compositional approach to shape analysis.
In particular, abstracted relations are used to represent the
shape transformation performed by a sequence of operations,
and an over-approximation to relational composition can be
performed using the meet operation of the domain of abstracted
relations.
-
It applies these ideas in a new algorithm for context-sensitive
interprocedural shape analysis. The algorithm creates procedure
summaries using abstracted relations over memory configurations, and
the meet-based composition operation provides a way to apply the
summary transformer for a procedure P at each call site from which
P is called.
The algorithm has been applied successfully to establish properties of
both (i) recursive programs that manipulate lists, and (ii) recursive
programs that manipulate binary trees.
(Click here to access the paper:
PDF.)