Foundations of Dataflow Analysis

Global constant propagation algorithm

Consider the following example:

d0: y = 3
d1: x = y + 4
d2: y = 11
d3: if e ...
d4: x = 5
d5: y = x + 6
d6: if e2 ...

Consider an alternate representation of constant information using sets where all variables are tracked simultaneously. This representation can provide both better precision and better efficiency, than running the single-variable implementation multiple times.

There are two options for the transfer function for d1: either use the in value to determine that x is a constant too, or simply represent the transfer function as a GEN/KILL set (as a function of the statement, but independent of the input value). The former is more precise than the latter, e.g., the former can have logic that says something like: if s: z=x+y, and both x,y are constants in in, then f_s(in) assigns z to a constant --- something like this cannot be captured in the GEN/KILL set based transfer function as these sets are only functions of s and have no visibility into in.

This representation allows transfer functions to be written using generate (Gen[s]) and propagate (in[s] - Kill[s]) definitions.

Can summarize a basic block through its own composite transfer function as follows:

• Gen[d0] = (y,3), Kill[d0] = (y,*), out[d0] = (in[d0] - Kill[d0]) U Gen[d0]
• Gen[d1] = empty, Kill[d1] = (x,*), out[d1] = (in[d1] - Kill[d1]) U Gen[d1]
• Gen[d2] = (y,11), Kill[d2] = (y,*), out[d2] = (in[d2] - Kill[d2]) U Gen[d2]
• ...

Gen[B]: locally exposed constant definitions, definitions available at the end of the basic block B

Kill[B]: the set of constant definitions killed by B

Effects of edges: nodes with multiple predecessor: meet operator is Intersection: in[b] = out[p1] n out[p2] ... n out[pn], for p1..pn predecessors of b

Cyclic graphs: equations still hold:

• out[b] = fb(in[b])
• in[b] = Intersection over out[pi] for preds pi of b

input: control flow graph CFG = (N, E, Entry, Exit)

//Boundary condition
OUT[Entry] = empty set

//Initialization for iterative algorithm
For each basic block B other than Entry
  OUT[B] = {(x,\Top) for all x}

//Iterate
While (changes to any OUT occur) {
    For each basic block B other than Entry {
      in[B] = intersection over (out[p]), for all preds p of B
      out[B] = fB(in[B]) //out[B] = gen[B] u (in[B] - kill[B])
    }
}

Summary of constant information analysis

	Constant information
Domain	Sets of constant definitions
Transfer function fb(x)	forward: out[b] = fb(in[b]) out[b] = Gen[b] U (x - Kill[b])
Meet operation	in[b] = n out[predecessors] intersection
Boundary condition	out[entry] = empty
Initial interior points	out[b] = {(x,\top): for all variables x}

• How is \bot encoded? By a missing constant definition for that variable
• Have we added an imprecision in the meet operator (compared to our previous formulation)? Yes, we now take an intersection at the meet operator, so (x,\top) and (x,3) will meet to return an empty set (bottom), which is more imprecise than our previous meet operator that would have resulted in (x,3). It is possible to make the meet operator more precise, by giving special treatment to the \top value, making the analysis more precise and still correct.
• We have already discussed the imprecision in the transfer function due to the GEN and KILL sets.

Live Variable analysis

• Direction: backward: in[b] = fb(out[b])
• Transfer function for statement s: x = y + z
  • generate live variables: Use[s] = {y, z}
  • propagate live variables: out[s] - Def[s], Def[s] = x
  • in[s] = Use[s] U (out[s] - Def[s])
• Transfer function for basic block B:
  • in[b] = Use[b] U (out[b] - Def[B])
  • Use[b] : set of locally exposed uses in B, i.e., uses not covered by definitions in B
  • Def[b] = set of variables defined in B.
• Meet operator: intersection: out[B] = in[s1] U in[s2] ... U in[sn], for successors s1, .., sn of B
• Boundary condition: in[exit] = empty (or return value as the case might be)

Some observations:

