中国科学技术大学：《程序分析与程序验证》课程教学资源（课件讲稿）第5章 类型和效果系统（Nielson等）Principles of Program Analysis - Type and Effect Systems

Principles of Program Analysis: Type and Effect Systems Transparencies based on Chapter 5 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 5 C F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 1

Principles of Program Analysis: Type and Effect Systems Transparencies based on Chapter 5 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 5 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 1

Basic idea:effect systems If an expression e maps entities of type T1 to entities of type 72 e:T1→T2 then we can annotate the arrow with properties of the program e:12 Example analysis Choice of the property of a function call Control Flow which function abstractions might arise Side Effect which side effects might be observed Exception which exceptions might be raised Region which regions of data might be effected Communication which temporal behaviour might be observed PPA Section 5.1 C F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 2

Basic idea: effect systems If an expression e maps entities of type τ1 to entities of type τ2 e : τ1 → τ2 then we can annotate the arrow with properties of the program e : τ1 ϕ → τ2 Example analysis Choice of the property ϕ of a function call Control Flow which function abstractions might arise Side Effect which side effects might be observed Exception which exceptions might be raised Region which regions of data might be effected Communication which temporal behaviour might be observed PPA Section 5.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 2

The plan a typed functional language with a traditional underlying type system several extensions to effect systems: Analysis characteristica properties Control Flow subeffecting sets Side Effect subtyping sets Exception polymorphism sets Region polymorphic recursion sets Communication polymorphism temporal PPA Section 5.1 F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 3

The plan • a typed functional language • with a traditional underlying type system • several extensions to effect systems: Analysis characteristica properties Control Flow subeffecting sets Side Effect subtyping sets Exception polymorphism sets Region polymorphic recursion sets Communication polymorphism temporal PPA Section 5.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 3

