Control Flow Analysis:axioms and rules (1) f上CFAC:Tc 广上CFAx: if广(x)=子 广[x→T】上CFAe0:T0 9 subeffecting 、 f卜CFA fnm=>e0: 0 fU一充巴le一创上CFAO:0 F卜CFA funm f=>e0:c 巴0 f上CFAe1:T2 0广卜CFAe2:2 F卜CFAe1e2:fo PPA Section 5.1 F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 11
Control Flow Analysis: axioms and rules (1) Γb `CFA c : τc Γb `CFA x : τb if Γ(b x) = τb Γ[ b x 7→ τbx] `CFA e0 : τb0 Γb `CFA fnπ x => e0 : τbx {π}∪ ϕ → τ0 subeffecting Γ[ b f 7→ τbx {π}∪ ϕ → τb0][x 7→ τbx] `CFA e0 : τb0 Γb `CFA funπ f x => e0 : τbx {π}∪ ϕ → τb0 Γb `CFA e1 : τb2 ϕ → τb0 Γb `CFA e2 : τb2 Γb `CFA e1 e2 : τb0 PPA Section 5.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 11
Control Flow Analysis:axioms and rules (2) F上CFAe0:boolr HCFA e1:子f上CFAe2:子 CFA if eo then e1 else e2: F上CFAe1:1f[c一1]上CFAe2:2 HCFA let x=e1 in e2:72 F上CFAe1:T广上CFAe2:T HCFA e1 op e2 Top PPA Section 5.1 C F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 12
Control Flow Analysis: axioms and rules (2) Γb `CFA e0 : bool Γb `CFA e1 : τb Γb `CFA e2 : τb Γb `CFA if e0 then e1 else e2 : τb Γb `CFA e1 : τb1 Γ[ b x 7→ τb1] `CFA e2 : τb2 Γb `CFA let x = e1 in e2 : τb2 Γb `CFA e1 : τ 1 op Γb `CFA e2 : τ 2 op Γb `CFA e1 op e2 : τop PPA Section 5.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 12
Example（1) let g=(funF f x =f (fny y =y)) in g (fnz z =z) Abbreviation:fx=[f一（行Y,Z)L(宁）[x一Y,Z] Inference tree: 广[y一]上CFAy:f fk上cFAf:(行YZ)E()「CFA fy y=>y:元Y守 Fk上CFAf(Enyy=>y):分O []CFA funp fx=>f(fnYy=>y):(行YZ)L(行) PPA Section 5.1 F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 13
Example (1) let g = (funF f x => f (fnY y => y)) in g (fnZ z => z) Abbreviation: Γb fx = [f 7→ (τb {Y,Z →} τb) {F →} (τb →∅ τb)][x 7→ τb {Y,Z →} τb] Inference tree: Γb fx[y 7→ τb] `CFA y : τb Γb fx `CFA f : (τb {Y,Z →} τb) {F →} (τb →∅ τb) Γfx `CFA fnY y => y : τb {Y,Z →} τb Γb fx `CFA f (fnY y => y) : τb →∅ τb [ ] `CFA funF f x => f (fnY y => y) : (τb {Y,Z →} τb) {F →} (τb →∅ τb) PPA Section 5.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 13
Example (2) let g (funF f x =f (fny y =y)) in g (fnz z=>z) Abbreviation:fg=[g→（宁Y:Z){(行@f】 Inference tree: fg[z一]HCFA z:子 fg上CFag:(行YZ)(行且)「g上CFA fnz z=>z:元ZY业デ fg上CFAg(fnZz=>z):守元 the program never terminates assuming {Y,Z}={Z,Y} PPA Section 5.1 C F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 14
Example (2) let g = (funF f x => f (fnY y => y)) in g (fnZ z => z) Abbreviation: Γb g = [g 7→ (τb {Y,Z →} τb) {F →} (τb →∅ τb)] Inference tree: Γb g[z 7→ τb] `CFA z : τb Γb g `CFA g : (τb {Y,Z →} τb) {F →} (τb →∅ τb) Γg `CFA fnZ z => z : τb {Z,Y →} τb Γb g `CFA g (fnZ z => z) : τb →∅ τb the program never terminates assuming {Y, Z} = {Z, Y} PPA Section 5.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 14
Example: Abbreviation:y int h,int Inference tree: [x一]HCFA x:Y [yint]HCFA y:int HCFA fnx x =>x HCFA fny y=>y:TY HCFA (fnx x =x)(fny y=>y): Note:the whole inference tree is needed to get full information about the control flow properties. PPA Section 5.1 C F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 15
Example: Abbreviation: τbY = int {Y →} int Inference tree: [x 7→ τbY] `CFA x : τbY [y 7→ int] `CFA y : int [ ] `CFA fnX x => x : τbY {X →} τbY [ ] `CFA fnY y => y : τbY [ ] `CFA (fnX x => x) (fnY y => y) : τbY Note: the whole inference tree is needed to get full information about the control flow properties. PPA Section 5.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 15