程序代写代做代考 algorithm chain Static Program Analysis

Static Program Analysis
Part 5 – widening and narrowing
http://cs.au.dk/~amoeller/spa/
Anders Møller & Michael I. Schwartzbach Computer Science, Aarhus University

Interval analysis
• Computeupperandlowerboundsforintegers
• Possibleapplications: – array bounds checking – integer representation –…
• Lattice of intervals:
Interval = lift({ [l,h] | l,hN  l  h })
where
N = {-, …,-2,-1,0,1,2, …, }
and intervals are ordered by inclusion: [l1,h1]⊑[l2,h2] iff l2  l1  h1  h2
2

The interval lattice
[-,]
[-2,2]
[-1,2]
[-2,0] [-1,1] [0,2]
[-,0]
[-2,1]
[0,]
[-,-1] [-,-2]
[1,] [2,]
[2,2]
[-2,-1] [-1,0] [0,1] [1,2]
[-2,-2] [-1,-1] [0,0] [1,1]
⊥
bottom element here interpreted as “not an integer”
3

Interval analysis lattice
• The total lattice for a program point is L = Vars  Interval
that provides bounds for each (integer) variable
• If using the worklist solver that initializes the worklist with only the entry node, use the lattice lift(L)
– bottom value of lift(L) represents “unreachable program point”
– bottom value of L represents “maybe reachable, but all variables are non-integers”
• Thislatticehasinfiniteheight,sincethechain
[0,0] ⊑ [0,1] ⊑ [0,2] ⊑ [0,3] ⊑ [0,4]…
occurs in Interval
4

Interval constraints
• Forassignments:
⟦ x = E ⟧ = JOIN(v)[xeval(JOIN(v),E)]
• For all other nodes: ⟦v⟧ = JOIN(v)
where JOIN(v) = ⨆⟦w⟧ wpred(v)
5

Evaluating intervals
• Theevalfunctionisanabstractevaluation: – eval(, x) = (x)
– eval(, intconst) = [intconst,intconst]
– eval(, E1 op E2) = op(eval(,E1),eval(,E2))
• Abstractarithmeticoperators: – op([l1,h1],[l2,h2]) =
not trivial to implement!
[ min xopy, max xopy] x[l1,h1], y[l2,h2] x[l1,h1], y[l2,h2]
• Abstractcomparisonoperators(couldbeimproved): – op([l1,h1],[l2,h2]) = [0,1]
6

Fixed-point problems
• The lattice has infinite height, so the fixed-point algorithm does not work
• In Ln, the sequence of approximants fi(⊥, ⊥, …, ⊥)
is not guaranteed to converge
• (Exercise: give an example of a program where this happens)
• Restricting to 32 bit integers is not a practical solution
• Widening gives a useful solution…
7

Widening
• Introduceawideningfunction:LnLnsothat (f)i(⊥, ⊥, …, ⊥)
converges on a fixed-point that is a safe approximation of each fi(⊥, ⊥, …, ⊥)
• i.e.thefunctioncoarsenstheinformation
8

Turbo charging the iterations

f
9

Widening for intervals
• ThefunctionisdefinedpointwiseonLn
• ParameterizedwithafixedfinitesubsetBN
–mustcontain-and (toretainthe⊤element)
– typically seeded with all integer constants occurring in the given program
• Idea: Find the nearest enclosing allowed interval • OnsingleelementsfromInterval:
([a,b]) = [ max{iB|ia}, min{iB|bi} ] (⊥) = ⊥
10

Divergence in action
y = 0;
x = 7;
x = x+1;
while (input) {
x = 7; x = x+1; y = y+1;
}
[x ,y ]
[x  [8,8], y  [0,1]] [x  [8,8], y  [0,2]] [x  [8,8], y  [0,3]] …
11

Widening in action
y = 0;
x = 7;
x = x+1;
while (input) {
x = 7; x = x+1; y = y+1;
}
B = {-,0,1,7, }
[x ,y ]
[x  [7,], y  [0,1]] [x  [7,], y  [0,7]] [x  [7,], y  [0,]]
12

Correctness of widening
• Wideningworkswhen:
–  is an extensive and monotone function, and – (L) is a finite-height lattice
• Safety: i: fi(⊥, ⊥, …, ⊥) ⊑ (f)i(⊥, ⊥, …, ⊥) since f is monotone and  is extensive
• f is a monotone function (L)(L)
so the fixed-point exists
• Almost“correctbydefinition”!
• When used in the worklist algorithm, it suffices to apply widening on back-edges in the CFG
13

Narrowing
• Widening generally shoots over the target
• Narrowing may improve the result by applying f
• Define:
fix = ⨆ fi(⊥, ⊥, …, ⊥) fix = ⨆ (f)i(⊥, ⊥, …, ⊥) then fix ⊑ fix
• But we also have that fix ⊑ f(fix) ⊑ fix
so applying f again may improve the result and remain sound!
• Thiscanbeiteratedarbitrarilymanytimes – may diverge, but safe to stop anytime
14

f
Backing up

15

Narrowing in action
y = 0;
x = 7;
x = x+1;
while (input) {
x = 7; x = x+1; y = y+1;
}
B = {-,0,1,7, }
[x ,y ]
[x  [7,], y  [0,1]] [x  [7,], y  [0,7]] [x  [7,], y  [0,]] …
[x  [8,8], y  [0,]]
16

Correctness of (repeated) narrowing
• f(fix)⊑(f(fix))=(f)(fix)=fix since  is extensive
– by induction we also have, for all i: fi+1(fix) ⊑ fi(fix) ⊑ fix
– i.e. fi+1(fix) is at least as precise as fi(fix) • fix⊑fixhencef(fix)=fix⊑f(fix)
by monotonicity of f
– by induction we also have, for all i:
fix ⊑ fi(fix)
– i.e. fi(fix) is a sound approximation of fix
17

More powerful widening
• Definingthewideningfunctionbasedonconstants occurring in the given program may not work
f(x) { // ”McCarthy’s 91 function”
var r;
if (x > 100) { r = x – 10;
} else {
r = f(f(x + 11));
}
return r; }
https://en.wikipedia.org/wiki/McCarthy_91_function
• Note: this example requires interprocedural analysis…
18

More powerful widening
• A widening is a function ∇: L  L →L that is extensive in both arguments and satisfies the following property:
for all increasing chains z0 ⊑ z1 ⊑ …,
the sequence y0 = z0, …, yi+1 = yi ∇ zi+1 ,… converges (i.e. stabilizes after a finite number of steps)
• Now replace the basic fixed point solver by computing x0 = , …, xi+1 = xi ∇ F(xi), … until convergence
19

More powerful widening for interval analysis
Extrapolates unstable bounds to B:
⊥∇y = y
x∇⊥=x
[a1,b1] ∇ [a2,b2] =
[if a1  a2 then a1 else max{iB|ia2}, if b2  b1 then b1 else min{iB|b2i}]
The ∇ operator on L is then defined pointwise down to individual intervals
For the small example program, we now get the same result as with simple widening plus narrowing (but now without using narrowing)
20