Lesson 17.8 — Phase ordering, combined analyses and equality saturation¶

Techniques: the phase-ordering problem (fixed pipelines, repeated passes, canonicalization); combined analyses (Click–Cooper 1995; NewGVN and GCC's RPO VN as production instances); equality saturation (Tate–Stepp–Tatlock–Lerner 2009) with rebuilding (egg, Willsey et al. 2021); acyclic e-graphs with elaboration (Cranelift's aegraph mid-end) · Pebble implements: nothing in the compiler; the ★ e-graph lab (labs/ch17-egraph) implements equality saturation · Prerequisites: Lesson 17.1 (SCCP), Lesson 17.5 (optimistic value numbering), e-graphs as an IR (Lesson 8.5), fixed points (Lesson 14.1) · Time: 5–7 hours

Lesson 17.1 proved x = 1 in the running example and Lesson 17.5 proved i.0 ≡ j.0. This lesson asks what happens when each pass needs the other's facts, and it compares three answers to that question. The first is to order and repeat the passes. The second is to solve all the analyses as one fixed point. The third is to stop choosing: record every rewrite in an e-graph and pick the best program at the end.

1. Problem and motivation¶

A pass maps programs to programs. An optimizer is a sequence of passes, and the result depends on the order. One pass can enable another: SCCP folds a branch and GVN then sees fewer paths. It can also disable one: an early strength reduction turns x * 4 into x << 2, and a later rule written for mul no longer matches. Choosing and repeating passes well is the phase-ordering problem. It has no general solution, because even for a fixed finite set of passes the best order depends on the input program.

Phase ordering¶

Production compilers answer with a hand-tuned fixed pipeline that runs cheap cleanup passes many times. LLVM 23's default<O2> runs simplifycfg 8 times, instcombine after almost every major pass, and early-cse and jump-threading twice each [LLVM-Pipelines]. GCC 15 runs CCP 5 times and DCE 11 times [GCC-TreeSSAPasses]. The running example shows the limits. No order or repetition of sccp, gvn and instcombine proves run returns 1, because LLVM's GVN is pessimistic about loop phis (Lesson 17.4). LLVM's -O2 does get ret i32 1, but only after a loop pass, IndVarSimplify (Ch 18), rewrites the exit values of i and j into the same expression, smax(n, 0) (§7 box).

Combined analyses¶

Click and Cooper's answer is to combine analyses rather than passes [CC95]. Constant propagation, unreachable-code detection and value numbering become one monotone system, solved optimistically from "every block unreachable, every value congruent to every other, every value constant". They prove that the combined fixed point is at least as good as any interleaving of the separate analyses (Theorem 17.8.6), and sometimes strictly better (Proposition 17.8.7). NewGVN (Lesson 17.5) is LLVM's instance of this design, and GCC's RPO value numbering, used by its FRE and PRE passes, is another [GCC-SCCVN].

Equality saturation¶

Tate, Stepp, Tatlock and Lerner go further [TSTL09]. Rewrites are applied non-destructively: x * 4 → x << 2 adds x << 2 to the class of x * 4 and keeps both. An e-graph (Lesson 8.5, Definition 17.8.2) stores all the equivalent programs compactly. When no rule adds anything the e-graph is saturated, and a cost model extracts the best program. At saturation the order of rewrites no longer matters (Theorem 17.8.9). The price is size: saturation may not terminate, so production users bound it with node, iteration and time limits. The egg library made the approach fast with rebuilding, which restores the congruence invariant once per batch of merges instead of after every merge [WNW+21].

Acyclic e-graphs¶

Cranelift, the code generator of Wasmtime, uses a restricted form in its mid-end, called an aegraph (acyclic e-graph) [CL-EgraphRFC, CL-Egraph]. Pure instructions leave the CFG and live in an e-graph. Rewrite rules written in ISLE [CL-Arith] fire eagerly, once, when a node is created. Classes are bounded to 5 e-nodes, and the graph stays acyclic because a node can only refer to values that already exist. An elaboration pass then walks the dominator tree and puts one chosen node per needed class back into the CFG. It does GVN (a scoped hash map), LICM (placing each value in the shallowest loop level where its operands are available) and rematerialization along the way. The aegraph gives up saturation in exchange for compile time close to that of a single pass.

2. Definitions and algorithms¶

Definition 17.8.1 (Combined analysis)

Let \(A_1\) and \(A_2\) be two optimistic analyses of the same function, with lattices \(L_1\) and \(L_2\) oriented as in Ch 14 (⊥ = no evidence yet, the most optimistic assumption; ⊤ = overdefined). Suppose each analysis can use the other's facts, so its transfer function is \(F_1 : L_1 \times L_2 \to L_1\) (respectively \(F_2 : L_1 \times L_2 \to L_2\)), and both are monotone in both arguments. Facts lower in a lattice are more precise. - The combined analysis is the least fixed point \((x_1^\ast, x_2^\ast)\) of \(F(x_1, x_2) = (F_1(x_1, x_2), F_2(x_1, x_2))\) on \(L_1 \times L_2\) (ordered componentwise). - A separate run of \(A_1\) given \(y_2 \in L_2\) computes \(\mathrm{lfp}\, F_1(\cdot, y_2)\), and symmetrically for \(A_2\). - A phase ordering is a finite sequence of separate runs, each given the latest result of the other analysis, and ⊤ (no information) for an analysis that has not run yet.

For SCCP combined with value numbering, \(L_1\) holds a lattice value per SSA value and an executable flag per edge, and \(L_2\) is the lattice of partitions of the values, with ⊥ = one class and ⊤ = all singletons (Lesson 17.5). \(F_1\) may fold sub a, b to 0 when \(a \equiv b\) in \(x_2\). \(F_2\) ignores phi operands on edges that \(x_1\) marks non-executable, so a phi with one executable operand is a copy of that operand, and it merges values that \(x_1\) proves equal to the same constant.

