Download CAV05c.pdf

Contents : A policy iteration algorithm for computing fixed points in static analysis of programs A. Costan S. Gaubert E. Goubault+ M. Martel+ S. Putot+ 1 2 Polytehnica Bucarest INRIA Rocquencourt 3 + CEA Saclay Abstract. We present a new method for solving the fixed point equations that appear in the static analysis of programs by abstract interpretation. We introduce and analyze a policy iteration algorithm for monotone self-maps of complete lattices. We apply this algorithm to the particular case of lattices arising in the interval abstraction of values of variables. We demonstrate the improvements in terms of speed and precision over existing techniques based on Kleene iteration including traditional widening/narrowing acceleration mecanisms. Appears in: Proceedings of the 17th International Conference on Computer Aided Verification (CAV'05) Edinburgh Scotland UK July 2005 LNCS 3576 pp. 462 475 Springer. 1 Introduction and related work One of the important goals of static analysis by abstract interpretation (see Cousot & Cousot 9 ) is the determination of invariants of programs. They are generally described by over approximation (abstraction) of the sets of values that program variables can take at each control point of the program. And they are obtained by solving a system of (abstract) semantic equations derived from the program to analyze and from the domain of interpretation or abstraction i.e. by solving a given fixed point equation in an order-theoretic structure. Among the classical abstractions there are the non-relational ones such as the domain of intervals 9 (invariants are of the form vi c1 c2 ) of constant propagation (vi c) of congruences 16 (vi aZ + b). Among the relational ones we can mention polyedra 28 (1 v1 + + n vn c ) linear equalities 23 (1 v1 + + n vn c) linear equalities modulo 17 (1 v1 + + n vn a) or more recently the octagon domain 26 (vi - vj c). All these domains are (order-theoretic) lattices for which we could think of designing specific fixed point equation solvers instead of using the classical and yet not very efficient value iteration algorithms based on Kleene's iteration. A classical way to improve these computations is to use widening/narrowing operators 10 . They improve the rapidity of finding an over-approximated invariant at the expense of accuracy sometimes i.e. they reach a post-fixed point or a fixed point but not always the least fixed point of the semantic equations (we review some elements of this method in Section 2 and give examples in the case of the interval lattice). In this paper we introduce a new algorithm based on policy iteration and not value iteration that correctly and efficiently solves this problem (Section 3). It shows good performances in general with respect to various typical programs see Section 4.4. We should add that this work started from the difficulty to find good widening and narrowing operators for domains used for characterizing the precision of floating-point computations used by some of the authors in 15 . Policy iteration was introduced by Howard 21 to solve stochastic control problems with finite state and action space. In this context a policy is a feedback strategy (which assigns to every state an action). The classical policy iteration generalizes Newton's algorithm to the equation x f (x) where f is monotone non-differentiable and convex. The convergence proof is based on the discrete version of the maximum principle for harmonic functions. This method is experimentally efficient although its complexity is still not well understood theoretically. We refer the reader to the book of Puterman 29 for background. It is natural to ask whether policy iteration can be extended to the case of zero-sum games: at each iteration one fixes the strategy of one player and solves a non-linear (optimal control problem) instead of a linear problem. This idea goes back to Hoffman and Karp 20 . The central difficulty in the case of games is to obtain the convergence because the classical (linear) maximum principle cannot be applied any more. For this reason the algorithm of 20 requires positivity conditions on transition probabilities which do not allow to handle the case of deterministic games. In applications to static analysis however even the simplest fixed point problems lead to deterministic game problems. A policy iteration algorithm for deterministic games with ergodic reward has been given by Cochet-Terrasson Gaubert and Gunawardena 6 14 : the convergence proof relies on max-plus spectral theory which provides nonlinear analogues of results of potential theory. In the present paper (elaborating on 8 ) we present a new policy iteration algorithm which applies to monotone self-maps of a complete lattice defined by the infimum of a certain family satisfying a selection principle. Thus policy iteration is not limited to finding fixed point that are numerical vectors or functions fixed points can be elements of an abstract lattice. This new generality allows us to handle lattices which are useful in static analysis. For the fixed point problem the convergence analysis is somehow simpler than in the ergodic case of 6 14 : we show that the convergence is guaranteed if we compute at each step the least fixed point corresponding to the current policy. The main idea of the proof is that the map which assigns to a monotone map its least fixed point is in some weak sense a morphism with respect to the inf-law see Theorem 1. This shows that policy iteration can be used to compute the minimal fixed points at least for a subclass of maps (Theorem 3 and Remark 3). Other fixed point acceleration techniques have been proposed in the literature. There are mainly three types of fixed point acceleration techniques as used in static analysis. The first one relies on specific information about the structure of the program under analysis. For instance one can define refined iteration strategies for loop nests 2 or for interprocedural analysis 1 . These methods are completely orthogonal to the method we are introducing here which does not use such structural properties. However they might be combined with policy iteration for efficient interprocedural analysis for instance. This is beyond the scope of this paper. Another type of algorithm is based on the particular structure of the abstract domain. For instance in model-checking for reachability analysis particular iteration strategies have been designed so that to keep the size of the state space representation small (using BDDs or in static analyzers by abstract interpretation using binary decision graphs see 25 ) by a combination of breadth-first and depth-first strategies as in 31 . For boolean equations some authors have designed specific representations which allow for relatively fast least fixed point algorithms. For instance 24 uses Bekic-Leszczyloiwski theorem. In strictness analysis representation of boolean functions by "frontiers" has been widely used see for instance 22 and 4 . Our method here is general as hinted in Section 3. It can be applied to a variety of abstract domains provided that we can find a "selection principle". This is exemplified here on the domain of intervals but we are confident this can be equally applied to octagons and polyedra. Last but not least there are some general purpose algorithms such as general widening/narrowing techniques 10 with which we compare our policy iteration technique. There are also incremental or "differential" computations (in order not to compute again the functional on each partial computations) 12 13 . In fact this is much like the static partitioning technique some of the authors use in 30 . Related algorithms can be found in 11 27 and 3 . 2 Kleene's iteration sequence widenings and narrowings In order to compare the policy iteration algorithm with existing methods we briefly recall in this section the classical method based on Kleene's fixed point iteration with widening and narrowing refinements (see 10 ). Let (L ) be a complete lattice. We write for its lowest element for its greatest element and for the meet and join operations respectively. We say that a self-map f of a complete lattice (L ) is monotone if x y f (x) f (y ). The least fixed point of a monotone f can be obtained by computing the sequence: x0 xn+1 f (xn ) (n 0) which is such that x0 x1 . . . If the sequence becomes stationary i.e. if xm xm+1 for some m the limit xm is the least fixed point of f . Of course this procedure may be inefficient and it needs not even terminate in the case of lattices of infinite height such as the simple interval lattice (that we use for abstractions in Section 4). For this computation to become tractable widening and narrowing operators have been introduced we refer the reader to 10 for a good survey. As we will only show examples on the interval lattice we will not recall the general theory. Widening operators are binary operators on L which ensure that any finite Kleene iteration x0 x1 f (x0 ) . . . xk+1 f (xk ) followed by an iteration of the form xn+1 xn f (xn ) for n k yields an ultimately stationary sequence whose limit xm is a post fixed point of f i.e. a point x such that x f (x). The index k is a parameter of the least fixed point solver. Increasing k increases the precision of the solver at the expense of time. In the sequel we choose k 10. Narrowing operators are binary operators on L which ensure that any sequence xn+1 xn f (xn ) for n m initialized with the above post fixed point xm is eventually stationary. Its limit is required to be a fixed point of f but not necessarily the least one. void main() int x 0 while (x 100) x x+1 // // // // 1 2 3 4 x1 x2 x3 x4 0 0 - 99 (x1 x3 ) x2 + 1 1 100 + (x1 x3 ) Fig. 1. A simple integer loop and its semantic equations Consider first the program at the left of Figure 1. The corresponding semantic equations in the lattice of intervals are given at the right of the figure. The intervals x1 . . . x4 correspond to the control points 1 . . . 4 indicated as comments in the C code. We look for a fixed point of the function f given by the right hand side of these semantic equations. The standard Kleene iteration sequence is eventually constant after 100 iterations reaching the least fixed point. This fixed point can be obtained in a faster way by using the classical (see 10 again) widening and narrowing operators: a b c d e f with e a b c d e f with e a if a c - otherwise c if a - a otherwise and f and f b if d b otherwise d if b b otherwise. The iteration sequence using widenings and narrowings takes 12 iterations because we chose k 10 and it reaches the least fixed point of f : x1 2 0 0 x1 3 1 1 x1 4 ... x9 2 0 8 x9 3 1 9 x9 4 (widening) x10 0 2 1 x10 3 x10 100 4 (narrowing) x11 0 99 2 1 100 x11 3 x11 100 100 4 3 3.1 Policy iteration algorithm in complete lattices Lower selection To compute a fixed point of a self-map f of a lattice L we shall assume that f is effectively given as an infimum of a finite set G of "simpler" maps. Here and in the sequel the infimum refers to the pointwise ordering of maps. We wish to obtain a fixed point of f from the fixed points of the maps of G . To this end the following general notion will be useful. Definition 1 (Lower selection). We say that a set G of maps from a set X to a lattice L admits a lower selection if for all x X there exists a map g G such that g (x) h(x) for all h G . Setting f inf G we see that G has a lower selection if and only if for all x X we have f (x) g (x) for some g G . We next illustrate this definition. Example 1. Take L R and consider the self-map of L f (x) 1im (ai + x) bi where ai bi R. Up to a trivial modification this is a special case of min-max function 18 6 19 . The set G consisting of the m maps x (ai + x) bi admits a lower selection. We represent on Figure 2 the case where m 5 b1 -5 a1 2.5 b2 -3 a2 0.5 b3 1 a3 -3 b4 1.5 a4 -4 b5 2.5 a5 -4.5. The graph of the map f is represented in bold. 3.2 Universal policy iteration algorithm In many applications and specially in static analysis of programs the smallest fixed point is of interest. We shall denote by f - the smallest fixed point of a monotone self-map f of a complete lattice L whose existence is guaranteed by Tarski's fixed point theorem. We first state a simple theoretical result which brings to light one of the ingredients of policy iteration. Theorem 1. Let G denote a family of monotone self-maps of a complete lattice L with a lower selection and let f inf G . Then f - inf gG g - . Theorem 1 is related to a result of 7 concerning monotone self-maps of Rn that are nonexpansive in the sup-norm (see also the last chapter of 5 ). We now state a very general policy iteration algorithm. The input of the algorithm consists of a finite set G of monotone self-maps of a lattice L with a lower selection. When the algorithm terminates its output is a fixed point of f inf G . Algorithm (PI: Policy iteration in lattices). 1. 2. 3. 4. 5. Initialization. Set k 1 and select any map g1 G . Value determination. Compute a fixed point xk of gk . Compute f (xk ). If f (xk ) xk return xk . Policy improvement. Take gk+1 such that f (xk ) gk+1 (xk ). Increment k and goto Step 2. We next show that the algorithm does terminate when at each step the - smallest fixed-point of gk xk gk is selected. We call height of a subset X L the maximal cardinality of a chain of elements of X .

INFO HASH : 6b85bdc0a024e65a03ab989d18dc19a2fba40bb2

Download now

File Size: 227.5 kb