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

Altogether,we obtain an upper complexity bound of O n k2 k8 O n k10 .A better running time can be obtained if we use a semi-naive fixpoint iteration strategy [16, 3, 7]. The idea here is that when thevalue of a fixpoint variable changes, we do not propagate the complete new value to all uses of the variable in right-hand sides ofconstraints but just the increment, i.e., in our case the new matrices extending the current basis (instead of the complete new basis).The total time spent with a constraint then sums up to O k8 whichoverall results in the desired complexity O n k8 .Finally, for c) we recall that we know from Theorem 1 that, frombases of Span Wr : r R u for all program points u, we cancompute the sets of all valid affine relations within the stated complexity bounds.Let us consider the example program from Figure 1 for illustration.

Due to lack of space, we cannot describe the fixpoint iterationin detail or give the full result. However, we report and discusssome characteristic values. The fixpoint iteration for Sα stabilizesafter 3 iterations. We obtain: Sα P Sα 9 Span I4 W1 andSα 3 Span W1 W2 , where W1 W2 are the matricesW10000100000001000 W21000010001000000 Also, Sα Main W3100000000 Sα 4 01001 Span W3 W4 , where000W4000000000000000k dAs there are no recursive calls to Main, reaching runs and samelevel runs coincide for the program points of Main. Consequently,we have, Rα 3 Sα 3 Span W1 W2 . Hence, at programpoint 3 just the affine relations a a0 ak t with W1 a 0 andW2 a 0 are valid which reduces to the requirements a0 0 anda1 .

Therefore, just the affine relations of the forma2 a3 a1 x1 a1 x2 a1 x3 0 are valid at program point 3, in particular,x1 x2 x3 0 which confirms our informal reasoning from theintroduction.For program point 4 we have Rα 4 Sα 4 Span W3 W4 .Here, the requirements W3 a 0 and W4 a 0 reduce to a0 a2 a3 0. Thus, just the affine relations of the form a1 x1 0 are validat program point 4, in particular, x1 0.

Again this confirms ourinformal reasoning that x1 is a constant of value zero.The computation of Rα for the program points of P stabilizes againafter 3 iterations. For the program point7 just before the recursivecall to P, we obtain Rα 7 Span W5 W6 , whereW51000010001000000 W60000110000001000polynomials of bounded degree. The degree of a polynomial p (orthe polynomial relation p 0) is the maximal sum j1 jk ofjjexponents of a monomial a x11 xkk occurring in p.

We denote theset of polynomials of degree at most d by d X . Here the conditions W5 a 0 and W6 a 0 for valid affine relationstranslate into a0 a1 a2 a3 0. Interestingly, this implies thatno non-trivial affine relation is valid at every call to P.In order to find out about validity of the polynomial relation x2 x3x1 x2 x3 0 at program point 7, hinted upon in the introduction,we must generalize our analysis to polynomial relations which isthe topic of the next section.

d X is an -vector space of dimension d O k d d :jj d X with coefficient 1obviously, the monomials x11 xkk form a basis of d X and we prove momentarily by inductionthat there are k d d such monomials. For d 0 or k 0 thereis just the single monomial x01 x0k or 1, respectively, and indeed 0k dd 1. So assume d 0 or k 0. By induction hypothesisthere are k d d 1 1 monomials of degree less than d. The monomialswith degree d over k variables are obtained from the k 1d d monojjmials x11 xkk 11 of degree at most d over the first k 1 variablesby multiplying with xlkk where lk d ∑ik 11 li .

Altogether, thereare thus k d d 1 1 k 1d d k d d monomials with coefficient 1of degree at most d.The polynomial relation p 0 is valid after a single run r iff for allx k , p $ r x x 0 or, equivalently, p Ar x br x 0 whereAr , br are defined as in Section 2. Thus, p Ar x br x 0 is theweakest precondition for validity of p 0 after run r. We observe:L EMMA 6.

1. The polynomial p Ar x br x is again of degree at most d.d2. The mapping Wr which maps polynomials p of degree atmost d to p Ar x br x is linear.P ROOF. For a proof of the first statement, it suffices to consider arun r @ xi : t, t @ t0 ∑km 1 tm xm , of a single assignment and ajjsingle monomial p @ x11 xkk . Thenp A r x br x 4 Polynomial Relations of Bounded DegreePolynomial relations are much more expressive than affine relations. In particular, they are closed under disjunction: p 0 q 0holds if and only if pq 0. For example, the relation:x11 x1x2 0∑κ0 κ0κkjiκk ji κ0 κk t0 tk j κ1x11p t xi xi i 11j κi 1xκi i xi i 11j κi 1j κkxkkwhere the κ0 κk are the multinomial coefficients for the ji -thpower of a sum on k 1 summands.

Since in each monomial ofthe result, κ0 κk ji , the degree of p t xi is bounded byj1 jk , i.e., the degree of p.jirepresents the disjunction of the two affine relations:x11 0 x1x20Also, the property whether a variable x j has a value in a given finiteset c1 cr ' with r elements can be expressed by a polynomial relation:xjc1 xjcr 0Formally, a polynomial relation over a vector space k is an equation p 0 where p is a polynomial over the unknowns X, i.e.,p X .