Definition 17.8.2 (E-graph, represented terms, congruence invariant)

As in Definition 8.5.7: an e-graph over a ranked alphabet \(\Sigma\) is a union-find structure over e-class ids with a hashcons \(H\) from canonical e-nodes \(f(c_1, \dots, c_k)\) (each \(c_i\) a root of the union-find) to e-class ids. A class \(c\) represents a term \(f(t_1, \dots, t_k)\) if \(c\) contains an e-node \(f(c_1, \dots, c_k)\) and each \(t_i\) is represented by \(\mathrm{find}(c_i)\). We write \(\mathrm{terms}(c)\) for the set of terms \(c\) represents. The e-graph satisfies the congruence invariant if two e-nodes with the same symbol and the same canonical children are in the same class, which makes \(H\) a function on canonical e-nodes. Congruence closure, the relation this invariant maintains, is Nelson and Oppen's [NO80]. It is the same congruence that the AWZ partition (Definition 17.5.1) computes, from the other side: AWZ splits an optimistic partition until it is congruent, and an e-graph merges classes until they are congruent.

Definition 17.8.3 (Rewrite rule, match, soundness, saturation)

A rewrite rule \(\ell \to r\) is a pair of patterns: terms over \(\Sigma\) plus variables \(?a, ?b, \dots\), where \(\ell\) is not a variable and every variable of \(r\) occurs in \(\ell\). A match of \(\ell\) in class \(c\) is a substitution \(\sigma\) from variables to classes such that \(c\) represents \(\ell\) with each variable \(?v\) standing for any term of \(\sigma(?v)\). E-matching finds all matches. A rule is sound for a semantics \([\![\cdot]\!]\) if \([\![\ell\theta]\!] = [\![r\theta]\!]\) for every substitution \(\theta\) of terms for variables. An e-graph is saturated under a rule set if, for every match \((\ell \to r, c, \sigma)\), the class \(c\) already represents \(r\sigma\).

Algorithm 17.8.4 (Equality saturation in rounds, with rebuilding)

Input: a term \(t\); rules \(R\); limits on rounds and e-nodes; a cost \(\mathrm{cost}(f(t_1..t_k)) = 1 + \sum \mathrm{cost}(t_i)\) (term size).
Output: a least-size term represented by \(t\)'s class; the counts of classes, e-nodes and rounds; the stop reason (saturated, iteration-limit, node-limit).
Precondition: the rules are sound for the intended semantics (Definition 17.8.3).
Postcondition: the output term has the same semantics as \(t\) (Theorem 17.8.8). If the stop reason is saturated, every term reachable from \(t\) by any sequence of rule applications is represented in the root class, so the output is no larger than any of them (Theorem 17.8.9).
Invariant: at the start of every round the congruence invariant holds and every term represented by a class has the same semantics as every other term of that class.

function Saturate(t, R, limits):
    root ← AddTerm(t); Rebuild()
    for round = 1, 2, …:
        changed ← false
        M ← [ (ℓ → r, c, σ) for every rule and every match σ of ℓ in class c ]   # read phase
        for (ℓ → r, c, σ) in M:                                                # write phase
            d ← AddTerm(rσ)           # sets changed when it creates an e-node
            Merge(c, d)               # sets changed when c and d were different classes
        Rebuild()                     # re-canonicalize; merge congruent e-nodes
        if not changed:          return Extract(root), "saturated"
        if #e-nodes > limit:     return Extract(root), "node-limit"
        if round = round limit:  return Extract(root), "iteration-limit"
function Rebuild():
    repeat:
        for each e-node n in H: n' ← n with children replaced by find(children)
            if n' already maps to a different class: Merge(both classes)      # congruence
        H ← the re-canonicalized table
    until no Merge happened
function Extract(root):                           # Bellman–Ford on classes
    best[c] ← ∞ for every class
    repeat: for each class c, each e-node n = f(c1..ck) in c:
                best[c] ← min(best[c], 1 + Σ best[find(ci)])
    until nothing improves
    return the term built from the e-nodes achieving best, from root down

The lab's Rebuild re-canonicalizes the whole table, which is simple and correct. egg re-canonicalizes only the parents of the classes merged in this round, using parent lists, which reaches the same fixed point with less work [WNW+21, §3].

Algorithm 17.8.5 (Aegraph optimization and elaboration, after Cranelift)

Input: an SSA function in CLIF (block parameters instead of phis); rewrite rules with a subsume flag; the dominator tree and loop nest.
Output: an equivalent function in which every pure value was rewritten eagerly, deduplicated, and placed at its earliest legal loop level.
Precondition: the rules are sound; pure instructions have no side effects and cannot trap (loads, stores, calls and trapping divisions stay in the skeleton).
Postcondition: the skeleton instructions run in the original order, and every value they use is computed before its use by an equivalent pure expression.
Invariant: the e-graph is acyclic (every e-node refers only to values created before it), and no class has more than 5 e-nodes (ECLASS_ENODE_LIMIT).

