Originally published on dl.acm.org
Authors:
Bertrand Jeannet, Alexey Loginov, Thomas W. Reps and Mooly Sagiv
Abstract:
This article addresses the verification of properties of imperative programs with recursive procedure calls, heap-allocated storage, and destructive updating of pointer-valued fields, that is, interprocedural shape analysis. The article 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 overapproximation 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.