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