Shape Analysis with Inductive Recursion Synthesis (thesis)

Abstract:

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 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