Scalable Context-Sensitive Flow Analysis Using Instantiation Constraints

Slide Note

Context-sensitive flow analysis using instantiation constraints plays a crucial role in type inference for flow analysis. This approach involves constraint-based polymorphic type inference, construction of type instantiation graphs, and analysis of flows on these graphs. By extending to higher-order programs, polymorphism enhances context-sensitivity, enabling effective flow analysis. The methodology involves Steensgaard's points-to analysis, semi-unification algorithms, and interprocedural flows within type instantiation graphs, offering a comprehensive overview of flow analysis techniques for program variables.

naev_802 Follow

Uploaded on Feb 23, 2025 | 1 Views

Download Presentation

Please find below an Image/Link to download the presentation.

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.

You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.

Download Presentation

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.

E N D

Presentation Transcript

Scalable Context-Sensitive Flow Analysis Using Instantiation Constraints Manuel Fahndrich Jakob Rehof Manuvir Das

Overview Constraint based Polymorphic Type Inference Construction of Type Instantiation Graph (TIG) Flow analysis on TIG

Introduction Using type inference for flow analysis Polymorphic version of Steensgaard s points-to analysis Polymorphism responsible for context-sensitivity Extends naturally to higher order programs

Outline Steensgaard s Analysis and Types Constraint Based Type Inference Intraprocedural Type Inference Interprocedural Type Inference without Polymorphism Interprocedural Type Inference with Polymorphism Semi-unification Algorithm with Interprocedural Flows Type Instantiation Graph Flow Analysis Extension to Higher-order Programs Thought Experiment Andersen s analysis and Type Inference

Steensgaards Analysis T1 T2 T3 x = &a; y = x; x y a b c y = &b; b = &c; Divides variables into equivalence classes and maintains points-to information *example taken from pointer analysis slides by G. Ramalingam

Inspired by Type Inference! Each equivalence class represents data flow information T1 T2 T3 T T1, T2, T3 are types of variables PTR(T) PTR(PTR(T)) x y a b c Variables in the same class have possible flows amongst themselves T1 points-to T2 T1 = PTR(T2) C Analogy : The direction of flow is unknown If T3 is int, T2 is int* and T1 is int**

x = &a; y = x; y = &b; b = &c; Type Checking Using the following rules we will type check the program ? ={ x:ptr(ptr(?)), y:ptr(ptr(?)), a:ptr(?), b:ptr(?), c: ?)} ?:? &? ???(?) ?:? ?:? ?:???(?) ? ? [var] [deref] [addr] ?1 ?2 ?1;?2 ?:? ?:? ? = ? [seq] [Assign]

Steensgaards Analysis and Type Inference Therefore, we can use type inference to divide the program variables into equivalence classes these equivalence classes are the flow relations between variables types also encode the points-to information among variables

Types and Locations Language : C Types : PTR(T) T PTR(PTR(T)) ? ? | ??? (?) x y a b c Flow labels : used to uniquely name the program objects (here, variables and pointers) Ranged over by [?] is the memory location named , holding values of type ? ??? (?) : pointer to a location named

Types and Locations Example: Types : int x, *p; p= &x; ? ? | ??? (?) Flow labels : used to uniquely name the program objects (here, variables and pointers) Ranged over by [?] is the memory location named , holding values of type ? ??? (?) : pointer to a location named label of x : 1 type of x : ? location of x : [?] 1 label of p : 2 type of p : ????1(?) location of p : [????1(?)] 2

Types and Locations Quick Practice int x, *p, **q; p = &x; q = &p; Q. Write the label, location and type of variable q. label of q : ? location of q : [?????(?????? )] ? type of p : ?????(?????(?))

Types and Locations c : [?]?1 a : [?] 2 b : [?] 3 x : [?] 4 y : [?] 5 b : [????1(?)] 3 x : [????2(?)] 4 y : [????3(????1(?))] 5 x = &a; PTR(T) T PTR(PTR(T)) x y a b c y = x; y = &b; b = &c;