The vector y k satisfies the polynomial relation p 0,y : p for short, iff p y x 0 where y x denotes the substitutionof the values yi for the variables xi .The set of polynomials X forms an -vector space. However,as the dimension of this vector space is infinite, we cannot effectively compute with bases. One way out is to restrict attention toThe second assertion follows since substitution commutes withsums and constant multiples.The only polynomial relation which is true for all program states isthe zero relation 0 0. As for affine relations, we conclude that thedpolynomial relation p 0 is valid after run r iff Wr p 0 (where0 denotes the zero polynomial).

Summarizing, we have:L EMMA 7. The polynomial relation p of degree at most d is validdat program point u iff Wr p 0 for all r R u .Now we can proceed analogously to Section 3. By applyingdLemma 2, we can safely replace the set Wr : r R u withits span. The resulting subspace of linear mappings can be described by a basis of at most O k d 2d matrices. The entries ofthese matrices are now indexed by pairs of tuples J j1 jk ,∑ki 1 ji d. Let I denote the set of all such tuples. We determinethe set of all valid polynomial relations at program point u for polynomials of degree at most d as follows:T HEOREM 3. Assume we are given a basis B for the setdSpan Wr : r R u .

Then we have:haveat most degree d and are uniquely determined by p. For 0i d let Ci be the mapping on d X that maps each p to its i-thcoefficient polynomial, i.e., Ci p pi . It is not hard to see that Ciis a linear map and hence can be represented by a matrix. We findthat α d S e can be finitely represented by C0 Cd :L EMMA 8.

If has more than d elements, thena) The polynomial relation p 0 of degree at most d is valid atprogram point u iff W p 0 for all W B.b) A basis of the subspace of all polynomial relations of degreeat most d valid at program point u can be computed in timeO k d 5d .P ROOF. Statement a) follows directly from Lemma 2 andLemma 7.For the proof of b), note that by a) the polynomial relation p 0jjis valid at u iff p @ ∑J j1 jk / I aJ x11 xkk , where the aJ J I are a solution of the equation:∑ wIJ aJ 0J/ IP ROOF. From the definitions we have α d S e Span Wrd: r R d1. Wx j : c Span C : lld2.

Cl Span Wx j : αd rSpan 0/ Span WrdSpan II cdmeans Wx j : c pAwe havep c x j11...1C0 p ...Cd p A0 0 d.∑ Ci p ci i 0To 2: Since the cardinality of is at least d 1, we can find d 1distinct elements c0 cd . Defining matrix A by for l∑di 0 ciCi , which implies 1.it is not hard to see, thatfor a single run r. In particular,α d εd Xfor all c .ddWx j : This0 d c c :To 1: For arbitrary p As in the case of affine relations, we have:α d 0/ α d x j : c :d c Span Wx j : c : c . It remains to show that this spanequals Span Cl : l 0 d . For this we show:By Theorem 3, it suffices to compute, for every program point u,dthe span of the set of all precondition transformers Wr , r R u .We do so by abstracting the run sets to subspaces of linear transformations now of polynomials of degree at most d. The abstraction isthus given by:α d Rα d x j : c : c Span Cl : l 0 d wIJ B and every I for every matrix W I .

The basis B maycontain at most O k d 2d matrices each of which contributesO k d d equations. Thus, we have to compute the solution ofan equation system with O k d 3d equations over O k d d variables. This can be done in time O k d 5d .α d S e c0c1...cd cd0cd1...cdd... p c0 x j ...p cd x j The determinant of A is an instance of what is known as Vandermonde’s determinant and has the value ∏0 i l d cl ci . As all ciare distinct, the determinant is different from 0. Therefore, matrixA is invertible and for the inverse matrix A 1 bil , we have where II is the diagonal matrix describing the identity.

The mapping α d is again monotonic (w.r.t. subset ordering on sets ofruns and subspaces) and commutes with arbitrary unions. Also,Lemma 4 analogously holds for α d . Therefore, the desired valuescan be computed by abstracting the constraint systems for samelevel and reaching run sets. In order to obtain an effective algorithm, it remains to derive explicit abstractions for the effects ofbase edges.CiFor a definite assignment x j : t, this is obviously possible. It remains to consider a base edge e 7 annotated by x j : ? withS e x j : c : c .Analogously to the last section, we construct constraint systemsSα d , Rα d which are obtained from the constraint systems S and Rby applying α d .

We conclude:In case contains less than d 1 elements, the set S e is also finiteand we simply may enumerate it. More interesting is the case when has at least d 1 elements, e.g., because has characteristic 0.T HEOREM 4. For every program of size n with k variables thefollowing holds:Each polynomial p d X can be written as p @forpolynomials pi not containing x j . The coefficient polynomials pi∑di 0 pi xijThus, Ci p C0 p ...Cd p ∑dl0 bil p cld∑dl 0 bil Wx j : cl ,xjA1∑dlp c0 x j ...p cd x j d0 bil Wx j : cl p .

This showswhich implies 2.a) The values:dSpan Wr : r S u , u N,dSpan Wr : r S p , p !"$# % ,dSpan Wr : r R p , p !"$#% , anddSpan Wr : r R u , u N,are the least solutions of the constraint systems Sα d andRα d , respectively.we again define: S e S ex j : t .