Massachusetts Institute of TMIT 6.035 F d ti f D t fl A l iFoundations of Dataflow Analysis Martin Rinard Laboratory for Computer Science Massachusetts Institute of Technology echnology•Dataflow Analysisy• Compile-Time Reasoning Aboutp g • Run-Time Values of Variables or Expressions • At Different Program PointsAt Different Program Points – Which assignment statements produced value of variable at this point?variable at this point? – Which variables contain values that are no longer used after this program point?used after this program point? – What is the range of possible values of variable at this program point?this program point?Program Representationg p • Control Flow Graphp– Nodes N – statements of program – Edges E – flow of controlg • pred(n) = set of all predecessors of n • succ(n) = set of all successors of n – Start node n0 – Set of final nodes Nfinalfinal•–Program Pointsg•One program point before each nodepg p • One program point after each node • Join point point with multiple predecessors Join point point with multiple predecessors • Split point – point with multiple successors•Basic Idea • Information about program represented usingpg p g values from algebraic structure called lattice • Analysis produces lattice value for eachAnalysis produces lattice value for each program point • Two flavors of analysisTwo flavors of analysis – Forward dataflow analysis Bk d d t fl l i– Backward dataflow analysisForward Dataflow Analysisy• Analysis propagates values forward through control flow graph with flow of control – Each node has a transfer function f • Input – value at program point before node • Output – new value at program point after node – Values flow from program points after predecessor nodes to program points before successor nodes – At join points, values are combined using a merge function • Canonical Example: Reaching DefinitionsBackward Dataflow Analysisy• Analysis propagates values backward through control flow graph against flow of control – Each node has a transfer function f • Input – value at program point after node • Output – new value at program point before node – Values flow from program points before successor nodes to program points after predecessor nodes – At split points, values are combined using a merge function – Canonical Example: Live Variables–Partial Orders •Set P • Partial order ≤ such that ∀x,y,z∈P – x ≤ x (reflexive)x ≤ x (reflexive) –x ≤ y and y ≤ x implies x = y (asymmetric) x ≤ yand y ≤ z implies x ≤ z (transitive)x ≤ y and y ≤ z implies x ≤ z (transitive) • Can use partial order to define U d l b d– Upper and lower bounds – Least upper bound – Greatest lower boundUpper Boundspp• If S ⊆ P then –x∈P is an upper bound of S if ∀y∈S. y ≤ x – x∈P is the least upper bound of S if pp• x is an upper bound of S, and •x ≤ y for all upper bounds y of S – ∨ - join, least upper bound, lub, supremum, sup • ∨ S is the least upper bound of S •x ∨ y is the least upper bound of {x,y}Lower Bounds • If S ⊆ P then –x∈P is a lower bound of S if ∀y∈S. x ≤ y – x∈P is the greatest lower bound of S if g• x is a lower bound of S, and •y ≤ x for all lower bounds y of S – ∧ - meet, greatest lower bound, glb, infimum, inf • ∧ S is the greatest lower bound of S g•x ∧ y is the greatest lower bound of {x,y}Coveringg •x< y if x ≤ y and x≠yy y y • x is covered by y (y covers x) if – x < yand x < y, and –x ≤ z < y implies x = z • Conceptually y covers x if there are no • Conceptually, y covers x if there are no elements between x and yExamplep• P = { 000, 001, 010, 011, 100, 101, 110, 111} (standard boolean lattice, also called hypercube) •x ≤ y if (x bitwise and y) = x 111 Hasse Diagram • If y covers x 011 101 110 • If y covers x • Line from y to x 010 001 100 • y above x in diagram 000•Lattices • If x ∧ y and x ∨ y exist for all x,y∈P,y y y then P is a lattice. • If ∧Sand ∨Sexist forall S ⊆ P,If ∧S and ∨S exist for all S ⊆ P, then P is a complete lattice. • All finite lattices are completeAll finite lattices are completeLattices • If x ∧ y and x ∨ y exist for all x,y∈P, then P is a lattice. • If ∧S and ∨S exist for all S ⊆ P, then P is a complete lattice. • All finite lattices are complete • Example of a lattice that is not complete – Integers I – For any x, y∈I, x ∨ y = max(x,y), x ∧ y = min(x,y) – But ∨ I and ∧ I do not exist I ∪ {+∞ ∞ } is a complete lattice – I ∪ {+∞,−∞ } is a complete latticeTop and Bottomp• Greatest element of P (if it exists) is top( ) p • Least element of P (if it exists) is bottom (⊥)Connection Between ≤, ∧, and ∨, , • The following 3 properties are equivalent: – x ≤ yy –x ∨ y = y –x ∧ y = x • Will prove: –x ≤ y implies x ∨ y = y and x ∧ y = x – x ∨ y = y implies x ≤ y –x ∧ y = x implies x ≤ y Th b i i i b i• Then by transitivity, can obtain –x ∨ y = y implies x ∧ y = x x ∧ y x implies x ∨ y y– x ∧ y = x implies x ∨ y = y•=Connecting Lemma Proofsg• Proof of x ≤ y implies x ∨ y = yy p y y –x ≤ y implies y is an upper bound of {x,y}. – Any upper bound z of {x,y} must satisfy y ≤ z.ypp { ,y} y y – So y is least upper bound of {x,y} and x ∨ y = y • Proof of x ≤ y implies x ∧ y = xProof of x ≤ y implies x ∧ y x –x ≤ y implies x is a lower bound of {x,y}. Any lower bound z of {x y} must satisfy z ≤ x– Any lower bound z of {x,y} must satisfy z ≤ x. – So x is greatest lower bound of {x,y} and x ∧ y = xConnecting Lemma Proofsg• Proof of x ∨ y = y implies x ≤ yy y p y – y is an upper bound of {x,y} implies x ≤ y • Proof of x ∧ y = x implies x ≤ yProof of x ∧ y x implies x ≤ y – x is a lower bound of {x,y} implies x ≤ yLattices as Algebraic Structuresg• Have defined ∨ and …