• How is \top (not live) encoded? By presence in the set.
• How is \bot (live) encoded? By absence in the set.

Liveness : Iterative algorithm

input: control flow graph CFG = (N, E, Entry, Exit)

//Boundary condition
In[Exit] = empty

//Initialization for iterative algorithm
For each basic block B other than Exit
    In[B] = empty

//Iterate
While (changes to any IN occur) {
  For each basic block B other than Exit {
    out[B] = U (in[s]) for all successors s of B
    in[B] = fB(out[B]) //in[B]=Use[B] U (out[B] - Def[B])
  }
}

Framework

	Constant information	Live variables
Domain	Sets of constant definitions	Sets of variables
Direction and Transfer function fb(x)	forward: out[b] = fb(in[b]) out[b] = Gen[b] U (x - Kill[b]) in[b] = n out[predecessors]	backward: in[B] = fb(out[B]) in[b] = Use[b] U (x - Def[b]) out[B] = U in[succ[B]]
Meet operation	intersection	union
Boundary condition	out[entry] = empty	in[exit] = empty
Initial interior points	out[b] = {(x,\top): for all variables x}	in[b] = empty

Exercise: must-reach definitions

• A definition D(a = b+c) must reach point P iff
  • D appears at least once along all paths leading to P
  • a is not redefined along any path after last appearance of D and before P

Exercise: reaching definitions

• A definition D(a = b+c) reaches point P if there exists a path from the point immediately following D to P, such that D is not killed (overwritten) along that path.

Would the following be a legal solution to reaching definitions?

Entry --> BB1

BB1 --> BB2

BB2 --> BB2

BB2 --> BB3

BB3 contains (d1: b = 1) definition

BB3 --> exit

in[BB1] = empty
out[BB1] = empty
in[BB2] = {d1}
out[BB2] = {d1}
in[BB3] = {d1}
out[BB3] = {d1}
in[exit] = {d1}

Answer: this is a legal fixed-point solution to the system of equations (it satisfies all the rules/constraints of the transfer function and the meet operator). However this is not a maximum fixed-point (later).

Framework

1. Prove properties of entire family of problems once and for all, e.g., will the program converge? what do the solution to the set of equations mean? how do we ensure the best solution?
2. Aid in software engineering: re-use code

Data-flow problems (F, V, ^) are defined by

• A semilattice
  • domain of values (V)
  • meet operator (^)
• A family of transfer functions F, s.t. f(: V --> V) \in F

• A semi-lattice S = < a set of values V, a meet operator ^ >
• Properties of the meet operator
  • idempotent: x ^ x = x
  • commutative: x ^ y = y ^ x
  • associative: x ^ (y ^ z) = (x ^ y) ^ z
• Examples of meet operators: set-union, set-intersection, and, or, max, min
• Non-examples: add, subtract, multiply, ...

Example of a semi-lattice diagram: V = { x | x is a subset of {d1,d2,d3}}, ^ = set-union

Draw the semi-lattice with arrows pointing downwards (>= relation)

Some interesting properties

• x^y is the first common descendant of x and y
• Define top element \Top such that x ^ \Top = x
• Define bottom element \Bottom such that x ^ \Bottom = \Bottom
• Semi-lattice diagram: picture of a partial order

A meet-operator defines a partial-order and vice-versa

• Definition of partial order ≤: x ≤ y if and only if x^y = x
• In the diagram, x ≤ y indicates that there is path from y to x, and vice versa
• Properties of meet operator guarantee that ≤ is a partial order
  • Reflexive: x ≤ x
  • Antisymmetric: if x≤y and y≤x then x=y
  • Transitive: if x ≤ y and y ≤ z then x ≤ z
• x < y is equivalent to ((x ≤ y) and !(x == y))
• A semi-lattice diagram:
  • Set of nodes: set of values
  • Set of edges: {(y,x): x<y and \not\existsz s.t. (x<z)^(z<y)}
• Example: meet operator = \union, partial order ≤ is ?
• Another example: meet operator = \intersection, partial order ≤ is ? Draw semilattice diagram for this

