Lesson 13.4 — Canonicalization and the theory of rewrite systems¶
Techniques: canonical forms as a design principle (operand order, constants on the right, strict predicates, one spelling per operation); termination and confluence of rewrite systems (well-founded measures, Newman's lemma, critical pairs and Knuth–Bendix completion) · Pebble implements: the canonicalizing rules R1, R8, R15 of
pebble-peepholeand the termination measure of its rule set (exercise E2) · Lab: Part D checks that two engines with different rule orders reach the same result on a corpus · Prerequisites: Lesson 13.2 · Time: 4 hours
x - 5, x + -5, -5 + x and (x + 1) - 6 are the same value. If an optimizer's rules had to recognize every spelling, the rule count would explode, and value numbering would miss that a + b and b + a are equal. Compilers therefore pick one canonical form — say "constants on the right, add instead of subtract of a constant, strict comparisons" — rewrite everything into it early, and write every other rule against canonical input only. Canonicalization is itself a set of rewrite rules, and two questions follow immediately: does rewriting always stop, and does the result depend on the order in which rules fire? The theory of term rewriting answers both: termination by a well-founded measure, order-independence by confluence, checkable through critical pairs.
1. Problem and motivation¶
A rule set \(\mathcal{R}\) is applied until no rule matches (Algorithm 13.2.4). For the result to be well defined we need termination (no infinite rewrite sequence: the engine stops) and ideally confluence (all maximal rewrite sequences from one program end in the same program: the result does not depend on worklist order or rule priority). Canonicalization makes the rule set smaller and value numbering more effective, but canonicalizing rules are exactly the ones that can loop: mul x, 2 → shl x, 1 plus a rule shl x, 1 → add x, x plus a rule add x, x → mul x, 2 cycle forever. In pebblec, pebble-peephole must terminate on every input; Theorem 13.4.9 proves it for R1–R17.
Canonical forms¶
Canonical forms are as old as optimizing compilers (Cocke and Schwartz normalize commutative expressions before value numbering [CS70]); LLVM makes canonicalization the explicit contract of InstCombine: "InstCombine is a target-independent canonicalization pass … the chosen canonical form needs to be the same for all targets" [LLVM-ICGuide]. Cranelift's ISLE mid-end has a "cprop" rule file whose first job is to "push immediates to the right" [Cranelift-ISLE]. GCC canonicalizes operand order in fold-const.cc (tree_swap_operands_p) and in match.pd.
Rewrite-system termination and confluence¶
Term rewriting studies exactly these questions. Newman proved in 1942 that a terminating system is confluent iff it is locally confluent [New42]; Knuth and Bendix showed in 1970 that local confluence reduces to finitely many critical pairs — overlaps of two rules' left-hand sides — and gave a completion procedure that adds rules until all critical pairs are joinable [KB70]. Baader and Nipkow's textbook is the standard reference [BN98]. Compiler rule sets are rarely proven confluent, but the concepts explain real bugs (combiners that loop, results that depend on pass order) and the discipline that avoids them.
2. Definitions and algorithms¶
Definition 13.4.1 (Abstract rewrite system)
An abstract rewrite system is a set \(A\) with a relation \(\to \subseteq A \times A\). Write \(\to^{*}\) for its reflexive-transitive closure and \(\leftrightarrow^{*}\) for the equivalence closure. \(a\) is in normal form if there is no \(b\) with \(a \to b\). The system is terminating if there is no infinite chain \(a_0 \to a_1 \to \cdots\); confluent if \(a \to^{*} b\) and \(a \to^{*} c\) imply \(b \to^{*} d\) and \(c \to^{*} d\) for some \(d\) ("\(b\) and \(c\) are joinable"); locally confluent if this holds for one-step \(a \to b\), \(a \to c\); convergent if terminating and confluent.
The peephole engine as a rewrite system
\(A\) is the set of functions in SSA form; \(f \to g\) if one rule of R1–R17 at one instruction, followed by EraseDead, turns \(f\) into \(g\) (Algorithm 13.2.4). A normal form is a function to which no rule applies — what the engine returns.
Definition 13.4.2 (Canonical form)
Let \(\equiv\) be an equivalence on programs contained in mutual refinement. A canonicalizer is a function \(\kappa\) with \(\kappa(p) \equiv p\); it is complete for \(\equiv\) if \(p \equiv q\) implies \(\kappa(p) = \kappa(q)\). For a convergent rewrite system whose rules are sound for \(\equiv\) in both directions, \(\kappa(p)\) = the unique normal form of \(p\) is a canonicalizer, complete for \(\leftrightarrow^{*}\). Practical canonicalizers are partial: they choose one spelling for a few syntactic variants (operand order, subtraction of a constant, predicate strictness) without deciding program equivalence.
Definition 13.4.3 (Critical pair)
Let \(l_1 \to r_1\) and \(l_2 \to r_2\) be rules (variables renamed apart), and let \(p\) be a position of \(l_1\) where \(l_1|_p\) is not a variable and \(l_1|_p\) and \(l_2\) unify with most general unifier \(\theta\). Then the term \(\theta(l_1)\) can be rewritten in two ways: to \(\theta(r_1)\) at the root, and to \(\theta(l_1)[\theta(r_2)]_p\) at \(p\). The pair \(\langle \theta(r_1),\ \theta(l_1)[\theta(r_2)]_p \rangle\) is a critical pair; it is joinable if both sides rewrite to a common term.
Canonical forms¶
Algorithm 13.4.4 (Canonical operand order by rank)
- Input: an instruction \(i\) with a commutative opcode, or an
icmp. - Output: \(i\) with its operands in canonical order.
- Precondition: a rank function \(\mathrm{cx}\) on values: 1 for constants, 2 for casts and negations, 3 for other instructions and arguments (InstCombine's
getComplexity;pebble-peepholeuses only "constant or not"). - Postcondition: \(\mathrm{cx}(\mathit{op}_0) \ge \mathrm{cx}(\mathit{op}_1)\); for
icmp, the predicate is swapped so the comparison means the same. - Invariant: the instruction's value never changes (commutativity, or the swapped predicate).
function Canonicalize(i):
if i is commutative and cx(op0(i)) < cx(op1(i)):
swap the operands of i # rule R1 const-rhs
if i = icmp P (a, b) and cx(a) < cx(b):
i ← icmp swap(P) (b, a) # slt ↔ sgt, ule ↔ uge, ...
if i = sub (x, C) with C a non-zero constant:
i ← add (x, −C) with flags per Theorem 13.8.13 # rule R8
if i = icmp P (x, C) with P non-strict and C not the extreme value:
i ← icmp strict(P) (x, C ∓ 1) # rule R15
Rewrite-system termination and confluence¶
Algorithm 13.4.5 (Knuth–Bendix completion)
- Input: a finite set of equations \(E\) over terms; a reduction order \(>\) (well-founded, closed under contexts and substitutions).
- Output: a convergent rewrite system \(\mathcal{R}\) with the same equational theory as \(E\) — or
fail(an equation that cannot be oriented) — or no answer (the procedure may run forever). - Precondition: \(>\) is a reduction order; every rule \(l \to r\) added satisfies \(l > r\).
- Postcondition: on success, every critical pair of \(\mathcal{R}\) is joinable and \(\mathcal{R}\) terminates (so it is convergent, Theorems 13.4.7–13.4.8).
- Invariant: \(\leftrightarrow^{*}_{E \cup \mathcal{R}}\) is unchanged, and every rule of \(\mathcal{R}\) decreases in \(>\).
function Complete(E, >):
R ← ∅
while E ≠ ∅:
take (s = t) from E
s', t' ← normal forms of s, t under R
if s' = t': continue # already joinable
if s' > t': add rule s' → t' to R
else if t' > s': add rule t' → s' to R
else: return fail # cannot orient
for each critical pair ⟨u, v⟩ between the new rule and R (Definition 13.4.3):
E ← E ∪ {u = v}
return R
Production compilers do not run completion; they use its logic by hand: when two rules overlap non-joinably, add a rule (or a guard) that joins them — Example 13.4.10.
3. Worked example¶
Running example: the function @peep of Lesson 13.2 §3 and its 16-step rewrite trace.
Canonical forms¶
Algorithm 13.4.4 on the instructions of @peep (constant rank 1, everything else 3):
| instruction | ranks \((\mathit{op}_0, \mathit{op}_1)\) | canonical form | rule |
|---|---|---|---|
a = mul 3, x |
(1, 3) | mul x, 3 |
R1 |
b = mul 8, a |
(1, 3) | mul a, 8 |
R1 |
c = add 0, y (after z → 0) |
(1, 3) | add y, 0 |
R1 |
e = sub d, 3 |
— | add d, -3 |
R8 |
r = xor b, e |
(3, 3) | unchanged | — |
After canonicalization every constant is on the right, so R2, R9 and R10 need only one pattern each (add x, 0, not also add 0, x) — the point of the discipline. LLVM goes further: its InstCombine also reassociates (x * 3) * 8 into x * 24 (box in §7), a rule our set does not have.
Rewrite-system termination and confluence¶
The termination measure of Theorem 13.4.9, \(\mu = (I, S, A, M)\), along the trace of @peep (only the steps that rewrite; the numbers are the state after the step):
| step | rule | \(I\) (instructions) | \(S\) (non-canonical sites) | \(A\) (add-chain depth) | \(M\) (reducible ops) | decreases |
|---|---|---|---|---|---|---|
| 0 | — | 8 | 3 (a, b, e) |
0 | 0 | — |
| 1 | R1 on a |
8 | 2 | 0 | 0 | \(S\) |
| 2 | R1 on b |
8 | 1 | 0 | 1 (b′ = mul a′, 8) |
\(S\) |
| 3 | R5 on z |
7 | 2 (c = add 0, y) |
0 | 1 | \(I\) |
| 4 | R1 on c |
7 | 1 | 1 (d = add c′, 5 over c′ = add y, 0) |
1 | \(S\) |
| 5 | R9 on d |
6 | 1 | 0 | 1 | \(I\) (\(c′\) died) |
| 6 | R8 on e |
6 | 0 | 1 (e′ = add d′, -3 over d′) |
1 | \(S\) |
| 10 | R10 on b′ |
6 | 0 | 1 | 0 | \(M\) |
| 12 | R9 on e′ |
5 | 0 | 0 | 0 | \(I\) (\(d′\) died) |
Components to the right of the decreasing one may grow (step 3 raises \(S\), step 6 raises \(A\)); the lexicographic order still decreases at every step.
A critical pair. R2 (\(\mathsf{add}(x, 0) \to x\)) overlaps R9 (\(\mathsf{add}(\mathsf{add}(x, C_1), C_2) \to \mathsf{add}(x, C_1 + C_2)\)) at position 1 with \(\theta = \{C_1 \mapsto 0\}\):
The two sides are already equal: joinable. This is step 5 of the trace, where R9 fired first; had R2 fired first, the same function would have resulted.
Try it
Change the priority order of two rules in your pebble-peephole and rerun tests/ch13/lab/compare.test: if the rule set is confluent on the corpus, both engines still agree. ./course drill rewrite-validity trains the other half: whether each rule is valid at all.
4. Invariants and correctness¶
Canonical forms¶
Proposition 13.4.6 (Canonicalization preserves values and halves the patterns)
Algorithm 13.4.4 replaces \(i\) by an instruction with the same value on every input (same poison, same flags' meaning). After it has run on every instruction, a rule written for the canonical order of a commutative operation with one constant operand matches every instance that its commuted variant would have matched.
Proof
Swapping the operands of a commutative operation preserves its value and its flags' conditions (nsw, nuw and disjoint are symmetric in the operands). icmp P a, b equals icmp swap(P) b, a by definition of the swapped predicate; samesign is symmetric. sub x, C → add x, -C and the predicate strictification are proven in Theorem 13.8.13 and Example 13.8.15 (with their flag conditions). For the second claim: an instance of the commuted pattern \(\mathsf{op}(C, x)\) has rank (1, 3), which the algorithm swaps to \(\mathsf{op}(x, C)\); so after canonicalization only the canonical variant occurs.
Rewrite-system termination and confluence¶
Theorem 13.4.7 (Newman's lemma)
A terminating, locally confluent abstract rewrite system is confluent.
Proof
By well-founded induction on \(\to^{+}\) (well-founded because the system terminates). Claim: every \(a\) is confluent, i.e. \(a \to^{*} b\) and \(a \to^{*} c\) imply \(b, c\) joinable. Assume the claim for every \(a'\) with \(a \to^{+} a'\). If \(a = b\) or \(a = c\) the claim is trivial. Otherwise \(a \to b_1 \to^{*} b\) and \(a \to c_1 \to^{*} c\). By local confluence, \(b_1 \to^{*} d\) and \(c_1 \to^{*} d\) for some \(d\). By the induction hypothesis for \(b_1\) (with \(a \to^{+} b_1\)), \(b\) and \(d\) are joinable: \(b \to^{*} e\), \(d \to^{*} e\). Then \(c_1 \to^{*} d \to^{*} e\) and \(c_1 \to^{*} c\), so by the induction hypothesis for \(c_1\), \(e\) and \(c\) are joinable: \(e \to^{*} g\), \(c \to^{*} g\). Hence \(b \to^{*} e \to^{*} g\) and \(c \to^{*} g\).
Theorem 13.4.8 (Critical pair lemma)
A term rewriting system is locally confluent if and only if all its critical pairs are joinable.
Proof sketch (full proof: [BN98, Ch. 6])
Only if: a critical pair arises from one term rewritten two ways, so local confluence joins it. If: take \(t \to_{p_1} t_1\) and \(t \to_{p_2} t_2\) by rules \(l_1 \to r_1\), \(l_2 \to r_2\) at positions \(p_1\), \(p_2\). If \(p_1\) and \(p_2\) are disjoint, apply the other rule to each result: they meet. If one is below the other, say \(p_2 = p_1 q\): either \(q\) lies at or below a variable position of \(l_1\) — then the inner redex sits inside the substituted value, and rewriting all copies of that variable in \(t_1\) (non-linear rules copy it) joins the two — or \(q\) is a non-variable position of \(l_1\), where \(l_1|_q\) and \(l_2\) unify: the situation is an instance of a critical pair, which is joinable by hypothesis, and joinability is closed under substitution and context.
Theorem 13.4.9 (Termination of the course rule set R1–R17)
For a function \(f\) define: \(I(f)\) = the number of instructions; \(S(f)\) = the number of non-canonical sites, counted per feature (one instruction can have two): (i) a commutative binary operator, fadd, fmul or icmp with a constant first operand and a non-constant second one; (ii) a sub x, C with \(C \ne 0\); (iii) an icmp with a non-strict predicate (sge, sle, uge, ule) and a constant operand — so icmp sle 5, x counts twice; \(A(f) = \sum_u \ell(u)\) over adds with a constant second operand, where \(\ell(u) = 1 + \ell(v)\) if \(u\)'s first operand \(v\) is such an add, and \(0\) otherwise; \(M(f)\) = the number of instructions matching the left side of R10–R14 (a strength-reducible operation). Every step of Algorithm 13.2.4 with R1–R17 strictly decreases \(\mu(f) = (I, S, A, M)\) in the lexicographic order on \(\mathbb{N}^4\). Hence the engine terminates on every input.
Proof
The lexicographic order on \(\mathbb{N}^4\) is well founded, so it suffices to check each rule; EraseDead only lowers \(I\).
R2–R7, R16, R17 replace the instruction by an existing value or a constant; it loses its uses and is erased: \(I\) decreases.
R1, R8, R15 replace the instruction by one new instruction (the old one is erased): \(I\) is unchanged. Each removes one feature and adds none: R1 removes (i) and keeps (iii) as it was (the swapped predicate is non-strict iff the old one was, and the constant is still an operand — icmp sle 5, x becomes icmp sge x, 5, which still counts once, for R15); R8 removes (ii) (the new add has no feature); R15 removes (iii) (its constant was already on the right). No other instruction's features change (they depend only on the instruction's own opcode, predicate and which operands are constant, and the new value is as non-constant as the old): \(S\) decreases.
R9 replaces \(u = \mathsf{add}(v, C_2)\), \(v = \mathsf{add}(x, C_1)\), by \(u' = \mathsf{add}(x, C_1 + C_2)\): \(I\) does not increase (\(v\) may die), \(S\) is unchanged (\(u'\) is canonical, like \(u\)). \(\ell(u') = \ell(v) = \ell(u) - 1\), and every add-with-constant whose chain went through \(u\) now goes through \(u'\) and loses 1; nothing gains. So \(A\) decreases (or \(I\) already did).
R10–R14 replace a strength-reducible instruction by a shl, lshr, ashr or and with a constant right operand: \(I\) unchanged, \(S\) unchanged (canonical), \(A\) unchanged (neither the old nor the new instruction is an add with a constant, so no \(\ell\) changes). The old instruction counted in \(M\), the new one does not, and no other instruction starts matching R10–R14 (their patterns look only at the instruction's own opcode and constant; for R11's add x, x, a user would need both operands replaced, i.e. it was add i, i and matched before). So \(M\) decreases.
Every step decreases \(\mu\) strictly; a strictly decreasing sequence in a well-founded order is finite.
Example 13.4.10 (A non-joinable critical pair, and how E2 avoids it)
Without E2's guard "skip instructions whose operands are all constants", R5 (\(\mathsf{sub}(x, x) \to 0\)) and R8 (\(\mathsf{sub}(x, C) \to \mathsf{add}(x, -C)\)) overlap on \(\mathsf{sub}(C, C)\) with \(\theta = \{x \mapsto C\}\): one side gives \(0\), the other \(\mathsf{add}(C, -C)\), to which no rule of R1–R17 applies (it has no non-constant operand for R1, and \(-C\) is not 0 for R2). The pair is not joinable: the result would depend on which rule fires first. Knuth–Bendix completion would add the missing rule "fold an all-constant instruction" — which is exactly constant folding (Lesson 13.1); E2 instead makes all-constant instructions constant folding's job, so the overlap never occurs.
When it breaks. Termination fails as soon as two rules undo each other or a rule can grow the measure unboundedly: the cycle mul x, 2 → shl x, 1 → add x, x → mul x, 2 has no decreasing measure. Confluence fails with non-joinable critical pairs (Example 13.4.10), and also through flags: two orders that reach the same instructions but with different nsw/nuw are different normal forms. Our proof covers termination only; confluence of R1–R17 is not proved here, and the lab measures agreement of two engines on a corpus instead.
5. Complexity¶
| Technique | Time (worst) | Time (typical) | Space | Variables |
|---|---|---|---|---|
| Canonical operand order (Algorithm 13.4.4) | \(O(1)\) per instruction, \(O(n)\) per pass | one pass | \(O(1)\) | \(n\) instructions |
| Rewriting to a normal form | bounded by the length of the longest decreasing \(\mu\)-chain | linear in practice | \(O(n)\) | \(\mu = (I, S, A, M)\) of Theorem 13.4.9 |
| Critical-pair check of a rule set | \(O(m^2 \ell^2)\) unifications | fast | \(O(m\ell)\) | \(m\) rules, \(\ell\) pattern size |
| Knuth–Bendix completion | may not terminate; undecidable in general | seconds for small theories | unbounded | — |
Justification. Algorithm 13.4.4 does a constant number of rank comparisons. For rewriting with R1–R17: \(S \le 2n\), \(M \le n\), and \(A \le n^2\) (each chain depth is below \(n\)), and every step lowers \(\mu\); a crude bound on the number of steps is the number of lexicographically decreasing tuples, \(O(n \cdot n \cdot n^2 \cdot n)\), but each rule application after the first few lowers \(I\) or \(S\) often, and the lab's corpus of 4 824 instructions needs 1 355 steps (§8 of Lesson 13.2). Critical pairs: for each ordered pair of rules and each non-variable position of the first, one unification of size \(O(\ell)\). Completion is undecidable in general because the word problem for equational theories is.
Pathological family. The chain \(u_1 = \mathsf{add}(x, 1)\), \(u_k = \mathsf{add}(u_{k-1}, 1)\) for \(k = 2..n\), each \(u_k\) also used elsewhere (so no intermediate add dies), has \(A = 0 + 1 + \dots + (n-1) = \Theta(n^2)\); R9 rewrites every \(u_k\) into \(\mathsf{add}(x, k)\), and in the worst worklist order (outermost first) each rewrite lowers \(A\) only by the length of one chain suffix, for \(\Theta(n)\) rewrites with \(\Theta(n)\) rule tries each: \(\Theta(n^2)\) work, versus \(\Theta(n)\) in program order.
6. Variants and refinements¶
Canonical forms¶
- Rank-based canonical order for reassociation: sort commutative operands by rank (Lesson 13.6) so that loop-invariant parts group together [BC94].
- Canonical forms with target reversal: InstCombine canonicalizes target-independently and the back end reverses unprofitable forms (
x << 1back tox + xwhere adds are cheaper) [LLVM-ICGuide]. Trade-off: two places to maintain. - Normalization of loops (LoopSimplify, LCSSA, rotated loops) is canonicalization at the CFG level (Ch 15).
Rewrite-system termination and confluence¶
- Reduction orders: recursive path orders and Knuth–Bendix orders prove termination of rule sets automatically [BN98]. Trade-off: generality vs. automation; compiler rule sets usually need custom measures like \(\mu\).
- Rewriting modulo AC (associativity and commutativity): match up to reordering instead of canonicalizing operand order [BN98]. Trade-off: exponential matching.
- Equality saturation (e-graphs) sidesteps confluence: apply all rules non-destructively and extract the best term by cost (Ch 17). Trade-off: memory and extraction cost.
7. In real compilers¶
Canonical forms¶
InstCombine's canonical forms
Reproduce (opt 23.1.2; any OS):
cat > canon.ll <<'EOF'
define i32 @c1(i32 %x) { %r = sub i32 %x, 5 ret i32 %r }
define i32 @c2(i32 %x) { %r = add i32 7, %x ret i32 %r }
define i1 @c3(i32 %x) { %r = icmp sge i32 %x, 10 ret i1 %r }
define i32 @c4(i32 %x) { %r = mul i32 %x, 16 ret i32 %r }
define i32 @c5(i32 %x) { %n = xor i32 %x, -1 %r = add i32 %n, 1 ret i32 %r }
define i1 @c6(i32 %x) { %r = icmp ugt i32 %x, 0 ret i1 %r }
define i32 @c7(i32 %x) { %a = mul i32 3, %x %b = mul i32 8, %a ret i32 %b }
EOF
opt -passes=instcombine -S canon.ll | grep -v '^;\|^$\|source_filename'
Output (complete):
define i32 @c1(i32 %x) {
%r = add i32 %x, -5
ret i32 %r
}
define i32 @c2(i32 %x) {
%r = add i32 %x, 7
ret i32 %r
}
define i1 @c3(i32 %x) {
%r = icmp sgt i32 %x, 9
ret i1 %r
}
define i32 @c4(i32 %x) {
%r = shl i32 %x, 4
ret i32 %r
}
define i32 @c5(i32 %x) {
%r = sub i32 0, %x
ret i32 %r
}
define i1 @c6(i32 %x) {
%r = icmp ne i32 %x, 0
ret i1 %r
}
define i32 @c7(i32 %x) {
%b = mul i32 %x, 24
ret i32 %b
}
What to notice: constants on the right (c2), subtraction of a constant as addition (c1, rule R8), strict predicates (c3: sge 10 → sgt 9, rule R15; c6: ugt 0 → ne 0), a multiply by a power of two as a shift (c4), ~x + 1 as 0 - x (c5), and constants folded through reassociation (c7: 3 * x * 8 → x * 24, beyond R1–R17).
How LLVM and Cranelift define 'canonical'
Reproduce (LLVM 23.1.2 and wasmtime 37.0.2 sources; curl):
L=https://raw.githubusercontent.com/llvm/llvm-project/llvmorg-23.1.2/llvm
curl -sL $L/include/llvm/Transforms/InstCombine/InstCombiner.h | sed -n '/This routine maps IR values to various complexity ranks/,/^ }$/p'
curl -sL $L/docs/InstCombineContributorGuide.md | sed -n '/^| Original Pattern/,/^$/p'
Output (complete):
/// This routine maps IR values to various complexity ranks:
/// 0 -> undef
/// 1 -> Constants
/// 2 -> Cast and (f)neg/not instructions
/// 3 -> Other instructions and arguments
static unsigned getComplexity(Value *V) {
if (isa<Constant>(V))
return isa<UndefValue>(V) ? 0 : 1;
using namespace llvm::PatternMatch;
if (isa<CastInst>(V) || match(V, m_Neg(m_Value())) ||
match(V, m_Not(m_Value())) || match(V, m_FNeg(m_Value())))
return 2;
return 3;
}
| Original Pattern | Canonical Form | Condition |
|------------------------------|----------------------------|-------------------------------|
| `icmp spred X, Y` | `icmp samesign upred X, Y` | `sign(X) == sign(Y)` |
| `smin/smax X, Y` | `umin/umax X, Y` | `sign(X) == sign(Y)` |
| `sext X` | `zext nneg X` | `X >=s 0` |
| `sitofp X` | `uitofp nneg X` | `X >=s 0` |
| `ashr X, Y` | `lshr X, Y` | `X >=s 0` |
| `sdiv/srem X, Y` | `udiv/urem X, Y` | `X >=s 0 && Y >=s 0` |
| `add X, Y` | `or disjoint X, Y` | `(X & Y) != 0` |
| `mul X, C` | `shl X, Log2(C)` | `isPowerOf2(C)` |
| `select Cond1, Cond2, false` | `and Cond1, Cond2` | `impliesPoison(Cond2, Cond1)` |
| `select Cond1, true, Cond2` | `or Cond1, Cond2` | `impliesPoison(Cond2, Cond1)` |
curl -sL https://raw.githubusercontent.com/bytecodealliance/wasmtime/v37.0.2/cranelift/codegen/src/opts/cprop.isle \
| sed -n '/^;; Canonicalize via commutativity: push immediates to the right./,/^ (iadd ty x k))/p'
Output (complete):
;; Canonicalize via commutativity: push immediates to the right.
;;
;; (op k x) --> (op x k)
(rule (simplify
(iadd ty k @ (iconst ty _) x))
(iadd ty x k))
What to notice: getComplexity is the rank function of Algorithm 13.4.4 (InstCombine sorts commutative operands so the more complex one is on the left); the contributor guide's table lists canonicalizations that are not optimizations by themselves (signed to unsigned forms with samesign, nneg, disjoint flags) — read its conditions critically: add X, Y becomes or disjoint X, Y when (X & Y) == 0 (no common bits, Definition 9.7.3), not != 0 as the table at this tag prints; Cranelift's ISLE rules state the same "immediates to the right" convention as rewrite rules.
Rewrite-system termination and confluence¶
InstCombine verifies its fixed point
Reproduce (opt 23.1.2; any OS):
cat > peep.ll <<'EOF'
define i32 @peep(i32 %x, i32 %y) {
%a = mul i32 3, %x
%b = mul i32 8, %a
%z = sub i32 %x, %x
%c = add i32 %z, %y
%d = add i32 %c, 5
%e = sub i32 %d, 3
%r = xor i32 %b, %e
ret i32 %r
}
EOF
opt -passes=instcombine -print-pipeline-passes -disable-output peep.ll
opt -passes='default<O2>' -print-pipeline-passes -disable-output peep.ll | tr ',' '\n' | grep -c '^instcombine'
opt -passes=instcombine -S peep.ll | sed -n '/^define/,/^}/p'
Output (complete):
function(instcombine<max-iterations=1;verify-fixpoint>),verify
8
define i32 @peep(i32 %x, i32 %y) {
%b = mul i32 %x, 24
%e = add i32 %y, 2
%r = xor i32 %b, %e
ret i32 %r
}
What to notice: opt -passes=instcombine means instcombine<max-iterations=1;verify-fixpoint>: one worklist iteration, then a check that another would change nothing (a fatal error otherwise, InstCombinerImpl::run in InstructionCombining.cpp). The -O2 pipeline runs InstCombine 8 times, between passes that create new opportunities. On @peep it reaches a different normal form than pebble-peephole (mul x, 24 instead of shl (mul x, 3), 3): different rule sets, different canonical forms.
8. Comparison¶
| Technique | Power / precision | Speed (asymptotic · practical) | Output / error quality | Implementation effort | Typical use |
|---|---|---|---|---|---|
| Canonical forms (partial canonicalization) | Removes syntactic variants; does not decide equivalence | \(O(n)\) · negligible | Fewer rules needed; later passes see equal things as equal | Low, but needs discipline across all rules | InstCombine, ISLE cprop, GCC fold; before value numbering |
| Termination and confluence reasoning (measures, critical pairs, completion) | Guarantees the engine stops and (if confluent) is order-independent | Critical pairs \(O(m^2\ell^2)\); completion may diverge | Proofs, not code; catches looping and order-dependent rule sets | Medium (by hand) to high (tools) | Designing rule sets (E2), term-rewriting tools, e-graph rule synthesis |
Choose canonical forms always: pick one spelling per operation, document it (as the InstCombine guide does), and write every rule against it. Choose explicit termination measures whenever you add a rule that does not shrink the program (canonicalizing and strength-reducing rules): name the measure it decreases. Choose critical-pair analysis when rules overlap and results must be order-independent — or switch to equality saturation.
9. Assessment¶
| Technique | Quiz questions | Drills | Flashcards | Exercises |
|---|---|---|---|---|
| Canonical forms | canon-form, find-getcomplexity |
justification: canonicalization is exercised by E2's R1/R8/R15 tests and the rewrite-validity drill; a separate drill would repeat them |
tag canonical-forms |
E2 (R1, R8, R15) |
| Rewrite-system termination and confluence | newman, measure-step, critical-pair |
justification: critical pairs are traced in this lesson and in the quiz; the lab's compare.test checks order-independence empirically |
tag rewriting |
E2 (termination), Lab Part D |
References¶
See the chapter references.