Region-based shape analysis with tracked locations

This paper proposes a novel approach to shape analysis: using local reasoning about individual heap locations of global reasoning about entire heap abstractions. We present an inter-procedural shape analysis algorithm for languages with destructive updates and formulate it as a dataflow analysis. The key feature is a novel memory ion that differs from traditional abstractions in two ways. First, we build the shape abstraction and analysis on pointer analysis. Second, we decompose the shape abstraction into a set of independent configurations, each of which characterizes one single heap location. Our approach: 1) leads to simpler algorithm specifications, because reasoning about the single location; 2) leads to efficient algorithms, because of the abstraction decomposition; and 3) makes it easier to develop context-sensitive, demand-driven, and incremental shape analyses. We have developed simple extensions that use the analysis results to find memory errors in programs with explicit d...

• Type: Conference
• Year: 2005
• Where: POPL
• Authors: Brian Hackett, Radu Rugina
• Keywords: Entire Heap Abstractions, Individual Heap Locations, POPL 2005, Programming Languages, Simpler Algorithm Specifications