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

Similarly for A e E@ x j : ?,x j : c : c b) The sets of all valid polynomial relations of degree at most dat program point u, u N, can be computed in time O n k d 8d .Consider again the example program from the introduction. Sinceit uses three program variables, the vector-space of polynomials ofdegree at most 2 has dimension 3 2 2 10. Assume we have ordered the index tuples of monomials lexicographically as follows:0 0 00 0 11 1 02 0 0Then the pre-condition transformer, e.g., of the assignment x1 : x1 x2 1 is given by the matrix:1000000000010000000000100000000001000000000010000000000100001001001000010010010000010100101002012021 The same-level runs of procedures and program nodes are thesmallest solution of the following constraint system S : S 1SSSS S 2 S 3 S 4S rq εS u ; S eS u ; %> > S p q eq v vNote that, for convenience, the application of the constructor %?> >to all sequences of a set S is denoted by %> > S .

Constraints S 1 , S 2 and S 3 are as in Section 2. The new constraint S 4 dealswith calls. If the ingoing edge e u v is a call to a procedure p,we concatenate a same-level run reaching u with a tree constructedfrom a same-level run of p by applying the constructor %> > . R 1εR u if u = >>pR p ; D 9 ; S u if u NpR MainR pR u R 2 R 3Constraints R 1 and R 2 are as in Section 3. The only modification occurs in R 3 where an D is inserted between the runreaching the current procedure p and the same-level run inside p.Each of these runs gives rise to a transformation of the underlyingprogram state x m . Here, we just explain how the transformations of D 9 and %> > s are obtained.

The transformation D passes the values of the globals x j ( j 1 k) and sets the localsx j , j k, to 0.2 Thus,5 Local Variables D 9 So far we have considered programs which operate on global variables only. In this section, we explain how our techniques can beextended to work on procedures with global and local variables. xk 1 : 0; ; xm : 0 x j : t :8%> > sst1 ; ; stn0nx j : t :8%> > s :" D rt1 ; ; rtnn0Trees represent base actions or complete executions of procedures.Same-level runs represent sequences of such completed executions,while reaching runs may enter a procedure—without ever leaving itagain.The set of runs reaching program point u N can again be characterized as the least solution of a system of subset constraints on runsets. If e is annotated by an affine assignment, i.e., A e 8@ x j : t,Ik000The transformation %> > s is more complicated.

