Interprocedural Shape Analysis with Separated Heap Abstractions

Alexey Gotsman, Josh Berdine, and Byron Cook

Abstract

We describe an interprocedural shape analysis that makes use of spatial locality (i.e. the fact that most procedures modify only a small subset of the heap) in its representation of abstract states. Instead of tracking reachability information directly and aliasing information indirectly, our representation tracks reachability indirectly and aliasing directly. Computing the effect of procedure calls and returns on an abstract state is easy because the representation exhibits spatial locality mirroring the locality that is present in the concrete semantics. The benefits of this approach include improved speed, support for programs that deallocate memory, the handling of bounded numbers of heap cutpoints, and support for cyclic and shared data structures.

Details

Publication typeInproceedings
Published inStatic Analysis, 13th International Symposium, SAS 2006, Seoul, Korea, August 29-31, 2006, Proceedings
Pages240-260
Volume4134
SeriesLecture Notes in Computer Science
ISBN3-540-37756-5
PublisherSpringer
> Publications > Interprocedural Shape Analysis with Separated Heap Abstractions