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