Overview of Chaotic Iterations, Mathematical Background, and Posets

Chaotic Iterations Mooly Sagiv

Content Mathematical Background Chaotic Iterations Examples Soundness, Precision and more examples next week

Mathematical Background Declaratively define The result of the analysis The exact solution Allow comparison

Posets A partial ordering is a binary relation : L L {false, true} For all l L : l l (Reflexive) For all l1, l2, l3 For all l1, l2 L : l1 l2, l2 l1 l1 = l2 (Anti-Symmetric) Denoted by (L, ) L : l1 l2, l2 l3 l1 l3(Transitive)

Posets In program analysis l1 l2 l1 is more precise than l2 l1 represents fewer concrete states than l2 Examples Total orders (N, ) Powersets (P(S), ) Powersets (P(S), ) Even/Odd Constant propagation Single variable Multiple variables Intervals Bad examples (N, <) Non-transitive x y x = y (x = 0 y=1) (x=1 y=2) Non anti-symmetric

Posets More notations l1 l1 l1 l2 l2 l2 l1 l2 l2 l1 l1 l2 l1 l2

Upper and Lower Bounds Consider a poset (L, ) A subset L L has a lower bound l l A subset L L has an upper bound u : l u A greatest lower bound of a subset L L is a lower bound l0 L such that l l0for any lower bound l of L A lowest upper bound of a subset L L is an upper bound u0 L such that u0 u for any upper bound u of L For every subset L L: The greatest lower bound of L is unique if at all exists L (meet) a b = {a, b} The lowest upper bound of L is unique if at all exists L (join) a b = {a, b} L if for all l L : l L if for all l L

Complete Lattices A poset (L, ) is a complete lattice if every subset has least and upper bounds L = (L, ) = (L, , , , , ) = = L = L = Examples Total orders (N, ) Powersets (P(S), ) Powersets (P(S), ) Constant propagation Intervals

Complete Lattices Lemma For every poset (L, ) the following conditions are equivalent L is a complete lattice Every subset of L has a least upper bound Every subset of L has a greatest lower bound

Cartesian Products A complete lattice (L1, 1) = (L1, , 1, 1, 1, 1) A complete lattice (L2, 2) = (L2, , 2, 2, 2, 2) Define a Poset L = (L1 L2, ) where (x1, x2) (y1, y2) if x1 y1and x2 y2 L is a complete lattice

Finite Maps A complete lattice (L1, 1) = (L1, , 1, 1, 1, 1) A finite set V Define a Poset L = (V L1, ) where e1 e2if for all v V e1v e2v L is a complete lattice

Chains A subset Y L in a poset (L, ) is a chain if every two elements in Y are ordered For all l1, l2 Y: l1 l2 or l2 l1 An ascending chain is a sequence of values l1 l2 l3 A strictly ascending chain is a sequence of values l1 l2 l3 A descending chain is a sequence of values l1 l2 l3 A strictly descending chain is a sequence of values l1 l2 l3 L has a finite height if every chain in L is finite Lemma A poset (L, ) has finite height if and only if every strictly decreasing and strictly increasing chains are finite

Monotone Functions A poset (L, ) A function f: L L is monotone if for every l1, l2 L: l2 f(l1 ) f(l2) l1

Fixed Points f( ) f2( ) A monotone function f: L L where (L, , , , , ) is a complete lattice Fix(f) = { l: l L, f(l) = l} Red(f) = {l: l L, f(l) l} Ext(f) = {l: l L, l f(l)} l1 l2 f(l1 ) Tarski s Theorem 1955: if f is monotone then: lfp(f) = Fix(f) = Red(f) Fix(f) gfp(f) = Fix(f) = Ext(f) Fix(f) Red(f) gfp(f) Fix(f) f(l2) lfp(f) f2( ) Ext(f) f( )

Chaotic Iterations A lattice L = (L, , , , , ) with finite strictly increasing chains Ln= L L L A monotone function f: Ln Ln Compute lfp(f) The simultaneous least fixed of the system {x[i] = fi(x) : 1 i n } for i :=1 to n do x[i] = WL = {1, 2, , n} x := ( , , , ) while (WL ) do select and remove an element i WL while (f(x) x ) do new := fi(x) if (new x[i]) then x := f(x) x[i] := new; Add all the indexes that directly depends on i to WL

Specialized Chaotic Iterations System of Equations S = dfentry[s] = dfentry[v] = {f(u, v) (dfentry[u]) | (u, v) E } FS:Ln Ln FS(X)[s] = FS(X)[v] = {f(u, v)(X[u]) | (u, v) E } lfp(S) = lfp(FS)