function OptimizeAndElaborate(F):
    gvn ← scoped hash map (Type, InstructionData) → Value          # scoped by the domtree
    for each block B in domtree preorder:                           # remove_pure_and_optimize
        for each instruction i in B:
            rewrite i's arguments to their latest optimized values
            if i is pure:
                remove i from the layout; v ← gvn-lookup or insert(i)
                for each rule rhs produced by simplify(v) (at most 5, depth ≤ 5):
                    if the rule subsumes: v ← rhs          # replace; drop the other forms
                    else: v ← union(v, rhs)             # a new union node; class ≤ 5 nodes
                record optimized(i's result) ← v
            else: keep i in the skeleton (idempotent ones are also GVN'd)
    best[v] ← min cost over the union tree of v (cost per opcode, plus a loop-depth factor)
    for each block B in domtree preorder:                           # elaborate
        for each skeleton instruction i in B, for each argument v:
            if v has not been computed in a dominating scope: emit best[v]'s node at the
                highest loop level where its arguments are available (recursively elaborating them)

3. Worked example¶

Phase ordering¶

The running example after mem2reg, pipeline by pipeline (the §7 box prints each ret):

pipeline	what each pass proves	result
`sccp,gvn,instcombine`	SCCP: `x.0 = x.1 = 1`, `if.then` unreachable. GVN: nothing about `i.0` and `j.0`, whose phis have different operands `add` and `add2`	`(i.0 − j.0) << 2 \\| 1`
`gvn,sccp,instcombine`	the same facts in the other order	same
repeat either twice	the second round starts from a program in which nothing new is foldable	same
`sccp,newgvn,instcombine`	NewGVN's optimistic phis prove `i.0 ≡ j.0` (Lesson 17.5)	`ret i32 1`
`default<O2>`	IndVarSimplify rewrites the exit values of `i.0` and `j.0` to `smax(n, 0)`, then GVN sees two identical `mul`s	`ret i32 1`

Combined analyses¶

The function mutual (§7 box) needs both facts at once. After mem2reg:

for.cond: j.0 = phi [0, entry], [add3, for.inc];  i.0 = phi [0, entry], [i.1, for.inc]
          k.0 = phi [0, entry], [inc, for.inc];    cmp = lt k.0, n;  cbr cmp, for.body, for.end
for.body: cmp1 = ne i.0, j.0;  cbr cmp1, if.then, if.else
if.then:  add  = add i.0, 2;   br if.end
if.else:  add2 = add i.0, 1;   br if.end
if.end:   i.1 = phi [add, if.then], [add2, if.else];  add3 = add j.0, 1;  br for.inc
for.inc:  inc = add k.0, 1;    br for.cond
for.end:  sub = sub i.0, j.0;  ret sub

analysis	assumption it starts from	what it concludes
SCCP given no congruences (⊤₂)	`i.0`, `j.0` overdefined after one trip	`cmp1` overdefined: both `if.then` and `if.else` executable; no constants
AWZ given every edge executable (⊤₁)	`i.1 = phi(add, add2)` and `add3 = add j.0, 1` have different opcodes	`i.0 ≢ j.0`; the partition is all singletons except `0`s
SCCP again, given AWZ's partition	nothing new: `i.0 ≢ j.0`	the same; the phase ordering is stuck
combined (Definition 17.8.1)	⊥: `if.then` unreachable, `i.0 ≡ j.0`	`cmp1 = ne i.0, i.0 = false`, so `if.then` stays unreachable. Then `i.1 = add2 = add i.0, 1 ≡ add j.0, 1 = add3`, so the phis stay congruent. The optimistic guess is a fixed point, and `sub = 0`

Proposition 17.8.7 turns this table into a proof. The least fixed point is coarser still: k.0 = phi [0, entry], [inc, for.inc] with inc = add k.0, 1 has the same shape, so k.0 joins i.0 and inc joins add2. NewGVN finds exactly that (the §7 box prints the result).

Equality saturation¶

The lab's running.rules states the running example's facts as rules: sccp-x: x → 1 (what SCCP proves), gvn-j: j → i (what value numbering proves), sub-self: (- ?a ?a) → 0, add-zero-l: (+ 0 ?a) → ?a and comm-add: (+ ?a ?b) → (+ ?b ?a). The term is (+ (- (* i 4) (* j 4)) x), i.e. t − u + x. Algorithm 17.8.4 runs as follows; the counts are egg's (§7 box), and ch17-egraph reports the same final numbers.

round	e-nodes, classes at the start	matches (read phase)	effect after the write phase and `Rebuild`
1	8, 8	`sccp-x` on `{x}`; `gvn-j` on `{j}`; `comm-add` on the root	`x ≡ 1`; `j ≡ i`, so `Rebuild` finds `(* j 4)` congruent to `(* i 4)` and merges them; the root gains `(+ x sub)`
2	11, 6	`sub-self` on `(- e2 e2)` (both children are now one class)	`sub ≡ 0`
3	12, 6	`add-zero-l` on `(+ sub x)`, since `sub` now represents `0`	root ≡ `{x, 1}`
4	12, 5	no match adds anything	saturated

Final e-graph (5 classes, 10 e-nodes):

e0 = { i, j }            e1 = { 4 }            e2 = { (* e0 e1) }
e5 = { (- e2 e2), 0 }    e6 = { (+ e5 e6), (+ e6 e5), 1, x }   <- root

The root class is cyclic: it contains (+ e5 e6), whose child is e6 itself, so it represents x, 1, 0 + x, 0 + (0 + 1) and infinitely many other terms. Extraction by size picks a leaf of cost 1: egg returns x and the lab's solution returns 1, which is the same class. Unlike the pass pipelines above, it did not matter which rule fired first. The rules only have to be present.

Acyclic e-graphs¶

Cranelift on a CLIF version of run's epilogue. v8 recomputes v0 * 4, and v9 = v8 − v3 is therefore 0:

step	node	eager rewrite (ISLE rule)	class / value
1	`v3 = imul v0, v2` (`v2 = 4`)	`imul x (power of two)` → `ishl x 2` (`arithmetic.isle`)	`v3 ≡ ishl v0, 2`
2	`v4 = imul v1, v2`	same rule	`v4 ≡ ishl v1, 2`
3	`v8 = imul v0, v2`	GVN map hit: the same `(Type, InstructionData)` as `v3`	`v8 = v3`
4	`v9 = isub v8, v3` = `isub v3, v3`	`isub x x` → `0`, subsuming	`v9 = iconst 0`
5	`v10 = iadd v7, v9` = `iadd v7, 0`	`x + 0` → `x`, subsuming	`v10 = v7`
6	elaborate `return v10`	pick the cheaper node per class: `ishl` over `imul`	`v12 = ishl v0, v11` … `return v7`

In sum (§7 box), the loop-invariant imul_imm v1, 8 becomes ishl v1, 3. Elaboration places it in block0, outside the loop, because its only operand is available there. That is LICM, done by the placement step and not by a separate pass.

4. Invariants and correctness¶

Theorem 17.8.6 (A combined analysis is at least as precise as every phase ordering)

Under Definition 17.8.1, let \((x_1^\ast, x_2^\ast)\) be the combined least fixed point, and let \((y_1, y_2)\) be the latest results of any phase ordering (⊤ for an analysis that has not run). Then \(x_1^\ast \sqsubseteq y_1\) and \(x_2^\ast \sqsubseteq y_2\).

Proof

Two facts about least fixed points of monotone maps on complete lattices (Knaster–Tarski: \(\mathrm{lfp}\, G\) is the least \(z\) with \(G(z) \sqsubseteq z\)) are used.

(a) lfp is monotone in the map. If \(G \sqsubseteq H\) pointwise, then \(G(\mathrm{lfp}\, H) \sqsubseteq H(\mathrm{lfp}\, H) = \mathrm{lfp}\, H\), so \(\mathrm{lfp}\, H\) is a pre-fixed point of \(G\) and \(\mathrm{lfp}\, G \sqsubseteq \mathrm{lfp}\, H\).

(b) Each component of the combined fixed point is a separate fixed point: \(x_1^\ast = \mathrm{lfp}\, F_1(\cdot, x_2^\ast)\). Let \(a = \mathrm{lfp}\, F_1(\cdot, x_2^\ast)\). Since \(x_1^\ast\) is a fixed point of \(F_1(\cdot, x_2^\ast)\), \(a \sqsubseteq x_1^\ast\). Conversely, \(F(a, x_2^\ast) = (a, F_2(a, x_2^\ast)) \sqsubseteq (a, F_2(x_1^\ast, x_2^\ast)) = (a, x_2^\ast)\) by monotonicity of \(F_2\) in its first argument. So \((a, x_2^\ast)\) is a pre-fixed point of \(F\), and \((x_1^\ast, x_2^\ast) \sqsubseteq (a, x_2^\ast)\), which gives \(x_1^\ast \sqsubseteq a\). The argument for \(x_2^\ast\) is symmetric.

Now induct on the length of the phase ordering, with the claim \(x_1^\ast \sqsubseteq y_1\) and \(x_2^\ast \sqsubseteq y_2\). Initially \(y_1 = \top\) and \(y_2 = \top\). Suppose the next run is \(A_1\), producing \(y_1' = \mathrm{lfp}\, F_1(\cdot, y_2)\). By the induction hypothesis \(x_2^\ast \sqsubseteq y_2\), so \(F_1(\cdot, x_2^\ast) \sqsubseteq F_1(\cdot, y_2)\) pointwise (monotonicity in the second argument). By (b) and (a), \(x_1^\ast = \mathrm{lfp}\, F_1(\cdot, x_2^\ast) \sqsubseteq \mathrm{lfp}\, F_1(\cdot, y_2) = y_1'\). The case of \(A_2\) is symmetric. The same argument applies to any number of analyses, and it is the content of Click and Cooper's theorem [CC95, §3].

Proposition 17.8.7 (The inclusion can be strict)

For SCCP (with the rule "sub a, b and ne a, b fold when \(a \equiv b\)") combined with AWZ value numbering (ignoring phi operands on non-executable edges, so that a phi with one executable operand is congruent to that operand), the function mutual of §3 has a combined fixed point that proves ret 0 and marks if.then unreachable. Every phase ordering of the two separate analyses proves neither.

Proof

Combined. Take the candidate \(x\) in which if.then and its out-edge are non-executable, every other edge is executable, {i.0, j.0} and {add2, add3, i.1} are congruence classes, cmp1 is the constant false, sub is the constant 0, add (in the unreachable if.then) stays ⊥, and every other value is overdefined and alone in its class. Check that \(F(x) = x\). cmp1 = ne i.0, j.0 with i.0 ≡ j.0 folds to false, so only if.else is executable from for.body. i.1's only executable operand is add2 = add i.0, 1, and add3 = add j.0, 1 is congruent to it because i.0 ≡ j.0. So i.1 ≡ add3. Then the loop phis i.0 and j.0 have congruent operands on both executable edges (0 and 0, i.1 and add3), so they stay congruent. Finally sub = sub i.0, j.0 folds to 0. The least fixed point lies below every fixed point, so it proves at least these facts, and in particular ret 0.

Separate. The first analysis to run is given ⊤ for the other. If SCCP runs first, it knows no congruences, so after i.0 and j.0 take their loop values it cannot fold cmp1. Both branches become executable, and add = add i.0, 2 and add2 = add i.0, 1 make i.1, and hence i.0, overdefined. No constant beyond the literals is found. If AWZ runs first, every edge counts as executable, so i.1 is a phi and add3 is an add. They differ in opcode, so AWZ splits them apart, and then i.0 and j.0 split because their back-edge operands differ. Each later run is given exactly these results again, so it reproduces them. The phase ordering is stuck at its first results, and they prove neither ret 0 nor the unreachability of if.then.

Theorem 17.8.8 (Equality saturation is sound)

If every rule is sound, then at every point of Algorithm 17.8.4 all terms represented by one class have the same semantics. In particular the extracted term has the semantics of \(t\).

Proof

Define \(c \approx d\) when the two classes are merged. It is enough to show that every merge joins two classes whose represented terms all have equal semantics, because then, by induction over merges, equality of semantics is preserved as classes grow. (Merging two classes \(C\) and \(D\) in which all terms are equal within \(C\) and within \(D\), and some term of \(C\) equals some term of \(D\), keeps all terms equal, because semantic equality is transitive.)

Rule merges. Suppose \((\ell \to r, c, \sigma)\) was matched in the read phase. By Definition 17.8.3, \(c\) represents \(\ell\theta\) for every choice \(\theta(?v) \in \mathrm{terms}(\sigma(?v))\), and \(\mathrm{AddTerm}(r\sigma)\) represents \(r\theta\) for the same choices. Soundness gives \([\![\ell\theta]\!] = [\![r\theta]\!]\). The e-graph has grown since the read phase, but classes only grow, so the match remains valid.

Congruence merges. Rebuild merges the classes of \(f(c_1, \dots, c_k)\) and \(f(c'_1, \dots, c'_k)\) when \(\mathrm{find}(c_i) = \mathrm{find}(c'_i)\) for all \(i\). By the induction hypothesis the terms of \(c_i\) and \(c'_i\) are all equal, and semantics is compositional (a term's value depends only on its symbol and the values of its children), so the two represented families of terms are equal.

Extraction returns a term built from e-nodes of the root class and, recursively, of its children's classes, so it is represented by the root class. The root class represents \(t\) from the start, and all its terms are equal.

Theorem 17.8.9 (Saturation subsumes every rewrite order)

Suppose Algorithm 17.8.4 stops with saturated, and \(t \to^\ast s\) by any finite sequence of rule applications, each rewriting one subterm \(\ell\theta\) into \(r\theta\). Then \(s\) is represented by the root class. Consequently the extracted term is no larger than any term that any order of destructive rewriting can reach.

Proof

Induction on the length of the sequence. The root class represents \(t\) itself. For the step, suppose the root class represents \(s\), and \(s'\) replaces the subterm \(u = s|_p = \ell\theta\) at position \(p\) by \(r\theta\).

Every subterm is represented. Walking from the root along \(p\), each e-node that represents a term has children representing its subterms. So some class \(d\) represents \(u\), and for each variable \(?v\) of \(\ell\) the subterm \(\theta(?v)\) is represented by some class \(\sigma(?v)\).

Saturation closes \(d\) under the rule. Then \((\ell \to r, d, \sigma)\) is a match. At saturation, \(d\) already represents \(r\sigma\), and therefore \(r\theta\), since \(\theta(?v) \in \mathrm{terms}(\sigma(?v))\).

Replacement inside a class. By Definition 17.8.2, whether a class represents \(f(t_1, \dots, t_k)\) depends on the children's classes, not on which of their terms is chosen. Replacing \(u\) by \(r\theta\), which is represented by the same class \(d\), therefore keeps every enclosing term on the path represented by the same class, up to the root. So the root represents \(s'\).

Extraction returns a least-size term among those the root class represents (the Bellman–Ford argument of Theorem 8.5.12 (c)), and every reachable \(s\) is among them.

What breaks it. Theorem 17.8.9 needs saturation. When a limit stops the run, the e-graph holds a subset of the reachable terms, and the order in which rules fire matters again, which is the reason egg ships a backoff scheduler. Theorem 17.8.8 needs sound rules for the target semantics. div-canc in the lab's div.rules (from the egg paper, and Lesson 8.5) is sound for mathematical integers with a non-zero divisor. It is wrong for LLVM's udiv on wrapping 64-bit integers: \((2^{63} \cdot 2) / 2 = 0 \ne 2^{63}\). Poison flags need care too: (+ ?a 0) → ?a is fine, but reassociating add nsw can create an overflow that the original did not have, so a rule that reassociates must drop the nsw flag. Cranelift keeps an e-graph acyclic and bounded so that elaboration terminates and costs are well defined. The price is that it loses Theorem 17.8.9: a rewrite that would be enabled only by a later union is never tried.

5. Complexity¶

\(I\) instructions (or e-nodes of the input term), \(\lvert R \rvert\) rules, \(N\) e-nodes at the end, \(k\) rounds, \(h\) the height of the combined lattice per value.

Technique	Time (worst)	Time (typical)	Space	Justification
Fixed pipeline of \(p\) passes	\(\sum\) of the passes' costs	dominated by a few analyses (alias analysis, LVI)	per pass	each pass is a separate traversal. The pipeline is fixed, so its cost is predictable
Combined analysis (Click, NewGVN)	\(O(I \cdot h)\) value changes, each re-evaluating its users	a few iterations per SCC	\(O(I)\)	every value moves up a finite lattice at most \(h\) times (Theorem 17.8.6's lattice)
Equality saturation (Alg. 17.8.4)	unbounded; with limits, \(O(k \cdot \lvert R \rvert \cdot N^{w})\) for patterns of width \(w\) (naive e-matching)	node and iteration limits reached on associative-commutative rules	\(O(N)\)	the e-graph grows each round; e-matching is NP-hard in general, and backtracking over class members is exponential in pattern depth. Lesson 8.5's family has \(2^k - 1\) classes
Aegraph (Alg. 17.8.5)	\(O(I \cdot 5 \cdot 5)\) rule applications (`MATCHES_LIMIT` = 5 results per call, `REWRITE_LIMIT` = depth 5) + elaboration \(O(I \cdot d)\) for dominator depth \(d\)	near one pass	\(O(I)\) with ≤ 5 e-nodes per class	eager rewriting at creation, bounded classes, one domtree walk

Pathological family. For equality saturation, take the lab's ring.rules (commutativity, associativity, distributivity) and the product \((a + b)(c + d)\). The e-graph grows every round. The lab's test suite records 19 classes and 46 e-nodes after 4 rounds, and a 25-node limit stops it after round 3 with 30 e-nodes. Nothing saturates, because distribute and factor keep producing new shapes. For combined analyses the worst case is the lattice height times the number of values. NewGVN counts how often it processes each value, and builds with assertions stop once one value is processed 100 times (updateProcessedCount), a guard against non-convergence rather than a limit on precision.

Pass pipelines tuned by search or learning. Iterative compilation and learned pass orders (for example, reinforcement learning over LLVM passes) search the phase-ordering space per program; trade-off: compile time many times that of -O2, unpredictable.
Canonicalization as a partial cure. InstCombine and MLIR's canonicalizer rewrite towards one normal form, so later patterns only need to match that form; trade-off: some optimizations need a non-canonical form, so a later pass has to undo it (e.g. x << 2 back to x * 4 for address modes).
Combining more analyses. Click's thesis adds ranges and type information [Cli95t]. Predicated value numbering (Lesson 17.5) adds branch predicates; trade-off: a taller lattice and more complex transfer functions.
E-class analyses. egg attaches a lattice value to each class (constants, intervals, free variables) and merges them on union, so constant folding happens inside saturation [WNW+21, §4]; trade-off: every analysis must be a semilattice with a sound merge.
Rule scheduling. egg's BackoffScheduler bans rules that match too often for a number of rounds; trade-off: faster, and the result depends on the schedule.
Extraction beyond size. A cost that is not a sum over a tree (for example, DAG cost with sharing) makes extraction NP-hard. It is solved with ILP or heuristics; trade-off: optimal code vs extraction time.
Relational e-matching and Datalog (egglog) express e-matching as a database join, which is worst-case optimal; trade-off: a different implementation model.
Verified rules — checking each rewrite rule with an SMT solver (Alive2 for LLVM peepholes, Ch 19) fits declarative rule sets well; trade-off: proof effort per rule.

7. In real compilers¶

Phase ordering¶

LLVM: buildFunctionSimplificationPipeline and buildModuleOptimizationPipeline in llvm/lib/Passes/PassBuilderPipelines.cpp hard-code the order. opt -passes='default<O2>' -print-pipeline-passes prints it [LLVM-Pipelines]. GCC: gcc/passes.def lists NEXT_PASS entries, and -fdump-passes prints them [GCC-TreeSSAPasses].

Four pipelines on the running example

Reproduce (clang 23.1.2, opt 23.1.2):

cat > run.c <<'EOF'
int run(int n) {
  int x = 1, i = 0, j = 0;
  while (i < n) {
    if (x != 1)
      x = 2;
    i = i + 1;
    j = j + 1;
  }
  int t = i * 4, u = j * 4;
  return t - u + x;
}
EOF
clang-23 -O0 -Xclang -disable-O0-optnone -fno-discard-value-names -S -emit-llvm run.c -o run.O0.ll
opt -passes=mem2reg -S run.O0.ll -o run.ll
for p in 'sccp,gvn,instcombine' 'gvn,sccp,instcombine' \
         'sccp,gvn,instcombine,sccp,gvn,instcombine' 'sccp,newgvn,instcombine'; do
  printf '%-45s ' "$p:"; opt -passes="$p" -S run.ll | grep -E '^  ret '
done
opt -passes='default<O2>' -print-changed=quiet -disable-output run.ll 2>&1 |
  grep -E '^\*\*\* IR Dump|^  ret ' | grep -B1 'ret i32 1' | head -2

Output:

sccp,gvn,instcombine:                           ret i32 %add4
gvn,sccp,instcombine:                           ret i32 %add4
sccp,gvn,instcombine,sccp,gvn,instcombine:      ret i32 %add4
sccp,newgvn,instcombine:                        ret i32 1
*** IR Dump After GVNPass on run ***
  ret i32 1

What to notice: repeating the classic passes gains nothing, because %add4 is still ((i.0 − j.0) << 2) | 1. Replacing gvn by the optimistic newgvn is enough. In default<O2>, GVN is the first pass to produce ret i32 1, but only because IndVarSimplify ran just before it. With -passes='loop(indvars),gvn', both muls become mul nsw i32 %smax, 4, where %smax = smax(n, 0), and GVN folds their difference. The fix came from a different chapter's pass, which is the phase-ordering problem in miniature.

Combined analyses¶

LLVM: NewGVN::iterateTouchedInstructions in llvm/lib/Transforms/Scalar/NewGVN.cpp iterates values and reachable edges to one fixed point [LLVM-NewGVN]. GCC: do_rpo_vn in gcc/tree-ssa-sccvn.cc is an RPO value numbering that tracks executable edges and iterates loop SCCs optimistically, and FRE runs it [GCC-SCCVN].

mutual: only the combined analyses prove ret 0

Reproduce (clang 23.1.2, opt 23.1.2, gcc 13.3.0):

cat > mutual.c <<'EOF'
int mutual(int n) {
  int i = 0, j = 0;
  for (int k = 0; k < n; k++) {
    if (i != j)       // never taken -- but only if i == j is already known
      i = i + 2;
    else
      i = i + 1;
    j = j + 1;
  }
  return i - j;       // always 0
}
EOF
clang-23 -O0 -Xclang -disable-O0-optnone -fno-discard-value-names -S -emit-llvm mutual.c -o mutual.O0.ll
opt -passes=mem2reg -S mutual.O0.ll -o mutual.ll
for p in 'sccp,gvn,instcombine' 'sccp,gvn,instcombine,sccp,gvn,instcombine,sccp,gvn,instcombine' \
         'gvn,sccp,instcombine,gvn,sccp,instcombine' 'newgvn'; do
  printf '%s\n    ' "$p:"; opt -passes="$p" -S mutual.ll | grep -E '^  ret '
done
clang-23 -O2 -S -emit-llvm mutual.c -o - | grep -cE '^ +%[0-9]+ = '   # instructions left at -O2
gcc -O2 -S -o - mutual.c | sed -n '/^mutual:/,/ret$/p' | grep -vE '^\.|\.cfi|endbr'

Output:

sccp,gvn,instcombine:
      ret i32 %sub
sccp,gvn,instcombine,sccp,gvn,instcombine,sccp,gvn,instcombine:
      ret i32 %sub
gvn,sccp,instcombine,gvn,sccp,instcombine:
      ret i32 %sub
newgvn:
      ret i32 0
41
mutual:
    xorl    %eax, %eax
    ret

What to notice: Proposition 17.8.7 on real compilers. Any number of rounds of SCCP and GVN leaves %sub. NewGVN alone proves ret i32 0, marks the branch br i1 false and even merges k into the same class as i and j. Clang's -O2 (which uses GVN, not NewGVN) unrolls the loop by 4 and keeps 41 instructions. GCC's -O2, whose FRE uses the optimistic RPO value numbering, returns 0.

Equality saturation¶

egg: Runner::run, EGraph::rebuild and Extractor in src/run.rs, src/egraph.rs and src/extract.rs (egg 0.11.0) [WNW+21]. The ★ lab's saturate follows the same round structure (read phase, write phase, rebuild), and its counts agree with egg's on the lab inputs.

egg saturates the running example

Reproduce (rustc 1.94.1, cargo 1.94.1, egg 0.11.0 from crates.io):

cargo new --quiet eggrun && cd eggrun
echo 'egg = "=0.11.0"' >> Cargo.toml
cat > src/main.rs <<'EOF'
use egg::{rewrite as rw, *};

fn main() {
    let rules: &[Rewrite<SymbolLang, ()>] = &[
        rw!("sccp-x"; "x" => "1"),              // what SCCP proves
        rw!("gvn-j"; "j" => "i"),               // what value numbering proves
        rw!("sub-self"; "(- ?a ?a)" => "0"),
        rw!("add-zero-l"; "(+ 0 ?a)" => "?a"),
        rw!("comm-add"; "(+ ?a ?b)" => "(+ ?b ?a)"),
    ];
    let start: RecExpr<SymbolLang> = "(+ (- (* i 4) (* j 4)) x)".parse().unwrap();
    let runner = Runner::default().with_expr(&start).run(rules);
    for (k, it) in runner.iterations.iter().enumerate() {
        let mut applied: Vec<_> = it.applied.iter().map(|(r, n)| format!("{r}×{n}")).collect();
        applied.sort();
        println!("iteration {}: {} nodes, {} classes before; applied {}", k + 1,
                 it.egraph_nodes, it.egraph_classes, applied.join(" "));
    }
    let (cost, best) = Extractor::new(&runner.egraph, AstSize).find_best(runner.roots[0]);
    println!("stop: {:?}; {} classes, {} nodes", runner.stop_reason.unwrap(),
             runner.egraph.number_of_classes(), runner.egraph.total_number_of_nodes());
    println!("best: {best} (cost {cost})");
}
EOF
cargo run --quiet --release

Output:

iteration 1: 8 nodes, 8 classes before; applied comm-add×1 gvn-j×1 sccp-x×1
iteration 2: 11 nodes, 6 classes before; applied sub-self×1
iteration 3: 12 nodes, 6 classes before; applied add-zero-l×1
iteration 4: 12 nodes, 5 classes before; applied 
stop: Saturated; 5 classes, 10 nodes
best: x (cost 1)

What to notice: the §3 table. Round 1's gvn-j makes the two muls congruent, and Rebuild merges them. That is value numbering done by congruence closure. Round 4 applies nothing and stops with Saturated. The per-iteration counts are egg's hashcons size (EGraph::total_size). The final count is the number of e-nodes stored in classes (total_number_of_nodes), the 10 listed in §3. The lab reproduces the result: ch17-egraph --rules labs/ch17-egraph/inputs/running.rules '(+ (- (* i 4) (* j 4)) x)' prints best: 1, classes: 5, nodes: 10, iterations: 4, stop: saturated.

Acyclic e-graphs¶

Cranelift: EgraphPass::run in cranelift/codegen/src/egraph.rs calls remove_pure_and_optimize (hashconsing into a ScopedHashMap GVN table and applying ISLE simplify rules eagerly) and then elaborate (cranelift/codegen/src/egraph/elaborate.rs, elaborate_block) [CL-Egraph]. The limits are constants in egraph.rs: MATCHES_LIMIT = 5, ECLASS_ENODE_LIMIT = 5, and REWRITE_LIMIT = 5 for the rewrite depth. The rules include (rule (simplify (imul ty x (iconst _ (imm64_power_of_two c)))) (ishl ty x (iconst ty (imm64 c)))) and (rule (simplify (isub (ty_int ty) x x)) (subsume (iconst_u ty 0))) in cranelift/codegen/src/opts/arithmetic.isle [CL-Arith] (all at wasmtime v37.0.2, which ships Cranelift 0.124).

Cranelift's aegraph: rewrite, GVN and LICM in one pass

Reproduce (rustc 1.94.1, cranelift-codegen / cranelift-reader / cranelift-control 0.124.2, target-lexicon 0.13):

cargo new --quiet clifopt && cd clifopt
cat >> Cargo.toml <<'EOF'
cranelift-codegen = "=0.124.2"
cranelift-reader = "=0.124.2"
cranelift-control = "=0.124.2"
target-lexicon = "0.13"
EOF
cat > src/main.rs <<'EOF'
use cranelift_codegen::settings::{self, Configurable};
use cranelift_codegen::{isa, Context};
use std::io::Read;
use std::str::FromStr;

fn main() {
    let mut text = String::new();
    std::io::stdin().read_to_string(&mut text).unwrap();
    let funcs = cranelift_reader::parse_functions(&text).unwrap();
    let mut b = settings::builder();
    b.set("opt_level", "speed").unwrap();
    let flags = settings::Flags::new(b);
    let isa = isa::lookup(target_lexicon::Triple::from_str("x86_64").unwrap())
        .unwrap().finish(flags).unwrap();
    for f in funcs {
        let mut ctx = Context::for_function(f);
        let mut cp = cranelift_control::ControlPlane::default();
        ctx.optimize(&*isa, &mut cp).unwrap();       // runs the egraph pass at opt_level=speed
        print!("{}", ctx.func.display());
    }
}
EOF
cat > run.clif <<'EOF'
function %run(i32, i32) -> i32 {
block0(v0: i32, v1: i32):
    v2 = iconst.i32 4
    v3 = imul v0, v2
    v4 = imul v1, v2
    v5 = isub v3, v4
    v6 = iconst.i32 1
    v7 = iadd v5, v6
    v8 = imul v0, v2
    v9 = isub v8, v3
    v10 = iadd v7, v9
    return v10
}
function %sum(i32, i32) -> i32 {
block0(v0: i32, v1: i32):
    v2 = iconst.i32 0
    jump block1(v2, v2)

block1(v3: i32, v4: i32):
    v5 = imul_imm v1, 8
    v6 = iadd v4, v5
    v7 = iadd_imm v3, 1
    v8 = icmp slt v7, v0
    brif v8, block1(v7, v6), block2

block2:
    return v6
}
EOF
cargo run --quiet --release < run.clif

Output:

function %run(i32, i32) -> i32 fast {
block0(v0: i32, v1: i32):
    v11 = iconst.i32 2
    v12 = ishl v0, v11  ; v11 = 2
    v14 = ishl v1, v11  ; v11 = 2
    v5 = isub v12, v14
    v6 = iconst.i32 1
    v7 = iadd v5, v6  ; v6 = 1
    return v7
}
function %sum(i32, i32) -> i32 fast {
block0(v0: i32, v1: i32):
    v2 = iconst.i32 0
    v9 = iconst.i32 1
    v11 = iconst.i32 3
    v12 = ishl v1, v11  ; v11 = 3
    jump block1(v2, v2)  ; v2 = 0, v2 = 0

block1(v3: i32, v4: i32):
    v14 = iconst.i32 1
    v15 = iadd v3, v14  ; v14 = 1
    v8 = icmp slt v15, v0
    v6 = iadd v4, v12
    brif v8, block1(v15, v6), block2

block2:
    return v6
}

What to notice: the §3 table. imul by 4 became ishl by 2, and the duplicate v8 was GVN'd into v3. v9 = v3 − v3 and v10 = v7 + 0 were subsumed, so return v7. In %sum, imul_imm v1, 8 became ishl v1, 3 and was elaborated into block0, outside the loop. The constant 1 is rematerialized inside the loop (v14) because Cranelift prefers recomputing cheap constants over keeping them live across the loop, which leaves v9 = iconst.i32 1 in block0 unused.

Find where Cranelift does it. In cranelift/codegen/src/egraph.rs, which constant bounds the number of e-nodes in one e-class, and what is its value? (Quiz cl-where-eclass-limit.)

8. Comparison¶

Technique	Power / precision	Speed (asymptotic · practical)	Output / error quality	Implementation effort	Typical use
Phase ordering (fixed pipeline)	Limited by the order: misses facts that need two analyses at once (Proposition 17.8.7)	sum of the passes · predictable	Each pass's output is inspectable (`-print-changed`)	Low per pass, high to tune the pipeline	LLVM `default<O2>`, GCC `passes.def`
Combined analyses	At least every phase ordering of the combined analyses (Theorem 17.8.6), sometimes strictly more	\(O(I \cdot h)\) · comparable to one GVN	One fixed point; hard to debug when it does not converge	High (one transfer function that knows every fact)	LLVM NewGVN, GCC RPO VN / FRE
Equality saturation	Every rewrite order at once, if saturated (Theorem 17.8.9)	unbounded; needs limits · slow on AC rules	Extraction chooses by a cost model; equivalences can be explained (egg's proofs)	Medium (e-graph, e-matching, extraction); rules are declarative	Research, rewrite-heavy domains (tensor graphs, floating-point accuracy with Herbie), superoptimizers
Acyclic e-graphs (aegraph)	Eager single application of each rule; no saturation guarantee	near one pass · production JIT speed	Rules in ISLE, verifiable one by one	Medium–high (elaboration, bounds)	Cranelift's mid-end in Wasmtime

Choose a fixed pipeline when compile time must be predictable and the passes are well understood; spend the effort on canonicalization so that passes agree on forms. Choose a combined analysis when facts are mutually dependent (constants, reachability and congruences in loops); it costs about one GVN. Choose equality saturation when the domain is a term language with many interacting algebraic rules and compile time is secondary. Choose an aegraph when you want declarative rewrite rules and GVN/LICM in one pass under JIT compile-time budgets.

9. Assessment¶

Quiz (./course quiz 17): phase-order-run, phase-order-indvars (tag phase-ordering); combined-precision, combined-mutual (tag combined-analysis); eqsat-running-classes, eqsat-closure (tag equality-saturation); aegraph-licm, cl-where-eclass-limit (tag aegraph).
Drill: none; the ★ e-graph lab is the hands-on exercise, and its tests check the counts of §3.
Flashcards: tags phase-ordering, combined-analysis, equality-saturation, aegraph.
Exercises: ★ lab labs/ch17-egraph/SPEC.md.

References¶

See the chapter references.

Lesson 17.8 — Phase ordering, combined analyses and equality saturation¶

1. Problem and motivation¶

Phase ordering¶

Combined analyses¶

Equality saturation¶

Acyclic e-graphs¶

2. Definitions and algorithms¶

3. Worked example¶

Phase ordering¶

Combined analyses¶

Equality saturation¶

Acyclic e-graphs¶

4. Invariants and correctness¶

5. Complexity¶

6. Variants and refinements¶

7. In real compilers¶

Phase ordering¶

Combined analyses¶

Equality saturation¶

Acyclic e-graphs¶

8. Comparison¶

9. Assessment¶

References¶