Computing Procedure Summaries for Interprocedural Analysis

Abstract. 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. We illustrate this general 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 [13]. In linear arithmetic case, we get new alg...

• Type: Conference
• Year: 2007
• Where: ESOP
• Authors: Sumit Gulwani, Ashish Tiwari
• Keywords: ESOP 2007, Interprocedural Analysis, Procedure Summaries, Programming Languages, Unary Uninterpreted Functions