Principles of Program Analysis: Abstract Interpretation Transparencies based on Chapter 4 of the book:Flemming Nielson, Hanne Riis Nielson and Chris Hankin:Principles of Program Analysis. Springer Verlag 2005.CFlemming Nielson Hanne Riis Nielson Chris Hankin. PPA Chapter 4 C F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 1
Principles of Program Analysis: Abstract Interpretation Transparencies based on Chapter 4 of the book: Flemming Nielson, Hanne Riis Nielson and Chris Hankin: Principles of Program Analysis. Springer Verlag 2005. c Flemming Nielson & Hanne Riis Nielson & Chris Hankin. PPA Chapter 4 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 1
A Mundane Approach to Semantic Correctness Semantics: Program analysis: pFU102 p-l112 where v1,v2∈V. where l1,l2∈L. Note:might be deterministic. Note:D should be deterministic: fp(l1)=l2. What is the relationship between the semantics and the analysis? Restrict attention to analyses where properties directly describe sets of values i.e."first-order'"analyses (rather than "second-order"analyses). PPA Section 4.1 F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 2
A Mundane Approach to Semantic Correctness Semantics: p ` v1 ❀ v2 where v1, v2 ∈ V . Note: ❀ might be deterministic. Program analysis: p ` l1 ✄ l2 where l1, l2 ∈ L. Note: ✄ should be deterministic: fp(l1) = l2. What is the relationship between the semantics and the analysis? Restrict attention to analyses where properties directly describe sets of values i.e. “first-order‘” analyses (rather than “second-order” analyses). PPA Section 4.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 2
Example:Data Flow Analysis Structural Operational Constant Propagation Analysis: Semantics: Properties:L Statecp =(Var*-Z)L Values:V=State Transitions: Transitions: S*卜61D52 S★卜01→02 iff iff 61=L 2=LCP.()eE final(S)} (S*,01〉→*02 (CP。,CP.)=CP=(S*) PPA Section 4.1 C F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 3
Example: Data Flow Analysis Structural Operational Semantics: Values: V = State Transitions: S? ` σ1 ❀ σ2 iff hS?, σ1i →∗ σ2 Constant Propagation Analysis: Properties: L = State d CP = (Var? → Z>)⊥ Transitions: S? ` σb1 ✄ σb2 iff σb1 = ι σb2 = F {CP•(`) | ` ∈ final(S?)} (CP◦, CP•) |= CP=(S?) PPA Section 4.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 3
Example:Control Flow Analysis Structural Operational Pure 0-CFA Analysis: Semantics: Properties:L=Env x Val Values:V=Val Transitions: Transitions: e*卜(p1,1)D(p2,i2) e*卜v1→v2 iff iff C(1)=01 []卜(e*经)2-*2 C(2)=2 P1=P2=p (C,p)=(e*c1)2 for some place holder constant c PPA Section 4.1 C F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 4
Example: Control Flow Analysis Structural Operational Semantics: Values: V = Val Transitions: e? ` v1 ❀ v2 iff [ ] ` (e? v `1 1 ) `2→ ∗ v `2 2 Pure 0-CFA Analysis: Properties: L = Env d × Val d Transitions: e? ` (ρb1, vb1) ✄ (ρb2, vb2) iff bC(`1) = vb1 bC(`2) = vb2 ρb1 = ρb2 = ρb ( bC, ρb) |= (e? c `1) `2 for some place holder constant c PPA Section 4.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 4
Correctness Relations R:Vx L{true,false) Idea:v Rl means that the value v is described by the property l. Correctness criterion:R is preserved under computation: pH Ul 之 V2 logical relation: R → R (pF→)(RR)(pF) P卜 l1 回 12 PPA Section 4.1 C F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 5
Correctness Relations R : V × L → {true,false} Idea: v R l means that the value v is described by the property l. Correctness criterion: R is preserved under computation: p ` v1 ❀ v2 ... ... R ⇒ R ... ... p ` l1 ✄ l2 logical relation: (p ` · ❀ ·) (R →→ R) (p ` · ✄ ·) PPA Section 4.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 5
Admissible Correctness Relations vRl1∧l1El2→vRl2 (l∈L'≤L:vRl)→vR(L)({l|vR}is a Moore family) Two consequences: U RT vRl1∧vRl2→vR(l1nl2) Assumption:(L,is a complete lattice. PPA Section 4.1 C F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 6
Admissible Correctness Relations v R l1 ∧ l1 v l2 ⇒ v R l2 (∀l ∈ L 0 ⊆ L : v R l) ⇒ v R ( L 0 ) ({l | v R l} is a Moore family) Two consequences: v R > v R l1 ∧ v R l2 ⇒ v R (l1 u l2) Assumption: (L, v) is a complete lattice. PPA Section 4.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 6
Example:Data Flow Analysis Correctness relation Rcp State x Statecp-{true,false) is defined by o Rcp a iff VxEFV(S):((x)=T V o(z)=(x)) PPA Section 4.1 C F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 7
Example: Data Flow Analysis Correctness relation RCP : State × State d CP → {true,false} is defined by σ RCP σb iff ∀x ∈ FV(S?) : (σb(x) = > ∨ σ(x) = σb(x)) PPA Section 4.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 7
Example:Control Flow Analysis Correctness relation RCFA Val x (Env x Val){true,false} is defined by RCEA (p,)iff v(p,) where 1 is given by: true if v=c (ffE dom(o)p()(()ifv=closet in PPA Section 4.1 C F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 8
Example: Control Flow Analysis Correctness relation RCFA : Val × (Env d × Val d ) → {true,false} is defined by v RCFA (ρb, vb) iff v V (ρb, vb) where V is given by: v V (ρb, vb) iff ( true if v = c t ∈ vb ∧ ∀x ∈ dom(ρ) : ρ(x) V (ρb, ρb(x)) if v = close t in ρ PPA Section 4.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 8
Representation Functions B:V→L Idea:3 maps a value to the best property describing it. Correctness criterion: U1 v2 3 → 冂 p卜 li D 12 PPA Section 4.1 C F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 9
Representation Functions β : V → L Idea: β maps a value to the best property describing it. Correctness criterion: p ` v1 ❀ v2 u u p ` l1 ✄ l2 ❄ ❄ β β ⇒ PPA Section 4.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 9
Equivalence of Correctness Criteria Given a representation function B we define a correctness relation Ra by v RB l iff B(v)l Given a correctness relation R we define a representation function BR by BR(v)=v R1} Lemma: (i)Given B:V-L,then the relation RB:VxL-{true,false}is an admissible correctness relation such that Br-B. (ii)Given an admissible correctness relation R:V x L-{true,falsel, then Br is well-defined and RBr=R. PPA Section 4.1 F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 10
Equivalence of Correctness Criteria Given a representation function β we define a correctness relation Rβ by v Rβ l iff β(v) v l Given a correctness relation R we define a representation function βR by βR(v) = {l | v R l} Lemma: (i) Given β : V → L, then the relation Rβ : V × L → {true,false} is an admissible correctness relation such that βRβ = β. (ii) Given an admissible correctness relation R : V × L → {true,false}, then βR is well-defined and RβR = R. PPA Section 4.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 10