Constant Propagation and Folding

Programmers write constants without noticing. A configuration flag set to 1, a loop that starts at 0, an array whose width is #define'd to 8 — the source is full of values that never actually change at run time. Constant propagation is the analysis that discovers, for each variable at each program point, whether it is guaranteed to hold a single known constant; constant folding is the transformation that then evaluates any now-fully-constant expression at compile time. Together they turn x = 3; y = x * 8 + 1; into y = 25; before the program ever runs — and, crucially, they expose more constants downstream, so the two feed each other in a cascade.

The analysis rides on the def–use structure exposed by reaching definitions: to know the value of x where it is used, you follow the definitions that reach that use. If exactly one definition reaches and it assigns a constant, the value is that constant. If two definitions reach with different constants, the value is unknowable — and capturing that "unknowable" precisely is what makes constant propagation a beautiful little exercise in lattice theory.

The constant-propagation lattice

Each variable, at each point, is assigned one of three kinds of value, drawn from a small lattice with three levels:

Element	Reads as	Meaning
\top (top)	"undefined"	no definition has been seen yet — optimistically, it could still be any single constant
c (a constant)	"the value c"	every definition reaching here assigns the same constant c (e.g. 7, -3)
\bot (bottom)	"NAC" — Not A Constant	the variable can hold different values on different paths; give up on it

The order is \top \sqsupseteq c \sqsupseteq \bot: top is the most optimistic ("might be constant"), bottom the most conservative ("definitely varies"), and the individual constants sit in an antichain in the middle — no constant is above or below another. Notice the picture: there is one \top, then an infinite fan of constants \dots, -1, 0, 1, 2, \dots, then one \bot. The lattice is technically infinitely wide, but its height is only 3 per variable: any single variable can drop at most twice — \top \to c \to \bot — and that finite height is exactly what guarantees the iterative analysis terminates.

The meet rule — where two paths collide

At a control-flow merge, a variable's value is the meet (\wedge) of its values on the incoming edges. Three rules, applied component-wise per variable, define it completely:

\top \wedge v = v, \qquad \bot \wedge v = \bot, \qquad c_1 \wedge c_2 = \begin{cases} c_1 & \text{if } c_1 = c_2,\\[2pt] \bot & \text{if } c_1 \neq c_2. \end{cases}

Read them in plain words. Meeting with \top ("no information yet") leaves the other value untouched — top is the identity. Meeting with \bot ("already varies") stays \bot — bottom is absorbing. And meeting two constants agrees only if they are literally the same constant; two different constants meet to \bot (NAC), because a variable that is 2 on one path and 3 on another is, at their join, simply not a constant.

The transfer function inside a block then just evaluates expressions in this three-valued arithmetic: c_1 + c_2 folds to the constant sum; anything combined with \bot yields \bot; anything with a \top operand stays \top (with the usual short-circuit exceptions, e.g. 0 \times \bot = 0).

Folding, in code

Once the lattice value of every variable is known, folding is a straight walk over the statements, replacing any expression whose operands are all constant with its computed value. The engine below propagates a three-valued environment through a straight-line block and folds as it goes.

// Constant-propagation lattice value: TOP (undefined), a number, or NAC (bottom). type CP = "TOP" | "NAC" | number; // meet of two lattice values (used at merges). function meet(a: CP, b: CP): CP { if (a === "TOP") return b; if (b === "TOP") return a; if (a === "NAC" || b === "NAC") return "NAC"; return a === b ? a : "NAC"; // two DIFFERENT constants -> NAC } // evaluate a op b in three-valued arithmetic. function apply(op: string, a: CP, b: CP): CP { if (a === "NAC" || b === "NAC") return "NAC"; if (a === "TOP" || b === "TOP") return "TOP"; switch (op) { case "+": return a + b; case "-": return a - b; case "*": return a * b; default: return "NAC"; } } type Stmt = { dst: string; a: string | number; op?: string; b?: string | number }; const env = new Map<string, CP>(); const val = (t: string | number): CP => typeof t === "number" ? t : (env.get(t) ?? "TOP"); // A straight-line block. x is a genuine constant; input n is NAC (unknown). env.set("n", "NAC"); const block: Stmt[] = [ { dst: "x", a: 3 }, // x = 3 { dst: "y", a: "x", op: "*", b: 8 }, // y = x * 8 -> 24 { dst: "z", a: "y", op: "+", b: 1 }, // z = y + 1 -> 25 { dst: "w", a: "z", op: "+", b: "n" }, // w = z + n -> NAC (n unknown) ]; for (const s of block) { const result: CP = s.op ? apply(s.op, val(s.a), val(s.b!)) : val(s.a); env.set(s.dst, result); const rhs = s.op ? `${s.a} ${s.op} ${s.b}` : `${s.a}`; const folded = typeof result === "number" ? `${s.dst} = ${result} (folded)` : `${s.dst} = ${rhs} [${result}]`; console.log(folded); }

x, y and z fold to 3, 24, 25; w stays symbolic because it depends on the unknown input n. The cascade is the whole point: folding x is what let y fold, which is what let z fold.

Sparse conditional constant propagation

The classic algorithm has a blind spot: it evaluates every branch, even ones that a constant condition proves can never run. Sparse Conditional Constant Propagation (SCCP, Wegman & Zadeck) fixes this by tracking two things at once — the lattice value of each variable and the reachability of each CFG edge — and letting them reinforce each other:

a variable's value is met only over edges currently marked reachable — so a definition on a dead branch never pollutes the value with a spurious \bot;
when a branch condition folds to a constant, only the taken edge is marked reachable — the other successor may become unreachable and its whole subgraph drops out;
the two worklists (SSA def–use edges and flow edges) run to a joint fixed point, discovering more constants and more dead code than either analysis could alone.

Because SCCP starts every variable at \top and every edge as unreachable (optimistic on both axes), it is strictly more powerful than doing constant propagation and dead-code elimination in separate passes: if (false) x = ...; never even lowers x off \top, so a constant that a pessimistic pass would have surrendered survives.

The subtlety is loops and merges. Consider i = 0; before a loop whose body does i = i + 1;. At the loop header, i's value is the meet of the entry (0) and the back-edge (i+1). On the first optimistic pass the back-edge carries \top, so the header holds 0; the body then computes 1, feeds it back, and 0 \wedge 1 = \bot. The header correctly settles on \bot — i is not a compile-time constant, exactly as intuition demands. The lattice's finite height is what stops this bouncing: each variable can only fall \top \to c \to \bot, so the loop's iteration must stop.

First trap: at a merge, 2 \wedge 3 is not some average or the latest value — it is \bot (NAC). A variable that is a different constant on two paths is simply not a constant at their join. Second, subtler trap: constant propagation is monotone but not distributive, which means the iterative solver can be strictly more conservative than the ideal meet-over-all-paths answer. The textbook witness: path A does a=2; b=3;, path B does a=3; b=2;, then both merge and compute c = a + b;. On each individual path c = 5, so the meet-over-all-paths (MOP) solution is c = 5, a constant. But the iterative analysis meets first — a \to \bot, b \to \bot — and only then computes c = \bot + \bot = \bot. So the iterative (MFP) result says NAC where MOP found 5. The analysis is safe (never claims a false constant) but imprecise: \mathrm{MFP} \sqsubseteq \mathrm{MOP}, with the gap opening precisely because + does not distribute over \wedge in this lattice.