2004. Precise Interprocedural Analysis through Linear Algebra

Precise Interprocedural Analysis through Linear AlgebraMarkus Müller-OlmHelmut SeidlFernUniversität Hagen, LG Praktische Informatik 558084 Hagen, GermanyTU München, Lehrstuhl für Informatik II80333 München, Germanymmo@ls5.cs.uni-dortmund.deseidl@informatik.tu-muenchen.deAbstractWe apply linear algebra techniques to precise interproceduraldataflow analysis. Specifically, we describe analyses that determine for each program point identities that are valid among theprogram variables whenever control reaches that program point.Our analyses fully interpret assignment statements with affine expressions on the right hand side while considering other assignments as non-deterministic and ignoring conditions at branches.Under this abstraction, the analysis computes the set of all affinerelations and, more generally, all polynomial relations of boundeddegree precisely.

The running time of our algorithms is linear in theprogram size and polynomial in the number of occurring variables.We also show how to deal with affine preconditions and local variables and indicate how to handle parameters and return values ofprocedures.Categories and Subject Descriptors: F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning aboutPrograms; D.3.3 [Programming Languages]: Language Constructsand Features—procedures, functions, and subroutines; D.3.4 [Programming Languages]: Processors—compilers; D.3.4 [Programming Languages]: Processors—optimizationGeneral Terms: algorithms, theory, verification.Keywords: interprocedural analysis, linear algebra, weakest precondition, affine relation, polynomial relation.circumstances.

Important application areas are optimizing compilers and validation or verification of programs. An often usedsimplification is to work with intraprocedural or context-insensitiveanalyses. Intraprocedural analyses treat bodies of single procedures(or methods) in isolation, while context-insensitive analyses assumeconservatively that a procedure called at one call site may return toany other call site of this procedure.

The context-insensitive approach, though interprocedural, still is limited in the quality of thecomputed information: if only weak information about one particular calling context of a procedure or method is available, this mayaffect all other calling contexts. The design of context-sensitive interprocedural analyses that mirror the actual call/return behavior ofprograms is generally deemed to be challenging. Here, if we speakabout interprocedural analyses without further qualification, we always will mean context-sensitive ones.In this paper, we show how linear algebra techniques can be usedfor interprocedural flow analysis.

Our specific goal is to determinefor each program point affine and, more generally, polynomial relations that are valid among the program variables whenever control reaches that program point. An affine relation is a conditionof the form a0 ∑ni 1 ai xi 0, where a0 an are constants andx1 xn are program variables; a polynomial relation is a condition of the form p x1 xn 0, where p is a multi-variate polynomial in x1 xn . We call an analysis precise (w.r.t. a given classof programs) if it computes for every program point u of a programall valid relations of the given form which are valid along every feasible program path reaching u. (A program path is called feasible ifit mirrors the actual call/return behavior of procedures.)Looking for valid affine and polynomial relations is a rather generalquestion with many applications.

First of all, many classical dataflow analysis problems can be seen as problems about affine andpolynomials relations. Some examples are: finding definite equalities among variables like x y; constant propagation, i.e. detectingvariables or expressions with a constant value at run-time; discovery of symbolic constants like x 5y 2 or even x yz2 42;detection of complex common sub-expressions where even expressions are sought which are syntactically different but have the samevalue at run-time; and discovery of loop induction variables.

Karr[10] also discusses applications in connection with parallelizationof do-loops.Affine and polynomial relations found by an automatic analysisroutine are also useful in program verification contexts, as they provide non-trivial valid assertions about the program. In particular,certain loop invariants can be discovered in this way fully automatically. As affine and, even more, polynomial relations express quitecomplex relationships among variables, the discovered assertions1 IntroductionThe field of program analysis is concerned with designing algorithms that compute information about the dynamic behavior ofprograms by a static analysis.

Such information is useful in manyOn leave from Universität Dortmund, FB 4, LS 5, 44221 Dortmund, Germany.c ACM, 2004. This is the author’s version of the work. It is posted hereby permission of ACM for your personal use. Not for redistribution. Thedefinitive version was published in Proceedings of POPL’04, January 14-16,2004, Venice, Italy. http://doi.acm.org/10/1145/nnnnnn.nnnnnn.may form the backbone of the program proof and thus significantlysimplify the verification task.In this paper we consider affine programs for which our analysis will be precise, i.e., compute not some but all affine relationswhich are valid at a program point.

We then extend this analysisto compute all valid polynomial relations up to a given degree dand to take affine preconditions into account completely. Affineprograms differ from ordinary programs over integers in that theyhave non-deterministic (instead of conditional) branching, and contain only assignments where the right-hand sides either equal “?”denoting an unknown value, or are affine expressions such as inx3 : x1 3x2 7. Clearly, in practice our analyses can also beapplied to arbitrary programs simply by ignoring the conditions atbranchings and simulating input operations and non-affine righthand sides in assignments through assignments of unknown values.To use linear algebra for program analysis is not a new idea.

