Control Flow Analysis versus Use-Definition chains The aim:to trace how definition points reach use points Control Flow Analysis definition points:where function abstractions are created use points:where functions are applied Use-Definition chains definition points:where variables are assigned a value use points:where values of variables are accessed PPA Section 3.1 F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 11
Control Flow Analysis versus Use-Definition chains The aim: to trace how definition points reach use points • Control Flow Analysis – definition points: where function abstractions are created – use points: where functions are applied • Use-Definition chains – definition points: where variables are assigned a value – use points: where values of variables are accessed PPA Section 3.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 11
Specification of the 0-CFA When is a proposed guess(C,p)of an analysis results an accept- able 0-CFA analysis for the program? Different approaches: abstract specification syntax-directed and constraint-based specifications algorithms for computing the best result PPA Section 3.1 C F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 12
Specification of the 0-CFA When is a proposed guess (bC, ρb) of an analysis results an acceptable 0-CFA analysis for the program? Different approaches: • abstract specification • syntax-directed and constraint-based specifications • algorithms for computing the best result PPA Section 3.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 12
Specification of the Abstract 0-CFA (C,)=e means that (C,p)is an acceptable Control Flow Analysis of the expression e The relation has functionality: :(Cache x Env x Exp){true,falsel PPA Section 3.1 C F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 13
Specification of the Abstract 0-CFA ( bC, ρb) |= e means that (bC, ρb) is an acceptable Control Flow Analysis of the expression e The relation |= has functionality: |= : (Cache d × Env d × Exp) → {true,false} PPA Section 3.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 13
Clauses for Abstract 0-CFA (1) (C,p)ce always (C,p)e iff p(x)C(e) (C,)=(1etx=t1int号)' iff (C,)=t1A(c,)=t经N C(1)(x)∧C(2)∈C() PPA Section 3.1 F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 14
Clauses for Abstract 0-CFA (1) ( bC, ρb) |= c ` always ( bC, ρb) |= x ` iff ρb(x) ⊆ bC(`) ( bC, ρb) |= (let x = t `1 1 in t `2 2 ) ` iff ( bC, ρb) |= t `1 1 ∧ ( bC, ρb) |= t `2 2 ∧ bC(`1) ⊆ ρb(x) ∧ bC(`2) ⊆ bC(`) PPA Section 3.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 14
c p (1etx=t好int号) 回 2 PPA Section 3.1 C F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 15
bC ρb (let x = t `1 1 in t `2 2 ) ` t `1 1 t `2 2 x ` 0 x ❅ ❄ ❅ ❅ ❅ ❅ ❅■ ✛ PPA Section 3.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 15