This paper describes a compositional shape analysis, where each
procedure is analyzed independently of its callers. The analysis
uses an abstract domain based on a restricted fragment of separation
logic, and assigns a collection of Hoare triples to each procedure;
the triples provide an over-approximation of data structure
usage. Compositionality brings its usual benefits – increased potential
to scale, ability to deal with unknown calling contexts, graceful
way to deal with imprecision – to shape analysis, for the first time.
The analysis rests on a generalized form of abduction (inference
of explanatory hypotheses) which we call bi-abduction. Biabduction
displays abduction as a kind of inverse to the frame problem:
it jointly infers anti-frames (missing portions of state) and
frames (portions of state not touched by an operation), and is the
basis of a new interprocedural analysis algorithm. We have implemented
our analysis algorithm and we report case studies on
smaller programs to evaluate the quality of discovered specifications,
and larger programs (e.g., an entire Linux distribution) to test
scalability and graceful imprecision.