Summary:

• Three ways to define a semi-lattice:
  • Set of values + meet operator
    • idempotent: x ^ x = x
    • commutative: x ^ y = y ^ x
    • associative: x ^ (y ^ z) = (x ^ y) ^ z
  • Set of values + partial order
    • Reflexive: x ≤ x
    • Antisymmetric: if x ≤ y and y ≤ x then x = y
    • Transitive: if x ≤ y and y ≤ z then x ≤ z
  • A semi-lattice diagram
    • No cycles
    • \Top is on top of everything
    • \Bottom is at the bottom of everything.
    • \Top or \Bottom may not necessarily exist; e.g., if domain is integers, and meet operator is Max, then bottom is \infinity.

Another example: semi-lattice with V = {x | such that x is a subset of {d1, d2, d3}}, ^ = \intersection

Descending chain

• Definition: The height of a lattice is the largest number of > relations that will fit in a descending chain:

  x0 > x1 > x2 > ... > ...
  

• Height of lattice in reaching definitions? Number of definitions
• Height of lattice in live variables? Number of variables
• Important property for the algorithm to work: finite descending chains
  • if V=integers, and ^=min, then height = \infinity
  • Note that it is not necessary for an infinite semi-lattice to have infinite height. example? constant propagation over integers

Product of semi-lattices. One element at a time

• A semi-lattice for data flow problems can get quite large; 2^n elements for n var/definitions, for example
• A useful technique
  • define semi-lattice for 1 element
  • product of semi-lattices for all elements
• Example: union of definitions
  • For each element d1, lattice is : {} --> {d1}
  • Similarly, for d2, lattice is : {} --> {d2}
  • Product lattice is: {} --> {d1}, {} --> {d2}, {d1} --> {d1, d2}, {d2} --> {d1, d2}.
• Defining product of lattices: <x1,x2> ≤ <y1,y2> iff x1≤y1 and x2≤y2
• The height of the product semi-lattice will be equal to the sum of the heights of the individual semi-lattices.
• For DFA problems, we may want to prune the product semi-lattice to remove values that are not expected to appear. For example, in the constant information analysis, a single value's semi-lattice has height 2: \top -> k -> \bottom. Two values' semi-lattice will have height 4: (\top,\top) -> (\top,k) -> (k,k) -> (\bot,k) -> (\bot,\bot). However, the values (\top,k) is not required for a precise-enough analysis as if the value is \top for one variable, it must be \top for another variable too. (Recall that during the transfer function definition, we say that if the incoming value is \top, then the outgoing value is \top irrespective of what the instruction is).

Transfer functions

• A family of transfer functions F
• Basic properties f: V --> V
  • Has an identity function, i.e., \Exists f such that f(x) = x for all x.
    • Required because an empty instruction, or a no-op instruction will always need to be supported.
  • Closed under composition, i.e., if f1,f2 \in F, then f1.f2 \in F.
    • Required because a sequence of two or more instructions may be treated as a single instruction at any time.
• Notice that GEN/KILL set-based definitions agree with these two properties listed above. Identity is achieved by using the empty sets. Closure is ensured by the fact that the composed function can also be represented by some GEN and KILL sets.

Monotonicity Consider the iterative fixed point algorithm. Recall that we intuitively concluded that the solution keeps descending, and because there is a finite number of steps that can be descended, the algorithm will convert. We used a (co)induction argument to conclude that the solution keeps descending: on a meet, if the current inputs are lower than previous inputs, then the current output is necessarily lower than the previous outputs (because the meet operator is defined as the greatest lower bound). However, what happens on a transfer across a statement: if it is possible that a lower input produces a higher output due to a transfer function f \in F, then we cannot make this argument that the solution keeps descending. To still be able to make this argument, we add a third constraint to F that all functions must be monotone.

