IA159 Formal Verification Methods
Static Analysis and Abstract Interpretation
Jan Strejˇcek
Faculty of Informatics
Masaryk University
Focus and sources
Focus
lattices and fixpoints
static analysis
abstract interpretation
Source
P. Cousot and R. Cousot: Abstract Interpretation: A Unified
Lattice Model for Static Analysis of Programs by
Construction or Approximation of Fixpoints, POPL 1977.
Special thanks to Marek Trtík for providing me his slides.
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 2/73
Motivation for static analysis
Floyd’s conjecture
To prove static properties of program it is often sufficient to
consider sets of states associated with each program point.
Examples
to check safety properties (reachability of an error state),
one only needs to know reachable states
for many optimizations during compilation, static
information is sufficient (e.g. detection of live variables,
available expressions, etc.)
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 3/73
Motivation for static analysis
Operational semantics
defines how a state changes along program execution
it is concerned about computational sequences
computes a function relating input and output states
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 4/73
Motivation for static analysis
Operational semantics
defines how a state changes along program execution
it is concerned about computational sequences
computes a function relating input and output states
Static semantic
observes which states pass which program location
it is concerned about observed sets of states at locations
computes a function assigning set of states to each
program location
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 5/73
Motivation for abstract interpretation
It is usually impossible to compute the sets of reachable
states precisely
we can compute them on some level of abstraction
for example, instead with precise numbers we work only
with abstract values {+, 0, −}
abstraction brings some level of imprecission, for example,
15 − 17 is seen as (+) − (+), which can be +, 0, −
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 6/73
Preliminaries
Lattices and fixpoints
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 7/73
Introduction to lattices
Let (L, ≤) be a partially ordered set and M ⊆ L.
x ∈ L is an upper bound of M iff y ≤ x holds for all y ∈ M
x ∈ L is a lower bound of M iff x ≤ y holds for all y ∈ M
supremum of M is the least upper bound of M
infimum of M is the greatest lower bound of M
sup(M) and inf(M) denote supremum and infimum of M,
respectively
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 8/73
Introduction to lattices
Let (L, ≤) be a partially ordered set and M ⊆ L.
x ∈ L is an upper bound of M iff y ≤ x holds for all y ∈ M
x ∈ L is a lower bound of M iff x ≤ y holds for all y ∈ M
supremum of M is the least upper bound of M
infimum of M is the greatest lower bound of M
sup(M) and inf(M) denote supremum and infimum of M,
respectively
Definition (Complete lattice)
An ordered set (L, ≤) is called complete lattice, if for each
M ⊆ L there exist both sup(M) and inf(M).
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 9/73
Introduction to lattices
Which of the partially ordered sets are complete lattices?
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 10/73
Introduction to lattices
Which of the partially ordered sets are complete lattices?
(All of the top row and the left of the bottom row.)
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 11/73
Introduction to lattices
For every set S, the powerset P(S) with the partial order ⊆ is
a complete lattice.
For example, (P({0, 1, 2, 3}), ⊆) looks like:
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 12/73
Introduction to lattices
Let (L, ≤) be a complete lattice.
the greatest element = sup(L) is called one of L
the least element ⊥ = inf(L) of L is called zero of L
the lattice is of finite height if there exists h ∈ N such that
the length of each strictly increasing chain of elements of L
is less than or equal to h
minimal such h is called lattice height
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 13/73
Fixpoint and Knaster-Tarski fixpoint theorem
Let (L, ≤) be a complete lattice.
a function f : L → L is monotone if for all x, y ∈ L it holds
x ≤ y =⇒ f(x) ≤ f(y)
x ∈ L is called a fixpoint of f if f(x) = x
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 14/73
Fixpoint and Knaster-Tarski fixpoint theorem
Let (L, ≤) be a complete lattice.
a function f : L → L is monotone if for all x, y ∈ L it holds
x ≤ y =⇒ f(x) ≤ f(y)
x ∈ L is called a fixpoint of f if f(x) = x
Theorem (Knaster-Tarski)
Let (L, ≤) be a complete lattice and f : L → L be a monotone
function. Then the set of fixpoints of f with partial order ≤ is
also a complete lattice.
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 15/73
Kleene fixpoint theorem
Theorem (Kleene)
Let (L, ≤) be a complete lattice of finite height and f : L → L a
monotone function. Then there exists n ∈ N such that for all
k ∈ N it is fn(⊥) = fn+k (⊥) and fn(⊥) is the least fixpoint of f.
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 16/73
Kleene fixpoint theorem
Theorem (Kleene)
Let (L, ≤) be a complete lattice of finite height and f : L → L a
monotone function. Then there exists n ∈ N such that for all
k ∈ N it is fn(⊥) = fn+k (⊥) and fn(⊥) is the least fixpoint of f.
Proof: Since ⊥ is the least element of L, we have ⊥ ≤ f(⊥).
Since f is monotone, them f(⊥) ≤ f(f(⊥)) and by induction
fi(⊥) ≤ fi+1(⊥). Thus, we have a nondecreasing chain
⊥ ≤ f(⊥) ≤ f2(⊥) ≤ . . .. Since L is assumed to be of a finite
height, there must exist n ∈ N such that fn(⊥) = fn+1(⊥). To
show that fn(⊥) is a least fixpoint of f, let us assume x is
another fixpoint of f. Since ⊥ ≤ x and f(⊥) ≤ f(x) = x from
monotonicity of f, we get by induction fn(⊥) ≤ x.
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 17/73
Fixpoint computation
Algorithm for the least fixpoint computation
x := ⊥;
do { t := x; x := f(x); } while (x = t);
If we start with x := ;, we get the greatest fixpoint.
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 18/73
Product lattice
Lemma (Product lattice)
Let (L1, ≤1), . . . , (Ln, ≤n) be complete lattices and order ≤ on
L1 × . . . × Ln is defined as (x1, . . . , xn) ≤ (y1, . . . , yn) iff
x1 ≤1 y1 ∧ . . . ∧ xn ≤n yn.
Then (L1 × . . . × Ln, ≤) is a complete lattice.
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 19/73
Fixpoints on product lattices
Let (L, ≤) be a complete lattice and (Ln, ) be the
corresponding product lattice. Further, let F1, . . . , Fn : Ln → L
be monotone functions, i.e. (x1, . . . , xn) (y1, . . . , yn) implies
Fi(x1, . . . , xn) ≤ Fi(y1, . . . , yn) for each 1 ≤ i ≤ n. Then the
function F : Ln → Ln defined as
F(x1, . . . , xn) = (F1(x1, . . . , xn), . . . , Fn(x1, . . . , xn))
is a monotone function in (Ln, ). Further, the least fixpoint of F
is the least solution of the system
x1 = F1(x1, . . . , xn)
...
xn = Fn(x1, . . . , xn)
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 20/73
Fixpoint comutation of product lattices
Naive algorithm for fixpoint computation
x := ⊥;
do { t := x; x := F(x); } while (x = t);
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 21/73
Fixpoint comutation of product lattices
Naive algorithm for fixpoint computation
x := ⊥;
do { t := x; x := F(x); } while (x = t);
Better algorithm for fixpoint computation (faster convergence)
x1 := ⊥; . . . xn := ⊥;
do {
t1 := x1; . . . tn := xn;
x1 := F1(x1, . . . , xn);
...
xn := Fn(x1, . . . , xn);
} while (x1 = t1 ∨ . . . ∨ xn = tn);
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 22/73
Moving to abstraction
Abstract interpretation
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 23/73
Abstract interpretation
an abstract interpretation of a program is kind of a static
semantic, where original data domains are replaced with
abstract ones
abstract data domain must constitute a complete lattice
semantic of program instructions have to be changed as
well: we define unique monotone function for each
program instruction
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 24/73
Abstract interpretation: Definition
Definition (Abstract interpretation)
An abstract interpretation I of a program P with n program
locations is a tuple
I = L, ◦, ≤, , ⊥, F
where (L, ≤) is complete lattice, and ⊥ are one and zero of
(L, ≤), ◦ is equal either to join or meet operation, and F is a
monotone function on product lattice (Ln, ≤) defining the
interpretation of basic instructions.
The meet operator is defined as a ◦ b = inf({a, b}), while
the join operator is defined as a ◦ b = sup({a, b}).
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 25/73
Abstract interpretation: Definition
Definition (Abstract interpretation)
An abstract interpretation I of a program P with n program
locations is a tuple
I = L, ◦, ≤, , ⊥, F
where (L, ≤) is complete lattice, and ⊥ are one and zero of
(L, ≤), ◦ is equal either to join or meet operation, and F is a
monotone function on product lattice (Ln, ≤) defining the
interpretation of basic instructions.
The meet operator is defined as a ◦ b = inf({a, b}), while
the join operator is defined as a ◦ b = sup({a, b}).
Typically, F(x) = (F1(x), . . . , Fn(x)), where each Fi : Ln → L
defines effect of i-th program instruction.
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 26/73
Example: Available expressions
A nontrivial expression in a program is available at a program
location if its current value has already been computed earlier
in the execution.
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 27/73
Example: Available expressions
A nontrivial expression in a program is available at a program
location if its current value has already been computed earlier
in the execution.
var x,y,z,a,b;
z := a+b;
y := a*b;
while (y > a+b) {
a := a+1;
x := a+b;
}
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 28/73
Example: Available expressions
A nontrivial expression in a program is available at a program
location if its current value has already been computed earlier
in the execution.
Available expressions: AExprs = {a+b, a*b, y>a+b, a+1}
var x,y,z,a,b;
z := a+b;
y := a*b;
while (y > a+b) {
a := a+1;
x := a+b;
}
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 29/73
Example: Available expressions
A nontrivial expression in a program is available at a program
location if its current value has already been computed earlier
in the execution.
Available expressions: AExprs = {a+b, a*b, y>a+b, a+1}
A.I.: I = P(AExprs), ∩, ⊆, AExprs, ∅, λx.(F1(x), . . . , F6(x))
var x,y,z,a,b;
z := a+b;
y := a*b;
while (y > a+b) {
a := a+1;
x := a+b;
}
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 30/73
Example: Available expressions
A nontrivial expression in a program is available at a program
location if its current value has already been computed earlier
in the execution.
Available expressions: AExprs = {a+b, a*b, y>a+b, a+1}
A.I.: I = P(AExprs), ∩, ⊆, AExprs, ∅, λx.(F1(x), . . . , F6(x))
Product lattice: (P6(AExprs), ≤).
var x,y,z,a,b; x1
z := a+b; x2
y := a*b; x3
while (y > a+b) { x4
a := a+1; x5
x := a+b; x6
}
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 31/73
Example: Available expressions
A nontrivial expression in a program is available at a program
location if its current value has already been computed earlier
in the execution.
Available expressions: AExprs = {a+b, a*b, y>a+b, a+1}
A.I.: I = P(AExprs), ∩, ⊆, AExprs, ∅, λx.(F1(x), . . . , F6(x))
Product lattice: (P6(AExprs), ≤).
var x,y,z,a,b; x1 = F1(x) = ∅
z := a+b; x2 = F2(x) = (x1 ∪ {a+b}) ∅
y := a*b; x3 = F3(x) = (x2 ∪ {a*b}) {y>a+b}
while (y > a+b) { x4 = F4(x) = (x3 ∩ x6) ∪ {a+b, y>a+b}
a := a+1; x5 = F5(x) = (x4 ∪ {a+1}) AExprs
x := a+b; x6 = F6(x) = (x5 ∪ {a+b}) ∅
}
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 32/73
Example: Available expressions
A nontrivial expression in a program is available at a program
location if its current value has already been computed earlier
in the execution.
Available expressions: AExprs = {a+b, a*b, y>a+b, a+1}
A.I.: I = P(AExprs), ∩, ⊆, AExprs, ∅, λx.(F1(x), . . . , F6(x))
Product lattice: (P6(AExprs), ≤).
var x,y,z,a,b; x1 = F1(x) = ∅
z := a+b; x2 = F2(x) = (x1 ∪ {a+b}) ∅
y := a*b; x3 = F3(x) = (x2 ∪ {a*b}) {y>a+b}
while (y > a+b) { x4 = F4(x) = (x3 ∩ x6) ∪ {a+b, y>a+b}
a := a+1; x5 = F5(x) = (x4 ∪ {a+1}) AExprs
x := a+b; x6 = F6(x) = (x5 ∪ {a+b}) ∅
}
Direction: Forward
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 33/73
Example: Available expressions
A nontrivial expression in a program is available at a program
location if its current value has already been computed earlier
in the execution.
Available expressions: AExprs = {a+b, a*b, y>a+b, a+1}
A.I.: I = P(AExprs), ∩, ⊆, AExprs, ∅, λx.(F1(x), . . . , F6(x))
Product lattice: (P6(AExprs), ≤).
var x,y,z,a,b; x1 = F1(x) = ∅
z := a+b; x2 = F2(x) = (x1 ∪ {a+b}) ∅
y := a*b; x3 = F3(x) = (x2 ∪ {a*b}) {y>a+b}
while (y > a+b) { x4 = F4(x) = (x3 ∩ x6) ∪ {a+b, y>a+b}
a := a+1; x5 = F5(x) = (x4 ∪ {a+1}) AExprs
x := a+b; x6 = F6(x) = (x5 ∪ {a+b}) ∅
}
Analysis: Must
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 34/73
Example: Available expressions
A nontrivial expression in a program is available at a program
location if its current value has already been computed earlier
in the execution.
Available expressions: AExprs = {a+b, a*b, y>a+b, a+1}
A.I.: I = P(AExprs), ∩, ⊆, AExprs, ∅, λx.(F1(x), . . . , F6(x))
Product lattice: (P6(AExprs), ≤).
var x,y,z,a,b; x1 = F1(x) = ∅
z := a+b; x2 = F2(x) = (x1 ∪ {a+b}) ∅
y := a*b; x3 = F3(x) = (x2 ∪ {a*b}) {y>a+b}
while (y > a+b) { x4 = F4(x) = (x3 ∩ x6) ∪ {a+b, y>a+b}
a := a+1; x5 = F5(x) = (x4 ∪ {a+1}) AExprs
x := a+b; x6 = F6(x) = (x5 ∪ {a+b}) ∅
}
Are all functions Fi monotone?
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 35/73
Example: Available expressions
A nontrivial expression in a program is available at a program
location if its current value has already been computed earlier
in the execution.
Available expressions: AExprs = {a+b, a*b, y>a+b, a+1}
A.I.: I = P(AExprs), ∩, ⊆, AExprs, ∅, λx.(F1(x), . . . , F6(x))
Product lattice: (P6(AExprs), ≤).
var x,y,z,a,b; x1 = F1(x) = ∅
z := a+b; x2 = F2(x) = (x1 ∪ {a+b}) ∅
y := a*b; x3 = F3(x) = (x2 ∪ {a*b}) {y>a+b}
while (y > a+b) { x4 = F4(x) = (x3 ∩ x6) ∪ {a+b, y>a+b}
a := a+1; x5 = F5(x) = (x4 ∪ {a+1}) AExprs
x := a+b; x6 = F6(x) = (x5 ∪ {a+b}) ∅
}
Proof F4: Let x, y ∈ P6(AExprs) such that x ≤ y. . . .
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 36/73
Example: Available expressions
A nontrivial expression in a program is available at a program
location if its current value has already been computed earlier
in the execution.
Available expressions: AExprs = {a+b, a*b, y>a+b, a+1}
A.I.: I = P(AExprs), ∩, ⊆, AExprs, ∅, λx.(F1(x), . . . , F6(x))
Product lattice: (P6(AExprs), ≤).
var x,y,z,a,b; x1 = F1(x) = ∅
z := a+b; x2 = F2(x) = (x1 ∪ {a+b}) ∅
y := a*b; x3 = F3(x) = (x2 ∪ {a*b}) {y>a+b}
while (y > a+b) { x4 = F4(x) = (x3 ∩ x6) ∪ {a+b, y>a+b}
a := a+1; x5 = F5(x) = (x4 ∪ {a+1}) AExprs
x := a+b; x6 = F6(x) = (x5 ∪ {a+b}) ∅
}
Then x3 ⊆ y3 and x6 ⊆ y6, which implies (x3 ∩ x6) ⊆ (y3 ∩ y6). . .
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 37/73
Example: Available expressions
After fixpoint computation ...
var x,y,z,a,b; x1 = ∅
z := a+b; x2 = {a+b}
y := a*b; x3 = {a+b, a*b}
while (y > a+b) { x4 = {a+b, y>a+b}
a := a+1; x5 = ∅
x := a+b; x6 = {a+b}
}
Solution: Minimal
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 38/73
Example: Available expressions
After fixpoint computation ...
var x,y,z,a,b; x1 = ∅
z := a+b; x2 = {a+b}
y := a*b; x3 = {a+b, a*b}
while (y > a+b) { x4 = {a+b, y>a+b}
a := a+1; x5 = ∅
x := a+b; x6 = {a+b}
}
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 39/73
Example: Live variables
A variable is live at a program point if its current value may be
read during the remaining execution of the program.
var x,y,z;
x := input;
while (x>1) {
y := x/2;
if (y>3)
x := x-y;
z := x-4;
if (z>0)
x := x/2;
z := z-1; }
output x;
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 40/73
Example: Live variables
A variable is live at a program point if its current value may be
read during the remaining execution of the program.
Vars = {x,y,z} and
I = P(Vars), ∪, ⊆, Vars, ∅, λx.(F1(x), . . . , F11(x))
var x,y,z;
x := input;
while (x>1) {
y := x/2;
if (y>3)
x := x-y;
z := x-4;
if (z>0)
x := x/2;
z := z-1; }
output x;
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 41/73
Example: Live variables
A variable is live at a program point if its current value may be
read during the remaining execution of the program.
Product lattice is (P11(Vars), ≤).
x1 = x2 {x,y,z} var x,y,z;
x2 = x3 {x} x := input;
x3 = (x4 ∪ x11) ∪ {x} while (x>1) {
x4 = (x5 {y}) ∪ {x} y := x/2;
x5 = (x6 ∪ x7) ∪ {y} if (y>3)
x6 = (x7 {x}) ∪ {x,y} x := x-y;
x7 = (x8 {z}) ∪ {x} z := x-4;
x8 = (x9 ∪ x10) ∪ {z} if (z>0)
x9 = (x10 {x}) ∪ {x} x := x/2;
x10 = (x3 {z}) ∪ {z} z := z-1; }
x11 = {x} output x;
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 42/73
Example: Live variables
A variable is live at a program point if its current value may be
read during the remaining execution of the program.
Direction: Backward
x1 = x2 {x,y,z} var x,y,z;
x2 = x3 {x} x := input;
x3 = (x4 ∪ x11) ∪ {x} while (x>1) {
x4 = (x5 {y}) ∪ {x} y := x/2;
x5 = (x6 ∪ x7) ∪ {y} if (y>3)
x6 = (x7 {x}) ∪ {x,y} x := x-y;
x7 = (x8 {z}) ∪ {x} z := x-4;
x8 = (x9 ∪ x10) ∪ {z} if (z>0)
x9 = (x10 {x}) ∪ {x} x := x/2;
x10 = (x3 {z}) ∪ {z} z := z-1; }
x11 = {x} output x;
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 43/73
Example: Live variables
A variable is live at a program point if its current value may be
read during the remaining execution of the program.
Analysis: May
x1 = x2 {x,y,z} var x,y,z;
x2 = x3 {x} x := input;
x3 = (x4 ∪ x11) ∪ {x} while (x>1) {
x4 = (x5 {y}) ∪ {x} y := x/2;
x5 = (x6 ∪ x7) ∪ {y} if (y>3)
x6 = (x7 {x}) ∪ {x,y} x := x-y;
x7 = (x8 {z}) ∪ {x} z := x-4;
x8 = (x9 ∪ x10) ∪ {z} if (z>0)
x9 = (x10 {x}) ∪ {x} x := x/2;
x10 = (x3 {z}) ∪ {z} z := z-1; }
x11 = {x} output x;
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 44/73
Example: Live variables
A variable is live at a program point if its current value may be
read during the remaining execution of the program.
Solution: Minimal
x1 = ∅ x1 = x2 {x,y,z} var x,y,z;
x2 = ∅ x2 = x3 {x} x := input;
x3 = {x} x3 = (x4 ∪ x11) ∪ {x} while (x>1) {
x4 = {x} x4 = (x5 {y}) ∪ {x} y := x/2;
x5 = {x,y} x5 = (x6 ∪ x7) ∪ {y} if (y>3)
x6 = {x,y} x6 = (x7 {x}) ∪ {x,y} x := x-y;
x7 = {x} x7 = (x8 {z}) ∪ {x} z := x-4;
x8 = {x,z} x8 = (x9 ∪ x10) ∪ {z} if (z>0)
x9 = {x,z} x9 = (x10 {x}) ∪ {x} x := x/2;
x10 = {x,z} x10 = (x3 {z}) ∪ {z} z := z-1; }
x11 = {x} x11 = {x} output x;
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 45/73
Example: Live variables
A variable is live at a program point if its current value may be
read during the remaining execution of the program.
Variables y,z are never live together.
x1 = ∅ x1 = x2 {x,y,z} var x,y,z;
x2 = ∅ x2 = x3 {x} x := input;
x3 = {x} x3 = (x4 ∪ x11) ∪ {x} while (x>1) {
x4 = {x} x4 = (x5 {y}) ∪ {x} y := x/2;
x5 = {x,y} x5 = (x6 ∪ x7) ∪ {y} if (y>3)
x6 = {x,y} x6 = (x7 {x}) ∪ {x,y} x := x-y;
x7 = {x} x7 = (x8 {z}) ∪ {x} z := x-4;
x8 = {x,z} x8 = (x9 ∪ x10) ∪ {z} if (z>0)
x9 = {x,z} x9 = (x10 {x}) ∪ {x} x := x/2;
x10 = {x,z} x10 = (x3 {z}) ∪ {z} z := z-1; }
x11 = {x} x11 = {x} output x;
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 46/73
Example: Reaching definitions
The reaching definitions for a given program point are those
assignments that may have defined the current values of
variables.
var x,y,z;
x := input;
while (x>1) {
y := x/2;
if (y>3)
x := x-y;
z := x-4;
if (z>0)
x := x/2;
z := z-1; }
output x;
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 47/73
Example: Reaching definitions
The reaching definitions for a given program point are those
assignments that may have defined the current values of
variables.
var x,y,z;
x := input;
while (x>1) {
y := x/2;
if (y>3)
x := x-y;
z := x-4;
if (z>0)
x := x/2;
z := z-1; }
output x;
Assignments:
Asgns = {x=input, y=x/2, x=x-y,
z=x-4, x=x/2, z=z-1}
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 48/73
Example: Reaching definitions
The reaching definitions for a given program point are those
assignments that may have defined the current values of
variables.
var x,y,z;
x := input;
while (x>1) {
y := x/2;
if (y>3)
x := x-y;
z := x-4;
if (z>0)
x := x/2;
z := z-1; }
output x;
Assignments:
Asgns = {x=input, y=x/2, x=x-y,
z=x-4, x=x/2, z=z-1}
I = P(Asgns), ∪, ⊆, Asgns, ∅,
λx.(F1(x), . . . , F11(x))
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 49/73
Example: Reaching definitions
The reaching definitions for a given program point are those
assignments that may have defined the current values of
variables.
var x,y,z;
x := input;
while (x>1) {
y := x/2;
if (y>3)
x := x-y;
z := x-4;
if (z>0)
x := x/2;
z := z-1; }
output x;
Assignments:
Asgns = {x=input, y=x/2, x=x-y,
z=x-4, x=x/2, z=z-1}
I = P(Asgns), ∪, ⊆, Asgns, ∅,
λx.(F1(x), . . . , F11(x))
Product lattice: (P11(Asgns), ⊆)
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 50/73
Example: Reaching definitions
The reaching definitions for a given program point are those
assignments that may have defined the current values of
variables.
var x,y,z;
x := input;
while (x>1) {
y := x/2;
if (y>3)
x := x-y;
z := x-4;
if (z>0)
x := x/2;
z := z-1; }
output x;
Assignments:
Asgns = {x=input, y=x/2, x=x-y,
z=x-4, x=x/2, z=z-1}
I = P(Asgns), ∪, ⊆, Asgns, ∅,
λx.(F1(x), . . . , F11(x))
Product lattice: (P11(Asgns), ⊆)
Direction: Forward
Analysis: May
Solution: Minimal
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 51/73
Example: Busy expressions
An expression is busy if it will definitely be evaluated again
before its value changes.
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 52/73
Example: Busy expressions
An expression is busy if it will definitely be evaluated again
before its value changes.
Direction: Backward
Analysis: Must
Solution: Minimal
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 53/73
Computing variable values: different abstraction levels
We may consider different abstraction levels of variable values:
sets of integer values: P(Z)
intervals: {[l, u] | l, u ∈ Z ∪ {−∞, ∞}, l ≤ u} ∪ {⊥}
only signs with zero: P({−, 0, +})
initialized or not: {⊥, }
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 54/73
Computing variable values: different abstraction levels
We may consider different abstraction levels of variable values:
sets of integer values: P(Z)
intervals: {[l, u] | l, u ∈ Z ∪ {−∞, ∞}, l ≤ u} ∪ {⊥}
only signs with zero: P({−, 0, +})
initialized or not: {⊥, }
Which abstraction is more precise than other?
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 55/73
Fixpoint approximation techniques
Widening and narrowing
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 56/73
Fixpoint approximation techniques
When the extreme fixpoints of the system of equations cannot
be computed in finitely many steps, they can be approximated.
Generally, we have these two approaches:
1 we can find more abstract interpretation
2 we can make approximations in the current interpretation
to accelerate convergence of Kleene’s sequence
Here we are concerned about second approach – the
technique called widening.
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 57/73
Fixpoint approximation techniques
Widening makes Kleene’s sequence to converge
to a fixpoint possibly greater than the least one or
to an element s, such that s > F(s).
In the second case, since s is greater then the least fixpoint, we
can use narrowing to make the solution more precise – i.e. to
find some fixpoint smaller than s but possibly greater than the
least fixpoint.
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 58/73
Widening
If the Kleene’s sequence does not converge, then there
exists a location xi on a program loop where the sequence
does not converge.
We need a widening function : L × L → L, which is
applied every time the location xi is updated: xi = xi Fi(x).
We must define such that
for each x, y ∈ L, x ◦ y ≤ x y, i.e. overapproximates
operation ◦,
it ensures that every infinite sequence of elements
occurring in xi is not strictly increasing.
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 59/73
Widening
Example: Interval bounds of integer variable x
{locations are after}
1 x := 1;
2 while (x <= 100) {
3 x := x + 1;
4 }
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 60/73
Widening
Example: Interval bounds of integer variable x
{locations are after}
1 x := 1;
2 while (x <= 100) {
3 x := x + 1;
4 }
{functions}
x1 = [1, 1]
x2 = (x1 ∪ x3) ∩ [−∞, 100]
x3 = x2 + [1, 1]
x4 = (x1 ∪ x3) ∩ [101, ∞]
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 61/73
Widening
Example: Interval bounds of integer variable x
{locations are after}
1 x := 1;
2 while (x <= 100) {
3 x := x + 1;
4 }
{functions}
x1 = [1, 1]
x2 = (x1 ∪ x3) ∩ [−∞, 100]
x3 = x2 + [1, 1]
x4 = (x1 ∪ x3) ∩ [101, ∞]
Widening operator :
[i, j] [k, l] = [ite(k < i, −∞, i), ite(l > j, ∞, j)]
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 62/73
Widening
Example: Interval bounds of integer variable x
{locations are after}
1 x := 1;
2 while (x <= 100) {
3 x := x + 1;
4 }
{functions}
x1 = [1, 1]
x2 = (x1 ∪ x3) ∩ [−∞, 100]
x3 = x2 + [1, 1]
x4 = (x1 ∪ x3) ∩ [101, ∞]
Widening operator :
[i, j] [k, l] = [ite(k < i, −∞, i), ite(l > j, ∞, j)]
{no widening}
x1 = [1, 1]
x2 = [1, 100]
x3 = [2, 101]
x4 = [101, 101]
100 iterations
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 63/73
Widening
Example: Interval bounds of integer variable x
{locations are after}
1 x := 1;
2 while (x <= 100) {
3 x := x + 1;
4 }
{functions}
x1 = [1, 1]
x2 = (x1 ∪ x3) ∩ [−∞, 100]
x3 = x2 + [1, 1]
x4 = (x1 ∪ x3) ∩ [101, ∞]
Widening operator :
[i, j] [k, l] = [ite(k < i, −∞, i), ite(l > j, ∞, j)]
{no widening}
x1 = [1, 1]
x2 = [1, 100]
x3 = [2, 101]
x4 = [101, 101]
100 iterations
{x3 = x3 (x2 + [1, 1])}
x1 = [1, 1]
x2 = [1, 100]
x3 = [2, ∞]
x4 = [101, ∞]
2 iterations
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 64/73
Widening
Example: Interval bounds of integer variable x
{locations are after}
1 x := 1;
2 while (x <= 100) {
3 x := x + 1;
4 }
{functions}
x1 = [1, 1]
x2 = (x1 ∪ x3) ∩ [−∞, 100]
x3 = x2 + [1, 1]
x4 = (x1 ∪ x3) ∩ [101, ∞]
Widening operator :
[i, j] [k, l] = [ite(k < i, −∞, i), ite(l > j, ∞, j)]
{no widening}
x1 = [1, 1]
x2 = [1, 100]
x3 = [2, 101]
x4 = [101, 101]
100 iterations
{x3 = x3 (x2 + [1, 1])}
x1 = [1, 1]
x2 = [1, 100]
x3 = [2, ∞]
x4 = [101, ∞]
2 iterations
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 65/73
Narrowing
When widening ends with s > F(s), we improve solution s
as follows: s ≥ F(s) ≥ . . . ≥ Fn(s) ≥ . . . ≥ s0, where s0 is
the least fixpoint.
When the sequence is finite, its limit is better
approximation of s0.
If the sequence is infinite, we apply narrowing function
: L × L → L at not stabilizing location xi such that
xi = xi Fi(x).
Operator must satisfy:
for each x, y ∈ L, x > y → (x ≥ x y ≥ y), i.e. tries to
slow down the decreasing of the sequence,
it ensures, that every infinite sequence of elements starting
from any s is not strictly decreasing.
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 66/73
Narrowing
Example: Interval bounds of integer variable x
{locations are after}
1 x := 1;
2 while (x <= 100) {
3 x := x + 1;
4 }
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 67/73
Narrowing
Example: Interval bounds of integer variable x
{locations are after}
1 x := 1;
2 while (x <= 100) {
3 x := x + 1;
4 }
{functions}
x1 = [1, 1]
x2 = (x1 ∪ x3) ∩ [−∞, 100]
x3 = x2 + [1, 1]
x4 = (x1 ∪ x3) ∩ [101, ∞]
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 68/73
Narrowing
Example: Interval bounds of integer variable x
{locations are after}
1 x := 1;
2 while (x <= 100) {
3 x := x + 1;
4 }
{functions}
x1 = [1, 1]
x2 = (x1 ∪ x3) ∩ [−∞, 100]
x3 = x2 + [1, 1]
x4 = (x1 ∪ x3) ∩ [101, ∞]
Narrowing operator :
[i, j] [k, l] = [ite(i = −∞, k, min(i, k)), ite(j = ∞, l, max(j, l))]
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 69/73
Narrowing
Example: Interval bounds of integer variable x
{locations are after}
1 x := 1;
2 while (x <= 100) {
3 x := x + 1;
4 }
{functions}
x1 = [1, 1]
x2 = (x1 ∪ x3) ∩ [−∞, 100]
x3 = x2 + [1, 1]
x4 = (x1 ∪ x3) ∩ [101, ∞]
Narrowing operator :
[i, j] [k, l] = [ite(i = −∞, k, min(i, k)), ite(j = ∞, l, max(j, l))]
{no widening}
x1 = [1, 1]
x2 = [1, 100]
x3 = [2, 101]
x4 = [101, 101]
100 iterations
{widening}
x1 = [1, 1]
x2 = [1, 100]
x3 = [2, ∞]
x4 = [101, ∞]
2 iteration
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 70/73
Narrowing
Example: Interval bounds of integer variable x
{locations are after}
1 x := 1;
2 while (x <= 100) {
3 x := x + 1;
4 }
{functions}
x1 = [1, 1]
x2 = (x1 ∪ x3) ∩ [−∞, 100]
x3 = x2 + [1, 1]
x4 = (x1 ∪ x3) ∩ [101, ∞]
Narrowing operator :
[i, j] [k, l] = [ite(i = −∞, k, min(i, k)), ite(j = ∞, l, max(j, l))]
{no widening}
x1 = [1, 1]
x2 = [1, 100]
x3 = [2, 101]
x4 = [101, 101]
100 iterations
{widening}
x1 = [1, 1]
x2 = [1, 100]
x3 = [2, ∞]
x4 = [101, ∞]
2 iteration
{x3 = x3 (x2 + [1, 1])}
x1 = [1, 1]
x2 = [1, 100]
x3 = [2, 101]
x4 = [101, 101]
+1 iteration
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 71/73
Narrowing
Example: Interval bounds of integer variable x
{locations are after}
1 x := 1;
2 while (x <= 100) {
3 x := x + 1;
4 }
{functions}
x1 = [1, 1]
x2 = (x1 ∪ x3) ∩ [−∞, 100]
x3 = x2 + [1, 1]
x4 = (x1 ∪ x3) ∩ [101, ∞]
Narrowing operator :
[i, j] [k, l] = [ite(i = −∞, k, min(i, k)), ite(j = ∞, l, max(j, l))]
{no widening}
x1 = [1, 1]
x2 = [1, 100]
x3 = [2, 101]
x4 = [101, 101]
100 iterations
{widening}
x1 = [1, 1]
x2 = [1, 100]
x3 = [2, ∞]
x4 = [101, ∞]
2 iteration
{x3 = x3 (x2 + [1, 1])}
x1 = [1, 1]
x2 = [1, 100]
x3 = [2, 101]
x4 = [101, 101]
+1 iteration
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 72/73
Coming next week
Shape Analysis via 3-Valued Logic
Static analysis of dynamic memory.
It can detect NULL dereferences, memory leaks, etc.
Applicable to real code.
IA159 Formal Verification Methods: Static Analysis and Abstract Interpretation 73/73