Data Flow Analysis

On this page

Data flow analysis establishes facts at program points, such as where a particular assignment may reach, whether a value is used later, or whether an expression has been computed on all paths. It compresses execution paths into computable abstract information and propagates it across the Control Flow Graph (CFG).

Results should be conservative relative to their use: proofs for code elimination cannot miss potential behaviors, while analyses reporting possible errors can tolerate some false positives. Conservative does not mean arbitrary guessing; it means explicitly defining the inclusion relationship between abstract results and actual execution.

Understanding may and must from branch merging

Control flow merging: first decide whether to preserve 'may' or 'must' Branch condition Left path: x = 1 Right path: x = 2 Merge: x may be 1 or 2

If asked which definition x may come from, merge the candidates from both paths; if asked whether expression a+b is must-computed, both paths must provide that fact. For classic set-based analysis, the former typically uses union, and the latter uses intersection.

However, may/must does not require all abstract domains to simply use set union and intersection. Lattice partial orders, top/bottom elements, and join/meet operators also vary by convention; define meanings first, then write formulas.

A unified framework requires five definitions

ItemWhat must be specified
Abstract domainWhat facts are stored at a program point
Propagation directionFrom predecessors forward, or successors backward
Merge operatorHow information from multiple paths is combined
Transfer functionHow a basic block transforms information
Boundary and initial valuesHow entry, exit, and other nodes start

Gen/Kill is a convenient form for many bit-vector analyses, not the unique form for all transfer functions. Even must analysis using intersection merge does not mean changing gen ∪ ... inside the transfer function to intersection.

Reaching Definitions: Forward may Analysis

Definition d reaches point p if there exists a path from d to p with no redefinition of the same variable in between. Assign independent IDs to each assignment rather than just recording variable names.

IN[B] = ∪ OUT[P], where P iterates over predecessors of B.

OUT[B] = GEN[B] ∪ (IN[B] − KILL[B]).

GEN contains definitions that survive to the block's exit; KILL contains other definitions of the same variable overwritten by assignments in this block. If a block sequentially executes d1: x=1; d2: x=2, d1 is not in the exit GEN, but d2 is.

Entry usually models definitions of parameters or external initial values; if the teaching model starts with an empty set, it should state that these are outside the analysis scope. In SSA, scalar uses directly associate with a unique static definition, but aliasing writes to memory still require separate analysis.

Live Variables: Backward may Analysis

A value is live at point p if there exists a subsequent path that uses the value before redefining it. Since the question looks to the future, propagation is backward from successors.

OUT[B] = ∪ IN[S], where S iterates over successors of B.

IN[B] = USE[B] ∪ (OUT[B] − DEF[B]).

USE is the set of variables used in the block before their first definition; DEF is the set of variables defined in the block, not requiring that the definition was never used before.

For example, in block x=x+1; y=x; return y, USE={x}, DEF={x,y}. When exit OUT=∅, entry IN={x}. It is perfectly reasonable for x to exist in both USE and DEF: the old x entering the block is needed for the first instruction, and a new x is produced within the block.

Loops cause live information to propagate across back edges. The live range of a value is the set of program points on relevant CFG paths, not simply connecting the definition line to the last use line in source code.

Available Expressions: Forward must Analysis

Expression e is available at p if every relevant path entering p has computed e, and its operands have not been modified since. In a pure scalar model:

IN[B] = ∩ OUT[P].

OUT[B] = GEN[B] ∪ (IN[B] − KILL[B]).

Note that x=x+y does not make x+y available at the exit based on the new x: the right-hand side calculation uses the old x, while the assignment changes x. When constructing GEN, consider subsequent assignments in the block and the definition of the statement itself.

Entry is usually empty; other reachable blocks can start from the universal set of expressions and shrink downwards. Unreachable blocks and nodes with no predecessors need explicit handling; do not arbitrarily take the intersection of empty sets and propagate false facts.

Worklist: Only recompute affected neighbors

Using forward analysis as an example, initialize boundaries and block states, enqueue blocks to be processed; pop B, re-merge predecessor outputs and apply the transfer function; if OUT changes, enqueue successors. For backward analysis, notify predecessors when IN changes.

On a lattice of finite height, monotonic iteration with correct initial values terminates. Merely having a maximum element does not imply finite height; interval domains of infinite height may require widening. The number of rounds is influenced by the CFG, loops, and domain, with no fixed guarantee of three to five rounds. Clang Data Flow Analysis Introduction

Reaching Definitions in Loops: First Pass at Header Has No Complete Answers

Analyze only two definitions of variable x: entry E executes d0: x=0, loop body B executes d1: x=x+1. Loop header H can enter B or go to exit X; B then returns to H. Conditions and other variables are not in the definition set of this model.

On the first pass from E to H, only d0 is known. Scanning B reveals d1; sending it along the back edge to H allows H to know that x may also come from d1 of the previous iteration. Here, d1 is the identity of a static assignment statement, not generating infinite definition IDs for each dynamic loop execution.

Back edges force loop headers to re-receive facts E: d0, x = 0 H: Loop condition X: Use x B: d1, x = x + 1 Enter Back edge H entry: initially {d0}, after propagating back edge {d0, d1}; not necessarily executed in all loops.

Below is the worklist implementation. State uses the inclusion order of definition sets, starting all blocks from an empty set; entry has no predecessors, so d0 is generated by GEN. All nodes are reachable, so unreachable inputs are not handled separately here.

from collections import deque

