Static Program Analysis
Part 5 – widening and narrowing
http://cs.au.dk/~amoeller/spa/
øller & . Schwartzbach Computer Science, Aarhus University
Copyright By PowCoder代写 加微信 powcoder
Interval analysis
• Computeupperandlowerboundsforintegers
• Possibleapplications: – array bounds checking – integer representation –…
• Latticeofintervals:
Intervals = lift({ [l,h] | l,h∈N ∧ l ≤ h })
N = {-∞, …,-2,-1,0,1,2, …, ∞}
[l,h]⊑[l,h]iffl ≤l ∧h ≤h 11222112
and intervals are ordered by inclusion:
The interval lattice
[-2,0] [-1,1] [0,2]
[-∞,-1] [-∞,-2]
[1,∞] [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”
Interval analysis lattice
• Thetotallatticeforaprogrampointis Vars → Intervals
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(Vars → Intervals)
– bottom value of lift(Vars → Intervals) represents “unreachable program point”
– bottom value of Vars → Intervals represents “maybe reachable,
but all variables are non-integers”
• Thislatticehasinfiniteheight,sincethechain
[0,0] ⊑ [0,1] ⊑ [0,2] ⊑ [0,3] ⊑ [0,4]…
occurs in Intervals
Interval constraints
• Forassignments:
⟦ x = E ⟧ = JOIN(v)[x→eval(JOIN(v),E)]
• Forallothernodes: ⟦v⟧ = JOIN(v)
where JOIN(v) = ⨆⟦w⟧ w∈pred(v)
Evaluating intervals
• Theevalfunctionisanabstractevaluation: – eval(σ, x) = σ(x)
– eval(σ, intconst) = [intconst,intconst]
– eval(σ, E1 op E2) = op(eval(σ,E1),eval(σ,E2))
• Abstractoperators:
– 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]
Fixed-point problems
• Thelatticehasinfiniteheight,
so the fixed-point algorithm does not work
f (⊥) for i = 0, 1, …
is not guaranteed to converge
• The sequence of approximants i
• (Exercise: give an example of a program where this happens)
• Restrictingto32bitintegersisnotapracticalsolution
• Wideninggivesausefulsolution…
Does the least fixed point exist?
• Thelatticehasinfiniteheight,
so Kleene’s fixed-point theorem does not apply
• Tarski’s fixed-point theorem:
In a complete lattice L, every monotone function f: L → L has a unique least fixed point given by
lfp(f) = ⨅{ x∈L | f(x) ⊑ x}
• Introduceawideningfunctionω:L→Lsothat (ωf)i(⊥) for i = 0, 1, …
approximation of each f (⊥)
• i.e. the function ω coarsens the information
converges on a fixed point that is a safe i
Turbo charging the iterations
Simple widening for intervals
• Thefunctionω:L→Lisdefinedpointwiseon L = (Vars → Intervals)n
– must contain -∞ and ∞ (to retain the ⊤ element)
• ParameterizedwithafixedfinitesetB
– typically seeded with all integer constants occurring in the given program
• Idea:Findthenearestenclosingallowedinterval • On single elements from Intervals :
-∞ -87 5 117 ∞
ω([a,b]) = [ max{i∈B|i≤a}, min{i∈B|b≤i} ]
[1,42] ω([1,42])
Divergence in action
while (input) {
[x→ ⊥,y→ ⊥]
[x → [8,8], y → [0,1]] [x → [8,8], y → [0,2]] [x → [8,8], y → [0,3]] …
Simple widening in action
while (input) {
B = {-∞,0,1,7, ∞}
[x→ ⊥,y→ ⊥]
[x → [7,∞], y → [0,1]] [x → [7,∞], y → [0,7]] [x → [7,∞], y → [0,∞]]
Correctness of simple widening
• Thisformofwideningworkswhen:
– ω is an extensive and monotone function, and – the sub-lattice ω(L) has finite height
so (ω f) (⊥) for i = 0, 1, … converges
• ω f is monotone and ω(L) has finite height,
• Let f = (ω f) (⊥) where (ω f) (⊥) = (ω f) (⊥) ω
• lfp(f) ⊑ f follows from Tarski’s fixed-point theorem, ω
i.e., fω is a safe approximation of lfp(f)
• Widening generally shoots over the target
• Narrowingmayimprovetheresultbyapplyingf
• We have f(f ) ⊑ f so applying f again may ωω
improve the result!
• And we also have lfp(f) ⊑ f(f ) so it remains safe!
• Thiscanbeiteratedarbitrarilymanytimes – may diverge, but safe to stop anytime
Backing up
Narrowing in action
while (input) {
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,∞]]
Correctness of (repeated) narrowing
Claim:lfp(f)⊑…⊑fi(f )⊑…⊑ f(f )⊑f ωωω
• f(f ) ⊑ ω(f(f )) = (ω f)(f ) = f since ω is extensive ωωωω
f (f)⊑f(f)⊑f
– by monotonicity of f and induction we also have, for all i:
• f(f )⊑f sof(f(f ))⊑f(f )bymonotonicityoff, ωωωω
– i.e. fi+1(f ) is at least as precise as fi(f ) ωω
hence lfp(f) ⊑ f(f ) by Tarski’s fixed-point theorem ω
i lfp(f)⊑f(f )
– by induction we also have, for all i:
– i.e. fi(fω) is a safe approximation of lfp(f)
Some observations
• Thesimplenotionofwideningisabitnaive…
• Wideninghappensateveryintervalandateverynode
• There’s no need to widen intervals that are not “unstable”
• There’s no need to widen
if there are no “cycles” in the dataflow
More powerful widening
• Awideningisafunction∇:L×L→Lthatisextensivein both arguments and satisfies the following property:
forallincreasingchainsz ⊑z ⊑…, 01
the sequence y = z , …, y = y ∇ z ,… converges 0 0 i+1 i i+1
(i.e. stabilizes after a finite number of steps)
• Nowreplacethebasicfixedpointsolverbycomputing
x =⊥ and x =x ∇f(x) untilconvergence 0 i+1ii
• Theorem: xk+1 = xk and lfp(f) ⊑ xk for some k (Proof: similar to the correctness proof for simple widening)
More powerful widening for interval analysis
[a1,b1] ∇ [a2,b2] =
Extrapolates unstable bounds to B:
[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 get the same result as with simple widening plus narrowing (but now without using narrowing)
Yet another improvement
• Divergence(e.g.intheintervalanalysiswithout widening) can only appear in presence of recursive dataflow constraint
• Sufficientto“breakthecycles”,performwideningonly at, for example, loop heads in the CFG
Choosing the set B
• Definingthewideningfunctionbasedonconstants
occurring in the given program may not work well
f(x) { // ”McCarthy’s 91 function”
if (x > 100) {
r = x – 10;
r = f(f(x + 11));
return r; }
https://en.wikipedia.org/wiki/McCarthy_91_function
• (This example requires interprocedural and control-sensitive analysis)
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com