1Abstract Interpretation
1
Announcements
n Will conclude with dataflow and abstract
interpretation this week and move on
n HW3 and HW4?
n Linh’s office hours: Fridays 1-2pm in AE127?
Program Analysis CSCI 4450/6450, A Milanova 2
2
2Why “k most recent call sites”?
n Well-defined, no clear alternative
n Likely to separate context meaningfully
n Data not passes too far up call chain/stack
n Lots of work on “selective” context sensitivity ---
looks at a context-insensitive call graph and
decides what a good context is
3
3
Abstract Interpretation
n Patrick Cousot and Radhia Cousot, POPL’77
n A general framework
n Combines ideas from dataflow analysis
(monotone frameworks and fixpoint iteration) and
formal verification (axiomatic semantics)
n Building static analyses
n Reasoning about correctness of static analysis
n Comparing static analyses
Program Analysis CSCI 4450/6450, A Milanova 4
4
3Lecture Notes Based On
n “Principles of Program Analysis” by Nielsen,
Nielsen and Hankin, Chapter 3
n Alex Salcianu’s friendlier account of Chapter 3:
https://web.eecs.umich.edu/~bchandra/courses/papers/
Salcianu_AbstractInterpretation.pdf
n Lecture notes by Xavier Rival, ENS
n https://www.di.ens.fr/~rival/semverif-2017/sem-11-ai.pdf
Program Analysis CSCI 4450/6450, A Milanova 5
5
Outline
n Overview
n Semantics
n Notion of abstraction
n Concretization and abstraction functions
n Galois Connections
n Applications of abstract interpretation
Program Analysis CSCI 4450/6450, A Milanova 6
6
4Overview
Program Analysis CSCI 4450/6450, A Milanova 7
Program Execution: Points-to Analysis (PTA):
x à hj:A
x = y.n(z)
passes value of z to
parameter p
x à oi:A
Points-to analysis is an abstraction.
Abstracts infinitely many heap objects
hj created at site i into a single oi
x = y.n(z)
pts(z) pts(p)
7
Operational Semantics
n Also called trace semantics, or concrete
semantics, models a trace of execution
n Memory state maps variables (V) to values (Z):
σ : V à Z
n Control state describes where we are
label l (note: we used the term program point)
n Describes transition (l1, σ1)à (l2, σ2)
(read: program executes statement at label l1 in
state σ1 transitioning to label l2 in state σ2)
8Program Analysis CSCI 4450/6450, A Milanova
8
5A Simple Imperative Language:
Syntax (We’ve Seen This Before!)
E ::= x | n simple expression
S ::= x = E | x = E Op E assignment
| while ( b ) Seq loop
| if ( b ) Seq else Seq conditional
Seq ::= { S; … S; } sequence
n V is the set of program variables, x V
n Z is the set of values variables take, n Z
Program Analysis CSCI 4450/6450, A Milanova 9
∈
∈
9
A Simple Imperative Language:
Operational Semantics
10
n Operational semantics of expressions:
n |[n]|(σ) = n // constant n evaluates to n
n |[x]|(σ) = σ(x) // variable x evaluates to the
value n that x maps to in σ
n Assignment: lj : x = E; li : …
(lj,σ) à (li, σ[xß|[E]|(σ)])
n Assignment: lj : x = E1 Op E2 ; li : …
(lj,σ) à (li, σ[xß|[E1]|(σ) Op |[E2]|(σ)])
10
6A Simple Imperative Language:
Operational Semantics
11
n Loop: lj : while ( b ) { li : S; … } lk : ...
if |[b]|(σ) == True then (lj, σ) à (li, σ)
if |[b]|(σ) == False then (lj, σ) à (lk, σ)
n Conditional: lj : if ( b ) { lT : … } else { lF : ... }
if |[b]|(σ) == True then (lj, σ) à (lT, σ)
if |[b]|(σ) == False then (lj, σ) à (lF, σ)
n Sequence: { l0 : S; l1 … }
n Transition defined by composition of individual
transition relations
11
Example
Program Analysis CSCI 4450/6450, A Milanova 12
3. x=1
7. z=x+y
2. if (b≥0)
8. x=10*z
1.
b = 0;
4. y=2
5. x=2
6. y=1
σ: empty map
σ: bà0
σ: bà0
σ: bà0, xà1, yà2
σ: bà0, xà1, yà2, zà3
σ: bà0, xà30, yà2, zà3
T F
σ: bà0, xà1
12
7Collecting Semantics
n Collects states (i.e., σ’s) along all traces of
execution at a given label (i.e., program
point)
n Given a label, we are interested in a function
n C : Labels à 2Σ
n The set of all states a program can have at li
Program Analysis CSCI 4450/6450, A Milanova 13
13
Collecting Semantics
Program Analysis CSCI 4450/6450, A Milanova.
Slide from MIT’s 2015 Program Analysis course on OpenCorseWare
14
14
8Collecting Semantics
n “Ground truth”
n We base reasoning about correctness (soundness)
of static analysis off of it
n Undecidable
n Relation to MOP solution?
n Define abstraction of state and semantics
n Goal: show that abstraction “accounts for” all
values computed by the collecting semantics
Program Analysis CSCI 4450/6450, A Milanova 15
15
Outline
n Overview
n Semantics
n Notion of abstraction
n Concretization and abstraction functions
n Galois Connections
n Applications of abstract interpretation
Program Analysis CSCI 4450/6450, A Milanova 16
16
9Abstraction Example 1: signs
n Concrete values: sets of integers
n Abstract values: signs
Lattice of signs:
Program Analysis CSCI 4450/6450, A Milanova 17
T
T
+ 0 -
• represents the empty set
• + represents any set of positive integers
• 0 represents set { 0 }
• - represents any set of negative integers
• T represents any set of integers
T
17
Abstraction Example 1: signs
Concrete space: Abstract space:
A lattice! A lattice!
Program Analysis CSCI 4450/6450, A Milanova 18
T
T
+ 0 -
{ … -2,-1,0,1,... }
{}
{-2,-1,0}
{1,2}
{-2,-1}
{0,1}
{0}
{0,1,2,... }
18
10
Abstraction Example 1: signs
Concrete space: Abstract space:
A lattice! A lattice!
Program Analysis CSCI 4450/6450, A Milanova 19
T
T
+ 0 -
{ … -2,-1,0,1,... }
{}
{-2,-1,0}
{1,2}
{-2,-1}
{0,1}
{0}
{0,1,2,... }
19
Abstraction Example 1: signs
n Concrete elements: elements of the concrete
lattice c 2Z
n Abstract elements: elements of abstract
lattice of signs
n Abstraction relation relates concrete
elements to abstract ones: c S a (i.e., a
represents c, or conversely c is represented by a)
{1,2,3} S +
{1,2,3} S T
Program Analysis CSCI 4450/6450, A Milanova 20
T
T
T
∈
20
11
Abstraction Example 1: signs
n We use the abstraction relation to define
abstract semantics, i.e., the execution of
program statements over abstract elements
n If x is + and y is + then x + y is +
n x’s value is a positive integer
n y’s value is a positive integer
n Therefore, the concrete value of x + y is a
positive integer too, thus represented by +
Program Analysis CSCI 4450/6450, A Milanova 21
21
Abstraction Example 1: signs
n If x is + and y is + then x + y is +
n Analysis computes over abstract elements
n Correctness conclusion, informally: if analysis
(works on abstract elements a) determines
that x at label l is a, then set of concrete
values c collected by collecting semantics at l
is represented by a
Program Analysis CSCI 4450/6450, A Milanova 22
22
12
Abstraction Example 1: signs
n We can also use U and
if x is + and y is + then x U y is +
How about if x is + and y is 0?
then x U y is T
because only {0,1,2,3,…} S T holds
No other relation holds
In the abstract, we include negative integers
in x U y (we lose precision!)
Program Analysis CSCI 4450/6450, A Milanova. Example from Xavier Rival’s lecture notes on AI 23
∩
T
T
T
+ 0 -
23
Abstraction Example 1: signs
n Refine the abstract space
Program Analysis CSCI 4450/6450, A Milanova 24
• represents the empty set
• + represents any set of positive integers
• 0 represents set { 0 }
• - represents any set of negative integers
• T represents any set of integers
• ≥0 represents any set of non-negative
integers
• ≤0 represents any set of non-positive
integers
• ≠0 represents any set of non-zero
integers
≥0 ≠0 ≤0
T
T
+ 0 -
T
24

学霸联盟