Types and Locations c : [?]?1 a : [?] 2 b : [?] 3 x : [?] 4 y : [?] 5 b : [????1(?)] 3 x : [????2(?)] 4 y : [????3(????1(?))] 5 ????1(?) ? ????3(????1(?)) x = &a; y = x; y = &b; b = &c; ?,?, ????2? , ????3(????1 (?)) ?, ? ? ????1(?) Equivalence class of types each variable can be assigned the representative of each class as its type

Recap Steensgaard s Algorithm Steensgaard s equivalence classes as types Types, Locations and Labels Next Type inference

Type Inference by Constraint Generation ? ?:? / C : type environment : set of assignments of the form ? [?]?, T : type or location , C : set of constraints equalities and inequalities ?3 = {? = ? } ?1 = ?2 ?1 ?2 ?3 ?1 ? ?1 ?2 ? ?2 ?1;?2 ?1 ?2 ?1 ?1 ?2 ?2 ? [?]? ? ? ? [Rval] [assign] [seq] ? [?]?? ? ????(?) ? ? [?]?? ? [?]? ? [?]?? &? ????(?) ? [addr] [deref] [var]

Type Inference by Constraint Generation seq {? = ????2(?) } = seq ????2(?) {? = ?} seq = x &a {? = ????5(?) } {? = ????4(?) } [?]?2 [?]?1 y x = = [?]?3 [?]?1 ????4(?) ????5(?) y &b b &c [?]?3 [?]?4 [?]?4 [?]?5 Post-order Walk on the AST

Type Inference by Constraint Generation Set of constraints generated {? = ????2(?) , ? = ?, ? = ????4(?), ? = ????5(?)} The types are represented as Type graphs nodes are type constructors (ptr in this case) and type variables, undirected edges between term and its subterms[ASU88] To infer types, we will solve them by Unification.

Unification Algorithm Returns only equalities in this case Finds the representatives and checks if they are equal Creates an equivalence class and sets a representative Incompatible types - error Generate more constraints for labels and sub terms in type expressions

Solving Constraints Substitution ? ?????? ? ?????? ? ?????? ? ?????? ????2 ????2 ????4 ????5 ? Type Graphs ????5 ? ? ? ? ????2? ?5 ????5(?) ?2 ? ?,?, ????2? , ????4? ?2 ?4 ?, ?, ????5(?) ? ?5 Equivalence Classes

Query are x and y aliased? ????2? ?5 ?2 ????5(?) ? ?,?, ?2 ?4 ?, ?, ????5(?) ????2? , ????4? ? ?5 x : [?]?1 a : [?] 2 y : [?] 3 b : [?] 4 c : [?] 5 YES they belong to the same class

Query does a points-to c? ????2? ?5 ?2 ????5(?) ? ?,?, ?2 ?4 ?, ?, ????5(?) ????2? , ????4? ? ?5 x : [?]?1 a : [?] 2 y : [?] 3 b : [?] 4 c : [?] 5 YES a may point-to c, as type of a is ????5(?), i.e. it is a pointer to [?]?5

Interprocedural Analysis Using Type Inference We can extend the framework for Interprocedural analysis Types : ? ? ??? ? ?2:? ? ?1, ,?? ? ? ?1 = ? {????(?)= ?} ??????? ? ?1 [return] ??:?? ?? (? = 1 ?) ?1 = ?=1 ?2 = {??= ?1, ,?? ? ?} ? ?1, ,?? :? ?1 ?2 ,?1:[?1]?1, ,??:[??]?? ?2 = {??= ?1, ,?? ? ????(?)} ? ?1, ,?? ? ? ? ?1 ?? [def] [call] ?1 ?2

