2004. Precise Interprocedural Analysis through Linear Algebra, страница 6

Therefore, an affine relation a is valid at u under precondition Pre if and only if it satisfiesthe equations:kkj 0i 1∑ a j w0 j ∑ x0i wi j 0andkkj 0i 1∑ a j ∑ xri wi j 0for r 1 lfor all W wi j B. We can hence compute the subspace of allvalid affine relations by setting up and solving the linear equationsystem consisting of all these equations.Let us estimate the complexity of this procedure. Each matrix W B contributes l 1 O k equations and there are at most O k2 matrices in B. Hence the equation system has O k3 equations.It is not hard to see, that the coefficients of each equation can becomputed in time O k2 .

Hence the equation system can be set upin time O k5 . As a linear equation system with O k3 equationsin the k 1 variables a0 ak it can be solved, e.g., by Gaussianelimination in time O k5 .From Theorem 2 we know that we can compute a basis ofSpan Wr : r R u in time O n k8 . Together with Theorem 6this implies:C OROLLARY 1.

The sets of all valid affine relations at programpoint u, u N, under precondition Pre can be computed in timeO n k8 .This approach for treating affine preconditions can straightforwardly be generalized to the setting of Section 4. Here a polynomial relation of degree at most d turns out to be valid at a programpoint u under precondition Pre if and only if for all W in a basis ofdSpan Wr : r R u :lx0 ∑ λr xr : r 1Wpfor all λ1 λl (6)This time, this translates to a polynomial equation (of degree at mostd) in the λr whose coefficients are affine combinations of the coefficients of p.

Again all these affine combinations must equal 0 whichgives rise to a linear equation system that we can set up and solve.C OROLLARY 2. The sets of all valid polynomial relations of degree at most d at program point u, u N, under precondition Precan be computed in time O n k d 8d .7 ConclusionWe have presented an interprocedural analysis that determines foreach program point of an affine program the set of all valid affinerelations. We generalized the algorithm to infer all polynomial relations of bounded degree and showed that our methods work also inpresence of local variables and parameter passing by value and result.

We also generalized our analyses to take affine preconditionsinto account.All our analyses run in polynomial time. More precisely, they arelinear in the program size and polynomial of a higher degree in thenumber of variables. It remains for future work to find out whetherthis theoretical complexity bound is prohibitive to apply the analysis in practice or in how far heuristic methods are necessary toidentify promising but sufficiently small sets of variables to be included in the analysis.Instrumental for our approach is that we can capture the effectof procedures as weakest precondition transformers for affine andpolynomial relations completely by subspaces of linear maps.

Thisprovides us with a kind of abstract “higher-order denotation” ofprocedures that we can compute in polynomial time and use at anycall site. Similar in spirit is “relational analysis” of recursive procedures as proposed by Cousot [5, 6] and the “functional approach”to interprocedural analysis [20, 11]. While these approaches relyon relations or functions, we capture the effects of procedures byfinitely representable sets of functions.Our results improve on the analysis of linear constants by Horwitz et al. [9, 17] and, upto the treatment of positive affine guards,also on the results obtained by Karr [10]. In a recent paper, Reps,Schwoon, and Jha [18] use a library for reachability analysis ofweighted pushdown systems for interprocedural dataflow analysis.They report that G.

Balakrishnan has created a prototype implementation of our interprocedural analysis for affine relations based on apreliminary version of the current paper.The results of this paper are still not strong enough to deal withpositive affine guards as Karr’s approach. Also, they do not generalize our intraprocedural analysis in [15, 14] where we succeed inchecking the validity of arbitrary polynomial relations for polynomial programs—even in presence of negative polynomial guards.

Itremains as challenging open problems whether or not precise interprocedural treatments of positive guards or precise interproceduralanalysis of polynomial programs are possible.AcknowledgmentsWe would like to thank the anonymous POPL reviewers for theirremarks that helped to improve our original submission.

