Computing Procedure Summaries for Interprocedural Analysis

Sumit Gulwani and Ashish Tiwari

Presented at ESOP 2007, Braga, Portugal, Mar 2007. Springer-Verlag. The final version will appear at the the Springer LNCS site.


We describe a new technique for computing procedure summaries for performing an interprocedural analysis on programs. Procedure summaries are computed by performing a backward analysis of procedures, but there are two key new features: (i) information is propagated using ``generic'' assertions (rather than regular assertions that are used in intraprocedural analysis); and (ii) unification is used to simplify these generic assertions (thus generalizing our recent technique of using unification to simplify regular assertions in intraprocedural analysis~\cite{GT:AssertionChecking}).

We describe conditions under which this technique yields efficient interprocedural analyses. We illustrate this technique by applying it to two abstractions: unary uninterpreted functions and linear arithmetic. In the first case, we get a PTIME algorithm for a special case of the long-standing open problem of interprocedural global value numbering (the special case being that we consider unary uninterpreted functions instead of binary). This also requires developing efficient algorithms for manipulating singleton context-free grammars, and builds on an earlier work by Plandowski~\cite{Plandowski94:ESA}. In linear arithmetic case, we get new algorithms for precise interprocedural analysis of linear arithmetic programs with complexity matching that of the best known deterministic algorithm~\cite{Seidl04}.

Long version of the paper: pdf.


In powerpoint: pdf

BibTeX Entry

	author = "S. Gulwani and A. Tiwari",
	title = "Computing Procedure Summaries for Interprocedural Analysis",
	booktitle = {European Symp. on Programming, ESOP 2007},
	year = 2007,
	editor = "De Nicola, R.",
	series = {LNCS},
	volume = 4421,
	pages = "253--267",

Return to the Ashish's home page
Return to the Computer Science Laboratory home page