The Dataflow Analysis Framework

Global optimizations need facts — "is this definition still in force here?", "has this expression already been computed on every path to here?", "will this variable ever be read again?". Every one of these questions has the same shape: attach a piece of information to each point in the flow graph, say how each basic block transforms that information, say how information from several incoming paths combines, and then solve the whole tangle of mutually-dependent equations by iterating to a fixed point. That single recipe is the dataflow analysis framework, and once you see it, a dozen separate-looking analyses become one algorithm with four knobs.

The framework is due to Kildall, and its monotone/lattice-theoretic foundations to Kam and Ullman. Its beauty is that you never argue about the solver again: you specify the four knobs, and the same round-robin loop computes the answer for reaching definitions, live variables, available expressions, constant propagation and more.

The four knobs

A dataflow problem is completely specified by four choices:

A domain (lattice) of values — what fact lives at each program point. Usually a set (of definitions, of expressions, of variables), ordered by \subseteq, with a top element \top (the identity of the meet) as the safe starting guess for interior points.
A transfer function f_B per block, describing how the block changes the fact. The overwhelmingly common form is gen/kill: f_B(X) = \text{gen}_B \cup (X - \text{kill}_B) — the block generates some new facts and destroys (kills) some old ones.
A meet operator \wedge — either union \cup or intersection \cap — that combines the facts arriving from several neighbours into one.
A direction — forward (facts flow along edges, from predecessors) or backward (facts flow against edges, from successors).

The dataflow equations

With the knobs chosen, the analysis is two equations per block, coupled across the graph. For a forward problem:

\text{IN}[B] \;=\; \bigwedge_{P \,\in\, \text{pred}(B)} \text{OUT}[P], \qquad \text{OUT}[B] \;=\; f_B\big(\text{IN}[B]\big).

For a backward problem, the roles of IN/OUT and predecessor/successor swap:

\text{OUT}[B] \;=\; \bigwedge_{S \,\in\, \text{succ}(B)} \text{IN}[S], \qquad \text{IN}[B] \;=\; f_B\big(\text{OUT}[B]\big).

With the gen/kill transfer expanded, the forward pair reads:

\text{OUT}[B] \;=\; \text{gen}_B \,\cup\, \big(\text{IN}[B] - \text{kill}_B\big).

There is one special block. In a forward problem the graph's ENTRY node has no predecessors, so its IN is set to a fixed boundary value (often \varnothing). In a backward problem the boundary is EXIT's OUT. Get that boundary right and the rest follows.

The lattice, and why iteration terminates

The domain is a lattice: the meet of any two facts is well-defined, and there is a top element \top. Picture the powerset of two definitions \{d_1, d_2\} as a Hasse diagram — every set sits above the sets it contains:

Iteration works because the transfer and meet functions are monotone (they never undo progress) and the lattice has finite height. Each block's estimate can only move in one direction along the lattice as we iterate; since there are finitely many steps to the top or bottom, the estimates must stop changing — the fixed point. The round-robin solver below is just "recompute every block's equation until nothing changes".

the value domain is a lattice of finite height;
every transfer function f_B and the meet \wedge are monotone;
therefore round-robin iteration reaches a unique maximum fixed point in a finite number of passes, independent of the visiting order.

The four canonical analyses

Almost every classical bit-vector analysis is one cell of a 2×2 grid — direction crossed with meet:

	Meet = union (∪) — "may"	Meet = intersection (∩) — "must"
Forward	Reaching definitions — which defs may reach here	Available expressions — which exprs are computed on all paths
Backward	Live variables — which vars may be used later	Very busy (anticipated) expressions — which exprs are used on all later paths

The two union ("may") analyses ask "is there some path…?" and start each interior point at \varnothing. The two intersection ("must") analyses ask "on every path…?" and start each interior point at the full universal set U (the top of the meet). This single grid organises most of Chapter 9.

A generic round-robin solver

Here is the whole framework as one function. Facts are sets of numbers; you pass in the CFG, the gen/kill sets, the meet, the direction and the boundary — and it iterates every block's equation until a whole pass changes nothing. Below we instantiate it as a forward-union analysis over a tiny three-block loop.

type Set = number[]; // a fact = a sorted list of ids const union = (a: Set, b: Set): Set => [...new Set([...a, ...b])].sort((x, y) => x - y); const inter = (a: Set, b: Set): Set => a.filter((x) => b.includes(x)); const minus = (a: Set, k: Set): Set => a.filter((x) => !k.includes(x)); const eq = (a: Set, b: Set): boolean => a.length === b.length && a.every((x, i) => x === b[i]); interface Block { succ: number[]; pred: number[]; gen: Set; kill: Set; } // Generic solver. forward=true uses pred+IN/OUT; meet combines neighbours. function solve(blocks: Block[], forward: boolean, meet: (a: Set, b: Set) => Set, boundary: Set) { const IN: Set[] = blocks.map(() => []); const OUT: Set[] = blocks.map(() => []); const order = forward ? blocks.map((_, i) => i) : blocks.map((_, i) => i).reverse(); let round = 0, changed = true; while (changed) { changed = false; round++; for (const i of order) { const B = blocks[i]; if (forward) { // Meet over predecessors; ENTRY (no preds) takes the boundary value. // [] is the identity for union; for an intersection problem start from the universal set instead. let inB: Set = B.pred.length ? [] : boundary.slice(); for (const p of B.pred) inB = meet(inB, OUT[p]); IN[i] = inB; const newOut = union(B.gen, minus(inB, B.kill)); // gen ∪ (IN − kill) if (!eq(newOut, OUT[i])) { OUT[i] = newOut; changed = true; } } } } return { IN, OUT, round }; } // Three blocks: B0 -> B1 -> B2 -> B1 (a loop). Each defines one definition id. const blocks: Block[] = [ { succ: [1], pred: [], gen: [1], kill: [] }, // B0: d1 { succ: [2], pred: [0, 2], gen: [2], kill: [] }, // B1: d2 { succ: [1], pred: [1], gen: [3], kill: [1] }, // B2: d3, kills d1 ]; const { IN, OUT, round } = solve(blocks, true, union, []); console.log(`converged in ${round} passes`); blocks.forEach((_, i) => console.log(`B${i}: IN={${IN[i].join(",")}} OUT={${OUT[i].join(",")}}`));

Swap union for inter and set the boundary to the universal set and the very same loop computes an available-expressions-style "must" analysis instead. That interchangeability is the whole point of a framework.

The equations can have many solutions — any consistent assignment of IN/OUT sets that satisfies them is technically a fixed point. We want the most precise safe one. Starting every interior point at the top element \top and iterating downward with monotone functions lands on the maximum fixed point: the tightest set of facts that is still consistent with every path. Start too low (an unsafe guess) and you might converge to something that claims more than the program guarantees — a wrong answer that an optimizer would act on. The lattice direction and the initial value are what pin you to the safe, maximally-precise solution rather than merely a solution.

The framework is only as correct as its four knobs. Three classic mistakes: (1) wrong initial value. Initialise a "must" (intersection) analysis to \varnothing instead of the universal set U and the very first meet wipes everything out — you converge instantly to a useless empty answer. The interior initial value must be the meet's identity (\top): U for \cap, \varnothing for \cup. (2) wrong boundary. ENTRY (forward) or EXIT (backward) carries the problem's boundary condition, not the interior default. (3) mismatched direction and meet. A backward problem solved with forward equations gives nonsense. Live variables is backward-union; run it forward, or with intersection, and every downstream optimization built on it is unsound. Fix the four knobs first; only then trust the solver.