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 51作业君版权所有