Interprocedural Analysis Using Type Inference main(){ p = &a; q = &b; c = foo(p); d = foo(q); } foo(x) { return x; } ??:?? ?? (? = 1 ?) ?1 = ?=1 ?2 = {??= ?1, ,?? ? ?} ? ?1, ,?? :? ?1 ?2 ? ?? ?:? ? ?1 = ? {????(?)= ?} ??????? ? ?1 [return] [call] ,?1:[?1]?1, ,??:[??]?? ?2 = {??= ?1, ,?? ? ????(?)} ? ?1, ,?? ? ? ?1 [def] ?1 ?2

Interprocedural Analysis Using Type Inference main(){ p = &a; q = &b; c = foo(p); d = foo(q); } foo(x) { return x; } Initial types: a : [?]?1 , b : [?]?2, c : [?]?3, d : [?]?4, p : [?]?5, q : [?]?6 x : [?]?10 Final Constraints : ? = ????1(?) ? = ????2? ???? = ????1? ?7 ? ???? = ????2? ?8 ? ???? =? ?9 ????(???) ????(???) = ?

Interprocedural Analysis Using Type Inference main(){ p = &a; q = &b; c = foo(p); d = foo(q); } foo(x) { return x; } Initial types: a : [?]?1 , b : [?]?2, c : [?]?3, d : [?]?4, p : [?]?5, q : [?]?6 x :[?]?10 Final Constraints : ? = ????1(?) ? = ????2? ???? = ????1? ?7 ? ???? = ????2? ?8 ? ???? = ? ?9 ????(???) ????(???) = ? ????1(?) ? ? ?, ? ? ????1(?) , ?,?, ?,?, ????2?

Query are p and q aliased? main(){ p = &a; q = &b; c = foo(p); d = foo(q); } foo(x) { return x; } Initial types: a : [?]?1 , b : [?]?2, c : [?]?3, d : [?]?4, p : [?]?5, q : [?]?6 x :[?]?10 Final Constraints : ? = ????1(?) ? = ????2? ???? = ????1? ?7 ? ???? = ????2? ?8 ? ???? = ? ?9 ????(???) ????(???) = ? ????1(?) ? ? ?, ? ? ????1(?) , ?,?, ?,?, ????2? No, but the analysis says YES

Query does the value of p flow to d? main(){ p = &a; q = &b; c = foo(p); d = foo(q); } foo(x) { return x; } Initial types: a : [?]?1 , b : [?]?2, c : [?]?3, d : [?]?4, p : [?]?5, q : [?]?6 x :[?]?10 Final Constraints : ? = ????1(?) ? = ????2? ???? = ????1? ?7 ? ???? = ????2? ?8 ? ???? = ? ?9 ????(???) ????(???) = ? ????1(?) ? ? ?, ? ? ????1(?) , ?,?, ?,?, ????2? No, but the analysis says YES

Ideal result ? ????1(?) main(){ p = &a; q = &b; c = foo(p); d = foo(q); } foo(x) { return x; } ? ?, ????1(?) ????2(?) ? ?, ? ????2?

Context Sensitive Analysis The analysis is currently context-insensitive uses monomorphic types introduction of polymorphic types for context-sensitivity solve with Instantiation Constraints

Polymorphism We have a Principal type or the most general type T for each expression T1 is called an instance of T if T1 = R(T) for some substitution R ( mapping of type variables to types) expressed as T T1 Here, we will specialize the type of function at each use, by instantiating the type constraints of the form ???? ???? will be generated Unification not enough for constraint solving

Interprocedural Analysis With Polymorphism main(){ p = &a; q = &b; c = foo(p); d = foo(q); } foo(x) { return x; } Instantiation at each use of a function here it means the call site Def and Ret rules same as before ignore the super- and sub- scripts for now The type here is not the def type rather depends upon the current value of expressions

