中国科学技术大学：《程序分析与程序验证》课程教学资源（课件讲稿）第3章 基于约束的分析（Nielson等）Principles of Program Analysis - Control Flow Analysis

Principles of Program Analysis: Control Flow Analysis Transparencies based on Chapter 3 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 3 C F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 1

Principles of Program Analysis: Control Flow Analysis Transparencies based on Chapter 3 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 3 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 1

The Dynamic Dispatch Problem proc p(procval q,val x,res y)isen Ical1 P(pi1v) [call q (x,y) which procedure is called? [cal1 p(p2,2.v ende These problems arise for: imperative languages with procedures as parameters object oriented languages functional languages PPA Chapter 3 C F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 2

The Dynamic Dispatch Problem ... [call p(p1,1,v)] ` 1 c ` 1 r ... [call p(p2,2,v)] ` 2 c ` 2 r ... proc p(procval q, val x, res y) is`n ... [call q (x,y)] ` p c ` p r which procedure is called? ... end`x These problems arise for: • imperative languages with procedures as parameters • object oriented languages • functional languages PPA Chapter 3 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 2

Example: let f fn x =x 1; g fn y =y+2; h fn z =z+3 in (f g)+(f h) The aim of Control Flow Analysis: For each function application,which functions may be applied? Control Flow Analysis computes the interprocedural flow relation used when formulating interprocedural Data Flow Analysis. PPA Chapter 3 C F.Nielson H.Rlis Nielson C.Hankin (Dec.2004) 3

Example: let f = fn x => x 1 ; g = fn y => y+2; h = fn z => z+3 in ( f g ) + ( f h ) The aim of Control Flow Analysis: For each function application, which functions may be applied? Control Flow Analysis computes the interprocedural flow relation used when formulating interprocedural Data Flow Analysis. PPA Chapter 3 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 3

Syntax of the Fun Language Syntactic categories: e∈Exp expressions (or labelled terms) t∈Term terms (or unlabelled expressions) f,x E Var variables Const constants Op∈ Op binary operators ∈ Lab labels Syntax: e :; t :c x fn x =eo fun f x=>eo e1 e2 if eo then e1 else e2 let x=e1 in e2 e1 op e2 (Labels correspond to program points or nodes in the parse tree. PPA Section 3.1 F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 4

Syntax of the Fun Language Syntactic categories: e ∈ Exp expressions (or labelled terms) t ∈ Term terms (or unlabelled expressions) f, x ∈ Var variables c ∈ Const constants op ∈ Op binary operators ` ∈ Lab labels Syntax: e ::= t ` t ::= c | x | fn x => e0 | fun f x => e0 | e1 e2 | if e0 then e1 else e2 | let x = e1 in e2 | e1 op e2 (Labels correspond to program points or nodes in the parse tree.) PPA Section 3.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 4

Examples: 。(fnx=>x2)2(fny=>y3)4)5 ●(1etf=(fnx=>(x112)3)4; in (let g=(fn y =y5)6; in (let h=(fn z =z7)8 in(f9g10)11+(f12h13)14)15)16)17)18 (1et g=(fun f x =>(f1 (fn y =y2)3)4)5 in(g5(fnz=>z7)8)9)10 PPA Section 3.1 F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 5

Examples: • ((fn x => x1) 2 (fn y => y3) 4) 5 • (let f = (fn x => (x1 1 2) 3) 4; in (let g = (fn y => y5) 6; in (let h = (fn z => z7) 8 in ((f9 g 10) 11 + (f12 h 13) 14) 15) 16) 17) 18 • (let g = (fun f x => (f 1 (fn y => y2) 3) 4) 5 in (g 6 (fn z => z7) 8) 9) 10 PPA Section 3.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 5

Abstract 0-CFA Analysis ●Abstract domains Specification of the analysis Well-definedness of the analysis PPA Section 3.1 C F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 6

Abstract 0-CFA Analysis • Abstract domains • Specification of the analysis • Well-definedness of the analysis PPA Section 3.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 6

Towards defining the Abstract Domains The result of a 0-CFA analysis is a pair (C,p): .C is the abstract cache associating abstract values with each labelled program point p is the abstract environment associating abstract values with each variable PPA Section 3.1 C F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 7

Towards defining the Abstract Domains The result of a 0-CFA analysis is a pair (bC, ρb): • bC is the abstract cache associating abstract values with each labelled program point • ρb is the abstract environment associating abstract values with each variable PPA Section 3.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 7

Example: (Enx=>x1)2(fny=>y3)4)5 Three guesses of a 0-CFA analysis result: (Ce;pe (C,) (Cg,) 1 {fn y = 3) {fn y =y3] {fn x = x1,fn y = 2 {fn x =x1} {fn x = x2} {fn x = , y=> y3) 3 0 0 fn ax -xl,fn y =y3 4 {fn y = y3) {fn y =>y3} {fn x = xl,fn y =y3) 5 {fn y => y3) {fn y => y3 {fn x = xl,fn y =y3] {fn y=>y3) 0 {fn x = x2, =>y3} y 0 0 fn x =>x1,fn y => y3) PPA Section 3.1 C F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 8

Example: ((fn x => x1) 2 (fn y => y3) 4) 5 Three guesses of a 0-CFA analysis result: ( bCe, ρbe) ( bC 0 e , ρb 0 e ) ( bC 00 e , ρb 00 e ) 1 2 3 4 5 x y {fn y => y3} {fn x => x1} ∅ {fn y => y3} {fn y => y3} {fn y => y3} ∅ {fn y => y3} {fn x => x1} ∅ {fn y => y3} {fn y => y3} ∅ ∅ {fn x => x1 , fn y => y3} {fn x => x1 , fn y => y3} {fn x => x1 , fn y => y3} {fn x => x1 , fn y => y3} {fn x => x1 , fn y => y3} {fn x => x1 , fn y => y3} {fn x => x1 , fn y => y3} PPA Section 3.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 8

Example: (let g=(fun f x=>(f1 (fn y =y2)3)4)5 in(g6(fnz=>z7)8)9)10 Abbreviations: f三 fun f x=>(f1 (fn y =y2)3)4 idy 三 fn y =y2 idz 三 fn z =z7 One guess of a 0-CFA analysis result: Cp(1) = f Cp(6) 三 (f) {f) (2) 0 Cp(7) Pip(f) = 0 Pp(g) {f} Cp(3) 二 idy Cp(8) 三 fidz Plp(x) === idy,idz Cp(4) 三 0 Cp(9) 三 0 pp(y） = 0 Cp(5) 三 (o) Cp(10) 三 0 PIp(z) 三 0 PPA Section 3.1 F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 9

Example: (let g = (fun f x => (f 1 (fn y => y2) 3) 4) 5 in (g 6 (fn z => z7) 8) 9) 10 Abbreviations: f = fun f x => (f 1 (fn y => y2) 3) 4 idy = fn y => y2 idz = fn z => z7 One guess of a 0-CFA analysis result: bClp(1) = {f} bClp(2) = ∅ bClp(3) = {idy} bClp(4) = ∅ bClp(5) = {f} bClp(6) = {f} bClp(7) = ∅ bClp(8) = {idz} bClp(9) = ∅ bClp(10) = ∅ ρblp(f) = {f} ρblp(g) = {f} ρblp(x) = {idy, idz} ρblp(y) = ∅ ρblp(z) = ∅ PPA Section 3.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 9

Abstract Domains Formally: Val -P(Term) abstract values p∈Env 三 Var-Val abstract environments c∈Cache=Lab→Val abstract caches An abstract value o is a set of terms of the forms ●fnx=>e0 ●fun f x=>e0 PPA Section 3.1 C F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 10

Abstract Domains Formally: vb ∈ Val d = P(Term) abstract values ρb ∈ Env d = Var → Val d abstract environments bC ∈ Cache d = Lab → Val d abstract caches An abstract value vb is a set of terms of the forms • fn x => e0 • fun f x => e0 PPA Section 3.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 10