• A framework (F, V, ^) is monotone iff x ≤ y implies f(x) ≤ f(y)
• Important: monotone framework does not mean that f(x) ≤ x.
  • e.g., reaching definition for two definitions in a program, d1 and d2. Suppose f: Gen = {d1}; Kill = {d2}; f({}) = {d1} which is not ≤ {}.
  • x: {} ≥ {d1} ≥ {d1,d2}; f(x): {d1} ≥ {d1} ≥ {d1}.
  • No relationship between f(x) and x!
• Equivalently, a framework (F, V, ^) is monotone iff
  • f(x^y) ≤ f(x)^f(y) for all x,y \in V and f \in F
  • (meet inputs, then apply f) ≤ (apply f individually to inputs, then meet results)
• This is an interesting way of interpreting monotonicity, as it provides insight into the solution produced by an iterative fixed point algorithm. Consider the constant propagation DFA with the following program: if (...) { x = 2; y = 3; } else { x = 3; y = 2; }; z = x + y; f(x)^f(y) = 5; f(x^y) = \Bottom.
  entry -> BB1, entry -> BB2, BB1 -> BB3, BB2 -> BB3. BB1 has x := 4; y := 3 and BB2 has x := 3; y := 4; whereas BB3 has z := x + y.
  • Assume we are tracking all registers simultaneously.
  • At the end of BB1 and BB2, we have values v1={(x,4),(y,3)} and v2={(x,3),(y,4)} respectively.
  • One way is to first meet the values at the beginning of BB3, so that v3=v1^v2={} and then apply BB3's transfer function f to obtain out3=f(v3)={}.
  • Another way is to first apply the transfer function of BB3, so that v4=f(v1)={(x,3),(y,4),(z,7)} and v5=f(v2)={(x,4),(y,3),(z,7)}, and then meet to obtain out4=v4^v5={(z,7)}.
  • The meet-at-the-end procedure is guaranteed to produce a better (or equal) solution, due to the monotonicity property described above, f(x^y) ≤ f(x)^f(y)
  • However, the iterative fixed point procedure will meet first in this case.

For some DFA frameworks, it is true that f(x^y) = f(x)^f(y) for all x,y \in V and f \in F. Can you think of some examples?

Example: reaching definitions: f(x) = Gen \union (x - Kill), ^ = \union

• Definition 1: Let x1 ≤ x2 (x1 is a superset of x2); f(x1): Gen \Union (x1 - Kill); f(x2): Gen \Union (x2 - Kill)
• Clearly, f(x1) ≤ f(x2) (because f(x1) is a superset of f(x2))

• Definition 2:
  • f(x1^x2) = Gen \union ((x1 \union x2) - Kill)
  • f(x1)^f(x2) = (Gen \union (x1 - Kill)) \Union (Gen \Union (x2 - Kill))
  • (x1 \union x2) - Kill = (x1 - Kill) \union (x2 - Kill)
  • hence monotone; actually distributive, because f(x1^x2)=f(x1)^f(x2)
  • In fact, every GEN/KILL based framework is distributive.

Also liveness. In fact, even for constant propagation, if I use GEN/KILL based transfer functions, my framework becomes distributive, as: f(v1) = (v1-KILL)\cup GEN and f(v2) = (v2-KILL)\cup GEN, and so f(v1)^f(v2) = f(v1) \cap f(v2) = ((v1-KILL)\cup GEN) \cap ((v2-KILL)\cup GEN) = ((v1 \cap v2) - KILL) \cup GEN which is the same as f(v1^v2). For a distributive framework, it does not matter if we meet earlier or later. Notice it is not necessary that a distributive framework is more precise than a monotone framework for the same problem, e.g., the GEN/KILL based framework for constant propagation is actually less precise, yet distributive.

Distributivity: A framework (F, V, ^) is distributive if and only if:

• f(x^y) = f(x)^f(y)

Distributivity implies monotonicity, but not vice-versa.

Properties of Iterative Algorithm

• Given:
  • ^ and monotone data flow framework
  • finite descending chain
  • THEN converges!
• Initialization of interior points to \Top.
  • yields Maximum Fixed Point (MFP) solution of equations. This is because, we move down by the smallest possible amount at each step (and yet we have not found an FP solution), and so we could not have skipped over another FP solution.

