Abstract:
In this talk we
describe a compositional inter-procedural shape analysis, where
each procedure is analyzed independently of its callers. The
analysis performs proof search in 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 interprocedural
algorithm rests on a new form of abduction (inference of
explanatory hypotheses), which is used in our analysis algorithm
to discover preconditions by abductive inference of missing heap
portions. We define a proof procedure for abduction, and
use it to define our analysis algorithm. We also report on
the effects of the application of compositionality to a variety
of large programs (up to >1 million LOC) by running
experiments with an implementation of our algorithm.