The firstauthor would also like to thank the members of IFIP WorkingGroup 2.2 for their constructive comments on a talk about a preliminary version of this paper.8 References[1] K. R. Apt and G. D. Plotkin. Countable Nondeterminism andRandom Assignment. Journal of the ACM, 33(4):724–767,1986.[2] R. Bagnara, P. Hill, E. Ricci, and E. Zaffanella. PreciseWidening Operators for Convex Polyhedra. In 10th Int. StaticAnalysis Symposium (SAS), pages 337–354.

LNCS 2694,Springer-Verlag, 2003.[3] I. Balbin and K. Ramamohanarao. A Generalization of theDifferential Approach to Recursive Query Evaluation. Journal of Logic Programming (JLP), 4(3):259–262, 1987.[4] P. Cousot. Constructive Design of a Hierarchy of Semantics of a Transition System by Abstract Interpretation. Elec-tronic Notes in Theoretical Computer Science, 6, 1997. URL:www.elsevier.nl/locate/entcs/volume6.html.[5] P. Cousot and R. Cousot.

Static Determination of Dynamic Propertiesof Recursive Procedures. In E. Neuhold, editor, IFIP Conf. on Formal Description of Programming Concepts, pages 237–277. NorthHolland, 1977.[6] P. Cousot and N. Halbwachs. Automatic Discovery of Linear Restraints among Variables of a Program. In 5th ACM SIGPLANSIGACT Symp. on Principles of Programming Languages (POPL),pages 84–97, 1978.[7] C. Fecht and H. Seidl. Propagating Differences: An Efficient NewFixpoint Algorithm for Distributive Constraint Systems. Nordic Journal of Computing (NJC), 5(4):304–329, 1998.[8] S.

Gulwani and G. Necula. Discovering Affine Equalities Using Random Interpretation. In 30th Ann. ACM Symp. on Principles of Programming Languages (POPL), pages 74–84, 2003.[9] S. Horwitz, T. Reps, and M. Sagiv. Precise Interprocedural DataflowAnalysis with Applications to Constant Propagation. TheoreticalComputer Science (TCS), 167(1&2):131–170, 1996.[10] M. Karr. Affine Relationships Among Variables of a Program. ActaInformatica, 6:133–151, 1976.[11] J.

Knoop and B. Steffen. The Interprocedural Coincidence Theorem. In Compiler Construction (CC), pages 125–140. LNCS 541,Springer-Verlag, 1992.[12] S. S. Muchnick and N. D. Jones, editors. Program Flow Analysis:Theory and Applications. Prentice Hall, Engelwood Cliffs, New Jersey, 1981.[13] M.

Müller-Olm and O. Rüthing. The Complexity of Constant Propagation. In 10th European Symposium on Programming (ESOP), pages190–205. LNCS 2028, Springer-Verlag, 2001.[14] M. Müller-Olm and H. Seidl. Computing Polynomial Program Invariants. Submitted for publication.[15] M. Müller-Olm and H. Seidl. Polynomial Constants are Decidable.In 9th Static Analysis Symposium (SAS), pages 4–19. LNCS 2477,Springer-Verlag, 2002.[16] B.

Paige and S. Koenig. Finite Differencing of Computable Expressions. ACM Trans. Prog. Lang. and Syst., 4(3):402–454, 1982.[17] T. Reps, S. Horwitz, and M. Sagiv. Precise Interprocedural DataflowAnalysis via Graph Reachability. In 22nd ACM SIGPLAN-SIGACTSymp. on Principles of Programming Languages (POPL), pages 49–61.

ACM Press, 1995.[18] T. Reps, S. Schwoon, and S. Jha. Weighted Pushdown Systems andtheir Application to Interprocedural Dataflow Analysis. In Int. StaticAnalysis Symposium (SAS), pages 189–213. LNCS 2694, SpringerVerlag, 2003.[19] H. Seidl and B. Steffen. Constraint-Based Inter-Procedural Analysisof Parallel Programs.

Nordic Journal of Computing (NJC), 7(4):375–400, 2000.[20] M. Sharir and A. Pnueli. Two Approaches to Interprocedural DataFlow Analysis. In [12], chapter 7, pages 189–233..