In hisseminal paper [10], Karr presents an intraprocedural analysis thatdetermines all intraprocedurally valid affine relations in an affineprogram. However, the potential of linear algebra has never beenexploited fully. We extend Karr’s work in three respects.

Firstly,we describe a precise interprocedural analysis of affine programs.Secondly, we extend our algorithm to an algorithm that computesall interprocedurally valid polynomial relations of degree boundedby some fixed d. Thirdly, we show how to treat local variables andindicate how to handle parameters and result values of procedures.Our base algorithm as well as the extended algorithms run in timelinear in the program size and polynomial in the number of programvariables.The key observation onto which our algorithms are based is that theweakest precondition of an affine or polynomial relation a along asingle run of an affine program can be determined by means of a linear transformation applied to a.

The set of all linear transformationsof a vector space again forms a vector space and we can computefor each program point u the finite-dimensional subspace generatedby the linear transformations induced by the program runs reachingu. A relation a turns out to be valid at u if and only if the subspace of linear transformations computed for u transforms a into 0(or a relation implied by the precondition, respectively). This implies that the set of all valid relations can be computed as the setof solutions of a linear equation system.

Thus, finite-dimensionalsubspaces of linear transformation describe the effect of procedurecalls precisely enough.The program in Figure 1 illustrates the kind of properties our analyses can handle. It consists of two procedures Main and P. Aftermemorizing the (unknown) initial value of variable x1 in variablex2 and initializing x3 by zero, Main calls P. Procedure P can eitherterminate without changing any variable or call itself recursively.In the latter case, it increments x1 by x2 1 and x3 by 1 before therecursive call and decrements x1 by x2 afterwards.

Therefore, thetotal effect of each instance of P with a recursive call is to increment both x1 and x3 by one. Thus, upon termination of the call toP in Main (i.e., at program point 3), x3 holds the number of recursive calls of P and x1 the value x2 x3 . Consequently, the finalassignment in Main always assigns zero to x1 . More formally, thisamounts to saying that the affine relation x1 x2 x3 0 is validat program point 3 and that the affine relation x1 0 is valid atprogram point 4.Another interesting relationship between the variables holds whenever P is called. As mentioned, variable x3 counts the number ofrecursive calls, and, thus, how often x1 has been incremented byMain:P:05x2 : x1x1 : x1x2116x3 : x3x3 : 0127PP38x1 : x14x2x1 : x1x3x29Figure 1.

An example program.x2 1. Consequently, at any call to P variable x1 holds the valuex2 x3 x2 1 x2 x3 x2 x3 . This amounts to saying that thepolynomial relation (of degree 2) x2 x3 x1 x2 x3 0 is validat program points 2, 5 and 7.Related WorkUnlike our algorithm, Karr’s intraprocedural algorithm [10] workswith a forward propagation of affine spaces and uses quite complicated subroutines to deal with join points and assignments x j : twhere the affine right-hand side depends on the variable x j on theleft-hand side. Similar to our approach, it abstracts non-affine assignments and general guards.

Due to the forward propagationstrategy, however, it is able to handle positive affine guards precisely. In [13] we observe that, in absence of affine guards, checking a given affine relation for validity at a program point can be performed by a simpler backward propagating algorithm which in turnis generalized to a backward propagating algorithm for checking arbitrary polynomial relations for polynomial programs (where polynomial right hand side of assignments are interpreted) in [15, 14].In a recent paper, Gulwani and Necula [8] present a probabilisticanalysis for finding affine relationships.

Their algorithm is also justintraprocedurally applicable but asymptotically faster than Karr’s—at the price of a (small) probability of yielding non-valid affine relations.A generalization of these approaches to the interprocedural case isnot obvious. The functional approach of Sharir/Pnueli [20, 11] todesigning interprocedural data flow analyses is limited to finite lattices of data flow informations. Accordingly, it has successfullybeen applied to the detection of copy constants [17]. In copy constant detection only assignments of the form x : a are treated exactly where a is a constant or a variable. The lattice of affine spaces,however, is clearly infinite. The call string approach of [20], on theother hand, is applicable to more general lattices but abstracts thecall/return behavior of procedures.

Thus, it does not lead to preciseinterprocedural analyses. In more recent work on precise interprocedural analysis, Horwitz et al. propose a polynomial-time algorithm for detecting linear constants [9] interprocedurally. In linear constant detection only those affine assignments are interpretedwhose right-hand sides contain at most one occurrence of a variable. We strictly improve on these results as our analyses treat allaffine assignments exactly and determine more general properties.Main:P:03x: 2x: 2 x1x: x5P2x: x26Figure 2.