Syntax of the Fun language e:=cxfnπx=>e0funπfx=>e0e1e2 ↑ ↑ program points if eo then e1 else e2 let x e1 in e2 e1 op e2 not polymorphic Examples:·(fnxx=>x)(fnYy=>y） .let g (funF f x =f (fny y =y)) in g (fnz z =z) PPA Section 5.1 C F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 4

Syntax of the Fun language e ::= c | x | fnπ x => e0 | funπ f x => e0 | e1 e2 ↑ ↑ program points | if e0 then e1 else e2 | | let x = {z e1 in e2} not polymorphic | e1 op e2 Examples: • (fnX x => x) (fnY y => y) • let g = (funF f x => f (fnY y => y)) in g (fnZ z => z) PPA Section 5.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 4

Underlying type system:typing judgements 「-uLe:T T:=int|boo1T1→2 「=[]|「[x→T] Assumptions: each constant c has a type Tc true has type Ttrue =bool;7 has type T7=int each operator op expects two arguments of type Top andp and ● gives a result of type Top expects two arguments of type int and gives a result of type bool PPA Section 5.1 F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 5

Underlying type system: typing judgements Γ `UL e : τ ✻ τ ::= int | bool | τ1 → τ2 ✻ Γ ::= [ ] | Γ[x 7→ τ] Assumptions: • each constant c has a type τc true has type τtrue = bool; 7 has type τ7 = int • each operator op expects two arguments of type τ 1 op and τ 2 op and gives a result of type τop > expects two arguments of type int and gives a result of type bool PPA Section 5.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 5

Underlying type system:axioms and rules (1) 「FULC:Tc 「上ULx:T if「(x)=T r[x→Tx]FUL eo:To 「FUL fnr 2=>e0:Tx→T0 「[f→Tx→To][x→Tx]上ULeo:To 「FUL funr f x=>eo:Tx→To 「卜ULe1:T2→T0「FULe2:T2 「-uLe1e2:To PPA Section 5.1 C F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 6

Underlying type system: axioms and rules (1) Γ `UL c : τc Γ `UL x : τ if Γ(x) = τ Γ[x 7→ τx] `UL e0 : τ0 Γ `UL fnπ x => e0 : τx → τ0 Γ[f 7→ τx → τ0][x 7→ τx] `UL e0 : τ0 Γ `UL funπ f x => e0 : τx → τ0 Γ `UL e1 : τ2 → τ0 Γ `UL e2 : τ2 Γ `UL e1 e2 : τ0 PPA Section 5.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 6

Underlying type system:axioms and rules (2) 「rULe0:boo1「FULe1:T「-ULe2:T FUL if eo then e1 else e2:T 厂上ULe1:T1「[x→T1]HULe2:T2 「FUL let x=e1ine2:T2 「huLe1:T品「FuLe2:T 「r-ULe1ope2:Top PPA Section 5.1 C F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 7

Underlying type system: axioms and rules (2) Γ `UL e0 : bool Γ `UL e1 : τ Γ `UL e2 : τ Γ `UL if e0 then e1 else e2 : τ Γ `UL e1 : τ1 Γ[x 7→ τ1] `UL e2 : τ2 Γ `UL let x = e1 in e2 : τ2 Γ `UL e1 : τ 1 op Γ `UL e2 : τ 2 op Γ `UL e1 op e2 : τop PPA Section 5.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 7

Example: let g=(funF f x =f (fny y =y)) in g (fn7 z =z) Abbreviation:「fx=[f一(r→T)→(T→T)][x一T→T] Inference tree: 「fx[y一T]FULy:T 「x FUL f:(T→T)一(T→T)「x上UL fny y=>y:T一T 「fx卜ULf(fnyy=>y):T一T []HUL funF f x=>f(fnYy=>y):(T→T)→(r一T) PPA Section 5.1 C F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 8

Example: let g = (funF f x => f (fnY y => y)) in g (fnZ z => z) Abbreviation: Γfx = [f 7→ (τ → τ) → (τ → τ)][x 7→ τ → τ] Inference tree: Γfx[y 7→ τ] `UL y : τ Γfx `UL f : (τ → τ) → (τ → τ) Γfx `UL fnY y => y : τ → τ Γfx `UL f (fnY y => y) : τ → τ [ ] `UL funF f x => f (fnY y => y) : (τ → τ) → (τ → τ) PPA Section 5.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 8

Control Flow Analysis The aim of the analysis: For each subexpression,which function abstractions might it evaluate to? Values of type int and bool can only evaluate to integers and booleans Values of type T1-72 can only evaluate to function abstractions annotate the arrow with the program points for these abstractions Example:fnx x =>x int (XL int fny x =x:int xY int subeffecting PPA Section 5.1 F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 9

Control Flow Analysis The aim of the analysis: For each subexpression, which function abstractions might it evaluate to? Values of type int and bool can only evaluate to integers and booleans Values of type τ1 → τ2 can only evaluate to function abstractions • annotate the arrow with the program points for these abstractions Example: fnX x => x : int {X →} int fnX x => x : int {X,Y →} int subeffecting PPA Section 5.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 9

Control Flow Analysis:typing judgements HCFA e 子：=int|bool|122 广：=[]|[x→] p:={π}|p1Up2|0 Back to the underlying type system:remove the annotations Lint」=int bool]=bool L方12=L」→L2 For type environments:[](x)=(x)]for all x PPA Section 5.1 C F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 10

Control Flow Analysis: typing judgements Γb `CFA e : τb ✻ τb ::= int | bool | τb1 →ϕ τb2 ✻ ϕ ::= {π} | ϕ1 ∪ ϕ2 | ∅ ✻ Γ ::= [ ] b | Γ[ b x 7→ τb] Back to the underlying type system: remove the annotations bintc = int bboolc = bool bτb1 ϕ → τb2c = bτb1c → bτb2c For type environments: bΓbc(x) = bΓ(b x)c for all x PPA Section 5.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 10