Lesson 21.7 — Rewriting-based selection: Cranelift ISLE and e-graphs¶

Techniques: ISLE term rewriting (Cranelift); e-graph-based selection (Denali, equality saturation, Cranelift's aegraph) · Prerequisites: Lesson 21.1 (tiles and munch), Lesson 8.5 (e-graphs as an IR) · Time: 3–5 hours

LLVM describes instructions as patterns and leaves the choice to a matcher. Another view is that lowering is term rewriting: the IR is a term, each lowering rule rewrites a term of the IR into a term of machine instructions, and a strategy decides which rule fires. Cranelift, the code generator of Wasmtime and of rustc's alternative back end, took this view with ISLE (instruction selection/lowering expressions): a small typed rewriting language whose rules compile to Rust matching code. Its AArch64 rules for iadd fold a shifted operand into add x, y, lsl #k and a product into madd, exactly Tessera's shadd and madd tiles, ordered by explicit priorities. Taking the rewriting view to its limit gives the second technique: put all equivalent forms of a program into an e-graph and extract the cheapest. Denali did this to find optimal instruction sequences. Cranelift applies the idea in its mid-end, before ISLE lowering.

1. Problem and motivation¶

The problem is the same: map an IR (here Cranelift IR, CLIF, an SSA IR with block parameters) to machine instructions. Two engineering problems motivated a rewriting language rather than a table generator. First, hand-written lowering code in Rust was long, and its bugs led to real miscompilations and security issues. Second, lowering rules and mid-end optimizations are both "match a shape, produce a shape", so one DSL can serve both [Fal23]. The e-graph line addresses a different weakness shared by every greedy selector in this chapter: rewrites are applied in some order, and a rewrite applied early can prevent a better one later (phase ordering). An e-graph applies all rewrites without committing to any, and chooses only at the end.

ISLE term rewriting¶

ISLE was designed by Chris Fallin and first shipped in Cranelift in 2022. Rules have the form (rule PRIO (lower PATTERN) EXPR). Patterns match CLIF instructions and their operands through extractors, which are programmable views such as "this value is a 12-bit immediate" or "this value is a load that can be sunk". Expressions build machine instructions through constructors. Rules are typed, overlapping rules must be disambiguated by priority, and the ISLE compiler merges all the rules of a term into one decision trie in Rust [ISLE, Fal23]. Crocus later verified a large part of the AArch64 rules against SMT models of both sides, finding real bugs [VPFSB24].

E-graph-based selection¶

An e-graph represents many equivalent terms compactly: equivalence classes of nodes whose children are classes (Definition 21.7.4). Denali (Joshi, Nelson and Randall) built an e-graph of an expression under algebraic and architectural axioms, then asked a SAT solver for the shortest instruction schedule that computes it, a "goal-directed superoptimizer" [JNR02]. Equality saturation [TSTL09] and the egg library [WNW+21] made e-graph rewriting fast and general, and it has been used for selection of vector and DSP instructions (Diospyros [VNLBS21]). Cranelift's aegraph (acyclic e-graph) runs its mid-end rewrites (opts/*.isle) in an e-graph, extracts the cheapest form per value, and re-emits it in the CFG (elaboration) before ISLE lowering [Fal23b].

2. Definitions and algorithms¶

Definition 21.7.1 (Terms, rules, priorities)

Let $\mathcal{T}$ be the set of typed first-order terms over a signature of constructors (CLIF opcodes such as iadd, machine-instruction constructors such as add_shift). A pattern is a term with variables and wildcards, and it matches a term $t$ if some substitution $\theta$ makes it equal to $t$ (extractors extend this: they are partial functions that decompose a term, and they may succeed or fail). A rule is $\rho = (p_\rho, \ell_\rho, e_\rho)$: a priority $p_\rho \in \mathbb{Z}$, a left-hand pattern $\ell_\rho$ (with its if-let guards) and a right-hand expression $e_\rho$. Two rules overlap if some term matches both left-hand sides.

Definition 21.7.2 (ISLE semantics for a term)

For a term $t$ in a rule set $\mathcal{R}$, the applicable rules are $A(t) = \{\rho \in \mathcal{R} \mid \ell_\rho \text{ matches } t\}$. The result of lowering $t$ is $e_\rho\theta$ for a rule $\rho \in A(t)$ of maximum priority. If $A(t)$ is empty, lowering fails (a compiler bug for a total rule set).

Algorithm 21.7.3 (Cranelift lowering with ISLE)

Input: a CLIF function; the target's compiled ISLE rules for the term lower.
Output: machine instructions (VCode) with virtual registers.
Precondition: the rule set is total on the instructions of the function (every instruction has an applicable rule).
Postcondition: every instruction whose value is used, or that has side effects, is lowered exactly once, unless its value was sunk (merged) into a user's instruction (Proposition 21.7.5).
Invariant: blocks and instructions are processed in reverse order. When an instruction is lowered, all its users have been lowered, so the lowering knows whether a user already merged it.

function LowerFunction(F):
    uses ← ComputeUseStates(F)            # Unused / Once / Multiple, transitively
    for each block b in reverse order:
        for each instruction I in b, in reverse order:
            if I has no side effects and its result is unused: continue
            if I was sunk into a user (IsInstSunk(I)): continue
            ApplyISLE("lower", I)         # Definition 21.7.2, via the compiled trie
        lower b's branch with the "lower_branch" rules

function ComputeUseStates(F):
    uses[v] ← Unused / Once / Multiple by counting direct uses
    propagate Multiple: if an instruction's result is Multiple, its operands become
    Multiple too (the instruction could be emitted more than once)  # to a fixed point

An extractor such as sinkable_load succeeds only if the load's result is Once, it lies in the same block and no side effect separates it from the user. When the rule that used it is applied, the load is marked sunk and folded into the user's memory operand.

Definition 21.7.4 (E-graph, e-class, extraction)

An e-graph is a set of e-classes $\mathcal{C}$. Each class is a non-empty set of e-nodes $f(c_1, \dots, c_k)$ with an operator $f$ and child classes $c_i$. A class represents every term $f(t_1, \dots, t_k)$ with $f(c_1, \dots, c_k)$ in the class and each $t_i$ represented by $c_i$. All terms a class represents are equal under the rewrite rules applied so far. With a cost $\mathrm{cost}(f) \ge 0$ per operator, the tree cost of a term is the sum of its operators' costs. Extraction picks, for a class, a represented term. Optimal tree extraction picks one of minimum tree cost.

Algorithm 21.7.5 (Equality saturation with tree-cost extraction)

Input: a term $t$ (or a DAG of terms); rewrite rules $\ell \to r$; costs per operator; an iteration or node limit.
Output: a term equal to $t$ under the rules, of minimum tree cost among the terms the e-graph represents.
Precondition: every rule is sound ($\ell = r$ in the semantics); costs are non-negative.
Postcondition: the extracted term is optimal among the represented terms for tree cost (Theorem 21.7.6). If the e-graph saturated, it is optimal among all terms reachable by the rules.
Invariant: the e-graph is congruence-closed after each rebuild (equal children imply equal parents), and every represented term is equal to $t$.

function EqSat(t, rules, limit):
    E ← e-graph containing t
    repeat until no rule adds anything (saturation) or limit is reached:
        matches ← [ (rule, class, θ) | ℓ matches some term represented by class ]
        for each (ℓ → r, c, θ) in matches: c' ← Add(E, rθ); Union(E, c, c')
        Rebuild(E)                            # restore congruence closure
    return Extract(E, class of t)

