Bottom-up Shape Analysis

In this paper we present a new shape analysis algorithm. The key distinguishing aspect of our algorithm is that it is completely compositional, bottom­up and non­iterative. We present our algorithm as an inference system for computing Hoare triples summarizing heap manipulating programs. Our inference rules are compositional: Hoare triples for a compound statement is computed from the Hoare triples of its component statements. These inference rules are used as the basis for a bottom­-up shape analysis of programs. Specifically, we present a logic of iterated separation formula (LISF) which uses the iterated separating conjunct of Reynolds [16] to represent program states. A key ingredient of our inference rules is a strong bi­-abduction operation between two logical formulas. We describe sound strong bi­abduction and satisfiability decision procedures for LISF. We have built a prototype tool that implements these inference rules and have evaluated it on standard shape analysis benchmark programs. Pre­liminary results show that our tool can generate expressive summaries, which are complete functional specifications in many cases.