Error Detection using Shape Analysis with Local Reasoning

Shape analyses are static analyses aimed at extracting invariants that describe the “shapes” of dynamically allocated recursive structures. Although existing shape analyses have been successful at verifying complex heap manipulations, they had limited success at being practical for larger programs. In particular, they have not been incorporated in scalable error-detection tools so far.

In this talk I will present a novel approach to shape analysis: using local reasoning about individual heap locations instead of global reasoning about entire heap abstractions. The key feature of this approach is a novel memory abstraction that models the heap using a set of independent configurations, each of which characterizes one single heap location. This approach: 1) leads to simpler algorithm specifications, because of local reasoning about the single location; 2) leads to efficient algorithms, because of the smaller abstraction granularity; and 3) makes it easier to develop context-sensitive, demand-driven, and incremental shape analyses.

I will also present a prototype system that uses shape analysis to detect memory leaks and accesses through dangling pointers in C programs. The current results suggest that the local reasoning approach is both sufficiently precise to accurately analyze a large class of heap manipulation algorithms, and sufficiently lightweight to scale to larger programs.