Behaviour of iterative algorithm (intuitively): For each IN/OUT of an interior program point:

• It's value cannot go up (new value < old value) during algorithm.
• Start with \Top (largest value)
• Proof by induction:
  • Apply first transfer function / meet operator ≤ old value (\Top)
  • Inputs to meet changes (get smaller), reapply
    • since input gets smaller, new output ≤ old output
  • Inputs to transfer function changes (get smaller), reapply
    • because of monotonicity of transfer function: since input gets smaller, new output ≤ old output
• Values do not come down unless some constraints drive them down (ensures "maximum")
• Algorithm iterates until equations are satisfied.
• Therefore, finds the largest solution that satisfies the equations.

What does the solution mean?

• Let f1, .., fm: \in F, fi is the transfer function for node i
• For a path p, fp = fn.f(n-1)...(f1), if p is a path through nodes n1,..,nk
• For an empty path p, fp = identity function
• For each node n: ^fp (boundary value) for all possibly executed paths (potentially infinite) p reaching n.
• example: if (sqr(y) ≥ 0) { x = 0; } else { x = 1; }. Here, the ideal solution is that x = 0 at the end of this program.
• However, determining all possibly executed paths is undecidable.

Meet over paths MOP solution:

• Err in the conservative direction
• Meet over paths MOP (over all paths, not just executed paths):
  • Assume every edge is traversed
  • For each node n: MOP(n) = ^ f(p) for all paths p reaching n
• Compare MOP with IDEAL
  • MOP includes more paths than IDEAL
  • MOP = IDEAL ^ Result(unexecuted paths)
  • MOP ≤ IDEAL
  • MOP is a "smaller" solution, more conservative, safe
• Data flow solution ≤ MOP ≤ IDEAL
  • because we don't just meet at the end, we meet all the time.
  • as close to MOP from below as possible.

What is the difference between MOP and MFP of data flow equations? Consider two paths F1.F3 and F2.F3. MOP = F3F1(x) ^ F3F2(x). MFP (through iterative algo) = F3(F1(x) ^ F2(x)). Therefore

• any FP ≤ MFP ≤ MOP ≤ IDEAL
• FP, MFP, MOP are safe
• If framework is distributive, FP ≤ MFP = MOP ≤ IDEAL

What should be the order of relaxing the values across CFG edges? If we examine edges in random order, we are likely to encounter nodes where no change has happened. This is tackled through Kildall's worklist algorithm. Every time something changes at a PC p, the nodes neighbouring (successor nods in case of forward DFA, predecessor nodes in case of backward DFA) that PC get added to the worklist. At every step, the fixed point algorithm picks a node from the worklist, and relaxes the value at that node (by considering the constraints at all predecessor/successor nodes); if nothing changed at that node, that node is simply removed from the worklist; if something changed at that node, the neighboring nodes are added to the worklist. This algorithm continues until the worklist becomes empty (i.e., nothing can potentially change). The invariant of the algorithm is that any nodes that can potentially change values are always in the worklist (nodes outside the worklist can never change values). At initialization time, the worklist is initialized with all nodes that can potentially cause some value to change (e.g., only the entry node for constant propagation). In some analyses, it is possible for the worklist to be initialized with all the CFG nodes.

However: given a worklist, should we have a preferred order in which to choose nodes from the worklist? Consider an example where we have "A->B->C" and "A->C". Let's say we have both "B" and "C" in the worklist. For a forward DFA, we should prefer picking B first. This is because B can reach C, but not vice-versa. Such reachability relationships require a topological sort order (for forward DFA), wherever a topological reachability order exists, e.g., it does not exist in the presence of cycles, in which case those nodes may be ordered arbitrarily. One convenient way of generating a topological sort order is the reverse postorder, which involves performing a depth-first search on the graph and numbering the nodes based on the order in which they are last visited. For a backward DFA, the postorder works best for picking a node from the worklist.