function Extract(E, root):
    best[c] ← ∞ for every class c
    repeat until no best[] changes:           # Bellman–Ford over classes
        for each class c, for each e-node n = f(c1..ck) in c:
            cand ← cost(f) + Σ best[ci]
            if cand < best[c]: best[c] ← cand; choice[c] ← n
    return the term built from choice[] starting at root

Theorem 21.7.6 (Tree-cost extraction is optimal; DAG-cost extraction is NP-hard)

(a) With non-negative operator costs, Extract terminates, and for every class $c$, best[c] is the minimum tree cost of a term represented by $c$ (∞ if $c$ represents no finite term). (b) If cost counts each shared subterm once (DAG cost, as when values in registers are reused), finding a minimum-cost represented DAG is NP-hard.

Proof

(a) This is the same argument as Theorem 21.2.7. best only decreases, and each value best[c] is the tree cost of an actual represented term (induction on updates), so $\mathrm{best}[c] \ge$ the minimum. Conversely, let $t^\ast$ be a minimum-cost term of $c$ and use induction on the height of $t^\ast$. Its subterms are minimum-cost terms of the child classes (exchange argument, as in Lemma 21.2.6), so once their best values are final, the e-node at the root of $t^\ast$ offers cand = cost($t^\ast$), and $\mathrm{best}[c]$ drops to it. A minimum-cost term never needs a class twice on one root-to-leaf path: with non-negative costs, the path can be shortcut. So the heights involved are at most $\lvert \mathcal{C} \rvert$, and $\lvert \mathcal{C} \rvert$ rounds suffice. After that no value changes, and the loop stops.

