Transcription
Control-Flow AnalysisCS252r Spring 2011Includes (a lot of) material from slides forPrinciples of Program Analysisby Nielson, Nielson, and Hankinhttp://www2.imm.dtu.dk/ riis/PPA/ppasup2004.html
Outline What’s the problem? 0-CFA Uniform k-CFA The k-CFA paradox 2011 Stephen Chong, Harvard University2
What is control-flow analysis? Data-flow analysis relied on a control-flow graph How do we construct CFG? For intra-procedural analysis, relatively straightforward Identify basic blocks, control-flow structures We will not delve into this For inter-procedural analysis If functions/procedures are not first-class, relatively simple For languages with dynamic dispatch, it’s harder Dynamic dispatch: which procedure/function gets invoked depends onruntime values Functional languages, OO, imperative languages with procedures asparameters, . 2011 Stephen Chong, Harvard University3
CFA in higher-order languages We’ll mostly focus today on control-flow analysisof functional languages For each function application, which functions may beple: applied? E.g.let f fn x x 1 ;g fn y y 2;h fn z z 3in ( f g ) ( f h )m of Control Flow Analysis:ach function application, which functions may be applied? 2011 Stephen Chong, Harvard University4
Syntax of languageSyntaxSyntax ofof thethe FunFun LanguageLanguageSyntacticSyntactic categories:categories:eettf,f,xxccopop Syntax:Syntax: ExpExp expressionsexpressions (or(or labelledlabelled terms)terms)TermTerm termsterms (or(or unlabelledunlabelled variablesvariablesconstantsconstantsbinarybinary operatorsoperatorslabelslabelsee :: :: t t tt :: :: cc xx fnfn xx ee00 funfun ff xx ee00 ee11 ee22 ifif ee00 thenthen ee11 elseelse ee22 letlet xx ee11 inin ee22 ee11 opop ee22(Labels(Labels correspondcorrespond toto programprogram pointspoints oror nodesnodes inin thethe parseparse tree.)tree.) 2011StephenChong, HarvardPPASection3.1 UniversityPPA Section 3.1c c HankinC.Hankin(Dec.(Dec.2004)2004)445
Examples:Examples:Examples1 )2 (fn y y3 )4 )5 ((fnx xExamples: ((fn x x1)2 (fn y y3)4)51 12 )3 )4 ; (letf (fnx (x12 ((fn x x ) (fn y y35)46)5in (let g (fn y y ) ; (let f (fn x (x1 12)3)47; 8in (let h (fn z 5 6 z )in (let g (fn9 y 10 11y ) ; 12 13 14 15 16 17 184 ;8 h ) ) ) ) )in ((fg(x1) 12) 3)7(f (let inf (let(fnx h (fn z z )5 )6 ; 12 13 14 15 16 17 189 g11in (let ing ((f(fny10 y) (fh ) ) ) ) )7 )8in (let h (fn z z1 (fn y y2 )3 )4 )5 (let g in(funfx (f9101112 h13 )14 )15 )16 )17 )18((fg) (fin (g6 (fn z z7)8)19)10 (let g (fun f x (f (fn y y2)3)4)5in (g6 (fn z z7)8)9)10 (let g (fun f x (f1 (fn y y2)3)4)5in (g6 (fn z z7)8)9)10PPA Section 3.1PPA Section 3.1 2011 Stephen Chong, Harvard Universityc F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 56
0-CFA 0-CFA is an context-insensitive CFA. ρ) Resultofa0-CFAanalysisispair(Ĉ,Abstract Domains Ĉ is an abstract cacheFormally: ρ is an abstract environment v Val Notes: ρ Env P(Term)Actually, just functionsabstract values abstract environments Var Val Cache abstract cachesC Lab ValAn abstractvalue v isthesea setintoof termsof the(VarformsCould combineone entity: Lab) Val Couldfn x ealso0require A-normal form, where all subterms areappropriately funf x e0 labeled by variables 2011 Stephen Chong, Harvard University7
Example:Example:Example1 )2 (fn y y3 )4 )5((fn 1x x((fn x x )2 (fn y y3)4)5Three guesses of a 0-CFA analysis result:Three guesses of a 0-CFA analysis result: , ρ ) , ρ ) , ρ )(C(C(Ce e , ρ ) e e , ρ ) e e (Ce, ρe)(C(Ce{fn x1e e x1, fn y3 {fn y3 y3} e{fny3 y3}1{fnx x , fn y1 y }{fn y y }{fny y }111{fn x1 x , fn y3 {fn x1 x }2{fn x1 x }{fn x x , fn y1 y }{fn x x }2{fn x x } {fn x1 x , fn y3 3 {fnx x , fn y1 y }3 334{fn y3 y }{fn x1 x , fn y3 {fn y3 y }4{fn y y }{fnx x , fn y1 y }{fny y}335{fn y3 y }{fn x1 x , fn y3 {fn y3 y }5{fn y y }{fn x x , fn y y }{fn y y }x {fn y3 y3}{fn x1 x1, fn y3 x {fn{fn x x , fn y1 y }y y y } {fnx x,fny 13y {fn x x , fn y y }Acceptable 2011 Stephen Chong, Harvard UniversityNot acceptableAcceptable but less precise8
Abstract specification What does it mean for (Ĉ, ρ) to be acceptable?fication of the Abstract 0-CFA Define relation indicating when (Ĉ, ρ) is , ρ)expression isofan e acceptablemeans that0-CFA(Cacceptable eControl Flow AnalysSpecification of theof the expression e e(C, ρ)ation has functionality: means that (C,of the expressi Env Exp) {true, false} : (CacheThe relation has functio 2011 Stephen Chong, Harvard University9
AbstractClauses forAbstractspecification0-CFA (1) , ρ) c always(C , ρ) x (Ciff ( ) ρ(x) C 1 2 (let x t1 in t2 )(C, ρ) 1 2 t1 (C, ρ) t2 iff(C, ρ) ( ) ρ(x) ( ) C ( ) C C12 2011 Stephen Chong, Harvard University10
Clauses for Abstract 0-CFA (2)Abstract specification , ρ) (if t00 then t11 else t22 ) (C , ρ) t00 iff(C , ρ) , ρ) t11 (C t22 (C ( ) C ( ) C ( ) C ( )C12 , ρ) (t11 op t22 ) (C , ρ) , ρ) t11 (C t22iff(CPPA Section 3.1 2011 Stephen Chong, Harvard Universityc F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 1611
Clauses for Abstract 0-CFA (3)Abstract specification 0 0 ( ) (C, ρ) (fn x t0 ) iff {fn x t0 } C , ρ) (t11 t22 ) (C , ρ) , ρ) t11 (C t22 iff(C 0 ( ) :( ( fn x t0 ) C1PPA Section 3.1 2011 Stephen Chong, Harvard University 0 t0 (C, ρ) ( ) ρ(x) ( ) C ( )) C C20c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 1712
Abstract specificationClauses for Abstract 0-CFA (4) , ρ) ( ) (fun f x e0) iff {fun f x e0} C(C , ρ) (t11 t22 ) (Ciff , ρ) , ρ) t11 (C t22 (C ( ) :( ( fn x t00 ) C1 , ρ) t00 (C ( ) ρ(x) ( ) C ( )) C C20 ( ) : (C , ρ) t00 ( ( fun f x t00 ) C1 ( ) ρ(x) ( ) C ( ) C C20 )){fun f x t00 } ρ(fPPA Section 3.1 2011 Stephen Chong, Harvard Universityc F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 1913
Example:What’sacceptable12Example:((fn x x ) (fn y y3)4)5Example:11a20-CFA34 )5result:2345((fnx x)(fny y)ThreeguessesofanalysisTwo guesses for ((fn x x ) (fn y y ) ) , ) ,(ρ C , ρ C,ρ)(ρ (C)(C,ρ(Ceeeee eee33Threeguessesofa0-CFAanalysisresult:33{fny y}{fny y}1{fn x x1, f{fn y y }1 {fn y y1 }1{fn x x }2{fn x x} {fn x x1, f11 {fnx x}2{fn x (Cx e,}ρ e) (C,ρ)ee 3 1, f y {fnx x3 4 1 {fn{fn 333{fn x y y } y }{fn y{fn yy3} y }3 }3 {fn1, f3}34 5{fny y{fnx xy y11y yx } x }{fn x x y } x }{fn y{fn2 {fn{fn3}1, f3}5{fny y{fnx x{fny y 3{fn x x3 xy{fn y y }3}3y{fn4 y {fn y y }5{fn y y3}Checking the guesses: 3} {fny y {fn x {fn 3}{fny y {fn x {fn x {fn y y3} , ρ )y ((fn x x1)2 (fn y y 3)4)5(Ce ex1, fx1, f{fn x {fn x c F.Nielson & H.Riis Nielson & C.Hankin (DePPA Section 3.1 , ρ ) ((fn x x1)2 (fn y y3)4)5(Ce e 2011 Stephen Chong, Harvard University14
Abstract specificationClauses for Abstract 0-CFA (4) Note that we can’t define by structural induction on(C, ρ) (fun f x e ) iff {fun f x e } C( )expressions 0 0 , ρ) (t11 t22 ) (Ciff , ρ) , ρ) t11 (C t22 (C ( ) :( ( fn x t00 ) C1 , ρ) t00 (C ( ) ρ(x) ( ) C ( )) C C20 ( ) : (C , ρ) t00 ( ( fun f x t00 ) C1 ( ) ρ(x) ( ) C ( ) C C20 )){fun f x t00 } ρ(f Instead, define coinductivelyPPA Section 3.1c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 19 Want the greatest fixed point that satisfies equations for Note: not an algorithm for solving, but a specification 2011 Stephen Chong, Harvard University15
Semantic correctness Also need to show that acceptability of analysisresults implies semantic correctness That is, C and p accurately describe the concreteexecution. Like a type-soundness statement 2011 Stephen Chong, Harvard University16
Syntax-directed 0-CFA Another formulation of 0-CFA that approximatesthe abstract specification i.e., Define s such thatif (Ĉ, ρ) s e then (Ĉ, ρ) e 2011 Stephen Chong, Harvard University17
Syntax-directed 0-CFASyntax Directed Specification (2) , ρ) s c always(C , ρ) s x (Ciff ( ) ρ(x) C 0 1 2 s (if t0 then t1 else t2 )(C, ρ) , ρ) s t00 iff(C , ρ) , ρ) s t11 (C s t22 (C ( ) C ( ) C ( ) C ( )C12 1 2 t1 in t2 ) 1 2 s t1 (C, ρ) s t2 ( ) ρ(x) ( ) C ( ) C C12 , ρ) s (let x (C , ρ) iff(C 1 2 s (t1 op t2 )(C, ρ) 2011 Stephen Chong, Harvard Universityiff 1 2 s t1 (C, ρ) s t2(C, ρ)18
Syntax-directed 0-CFASyntax Directed Specification (1) , ρ) s (fn x e0) (C ( ) iff{fn x e0} C , ρ) s e0(C , ρ) s (fun f x e0) (C ( ) iff{fun f x e0} CNote: may check somefunction bodies thataren’t reachable, inreturn for enablinginduction on syntax , ρ) s e0 {fun f x e0} ρ(f )(C 1 2 (C, ρ) s (t1 t2 ) 1 2 iff(C, ρ) s t1 (C, ρ) s t2 ( ) :( (fn x t00 ) C1 ( ) ρ(x) ( ) C ( ) C C20 ( ) :( (fun f x t00 ) C1 ( ) ρ(x) ( ) C ( ) C C20PPA Section 3.3 2011 Stephen Chong, Harvard Universityc F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) ) )5619
Syntax-directed 0-CFA For any expression e, there is a least (Ĉ, ρ)such that (Ĉ, ρ) s e Can turn this syntax-directed 0-CFA specificationinto an equivalent algorithm that generates a setof constraints Least solution to set of constraints is least solution tosyntax-directed 0-CFA 2011 Stephen Chong, Harvard University20
Constraint-based 0-CFAConstraint Based 0-CFA AnalysisC [[e ]] is a set of constraints of the formlhs rhs{t} rhs lhs rhswhererhs :: C( ) r(x)lhs :: C( ) r(x) {t}and all occurrences of t are of the form fn x e0 or fun f x e0PPA Section 3.4 2011 Stephen Chong, Harvard Universityc F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 6221
Constraint-based 0-CFAConstraint Based Control Flow Analysis (2)C [[c ]] C [[x ]] { r(x) C( ) } 0 1 2 0 1 2C [[(if t0 then t1 else t2 ) ]] C [[t0 ]] C [[t1 ]] C [[t2 ]] { C( 1) C( ) } { C( 2) C( ) } 1 2 1 2C [[(let x t1 in t2 ) ]] C [[t1 ]] C [[t2 ]] { C( 1) r(x) } {C( 2) C( ) } 1 2 1 2C [[(t1 op t2 ) ]] C [[t1 ]] C [[t2 ]] 2011 Stephen Chong, Harvard University22
Constraint-based 0-CFAConstraint Based Control Flow Analysis (1)C [[(fn x e0) ]] { {fn x e0} C( ) } C [[e0]]C [[(fun f x e0) ]] { {fun f x e0} C( ) } C [[e0]] { {fun f x e0} r(f ) } C [[(t11 t22 ) ]] C [[t11 ]] C [[t22 ]] { {t} C( 1) C( 2) r(x) t (fn x t00 ) Term } { {t} C( 1) C( 0) C( ) t (fn x t00 ) Term } { {t} C( 1) C( 2) r(x) { {t} C( 1) C( 0) C( ) 0 t (fun f x t0 ) Term } t (fun f x t00 ) Term }Eager rather than lazy unfolding – easy but costly.) 2011 Stephen Chong, Harvard University23
Examplexample:C [[((fn x x1)2 (fn y y3)4)5]] { {fn x x1} C(2),r(x) C(1),{fn y y3} C(4),r(y) C(3),{fn x x1} C(2) C(4) r(x),{fn x x1} C(2) C(1) C(5),{fn y y3} C(2) C(4) r(y),{fn y y3} C(2) C(3) C(5) } 2011 Stephen Chong, Harvard University24
CorrectnessPreservation of SolutionsTranslating syntactic entities to sets of terms: , ρ)[[ ( ) C( )]] C(C , ρ)[[ r(x)]] ρ(x) (C , ρ)[[{t}]] (C {t} , ρ) c (lhs rhs)Satisfaction relation for constraints: (C , ρ) c (lhs rhs)(C , ρ)[[lhs]] , ρ)[[rhs]] iff (C (C , ρ) c ({t} rhs lhs rhs)(C ]] (C , ρ)[[rhs , ρ)[[lhs]] , ρ)[[rhs]]) iff ({t} (C (C ]]) , ρ)[[rhs ({t} (CProposition: 2011 Stephen Chong, Harvard University , ρ) , ρ) s e if and only if (C c C [[e ]].(C25
Adding data-flow analysisAbstract Domains Current domain equationsActually, just functionsFormally: v Val ρ Env P(Term)abstract values abstract environments Var Val Cache abstract cachesC Lab Val Idea:extendabstractvaluestoincludeotherAn abstract value v is a set of terms of the formsAbstractValuesas Powersetsthings thanjust functions fn x e0 E.g.,letDatabesetofabstractdatavalues fun f x e0Let Data be a setof abstract data values (i.e. abstract proper e.g.,{tt,ff,-,0, }ooleans and integers) P(Term Data)v ValdPPA Section 3.1 2011 Stephen Chong, Harvard Universityabstract valuesc F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 1026
AbstractdatavaluesExample: Detection of Signs AnalysisDatasign {tt, ff, -, 0, } For each constant c, need abstract data value dctrue tt For each doperatorop need abstract operatorop : Data Data P(Data)d 7Example: Detection of Signs Analysis is defined from Datasign {tt, ff, -, 0, }d ttff0 dtrue ttd7 is defined from d tt ff 2011 Stephen Chong, Harvard UniversityPPA Section 3.5-tt 0ff {- }{- }{-, 0, }0 { -}{ 0}{ } {-, 0, }{ }{ } 27c F.Nielson & H.Riis Nielson & C.Hankin (Dec.
Data-flowandcontrol-flowspecAbstract Values as Powersets (2) , ρ) d c (C ( ){dc} Ciff , ρ) d x (C ( ) ρ(x) Ciff , ρ) d (if t00 then t11 else t22 ) (C , ρ) d t00 iff(C 1 ( ) ( (C , ρ) ( ) C ( ))) (dtrue C t C01d 1 2 ( ) ( (C , ρ) ( ) C ( ))) (dfalse C t C02d 2 , ρ) d (let x t11 in t22 ) (C , ρ) , ρ) ( ) ρ(x) ( ) C ( ) d t11 (C d t22 C iff(C C12 , ρ) d (t11 op t22 ) (C , ρ) , ρ) ( ) o ( ) C ( ) d t11 (C d t22 Ciff(CpC12c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004)Section 3.5 76 Is PPAflowsensitive: candetermine whether true or falsebranches can be taken 2011 Stephen Chong, Harvard University28
Arbitrary lattices Val P(Term Data) P(Term) P(Data) Could also use an arbitrary lattice Val P(Term Data) P(Term) L 2011 Stephen Chong, Harvard University29
Adding contexts 0-CFA is a context-insensitive (or mono-variant)analysis Does not distinguish various instances of programvariables and program points from each other Context-sensitive (or poly-variant) analysis doesdistingtuish 2011 Stephen Chong, Harvard University30
Uniform k-CFAAbstract DomainsFormally: v Val ρ Env P(Term)abstract values abstract environments Var Val Cache abstract cachesC Lab Val Val to include context information Idea:extendAbstractDomainsAn abstractvalue v is a set of terms of the forms fnδx will e0 record last k dynamic call-sites Contexts δfun f x e0 Lab kDefinition pointof free variablesof termsce CEnv ValvPPA Section 3.1 ρ Env Var context informationcontext environments P(Term CEnv) abstract valuesc F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 10 abstract environments (Var ) Val Cache abstract cachesC (Lab ) Val Called “uniform” because bothenvironmentandcacheuse .) and Cache(Uniform because used both for Envsame precision 2011 Stephen Chong, Harvard University31
ility RelationAcceptability relationce δ e(C, ρ) ce is current context environment i.e., forfree variablesof e, in whichcontexttheycurrentcontextenvironment– willbewerechangedbound?are made Changes as variables are boundurrent– will be changed when functions δ is contextcurrent context Changes as functions are applied , ρ) is an acceptable analyrmula expresses that (Cpecified by ce and δ. 2011 Stephen Chong, Harvard University32
Acceptability relationControl Flow Analysis with Context (2) always , ρ) ce(Ccδ , ρ) ce(Cxδ ( , δ) ρ(x,ce(x) ) Ciff 0 1 2 ce δ (if t0 then t1 else t2 )(C, ρ) 0 1 2cecece iff(C, ρ) δ t0 (C, ρ) δ t1 (C, ρ) δ t2 ( , δ) C ( , δ) C ( , δ) C ( , δ)C12 , ρ)1 in t 2 ) ce(letx t(C21δ 2 cece 1 iff(C, ρ) δ t1 (C, ρ) δ t2 ( , δ) ρ(x, ( , δ) C ( , δ) Cδ) C12where ce ce[x δ] 1 2 ce δ (t1 op t2 )(C, ρ)PPASection3.6 2011 StephenChong,Harvard Universityiff 1 2cece δ t1 (C, ρ) δ t2(C, ρ)c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 9533
Acceptability relationControl Flow Analysis with Context (1) , ρ) ce(C(fnx e)0δ , ρ) ce(C(funfx e)0δ iffiff ( , δ){(fn x e0, ce )} C ( , δ){(fun f x e0, ce )} C , ρ)1 t 2 ) ce(C(t1 2δ 1ce t 2 , ρ) , ρ) ce iff(Ct (C δ 1δ 2 ( , δ) :( (fn x t00 , ce0 ) C1 ce , ρ) ( , δ) ρ(x, ( , δ ) C ( , δ) δ 0 t00 C (Cδ) C200 00where δ0 δ, k and ce 0 ce0[x δ0]) 0 ( , δ) :( (fun f x t0 , ce0 ) C1 ce , ρ) ( , δ) ρ(x, ( , δ ) C ( , δ) δ 0 t00 C (Cδ) C200 00 {(fun f x t00 , ce0 )} ρ(f,δ0 )where δ0 δ, k and ce 0 ce0[f δ0, x δ0])PPASection 3.6 2011 Stephen Chong, Harvard Universityc F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 9434
ample:ExampleExample:1 )2 in ((f3 f4 )5 (fn y y6 )7 )8 )9(letf (fnx xExample:(let f (fn x x1)2 in ((f3 f4)5 (fn y y6)7)8)9 Contexts of interest for uniform 1-CFA(let f (fn x x1)2 in ((f3 f4)5 (fn y y6)7)8)9of interestfor uniform 1-CFA:1-CFA:texts ofContextsinterestfor uniformΛ: the initial contextContextsof interestfortheuniform1-CFA:point labelled 5 has been passedthe initialcontext5: thecontextwhenapplicationΛ:the contextinitial context8: thewhentheapplication pointlabelled8 has been5passedthe contextwhentheapplicationpointlabelledhas been p5: the context when the application point labelled 5 has been passedthe contextwhenwhentheoftheapplicationpointlabelledhas been pContextinterestfor uniform1-CFA:8: the environmentscontextapplicationpointlabelled8 has been8passedce0 [ ]the initial (empty) context environmentContextofinterestfor uniformfor1-CFA:ce1 ceenvironments[f Λ]thecontextenvironmentthe analysis of the body of0text environmentsofinterestforuniform1-CFA:ce0 [ ]theinitial(empty)contextenvironmentthe let-construct the contextcontext environmentenvironmentusedfor theanalysisof thebodyofce12 cece00[[fx the Λ]5] initialthefor theanalysisof thebody [ ] ce(empty)contextenvironmenttheof f let-constructinitiated at the application point 5 ce0[fce ce Λ]thecontextenvironmentfortheanalysisofthece[x 2 03 ce0 [x 8] the context environment used for the analysis of the bodyofof ff initiatedinitiated atat thethe applicationapplication pointpoint 58.the let-constructce3 ce0[x 8] the context environment used for the analysis of the body ce0[xPPA Section5] 3.6the contextenvironmentusedforofof f theNielsonapplication8. the analysisc initiatedF.Nielson &atH.Riis& C.Hankinpoint(Dec. 2004)96 Context environments of interest for uniform 1-CFAoffinitiatedattheapplicationpoint5c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004)PPA Section 3.6 96 2011 Stephen Chong, Harvard University35 ce [x 8] the context environment used for the analysis of
Example and ρ to be:Example: Let us take Cidid (1, 5) {(fn x x1,ce )}C0id (2, Λ) {(fnCid (4, Λ) {(fnCid (7, Λ) {(fnCid (9, Λ) {(fnCidx x1,ce0)}x x1,ce0)}y y6,ce0)}y y6,ce0)}ρ id (f, Λ) {(fn x x1,ce0)}ρ id (x, 5) {(fn x x1,ce0)}This is an acceptable analysis result: (1, 8) {(fn y y6,ce )}C0id (3, Λ) {(fn x x1,ce )}C0id (5, Λ) {(fn x x1,ce )}C0id (8, Λ) {(fn y y6,ce )}C0idρ id (x, 8) {(fn y y6,ce0)}ce , ρ ) 0 (let f (fn x x1)2 in ((f3 f4)5 (fn y y6)7)8)9(CididΛPPA Section 3.6 2011 Stephen Chong, Harvard Universityc F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 9736
ComplexityAbstract Domainsδ ce CEnv v Val ρ Env Lab kcontext information Var context environments P(Term CEnv)abstract values abstract environments (Var ) Val Cache abstract cachesC (Lab ) Val k-CFA has worst-case exponential complexityin size of program (Uniform because used both for Env and Cache.) Size n program, p variables Δ has O(n) elementsPPA Section 3.6 Size of CEnv isO(np)c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 92 Val is powerset of pairs (t, ce), and there are O(n np) pairs, so Val has heightO(n np) p O(n) 0-CFA has worst-case polynomial complexity 2011 Stephen Chong, Harvard University37
Variations on k-CFAVariations (based on call-strings)Uniform k-CFAcev ρ C CEnv Val Env Cache Var P(Term CEnv) (Var ) Val (Lab ) Valcontext environmentsabstract valuesabstract environmentsabstract cachesk-CFA Cache abstract cachesC (Lab CEnv) ValPolynomial k-CFA P(Term ) abstract valuesv Val 2011 Stephen Chong, Harvard University38
k-CFA Paradox [Might, Smaragdakis, van Horn, PLDI 10] k-CFA is exponential for k 1 But k-CFA is like using context of k most recentcall-sites Polynomial for OO languages Doop implemented in Datalog, which only allows polynomialtime alogrithms OO has dynamic dispatch What gives? 2011 Stephen Chong, Harvard University39
Wait, which k-CFA? In OO world, translate k-CFA to“k-call-site sensitive interprocedural pointeranalysis with a k-context-sensitive heap and onthe-fly call-graph construction” i.e., data flow (points-to relation) and call-graphdependent on each other Is it the same analysis? Yes. And paradox still holds. 2011 Stephen Chong, Harvard University40
Paradox resolved In functional languages, closures are created incrementally Each variablein a Domainsclosure could be bound in a different contextAbstract Source of exponentiallityδ ce CEnv v Val ρ Env Lab kcontext information Var context environments P(Term CEnv)abstract values abstract environments (Var ) Val Cache abstract cachesC (Lab ) Val In OO languages, closures created explicitlybyinvokingconstructor (Uniform because used both for Env and Cache.) Variables are copied, and so effectively all variables bound in samecontext PPA Section 3.6 92c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) CEnv Δ instead of Var Δ 2011 Stephen Chong, Harvard University41
new ClosureXY(x,y);cxy.baz( );.cx.bar(oyM);y}Examplebaz( ) {. x . y .}}},&-., #.% ./,(0& ")1Ͳ)& "2&caller@1: foo x - [ox1]foo@1: bar y - [oy1].caller@N: foo x - [oxN]foo@M: bar y - [oyM] OO program}56789:!"# %&"'(")* ox1caller@1: new Object(); oxN new Object();oy1 newObject(); oyM new Object();foo@1:("# %&"'(")1foo::ClosureX.x - [ox1]bar::ClosureXY.x- [ox1, ,oxN]class ClosureX {bar::ClosureXY.y- [oy1]Objectx;.3(.0 &/4(-)caller() {class ClosureXY {ClosureX(Object( jx0)) {.foo(ox1);0& ")1 )& "2&0& ")1Ͳ)& "2&Object x,y;x) {caller@N:ll foo(Object@Nx x0;.ClosureXY(Object x0,ClosureX cxfoo@M:foo::ClosureX.x- [oxN]} // constructorfoo(oxN);Object y0) {new ClosureX(x);bar::ClosureXY.x - [ox1, , oxN]bar(Objecty){}x x0; y y0;cx.bar(oy1);bar::ClosureXY.y - [oyM]ClosureXYcxy } // constructor.newClosureXY(x,y);cx.bar(oyM);ybaz( ){ types, the class containingFigure 1. An example OO program,}analyzed under 1-CFA. Parts that cxy.baz( );are orthogonal to the analysis (e.g.,returnx . vary .foo, the body of baz) are elided. The bottom part shows the (points-to).results of the analysis in the form.“context:- abstractObject”.}}Conventions: we use [ox1], ., [oxN], [oy1], ., [oyM] to mean the abstract objects pointed to by the corresponding environment variables.}} (We only care that these objects be distinct.) method var names a local variable, var inside a method. method::Type.field refers to a field ofthe object of type Type allocated inside method. (This example allocates a single object per method, so no numeric distinction of allocationcaller@1:foo x - bar y - [oy1]sites is necessary.) callermethod@numdesignatesthe [ox1]num-th call-sitefoo@1:inside methodcallermethod.,&-., #.% ./,(.0& ")1Ͳ)& "2& Equivalent functional programcaller() {foo(ox1);.foo(oxN);}3(.0 &/4(-)0& ")1 )& "2&0& ")1Ͳ)& "2&caller@N: foo x - [oxN]!foo(Object x) {Clos e cClosurecx caller@1:cx(oy1);foo::ClosureX.x- [ox1].!.cx(oyM);}caller@N:ll @Nfoo::ClosureX.x - [oxN]caller@1: foo x - [ox1] 2011 Stephen"# %" &%'(%)"*Chong, Harvard University.foo@M: bar y - [oyM]56789:foo@1:lambda(Object y) {("# %&"'(")1bar::ClosureXY.x- [ox1, , oxN]Closure cxy bar::ClosureXY.y - [oy1]cxy( );lambda( ) {. x . y .foo@M:}}bar::ClosureXY.x - [ox1, , oxN]bar::ClosureXY.y - [oyM]foo@1: lambda y - [oy1].Figure 1. An example OO program, analyzed under 1-CFA. Parts thatare orthogonal to the analysis (e.g., return types, the class containing42
m-CFA From this insight, Might, Smaragdakis and VanHorn develop m-CFA Contexts are the top m stack frames (Different from last k call sites when in continuationpassing style) Essentially CEnv Δ instead of Var Δ Polynomial-time analysis, seems as precise a kCFA for significantly less time 2011 Stephen Chong, Harvard University43
0-CFA 0-CFA is an context-insensitive CFA. Result of a 0-CFA analysis is pair (Ĉ, ρ) Ĉ is an abstract cache ρ is an abstract environment Notes: Could combine these into one entity: (Var Lab) Val Could also require A-normal form, where all subterms are appropriately labeled by variables 7 Abstract Domains .