Interprocedural Analysis With Polymorphism Initial types: a : [?]?1 , b : [?]?2, c : [?]?3, d : [?]?4, p : [?]?5, q : [?]?6, x :[?]?10 Final Constraints : ? = ????1(?) ? = ????2? ???? ????1? ?7 ? ???? ????2? ?8 ? ???? =? ?9 ????(???) ????(???) = ?

Semi-Unification Extension of unification to solve a set of constraints involving equalities and inequalities [Hen93, KTU94] An inequality ? ? is called solvable if ? is a substitution of ? for some substitution instance ?, i.e. R ? = ? Substitution ? is a solution to a constraint set ? iff S ? = ?(? ) for every equality ? = ? ? and S(?) ?(? ) is solvable for every ? ? ?.

Constraint Indices Textual references to a function are tagged with a unique index i, identifying the occurrence In first order case, it is same as tagging different call-sites with unique indices. For each occurrence ??,[FUN] rule gives rise to a constraint ? ?? Therefore, rephrasing the semi-unification definition Substitution ? is a solution to a constraint set ? iff ? ? = ?(? ) for every equality ? = ? ? and ?(?) ??(? ) is solvable for every ? ?? ?.

Constraint Polarity Keeps track of input and output position in types ? +, , , p is polarity Ordering + and . + - positive polarity, - negative polarity Polarity of a term - Term T occurs positively if it occurs nested to the left of the type constructor ( ) an even number of times, else negatively In type - ? ? ? ?,? occur positively, and ? and (? ?) occur negatively Targets of pointer types ptr(T) occur at polarity T.

Propagation of Constraint polarities ? ? Each inequality carries polarity information, ? ? During resolution inequalities propagate to their subterms Polarities switch according to the polarities of the subterms [FUN] rule provides the initial polarity, ? ? + ? ? ? ? ? ? ? ? + Propagation : Propagation in pointers loses polarity! ?? ? ? ? + ?

Data flow due to polarities Decide the direction of data flow ? ? ? ? ? + ?? ?? ? + ? Flow opposite to the direction of inequality Flow in the direction of inequality From actual parameter to formal Return value to return point

Exercise Polarity Propagation ? (?1 ?1) ???(?3) + ?1 ?2 ??? ?3 Solution : (?1 ?1) ??? ?3 + ?1 + ?2 ?3 ? ?(?1 ?2) ???? ?3 ??1 ??2 ??3

Constraints with indices main(){ p = &a; q = &b; c = foo(p); d = foo(q); } foo(x) { return x; } Initial types: a : [?]?1 , b : [?]?2, c : [?]?3, d : [?]?4, p : [?]?5, q : [?]?6, x :[?]?10 Final Constraints : ? = ????1(?) ? = ????2? ?? ?7 ? ???? + ?? ?8 ? ???? + ???? =? ?9 ????(???) ????(???) = ?

Semi Unification Algorithm

Type Instantiation Graph ? ? + + ?9 ?7 ?8 ????1 ? ????2 ? ? ? ? ? ? ? ? ?

Flow Graph + + ?9 ?7 ?8 ????1 ? ? ????2 ? ? + + ? - ? ? -

main(){ p = &a; q = &b; c = foo(p); d = foo(q); } foo(x) { return *x; } Flow Graph + + ?9 ?7 ?8 ????1 ? ? ????2 ? ? + + ? - ? ? - What values flow to the variable c? Both p and q flow to c!

main(){ p = &a; q = &b; c = foo(p); d = foo(q); } foo(x) { return *x; } Flow Graph PosNeg Paths + + ?9 ?7 ?8 ????1 ? ? ????2 ? ? + + ? Restriction Valid flow path : any number of positive edges, Followed by any number of negative edges - ? ? -

main(){ p = &a; q = &b; c = foo(p); d = foo(q); } foo(x) { return *x; } Flow Graph + + ?9 ?7 ?8 ????1 ? ? ????2 ? ? + + ? Restriction Valid flow path : any number of positive edges, Followed by any number of negative edges - ? ? - Only p flows to c and q flows to d