Shape Analysis with Inductive Recursion Synthesis [abstract] (PDF)
Bolei Guo
Ph.D. Thesis, Department of Computer Science, Princeton University, June 2008.

For program optimization and verification purposes, shape analysis can be used to statically determine structural properties of the runtime heap. One promising formalism for describing heap is separation logic, with recursively defined predicates that allow for concise yet precise summarization of linked data structures. A major challenge in this approach is the derivation of the predicates directly from the program being analyzed. As a result, current uses of separation logic rely heavily on predefined predicates, limiting the class of programs analyzable to those that manipulate only predefined data types. This thesis addresses this problem by proposing a general algorithm based on \emph{inductive program synthesis} that automatically infers recursive predicates in a canonical form. This technique yields a separation logic based shape analysis that can be effective on a much wider range of programs.

A key strength of separation logic is that it facilitates, via explicit expression of structural separation, local reasoning about heap where the effects of altering one part of a data structure are analyzed in isolation from the rest. The interaction between local reasoning and the global invariants given by recursive predicates is a difficult area, especially in the presence of complex internal sharing in the data structures. Existing approaches, using logic rules specifically designed for the list predicate to unfold and fold linked lists, again require a priori knowledge about the data structures and do not easily generalize to more complex data structures. We introduce a notion of ``truncation points" in a recursive predicate, which gives rise to generic algorithms for unfolding and folding arbitrary data structures.

We present a fully implemented interprocedural analysis algorithm that handles recursive procedures. A combination of pointer analysis and program slicing is used to deal with the scalability issue typically faced by shape analyses.

Finally, we present a data dependence test for recursive data structures that takes advantage of the results of our shape analysis.