Generating Precise and Concise Procedure Summaries
Yorsh, Eran Yahav, and Satish Chandra
In Proc. ACM Symposium on Principles of Programming Languages,
2008 (POPL 2008)
We present a framework for generating procedure summaries that
precise - applying the summary in a given
context yields the same result as re-analyzing the procedure in
that context, and
concise - the summary exploits the commonalities
in the ways the procedure manipulates abstract values, and
does not contain superfluous context information.
The use of a precise and concise procedure summary in
modular analyses provides a way to capture infinitely
many possible contexts in a finite way; in interprocedural
analyses, it provides a compact representation of an
explicit input-output summary table without loss of precision.
We define a class of abstract domains and transformers for
which precise and concise summaries can be efficiently
generated using our framework.
Our framework is rich enough to encode a wide range of problems,
including all IFDS and IDE problems.
In addition, we show how the framework is instantiated to provide novel
solutions to two hard problems: modular linear constant
propagation and modular typestate verification, both in the presence of aliasing.
We implemented a prototype of
our framework that computes summaries for the typestate domain,
and report on preliminary experimental results.