Specialized Chaotic Iterations Chaotic(G(V, E): Graph, s: Node, L: Lattice, : L, f: E (L L) ){ for each v in V to n do dfentry[v] := df[s] = WL = {s} while (WL ) do select and remove an element u WL for each v, such that. (u, v) E do temp = f(e)(dfentry[u]) new := dfentry(v) temp if (new dfentry[v]) then dfentry[v] := new; WL := WL {v}

Constant Propagation N 1 Value [x ?, y ?, z ?] WL {2, 3, 4, 5, 6, 7} 1 z :=3 z <=0 [x ?, y ?, z 3] 2 { 3, 4, 5, 6, 7} 2 7 [x ?, y ?, z 3] [x 1, y 7, z 3] [x ?, y 7, z 3] 3 4 5 6 { 4, 5, 6, 7} {5, 6, 7} {6, 7} {7} z >0 3 [x ?, y ?, z 3] [x ?, y 7, z 3] 4 5 6

Example Constant Propagation DF(1) = [x 0] DF(2) = DF(1)[x 3] DF(2) 1 e.e[x 3] e.e skip x :=3 DF(3) = DF(2) 3 2 3t e.e skip DF[1] [x 0] [x 0] [x 7] [x ?] DF[2] [x 3] [x ?] [x 9] [x 3] DF[3] [x 3] [x ?] [x 7] [x 3]

Complexity of Chaotic Iterations Parameters: n the number of CFG nodes k is the maximum outdegree of edges A lattice of height h c is the maximum cost of applying f(e) L comparisons Complexity O(n * h * c * k)

Soundness Every detected constant is indeed such Every error will be detected The least fixed points represents all occurring runtime states Next week

a: f((a)) (f#(a)) f( ) f#( ) f2( ) f#2( ) f(x) x f#(y) y gfp(f) gfp(f#) f(x)=x f#(y)=y lfp(f) lfp(f#) f2( ) f#2( f(x) x f#(y) y f( ) f#( ) )

Finite Height Case f Lfp(f ) Lfp(f #) f# f f # f f #

Soundness Theorem(1) Let( , ) form Galois connection from C to A 1. f: C Cbe a monotone function 2. f#: A Abe a monotone function 3. a A: f( (a)) (f#(a)) 4. lfp(f) (lfp(f#)) (lfp(f)) lfp(f#)

Completeness Every constant is indeed detected as such Every detected error is real Cannot be guaranteed in general

The Join-Over-All-Paths (JOP) Let paths(v) denote the potentially infinite set paths from start to v (written as sequences of labels) For a sequence of edges [e1, e2, , en] define f [e1, e2, , en]: L L by composing the effects of basic blocks f [e1, e2, , en](l) = f(en)( (f(e2)(f(e1) (l)) ) JOP[v] = {f[e1, e2, ,en]( ) [e1, e2, , en] paths(v)}

JOP vs. Least Solution The DF solution obtained by Chaotic iteration satisfies for every l: JOP[v] DFentry(v) A function f is additive (distributive) if f( {x| x X}) = {f(x) | X} If every flis additive (distributive) for all the nodes v JOP[v] = DFentry(v)

Conclusions Chaotic iterations is a powerful technique Easy to implement Rather precise But expensive More efficient methods exist for structured programs Abstract interpretation relates runtime semantics and static information The concrete semantics serves as a tool in designing abstractions More intuition will be given in the sequel

Widening Accelerate the termination of Chaotic iterations by computing a more conservative solution Can handle lattices of infinite heights

Specialized Chaotic Iterations+ Chaotic(G(V, E): Graph, s: Node, L: lattice, : L, f: E (L L) ){ for each v in V to n do dfentry[v] := In[v] = WL = {s} while (WL ) do select and remove an element u WL for each v, such that. (u, v) E do temp = f(e)(dfentry[u]) new := dfentry(v) temp if (new dfentry[v]) then dfentry[v] := new; WL := WL {v}

Example Interval Analysis Find a lower and an upper bound of the value of a variable Usages? Lattice L = (Z {- , } Z {- , }, , , , , ) [a, b] [c, d] if c a and d b [a, b] [c, d] = [min(a, c), max(b, d)] [a, b] [c, d] = [max(a, c), min(b, d)] = =

Example Program Interval Analysis IntEntry(1) = [minint,maxint] [x := 1]1; while [x 1000]2do [x := x + 1;]3 IntExit(1) = [1,1] IntEntry(2) = IntExit(1) IntExit(3) IntExit(2) = IntEntry(2) IntEntry(3) = IntExit(2) [minint,1000] [x:=1]1 IntExit(3) = IntEntry(3)+[1,1] [x 1000]2 [exit]4 IntEntry(4) = IntExit(2) [1001,maxint] [x := x+1]3 IntExit(4) = IntEntry(4)

Widening for Interval Analysis [c, d] = [c, d] [a, b] [c, d] = [ if a c then a else - , if b d then b else ]

Example Program Interval Analysis IntEntry(1) = [- , ] [x := 1]1; while [x 1000]2do [x := x + 1;]3 IntExit(1) = [1,1] IntEntry(2) = InExit(2) (IntExit(1) IntExit(3)) IntExit(2) = IntEntry(2) IntEntry(3) = IntExit(2) [- ,1000] [x:=1]1 IntExit(3) = IntEntry(3)+[1,1] [x 1000]2 [exit]4 IntEntry(4) = IntExit(2) [1001, ] [x := x+1]3 IntExit(4) = IntEntry(4)

Requirements on Widening For all elements l1 For all ascending chains l0 l1 l2 the following sequence is finite y0= l0 yi+1= yi li+1 For a monotonic function f: L L define x0 = xi+1= xi f(xi ) l2 l1 l2 Theorem: There exits k such that xk+1= xk xk Red(f) = {l: l L, f(l) l}

Narrowing Improve the result of widening y x y (x y) For all decreasing chains x0 the following sequence is finite y0= x0 yi+1= yi xi+1 For a monotonic function f: L L and x Red(f) = {l: l L, f(l) l} define y0 = x yi+1= yi f(yi ) x x1 Theorem: There exits k such that yk+1=yk yk Red(f) = {l: l L, f(l) l}

Narrowing for Interval Analysis [a, b] [a, b] [c, d] = [ if a = - = [a, b] then c else a, if b = then d else b ]

Example Program Interval Analysis IntEntry(1) = [- , ] [x := 1]1; while [x 1000]2do [x := x + 1;]3 IntExit(1) = [1,1] IntEntry(2) = InExit(2) ( IntExit(1) IntExit(3)) IntExit(2) = IntEntry(2) IntEntry(3) = IntExit(2) [- ,1000] [x:=1]1 IntExit(3) = IntEntry(3)+[1,1] [x 1000]2 [exit]4 IntEntry(4) = IntExit(2) [1001, ] [x := x+1]3 IntExit(4) = IntEntry(4)

Non Montonicity of Widening [0,1] [0,2] = [0, ] [0,2] [0,2] = [0,2]

Widening and Narrowing Summary Very simple but produces impressive precision Sometimes non-monotonic The McCarthy 91 function int f(x) [- , ] if x > 100 then [101, ] return x -10 [91, -10]; else [- , 100] return f(f(x+11)) [91, 91] ; Also useful in the finite case Can be used as a methodological tool

Numeric Abstract Domain Examples y y y y x x x x signs intervals octagons polyhedra x 0 x [a, b] x y c aixi c

Pointer Language a ::= x | *x | &x | b ::= true | a = a| not b assume b x := a *x := y

Collecting Semantics for Pointers State1= [Loc Loc Z]

Points-To Analysis Lattice Lpt= Galois connection Meaning of statements

t := &a; y := &b; z := &c; if x> 0 then p:= &y; else p:= &z; *p := t;

/* */ t := &a; /* {(t, a)}*/ /* {(t, a)}*/ y := &b; /* {(t, a), (y, b) }*/ /* {(t, a), (y, b)}*/ z := &c; /* {(t, a), (y, b), (z, c) }*/ if x> 0; then p:= &y; /* {(t, a), (y, b), (z, c), (p, y)}*/ else p:= &z; /* {(t, a), (y, b), (z, c), (p, z)}*/ /* {(t, a), (y, b), (z, c), (p, y), (p, z)}*/ *p := t; /* {(t, a), (y, b), (y, c), (p, y), (p, z), (y, a), (z, a)}*/

Abstract Transformers State#= P(Var* Var*) x := a # x := &y # x := *y # x := y # *x := y # assume x ==y # assume x !=y #

/* */ t := &a; /* {(t, a)}*/ /* {(t, a)}*/ y := &b; /* {(t, a), (y, b) }*/ /* {(t, a), (y, b)}*/ z := &c; /* {(t, a), (y, b), (z, c) }*/ if x> 0; then p:= &y; /* {(t, a), (y, b), (z, c), (p, y)}*/ else p:= &z; /* {(t, a), (y, b), (z, c), (p, z)}*/ /* {(t, a), (y, b), (z, c), (p, y), (p, z)}*/ *p := t; /* {(t, a), (y, b), (y, c), (p, y), (p, z), (y, a), (z, a)}*/

Flow insensitive points-to-analysis Steengard 1996 Ignore control flow One set of points-to per program Can be represented as a directed graph Conservative approximation Accumulate pointers Can be computed in almost linear time Union find

t := &a; y := &b; z := &c; if x> 0; then p:= &y; else p:= &z; *p := t;