(b) By reduction from DAG-COVER (Theorem 21.4.4), for a chain-rule-acyclic grammar such as $G_{\mathrm{SAT}}$. Given $D$ and $G$, build one class $c_{v,A}$ for every node $v$ and nonterminal $A$. For every rule $r$ that derives $A$ at $v$, put into $c_{v,A}$ an e-node with a fresh operator of cost $c(r)$ whose children are the classes $c_{u,B}$ of $r$'s operands at $v$ (for a chain rule $A \to B$, the single child $c_{v,B}$). Add a root class holding one e-node of cost 0 whose children are the classes $c_{v,S}$ of the roots. A DAG extraction chooses one e-node in each class it reaches and pays each chosen class once, so it is exactly a cover that has one instance per (node, nonterminal) pair it uses, with the same cost. Conversely, a minimum cover never needs two instances for the same pair. So a minimum-cost DAG extraction gives $\mathrm{OPT}(D)$, the construction is polynomial, and DAG extraction is NP-hard.

Proposition 21.7.7 (ISLE's priority-and-overlap discipline makes lowering deterministic)

Suppose the ISLE compiler's check succeeds: no two rules of the same priority may overlap, and no rule is shadowed by a higher-priority rule with fewer constraints. Then for every term $t$ with $A(t) \ne \emptyset$, exactly one rule of maximum priority in $A(t)$ applies. The result of lowering is independent of the order of rules in the source files.

Proof

Let $p^\ast = \max\{p_\rho \mid \rho \in A(t)\}$. If two different rules $\rho, \rho'$ of priority $p^\ast$ were in $A(t)$, the term $t$ would match both, so they overlap. The overlap checker (check_overlaps in cranelift/isle/isle/src/overlap.rs) rejects overlapping rules of equal priority, contradicting the assumption. Its test may_overlap is conservative (it may report overlap that no term realizes, never the reverse), so a rule set that passes has no real overlap either. Hence the rule of maximum priority is unique. Definition 21.7.2 refers only to priorities and matching, not to source order, so the result does not depend on the order. The shadowing check guarantees in addition that every rule can fire on some term.

3. Worked example¶

ISLE term rewriting¶

Lower the CLIF computation of the running example's address, v7 = iadd v2, v6 with v6 = ishl v3, v5 and v5 = iconst 3, on AArch64. The applicable rules for iadd in cranelift/codegen/src/isa/aarch64/lower.isle (the §7 box lists them):

rule (priority)	left-hand side	matches `iadd v2, (ishl v3 (iconst 3))`?	why
`iadd_ishl_right` (7)	`(iadd x (ishl y (iconst k)))` with `lshl_from_imm64 ty k`	yes	$k = 3$ is a valid shift amount
`iadd_imul_right` (7)	`(iadd x (imul y z))`	no	the right operand is `ishl`, not `imul`
`iadd_ishl_left` (6)	`(iadd (ishl x (iconst k)) y)`	no	the left operand is not a shift
`iadd_imm12_right` (4), `iadd_imm12_left` (5)	an operand that is a 12-bit immediate	no	neither operand is a constant
`iadd_extend_right` (0)	`(iadd x (extended_value_from_value y))`	no	no extension
`iadd_base_case` (−1)	`(iadd x y)`	yes	always

The maximum priority among applicable rules is 7, held by iadd_ishl_right alone, as Proposition 21.7.7 guarantees. It rewrites to (add_shift ty x y amt), which becomes add w10, w4, w5, lsl #3. The ishl and the iconst are then unused and never lowered. The two rules at priority 7 share a priority, but they cannot both match one term (ishl versus imul at the same position), so the overlap check accepts them.

E-graph-based selection¶

Take the §7 example f(x, y) = (x * 8 + y) − y in CLIF, and the rule set $\{x \cdot 2^k \to x \ll k,\ (a + b) - b \to a\}$. The second rule is not in Cranelift's rule set in Wasmtime 37, which the output confirms.

iteration	rule applied	e-classes after rebuild (members)
0	—	$c_1 = \{x\}$, $c_2 = \{8\}$, $c_3 = \{c_1 \cdot c_2\}$, $c_4 = \{y\}$, $c_5 = \{c_3 + c_4\}$, $c_6 = \{c_5 - c_4\}$
1	$x \cdot 8 \to x \ll 3$	$c_7 = \{3\}$; $c_3 = \{c_1 \cdot c_2,\ c_1 \ll c_7\}$
1	$(a + b) - b \to a$ (if present)	$c_6 = \{c_5 - c_4,\ c_1 \ll c_7\}$, merged with $c_3$
2	nothing new	saturated

Extraction with costs mul 3, shl 1, add 1, sub 1, constants 0 and variables 0: $\mathrm{best}(c_3) = \min(3, 1) = 1$ via shl. With the second rule, $c_6 = c_3$ and the result is x << 3 (cost 1). Without it, $\mathrm{best}(c_6) = 1 + \mathrm{best}(c_5) = 1 + (1 + 1) = 3$: ((x << 3) + y) − y. Cranelift's output in §7 is the second case: ishl, iadd and isub survive into CLIF, and ISLE then lowers iadd(ishl …) to one lea.

Try it

Write the rule (a + b) − b → a in ISLE syntax, (rule (simplify (isub ty (iadd ty a b) b)) (subsume a)), and find where it would go in cranelift/codegen/src/opts/arithmetic.isle. To practice cost-based choice by hand, ./course drill dp-tiling --difficulty medium is the tree analogue of Extract.

4. Invariants and correctness¶

ISLE term rewriting¶

Proposition 21.7.7 gives determinism. Correctness is per rule: the right-hand side must compute the left-hand side's value for every term the rule accepts, including the guards (a shift amount out of range must not match). ISLE's type system catches type mismatches but not semantic errors. Crocus closes the gap for a subset: it gives SMT semantics to both CLIF and AArch64 terms, and for every rule proves that the right-hand side equals the left for all inputs of the accepted widths. It found real bugs, including a 9.9/10 CVE reproduction [VPFSB24]. Sinking (Algorithm 21.7.3) is correct only if the sunk instruction's value is used once (ValueUseState::Once), lies in the same block, and no side effect intervenes. Otherwise the load would move past a store or be duplicated.

E-graph-based selection¶

Theorem 21.7.6: optimal for tree cost, NP-hard for DAG cost. Every represented term is equal to the input only if every rule is sound: one unsound rule makes the whole class unsound, which is harder to debug than a single wrong rewrite. Saturation may never arrive (associativity plus commutativity generate exponentially many terms), so real systems stop at node or iteration limits, and then "optimal" means "optimal among what was explored".

5. Complexity¶

Variables: $n$ instructions, $R$ rules, $\lvert \mathcal{C} \rvert$ e-classes, $\lvert \mathcal{N} \rvert$ e-nodes.

Technique	Time (worst)	Time (typical)	Space	Justification
ISLE term rewriting	$O(n \cdot \text{trie depth})$ plus use-state propagation $O(n + \text{uses})$	linear	the generated trie (compiled Rust)	one trie walk per lowered instruction
E-graph selection (equality saturation)	exponential in the worst case (no saturation)	bounded by limits; Cranelift's aegraph is designed to be near linear	$O(\lvert \mathcal{N} \rvert)$	matching is per iteration; tree extraction is $O(\lvert \mathcal{C} \rvert \cdot \lvert \mathcal{N} \rvert)$ with Bellman–Ford, near linear in practice

A pathological family for equality saturation. With associativity and commutativity of +, the sum $x_1 + \dots + x_m$ has a number of equivalent parenthesized, permuted forms that grows super-exponentially in $m$ (Catalan numbers times $m!$). The e-graph shares subterms, so it needs one class per non-empty subset of $\{x_1, \dots, x_m\}$, that is $2^m - 1$ classes. Saturation is therefore exponential in $m$, although it never enumerates the forms themselves.

Real-world scale. Cranelift's aegraph avoids this by being acyclic and running each rewrite rule once per new node, without iterating to saturation. Fallin presents these choices (acyclicity, eager single application of rules, no iteration to saturation) as what made an e-graph affordable in Cranelift's compile-time budget [Fal23b].

ISLE term rewriting¶

Explicit priorities vs specificity: ISLE requires priorities where rules overlap, while LLVM's TableGen infers an order from pattern size (Lesson 21.1). ISLE is more explicit and more verbose. TableGen is implicit and surprises you sometimes.
Multi-constructors ((decl multi …)): terms that return all matching results. The mid-end uses them to add every rewrite to the e-graph. This is how ISLE serves both greedy lowering and saturation.
Verification (Crocus [VPFSB24]): machine-checked rule correctness. It costs a semantic model per instruction.
Go's rulegen (src/cmd/compile/internal/ssa/_gen/*.rules): a similar rewrite-rule DSL compiled to Go, applied greedily to a fixed point for lowering and optimization [GO-Rules]. It has no priorities; the first rule in file order wins.

E-graph-based selection¶

Denali [JNR02]: e-graph plus SAT for provably shortest code. It is exact but only practical for short sequences.
Equality saturation with egg [WNW+21]: a general library. Selection for DSP vector instructions (Diospyros [VNLBS21]) extracts with ILP when sharing matters.
Acyclic e-graph with elaboration (Cranelift [Fal23b]): no cycles, rewrites applied eagerly once, extraction by per-class best cost, then re-placement of values in the CFG (elaboration) with scoped GVN and LICM. It is less complete than saturation but fast enough for a JIT.

7. In real compilers¶

ISLE term rewriting¶

The rules are in cranelift/codegen/src/isa/{x64,aarch64,riscv64,s390x}/lower.isle, the lowering driver is Lower::lower_clif_block in cranelift/codegen/src/machinst/lower.rs (reverse order, ValueUseState for sinking), and the ISLE compiler with its overlap checker is in cranelift/isle/isle/src/ (overlap.rs, trie_again.rs, codegen.rs) (Wasmtime v37.0.2) [CL-ISLE-Src].

Cranelift's AArch64 rules for iadd, and what they produce

Reproduce (Wasmtime 37.0.2 release binary; store.wat from Lesson 21.1 §7; needs network access to GitHub for the rules file):

curl -sL https://raw.githubusercontent.com/bytecodealliance/wasmtime/v37.0.2/cranelift/codegen/src/isa/aarch64/lower.isle \
  | sed -n '/^(rule iadd_ishl_right/,/add_shift ty x y amt))/p;/^(rule iadd_imul_right/,/madd ty y z x))/p'
wasmtime compile --target aarch64-unknown-linux-gnu store.wat -o store-a64.cwasm
wasmtime objdump store-a64.cwasm | sed -n '/function\[0\]:/,/^$/p'

Output (complete):

(rule iadd_ishl_right 7 (lower (has_type (fits_in_64 ty)
                       (iadd x (ishl y (iconst k)))))
      (if-let amt (lshl_from_imm64 ty k))
      (add_shift ty x y amt))
(rule iadd_imul_right 7 (lower (has_type (fits_in_64 ty) (iadd x (imul y z))))
      (madd ty y z x))
wasm[0]::function[0]:
            stp     x29, x30, [sp, #-0x10]!
            mov     x29, sp
            ldr     x8, [x2, #0x38]
            add     x7, x8, #0x18
            ldr     x9, [x7, w6, uxtw]
            ╰─╼ trap: MemoryOutOfBounds
            add     w10, w4, w5, lsl #3
            str     x9, [x8, w10, uxtw]
            ╰─╼ trap: MemoryOutOfBounds
            ldp     x29, x30, [sp], #0x10
            ret

What to notice: the two rules are Tessera's r16 shadd and r13 madd written as rewrite rules, with priority 7 over the base case (−1). add w10, w4, w5, lsl #3 is iadd_ishl_right firing on a + (i << 3): the §3 trace. The heap access uses [x8, w10, uxtw], a register-offset address with zero extension (wasm32 addresses are 32-bit), chosen by the load/store address rules.

E-graph-based selection¶

The aegraph pass is EgraphPass in cranelift/codegen/src/egraph.rs, with elaboration in cranelift/codegen/src/egraph/elaborate.rs and cost-based extraction in cranelift/codegen/src/egraph/cost.rs. The rewrite rules are ISLE files under cranelift/codegen/src/opts/, for example (rule (simplify (imul ty x (iconst _ (imm64_power_of_two c)))) (ishl ty x (iconst ty (imm64 c)))) in arithmetic.isle (Wasmtime v37.0.2) [CL-Egraph]. Denali and egg-based selectors are research systems. Denali's code is not publicly maintained.

The aegraph rewrites x * 8, then ISLE lowers the shifted add to lea

Reproduce (Wasmtime 37.0.2 release binary; --emit-clif writes the CLIF after the mid-end optimizations; -O opt-level=0 disables them):

cat > comb.wat <<'EOF'
(module
  (func (export "f") (param $x i64) (param $y i64) (result i64)
    (i64.sub (i64.add (i64.mul (local.get $x) (i64.const 8)) (local.get $y)) (local.get $y))))
EOF
mkdir -p clif && wasmtime compile --emit-clif clif comb.wat -o comb.cwasm
sed -n '/block1:/,/^}/p' 'clif/wasm[0]--function[0].clif'
wasmtime objdump comb.cwasm | sed -n '/function\[0\]:/,/^$/p'
wasmtime compile -O opt-level=0 comb.wat -o comb0.cwasm
wasmtime objdump comb0.cwasm | sed -n '/function\[0\]:/,/^$/p'

Output (complete):

                                block1:
                                    v9 = iconst.i64 3
                                    v10 = ishl.i64 v2, v9  ; v9 = 3
@0028                               v7 = iadd v10, v3
@002b                               v8 = isub v7, v3
@002c                               return v8
}
wasm[0]::function[0]:
            pushq   %rbp
            movq    %rsp, %rbp
            leaq    (%rcx, %rdx, 8), %rax
            subq    %rcx, %rax
            movq    %rbp, %rsp
            popq    %rbp
            retq
wasm[0]::function[0]:
            pushq   %rbp
            movq    %rsp, %rbp
            imulq   $8, %rdx, %r8
            leaq    (%r8, %rcx), %rax
            subq    %rcx, %rax
            movq    %rbp, %rsp
            popq    %rbp
            retq

What to notice: the optimized CLIF has ishl v2, 3 where the wasm had a multiply by 8. The aegraph added x << 3 to x * 8's e-class, and extraction chose the cheaper member (Algorithm 21.7.5). (x·8 + y) − y was not simplified to x << 3: Cranelift's rule set has no rule for it, and extraction can only pick what the rules put into the e-graph. ISLE's x64 base rule for iadd builds an address (to_amode_add), which absorbs the shift into leaq (%rcx,%rdx,8). With the mid-end off (opt-level=0), the multiply survives as imulq $8, and the add still becomes a lea, because that happens in lowering.

8. Comparison¶

Technique	Power / precision	Speed (asymptotic · practical)	Output / error quality	Implementation effort	Typical use
ISLE term rewriting	greedy per instruction with explicit priorities; deterministic (Proposition 21.7.7); patterns see operand trees through extractors	linear; compiled to a Rust trie	comparable to LLVM's selectors on common code; rules verifiable (Crocus)	moderate: rules are concise, extractors are Rust	Cranelift (Wasmtime, rustc_codegen_cranelift); Go's rulegen is a cousin
E-graph-based selection	all rewrites at once; optimal tree extraction (Theorem 21.7.6), DAG extraction NP-hard	exponential worst case; limits or acyclic variants make it practical	best when rules are rich; limited by the rule set (the `isub` example)	high: e-graph, rebuild, extraction, elaboration	Denali (research), Diospyros/egg (DSP vectorization), Cranelift's mid-end (aegraph)

Choose ISLE-style rewriting when you want a small, typed, verifiable rule language, especially for a JIT where compile time matters.
Choose e-graphs when phase ordering between rewrites costs you real code quality and you can bound the search. Use them in the mid-end or for small hot kernels, not for whole programs in a baseline JIT.

9. Assessment¶

Technique	Quiz ids (`solutions/quizzes/ch21.yaml`)	Drill	Flashcard tag	Exercises
ISLE term rewriting	`isle-priority-winner`, `isle-overlap`	`./course drill munch-tiling` (the same greedy choice at a node, by size instead of priority)	`isle`	—
E-graph-based selection	`egraph-extract-cost`, `egraph-dag-hard`	`./course drill dp-tiling` (tree extraction is the same recurrence)	`egraph-isel`	—

Expecting the e-graph to find rewrites it was never given

An e-graph finds the best represented term, and it represents only what the rules can derive. Cranelift did not simplify (x·8 + y) − y because no rule relates the two forms, even though a human sees it at once. "Optimal" in Theorem 21.7.6 is always relative to the rule set and to the exploration limits.

References¶

See the chapter references.

iteration	rule applied	e-classes after rebuild (members)
0	—	\(c_1 = \{x\}\), \(c_2 = \{8\}\), \(c_3 = \{c_1 \cdot c_2\}\), \(c_4 = \{y\}\), \(c_5 = \{c_3 + c_4\}\), \(c_6 = \{c_5 - c_4\}\)
1	\(x \cdot 8 \to x \ll 3\)	\(c_7 = \{3\}\); \(c_3 = \{c_1 \cdot c_2,\ c_1 \ll c_7\}\)
1	\((a + b) - b \to a\) (if present)	\(c_6 = \{c_5 - c_4,\ c_1 \ll c_7\}\), merged with \(c_3\)
2	nothing new	saturated

Technique	Time (worst)	Time (typical)	Space	Justification
ISLE term rewriting	\(O(n \cdot \text{trie depth})\) plus use-state propagation \(O(n + \text{uses})\)	linear	the generated trie (compiled Rust)	one trie walk per lowered instruction
E-graph selection (equality saturation)	exponential in the worst case (no saturation)	bounded by limits; Cranelift's aegraph is designed to be near linear	\(O(\lvert \mathcal{N} \rvert)\)	matching is per iteration; tree extraction is \(O(\lvert \mathcal{C} \rvert \cdot \lvert \mathcal{N} \rvert)\) with Bellman–Ford, near linear in practice

Lesson 21.7 — Rewriting-based selection: Cranelift ISLE and e-graphs¶

1. Problem and motivation¶

ISLE term rewriting¶

E-graph-based selection¶

2. Definitions and algorithms¶

3. Worked example¶

ISLE term rewriting¶

E-graph-based selection¶

4. Invariants and correctness¶

ISLE term rewriting¶

E-graph-based selection¶

5. Complexity¶

6. Variants and refinements¶

ISLE term rewriting¶

E-graph-based selection¶

7. In real compilers¶

ISLE term rewriting¶

E-graph-based selection¶

8. Comparison¶

9. Assessment¶

References¶