Like D 9 , itmust pass the values of the globals into the execution of the calledprocedure and initialize its local variables. In addition, it must return the values of the globals to the calling context and restore thevalues of the local variables. Given that s x As x bs as in Section 2, we define: %?> > s x E 9 s E x T x E A s E T x E bs Let us denote this m ( m matrix by E .For notational convenience, we assume that all procedures have thesame set X x1 xm of variables where the first k are globaland the remaining m k are local.

For describing program executions, it now no longer suffices to consider execution paths. Instead,we have to take the proper nesting of calls into account. Therefore,same-level runs s and reaching runs r are now finite sequences of(unranked) trees b and, possibly, D ::: :: :: :: For characterizing the runs that reach program points and procedures, we construct the constraint system R :We refrain from describing the details of the fixpoint iteration.

Theleast fixpoint computation for analyzing the valid quadratic relations at the entry of procedure p stabilizes after three iterationswith three matrices. The rows of these matrices span a vectorspace of dimension 9 and have the (coefficients of) the relationx2 x3 x1 x2 x3 0 as their only non-trivial solution (up toconstant multiples, of course). Again, this confirms our informalreasoning from the introduction.stsrtru v 7 9 u v 8= ?> > pif e if e 00.

The outermost appli0 Im kcation of E in the first summand prohibits propagation of the calledprocedure’s local variables and the second summand, T x bypassesthe values of the local variables of the calling context. The abovecalculation shows that %?> > s is an affine transformation as well.where T is the m ( m matrix2 Byconvention, local variables are initialized by 0.

Other conventions could easily be modeled as well. Uninitialized local variables as in C, for instance, can be handled by adding x j : ? statements for j k 1 m at the beginning of each procedure body.We want to determine for every (reaching or same-level) run thetransformation which produces the weakest precondition. For simplicity, we construct the weakest precondition transformer only foraffine relations. The weakest precondition transformer for D isgiven by:W2 Wxk 1:Ik 10 0; ;xm : 0 00Let E denote this matrix. To obtain analogous results as in Section 3, we determine the weakest precondition transformation of%?> > s . We define an operator: m 1 k 1 m 1 k 1on m 1 ( m 1 matrices by:WEW E w Twhere w is the element in the left upper corner of W , and T is the00 m 1 ( m 1 matrix.0 Im k6 Affine PreconditionsThe analyses considered so far assume that we have no knowledgewhatsoever about the initial state in which the program is started.However, in a verification context we are often in a more lucky situation when we are given a precondition that constrains potentialinitial states.

Of course, if less initial states are possible more relations may be valid at the nodes of a program and an analyses thatignores the precondition may be overly pessimistic. In this sectionwe extend the analyses of Section 3 and Section 4 to take into account affine preconditions completely. The analyses of this sectionthus compute for each program point of an affine program the spaceof all those affine or polynomial relations that are valid wheneverthe program is started in a state satisfying a given affine precondition.The operator returns a linear transformation and is itself linear.This implies that maps subspaces of k 1 k 1 to subspacesof k 1 k 1 and, considered as a mapping on subspaces, commutes with arbitrary least upper bounds.

Moreover, we have:L EMMA 9. Let Ws denote the precondition transformer for s.Then for an affine relationa m and a program state x m , %?> > s x : a iff x : Ws a. Ws is the weakest precondition transformer forThus, W4 s %?> > s . In order to furnish the same approach as for global variables, we define the abstraction function α for sets R of (same-levelor reaching) runs by:Assume given a finite set Pre ' F k 1 of affine relations, representing the affine precondition.

We say that Pre is satisfiable ifthere is an x k such that x : h for all h Pre. If Pre is notsatisfiable, all relations are valid at all program points under precondition Pre. As we can check whether Pre is satisfiable or notwith the aid of Gaussian elimination, we can detect this trivialcase. Thus, we assume without loss of generality that Pre is satisfiable in the following.In this case, the set of states satisfyingPre, Sat Pre x k : x : h h Pre , is an affine subspace of k and can be represented in the form Sat Pre x0 L, wherex0 Sat Pre andL is a (linear) subspace of k . Assume thatx1 xl with l k is a basis of L. Then we haveα RIn particular, α D 9 Span Wr : r R Span E .

L EMMA 10. For every set S of same-level runs,α %?> > s : s S α S Finally, we construct constraint systems Sα and Rα from S andis replaced with “ ” and theR by applying α where concatenationconstructor %> > is replaced with “ ”. Then we obtain our maintheorem for programs with local variables:T HEOREM 5. For a program of size n with m global and localvariables the following holds:a) The values:Span Ws : s S u , u N,Span Ws : s S p , p !"$#% ,Span Ws : s R p , p !"$#% , andSpan Wr : r R u , u N,are the least solutions of the constraint systems Sα and Rα ,respectively.lx0 ∑ λr xr : λ1 λl r 1 (4)Vectors x0 xl k with this property can be computed from Prewith standard techniques from linear algebra.Obviously, an affine relation a is valid at a program point u under precondition Pre, iff its weakest precondition for each programpath r reaching u is valid for all x Sat Pre , i.e., if x : Wr a forall r R u , x Sat Pre .

By the characterization of Sat Pre inEquation 4, we thus have:Analogously to Lemma 4, we find:α %> > SSat Pre b) The sets of all valid affine relations at program point u, u N,can be computed in time O n m8 .Our technique can be adapted to procedures with parameters. Valueparameters, for instance, can be simulated via a scratch pad of globals through which the actual parameters are communicated from thecaller to the callee. Return values can be treated similarly.L EMMA 11. The affine relation a k 1 is valid at programpoint u under precondition Pre iff x0 ∑lr 1 λr xr : Wr a for allλ1 λl , r R u .By arguing analogously to Section 3 we can equivalentlyrequirethis property for all matrices W in a basis of Span Wr : r R u .Thus, we obtain the following generalization of Theorem 1:T HEOREM6.

Assume we are given a basis B for the setSpan Wr : r R u . Then we have:a) Affine relation a k 1 is valid at program point u underprecondition Pre iff x0 ∑lr 1 λr xr : Wa for all λ1 λl , W B.b) A basis for the subspace of all affine relations valid at program point u under precondition Pre can be computed in timeO k5 .P ROOF. As a) has already been justified we prove only b).

By a)an affine relation a is valid at u if and only if for all W B:lx0 ∑ λr xr : r 1Wafor all λ1 λl (5)By unfolding the definition of “ : ” and writing W wi j and xi xi1 xik t for i 0 l, Formula (5) means thatkk∑ a j w0 j ∑ x0i wi j j 0i 1lkkr 1j 0i 1∑ λr ∑ a j ∑ xri wi j 0for all λ1 λl . This is an affine equation in the λr whosecoefficients are affine combinations of the a j . It is valid for all λr ifand only if all these combinations are 0.