succ = {"E": ["H"], "H": ["B", "X"], "B": ["H"], "X": []}
pred = {b: [p for p in succ if b in succ[p]] for b in succ}
gen = {"E": {"d0"}, "H": set(), "B": {"d1"}, "X": set()}
kill = {"E": {"d1"}, "H": set(), "B": {"d0"}, "X": set()}


def solve(order):
    out = {b: set() for b in succ}
    work = deque(order)
    queued = set(order)
    history = []
    while work:
        b = work.popleft()
        queued.remove(b)
        incoming = set().union(*(out[p] for p in pred[b]))
        new = gen[b] | (incoming - kill[b])
        if new != out[b]:
            out[b] = new
            history.append((b, tuple(sorted(new))))
            for nxt in succ[b]:
                if nxt not in queued:
                    work.append(nxt)
                    queued.add(nxt)
    return out, history


expected = {"E": {"d0"}, "H": {"d0", "d1"}, "B": {"d1"}, "X": {"d0", "d1"}}
out, history = solve(["E", "H", "B", "X"])
assert out == expected
assert [v for b, v in history if b == "H"] == [("d0",), ("d0", "d1")]
assert solve(["X", "B", "H", "E"])[0] == expected
# Check not only against expected but also that each block satisfies the original equation.
for b in succ:
    incoming = set().union(*(out[p] for p in pred[b]))
    assert out[b] == gen[b] | (incoming - kill[b])
NodeFinal INFinal OUTExplanation
E∅{d0}Establish initial value
H{d0,d1}{d0,d1}Initial entry and back-edge merge
B{d0,d1}{d1}Current assignment overwrites previous x
X{d0,d1}{d0,d1}Loop may execute zero or more times

Worklist order changes the intermediate process, but with the same finite, monotonic framework and boundary conditions, the final solution is identical. If traversing the CFG only once, H might never see the back edge; stopping if any node doesn't change might also miss new information from other nodes in the queue.

When do facts on back edges propagate back to the exit?

The buttons below are not prescribed course steps, but real analysis tasks in the pending set. You can process the exit first, letting it temporarily receive an empty set; when entry or back edges subsequently produce new facts, the exit will re-queue via successors. One invariance only indicates that this specific calculation added no new information; the global stop condition is an empty queue. d1 in the model remains a static assignment identity.

Preparing the visual
When do facts on back edges propagate back to the exit?

Processing a block with no change does not mean global termination. Only when all pending blocks are done has d1 from the back edge propagated to H and X; different processing orders yield the same final solution.

Fixed Points and Path-by-Path Solving: Where Precision is Lost

MOP transforms along each CFG path first, then merges; iterative equations merge paths midway and continue transforming. Under conditions where transfer functions are distributive over merge, they are consistent; otherwise, premature merging may lose correlated information.

For example, two paths yield (x=1,y=2) and (x=2,y=1) respectively, followed by calculating z=x+y. Path-by-path calculation both yield 3; non-relational constant propagation merging first marks x and y as non-constant, potentially failing to derive z=3. Abstract domains preserving variable relationships can improve precision at higher cost.

MOP also typically traverses syntactic paths in the CFG, which may include paths where conditions cannot be simultaneously satisfied, so it cannot be directly called a perfect solution for actual program semantics. The magnitude direction of MFP vs MOP depends on the lattice order used; do not state an inequality without specifying the lattice-order convention.

After losing correlation, do not treat all combinations as real paths

Writing the previous two paths directly as sets, the precise path state is {(1,2),(2,1)}; after separately retaining possible values for x and y, both become {1,2}. Subsequently taking the Cartesian product introduces extra (1,1) and (2,2), yielding sums 2 and 4 that do not actually exist.

paths = {(1, 2), (2, 1)}
xs, ys = {x for x, y in paths}, {y for x, y in paths}
precise = {x + y for x, y in paths}
nonrelational = {x + y for x in xs for y in ys}
assert precise == {3}
assert nonrelational == {2, 3, 4}
assert precise <= nonrelational

The non-relational result still contains the real result, so it is conservative to say "z may belong to {2,3,4}", but one cannot prove z is always 3. This precision loss comes from the abstract state not saving pairing relationships; adding more worklist rounds cannot recover discarded information. To improve, change the abstract domain, delay merging, or utilize path conditions, rather than just repeatedly running the same equation.

What is lost by remembering x and y separately?

Drawing specific paths as points in a 2D coordinate system accurately locates "correlation loss". Projecting separately onto x and y axes and then combining, the two real points may expand to four; the extra points are not newly discovered execution paths, but additional states allowed by the abstraction. Modifying the second path allows observing when extra combinations do not occur. Repeating the same iteration cannot recover lost pairing relationships.

Preparing the visual
What is lost by remembering x and y separately?

Independent sets only remember what x appeared and what y appeared, not how they paired. The gold grid represents states additionally allowed by abstraction, potentially making a previously constant x+y unprovable.

SSA and Sparse Analysis

SSA makes scalar def-use explicit, allowing many facts to propagate along relevant values, reducing work on irrelevant CFG edges. However, φ inputs depend on predecessor edges, loops may still require fixed points, and memory still has aliasing and side effects. SSA is not a guarantee that "all analyses degenerate to a single pass over the dominance tree."

Quick Reference

AnalysisDirectionTypical MergeUse Case
Reaching DefinitionsForwardUnionNon-SSA def-use, possible sources
Live VariablesBackwardUnionRegister allocation, value lifetime
Available ExpressionsForwardIntersectionRedundant computation elimination

Related chapters: Classic Optimizations, Register Allocation, SSA.

References

Keywords: dataflow, CFG, may, must, gen, kill, liveness, reaching definitions, available expressions, fixed point, MOP