Lesson 13.3 — Superoptimization and learned rewrite rules

Techniques: enumerative superoptimization (Massalin 1987; the GNU superoptimizer; Bansal–Aiken's peephole superoptimizer 2006); stochastic superoptimization (STOKE, 2013); solver-based synthesis (Souper, 2017, with counterexample-guided inductive synthesis); learning and generalizing rewrite rules (Alive-Infer 2017, Hydra 2024) · Pebble implements: nothing in the compiler · Lab: ★ ch13-superopt, a brute-force superoptimizer for short i8 sequences (Part C), whose answers are checked by your ch13-rewrite-check (Part B) · Prerequisites: Lesson 13.2, refinement from Lesson 9.7 · Time: 4 hours

A peephole engine applies rules that people wrote. Where do new rules come from? A superoptimizer searches for the best program equivalent to a given one, instead of improving it step by step: for sgn(x) (−1, 0 or 1) it finds a four-instruction branch-free sequence no human had written down. Superoptimizers are too slow to run inside a compiler, but they are excellent rule finders: run one offline over code fragments, and every improvement it finds is a candidate peephole rule. This lesson covers the four generations of that idea — exhaustive enumeration, stochastic search, synthesis with an SMT solver, and generalizing concrete findings into rules with preconditions — and connects each to the lab's brute-force superoptimizer and rewrite checker.

1. Problem and motivation

Given a loop-free code fragment \(s\), find a fragment \(t\) of minimal cost (instructions, latency, bytes) that refines \(s\). The problem is decidable for bounded-length fragments over finite-width integers (enumerate and check) but its search space grows exponentially with the length of \(t\). Compilers use superoptimizers offline, to discover missing rules for their peephole engines (Lesson 13.2); pebblec does not run one, but the lab's ch13-superopt is a working miniature.

Enumerative superoptimization

Massalin coined the term and built the first superoptimizer for the Motorola 68020: enumerate every instruction sequence in order of length, run each on a few test inputs, and report the first one that matches the target on all of them — after which a human (or, later, a prover) checks it [Mas87]. Famous results were branch-free sequences using the carry flag, such as signum in four instructions. Granlund and Kenner's GNU superoptimizer (GSO) generalized it to many architectures and used it to eliminate branches in GCC's code generator [GK92]. Bansal and Aiken turned the idea into a peephole superoptimizer: enumerate all short sequences once, index them by their behavior on test vectors, and use the database to optimize windows of real programs, with a SAT solver proving each replacement [BA06].

Stochastic superoptimization

Enumeration stops being feasible around five instructions. Schkufza, Sharma and Aiken's STOKE instead performs a random walk over programs (Markov chain Monte Carlo): it proposes small edits, scores each program by how wrong it is on test cases plus how slow it is, and accepts worse programs with a probability that decreases with how much worse they are. It finds long x86-64 sequences that enumeration cannot reach [SSA13].

Solver-based synthesis

Souper (Sasnauskas, Regehr et al.) extracts integer dataflow fragments from LLVM IR, asks an SMT solver whether a cheaper fragment (a constant, an existing value, or a small new expression) refines each one, and reports or applies the improvements; its synthesis uses counterexample-guided inductive synthesis (CEGIS) over a component library [SCC+17, GJTV11]. Souper found hundreds of missing LLVM optimizations that became InstCombine rules.

Learned rewrite rules

A superoptimizer's output is concrete: (x << 3) >> 3 → x & 31 for i8. A peephole rule needs symbolic constants and a precondition that says when it holds. Alive-Infer learns such preconditions from positive and negative examples and verifies them with Alive [MN17]; Hydra generalizes Souper's concrete optimizations into rules with symbolic constants and synthesized preconditions, and emits them as compiler code [MR24]. Together these close the loop "find → generalize → verify → implement".

2. Definitions and algorithms

Definition 13.3.1 (Superoptimization problem)

Let \(I\) be a set of instructions (operations with operand shapes), \(K\) a set of allowed constants, and \(c\) a cost function on straight-line programs over \(I\) and \(K\). Given a source program \(s\) with inputs \(\vec{x}\), the superoptimization problem asks for a program \(t\) over \(I \cup K\), with the same inputs, such that \(s \sqsupseteq t\) (Definition 9.7.8) and \(c(t)\) is minimal. The bounded problem restricts \(t\) to at most \(L\) instructions.

Definition 13.3.2 (Test vectors and fingerprints)

A set of test vectors is a finite set \(T\) of inputs. The fingerprint of a program \(p\) on \(T\) is the tuple \((p(\tau))_{\tau \in T}\). A candidate \(t\) passes \(T\) if for every \(\tau \in T\), \(s(\tau)\) allows \(t(\tau)\) (Definition 13.8.4). Passing \(T\) is necessary for \(s \sqsupseteq t\), not sufficient.

Enumerative superoptimization

Algorithm 13.3.3 (Massalin-style enumeration)

• Input: a source program \(s\), instructions \(I\), constants \(K\), a length bound \(L\), test vectors \(T\).
• Output: a shortest program \(t\) over \(I\) and \(K\) with \(s \sqsupseteq t\), or none within length \(L\).
• Precondition: inputs have finite width, so \(s \sqsupseteq t\) is decidable by enumeration (or by an SMT solver).
• Postcondition: if \(t\) is returned, \(s \sqsupseteq t\) and no program shorter than \(t\) refines \(s\) (Theorem 13.3.9).
• Invariant: when length \(\ell\) is being enumerated, no program of length \(< \ell\) refines \(s\).

function Superopt(s, I, K, L, T):
    for ℓ in 0, 1, ..., L:
        for t in Programs(ℓ, I, K):                 # every program of length ℓ, in a fixed order
            if not UsesAll(t): continue            # an unused intermediate result: a shorter program exists
            if not Passes(t, s, T): continue        # cheap filter (Definition 13.3.2)
            if Refines(s, t): return t              # full check: all inputs, or an SMT query
    return none

function Programs(ℓ, I, K):
    # instruction j reads operands from: the inputs, K, and the results of instructions 1..j-1
    yield every sequence of ℓ instructions (op, a, b) with op ∈ I and a, b in that pool,
        with a ≤ b for commutative op, and not both operands in K

function Refines(s, t):                             # Algorithm 13.9.6 of Lesson 13.9
    return for every input x (all bit patterns, and poison): s(x) allows t(x)

This is the lab's ch13-superopt (Part C) with \(I\) = {add, sub, mul, and, or, xor, shl, lshr, ashr} and \(K\) = {1, −1, \(N - 1\)} plus the source's constants and their neighbours.

Algorithm 13.3.4 (Bansal–Aiken peephole superoptimizer)

• Input: a training set of programs; a target instruction set; a window length \(w\) and candidate length \(L\); test vectors \(T\).
• Output: a table of rules (window → cheaper equivalent) to be applied by a peephole engine (Algorithm 13.2.4).
• Precondition: windows are canonicalized (registers renamed in order of first use) so that one rule covers all renamings.
• Postcondition: every rule in the table has been proven correct (SAT/SMT).
• Invariant: the database maps each fingerprint to the cheapest enumerated candidate with that fingerprint.

function BuildRules(training, w, L, T):
    DB ← empty map from fingerprint to program
    for t in all programs of length ≤ L (canonical register names):     # once, offline
        f ← Fingerprint(t, T)
        if f ∉ DB or cost(t) < cost(DB[f]): DB[f] ← t
    rules ← ∅
    for each window W of ≤ w consecutive instructions in the training programs:
        W ← Canonicalize(W)
        f ← Fingerprint(W, T)
        if f ∈ DB and cost(DB[f]) < cost(W) and Prove(W ⊒ DB[f]):     # SAT query
            rules ← rules ∪ {W → DB[f]}
    return rules

Stochastic superoptimization

Algorithm 13.3.5 (STOKE's Markov chain Monte Carlo search)

• Input: a target \(s\), test cases \(T\), a cost \(c(R) = \mathrm{eq}(R; T) + \mathrm{perf}(R)\) where \(\mathrm{eq}\) counts differing output bits over \(T\) (Hamming distance) and \(\mathrm{perf}\) estimates latency; a temperature parameter \(\beta > 0\); a proposal distribution \(q\) over small edits.
• Output: the lowest-cost rewrite with \(\mathrm{eq} = 0\) that a verifier proves equivalent.
• Precondition: \(q\) is symmetric (\(q(R \to R') = q(R' \to R)\)) and can reach every program of the fixed length from every other.
• Postcondition: returned rewrites are verified; the chain's stationary distribution is \(\pi(R) \propto e^{-\beta c(R)}\) (Theorem 13.3.10).
• Invariant: best is the cheapest verified rewrite seen so far.

function Stoke(s, T, β, iterations):
    R ← random program of the fixed length (unused slots are no-ops)
    best ← none
    repeat iterations times:
        R' ← Propose(R)                      # change an opcode, an operand, swap two instructions, or
                                             # replace an instruction by a random one (or a no-op)
        Δ ← c(R') − c(R)
        if Δ ≤ 0 or Uniform(0, 1) < exp(−β · Δ):
            R ← R'                           # always accept improvements; sometimes worse
        if eq(R; T) = 0 and (best = none or perf(R) < perf(best)) and Verify(s, R):
            best ← R
        else if eq(R; T) = 0 and not Verify(s, R):
            T ← T ∪ {a counterexample from Verify}      # refine the tests
    return best

Solver-based synthesis

Algorithm 13.3.6 (Counterexample-guided inductive synthesis, CEGIS)

• Input: a specification \(s\) over a finite input domain \(D\); a template \(t_{\vec{h}}\) with unknown holes \(\vec{h}\) (constants, or choices of components and their wiring [GJTV11]); a synthesizer \(\mathrm{Synth}(E)\) returning some \(\vec{h}\) with \(s \sqsupseteq t_{\vec{h}}\) on every input of \(E \subseteq D\), or none.
• Output: holes \(\vec{h}\) with \(s \sqsupseteq t_{\vec{h}}\) on all of \(D\), or none if no instance of the template works.
• Precondition: \(D\) is finite (or verification is decidable), and \(\mathrm{Synth}\) is complete for finite \(E\).
• Postcondition: a returned \(\vec{h}\) is correct on all of \(D\) (Theorem 13.3.11).
• Invariant: every \(\vec{h}\) rejected so far fails on some input of \(E\), and \(E\) grows by one new input per iteration.

function CEGIS(s, t, D):
    E ← {some input}
    loop:
        h ← Synth(E)                          # one SMT query: ∃h. ∀x ∈ E. s(x) allows t_h(x)
        if h = none: return none
        x ← Verify(s, t_h)                    # one SMT query: ∃x ∈ D. not (s(x) allows t_h(x))
        if x = none: return h
        E ← E ∪ {x}                           # x is new: t_h is correct on E but not on x

Learned rewrite rules

Definition 13.3.7 (Generalized rule and weakest precondition)

A concrete rule has literal constants; its generalization replaces them by symbolic constants \(\vec{C}\) and, where needed, derived constant expressions \(e(\vec{C})\), and ranges over all widths \(N\). The weakest precondition \(\mathrm{WP}(\vec{C}, N)\) of a generalized rule is the set of constant values and widths for which every instance is a refinement. A precondition \(P\) is sound if \(P \Rightarrow \mathrm{WP}\) and weakest if \(P \iff \mathrm{WP}\).

Algorithm 13.3.8 (Generalize, infer a precondition, verify)

• Input: a concrete rule \(L_0 \to R_0\) (from a superoptimizer), a grammar of constant expressions, a grammar of predicates.
• Output: a generalized rule \((L, R, P)\) with \(P\) sound, verified for all widths up to a bound, or none.
• Precondition: the concrete rule is valid.
• Postcondition: every instance allowed by \(P\) is a refinement (checked with Alive or bounded enumeration).
• Invariant: \(P\) holds on every positive example and fails on every negative example collected so far.

function Generalize(L0 → R0):
    L, R ← replace each literal constant by a fresh symbol C_i
    for each constant of R0 that is a function of those of L0:
        e ← first expression in the grammar that agrees with it on all sampled (C, N)   # e.g. -1 >>u C
        substitute e into R
    Pos, Neg ← instances (C, N) where the rule holds / fails     # sampled, checked by enumeration
    P ← simplest predicate in the grammar true on Pos and false on Neg   # Alive-Infer's learner
    if Verify(L, R, P) for all widths ≤ 64: return (L, R, P)
    else add the counterexample to Neg and repeat the last two steps

3. Worked example

Running example: sgn(x) for 8-bit \(x\) (labs/.../Inputs/superopt-signum.ll), and, for the symbolic methods, x udiv 515 on i16, one of Souper's test cases.

Enumerative superoptimization

A toy run of Algorithm 13.3.3 on \(s(x) = 3x \bmod 16\) (\(\texttt{i}4\)), \(I = \{\mathsf{add}, \mathsf{shl}\}\), \(K = \{1\}\), tests \(T = \{1, 2, 7\}\) with expected fingerprint \((3, 6, 5)\):

length	candidate (in enumeration order)	UsesAll?	fingerprint on \(T\)	outcome
0	\(x\); \(1\)	—	(1, 2, 7); (1, 1, 1)	fail
1	add x, x	yes	(2, 4, 14)	fail
1	add x, 1	yes	(2, 3, 8)	fail
1	shl x, x	yes	(2, 8, poison): \(7 \ge 4\) is an oversized shift	fail
1	shl x, 1	yes	(2, 4, 14)	fail
1	shl 1, x	yes	(2, 4, poison)	fail
2	t1 = add x, x; t2 = add x, x	no (\(t_1\) unused)	—	skip
2	t1 = add x, x; t2 = add x, 1	no	—	skip
2	t1 = add x, x; t2 = add x, t1	yes	(3, 6, 5)	pass → full check of all 17 inputs (\(16\) values and poison): valid

Every length-1 candidate fails a test, so by Theorem 13.3.9 the answer t1 = add x, x; t2 = add x, t1 is a shortest one. On the real target, ch13-superopt --max-len=4 enumerates 80 852 083 candidates for 8-bit signum in about 8 s and returns a 4-instruction sequence (box in §7).

Bansal–Aiken (Algorithm 13.3.4) on the window t = add x, x; r = add t, t from some training program, tests \(T = \{1, 2, 7\}\) on \(\texttt{i}8\): the window's fingerprint is \((4, 8, 28)\); the database built from all length-1 programs contains shl x, 2 under the same fingerprint (and mul x, 4 and add (shl x, 1), ..., none cheaper); the SAT query "∃x. window(x) ≠ shl x, 2" is unsatisfiable, so the rule add (add x, x), (add x, x) → shl x, 2 enters the table.

Stochastic superoptimization

Algorithm 13.3.5 on \(s(x) = 3x \bmod 16\) with two instruction slots, tests \(\{1, 3, 5, 7, 9, 11\}\) (targets \(3, 9, 15, 5, 11, 1\)), \(c = \mathrm{eq}\) (total differing bits; both rewrites have the same length, so \(\mathrm{perf}\) is constant), \(\beta = 1\); the column \(u\) is the uniform random number drawn for the acceptance test:

step	proposal	rewrite \(R'\)	outputs	\(c(R')\)	\(\Delta\)	\(p = \min(1, e^{-\Delta})\)	\(u\)	decision
0	(start)	and x, 1; sub t1, 1	0 0 0 0 0 0	14	—	—	—	current
1	opcode of slot 2: sub → add	and x, 1; add t1, 1	2 2 2 2 2 2	14	0	1	0.52	accept
2	operand 2 of slot 2: 1 → x	and x, 1; add t1, x	2 4 6 8 10 12	13	−1	1	0.93	accept
3	operand 2 of slot 1: 1 → x	and x, x; add t1, x	2 6 10 14 2 6	15	+2	0.135	0.61	reject
4	opcode of slot 1: and → shl	shl x, 1; add t1, x	3 9 15 5 11 1	0	−13	1	0.27	accept; \(\mathrm{eq} = 0\) → verify: valid

Step 3 would have been accepted with \(u < 0.135\): that is how the chain climbs out of local minima.

Solver-based synthesis

CEGIS (Algorithm 13.3.6) for Souper's test udiv i16 %x, 515, template \(t_{C,s}(x) = \mathrm{trunc}((\mathrm{zext}_{32}(x) \cdot C) \gg s)\) with holes \(C < 2^{17}\), \(16 \le s \le 32\); the synthesizer returns the lexicographically smallest \((s, C)\) consistent with \(E\), the verifier the smallest counterexample. (Computed exhaustively; an SMT solver returns some model, so its sequence differs, but not its end point's correctness.)

iteration	examples \(E\)	\(\mathrm{Synth}(E) = (C, s)\)	counterexample \(x\)	\(t(x)\) vs \(x / 515\)
1	{0}	(0, 16)	515	0 vs 1
2	{0, 515}	(128, 16)	512	1 vs 0
3	+ 512	(255, 17)	1029	2 vs 1
4	+ 1029	(1019, 19)	1544	3 vs 2
5	+ 1544	(2037, 20)	2574	5 vs 4
6	+ 2574	(4073, 21)	5149	10 vs 9
7	+ 5149	(8145, 22)	11329	22 vs 21
8	+ 11329	(16289, 23)	37079	72 vs 71
9	+ 37079	(65155, 25)	none	correct on all 65 536 inputs

Nine examples out of 65 536 pin down the answer. It is exactly Souper's recorded result (box in §7), and exactly the magic number of Lesson 13.7: \(d = 515\), \(N = 16\) gives \(\ell = 9\) and \(m = \lceil 2^{25} / 515 \rceil = 65155\).

Learned rewrite rules

Algorithm 13.3.8 on the concrete rule (x << 3) >>u 3 → x & 31 (\(\texttt{i}8\)): symbols \(C = 3\), \(D = 31\); candidate expressions for \(D\) from a small grammar, checked on \((C, N) \in \{1, 2, 3\} \times \{8\}\) (\(D\) must be 127, 63, 31):

candidate \(e(C)\)	\(C = 1\)	\(C = 2\)	\(C = 3\)	agrees?
\((1 \ll C) - 1\)	1	3	7	no
\(-1 \ll C\)	254	252	248	no
\(\sim(1 \ll C)\)	253	251	247	no
\(-1 \gg_u C\)	127	63	31	yes

The generalized rule (x << C) >>u C → x & (-1 >>u C) needs no precondition beyond the shift being in range, which both sides already make poison when violated; with C replaced by a variable %y Alive proves it for every width from 1 to 64 (box in §7). The arithmetic shift version (x << y) >>s y → x — a tempting over-generalization — fails already at \(\texttt{i}2\) (\(x = -2\), \(y = 1\)).

Try it

./course drill rewrite-validity --difficulty hard gives rewrites like these, including over-generalized ones, and asks for a verdict and a counterexample; lab Part C is the enumerative algorithm (./course test 13, milestone "superopt").

4. Invariants and correctness

Enumerative superoptimization

Theorem 13.3.9 (Enumeration finds a shortest refinement)

If Algorithm 13.3.3 returns \(t\), then \(s \sqsupseteq t\) and no program over \(I\) and \(K\) with fewer instructions refines \(s\). If it returns none, no program of length \(\le L\) over \(I\) and \(K\) refines \(s\).

Proof

Soundness: \(t\) is returned only after Refines, which checks every input (or is an exact SMT query), so \(s \sqsupseteq t\) by Definition 9.7.8. Optimality: lengths are tried in increasing order, and for each length every program is generated. A program skipped by UsesAll has an instruction whose result is never used; deleting it gives a program of smaller length with the same final value (the unused instruction has no side effects, and its possible poison is unobservable), which was enumerated earlier and, if it refined \(s\), would have been returned. A program skipped by Passes fails some test vector and so does not refine \(s\) (Definition 13.3.2). Skipping commutative duplicates and all-constant instructions removes only programs equal to, or foldable into shorter, enumerated ones. Hence when length \(\ell\) starts, no shorter program refines \(s\) (the invariant), and the first program returned is shortest. The none case is the invariant at \(\ell = L + 1\).

When it breaks: Massalin's original tool accepted a candidate after test vectors alone and relied on a human to check it; the GNU superoptimizer's README still warns that "the generated sequences might be incorrect with a very small probability". Without Refines, Theorem 13.3.9 is false. Optimality is also only relative to \(I\) and \(K\): GSO does not try arbitrary immediate constants, and neither does the lab's tool (the superopt-two test finds \(9x\) as two multiplications because 9 is not in \(K\)).

Stochastic superoptimization

Theorem 13.3.10 (Metropolis–Hastings acceptance targets \(e^{-\beta c}\))

With a symmetric, irreducible proposal \(q\) over a finite program space, the chain of Algorithm 13.3.5 (without the test-set updates) has stationary distribution \(\pi(R) = e^{-\beta c(R)} / Z\), where \(Z = \sum_{R} e^{-\beta c(R)}\).

Proof

It suffices to check detailed balance \(\pi(R)\, P(R \to R') = \pi(R')\, P(R' \to R)\) for \(R \ne R'\), where \(P(R \to R') = q(R \to R')\, \alpha(R \to R')\) and \(\alpha(R \to R') = \min(1, e^{-\beta (c(R') - c(R))})\). Suppose \(c(R') \ge c(R)\) (the other case is symmetric). Then \(\alpha(R \to R') = e^{-\beta(c(R') - c(R))}\) and \(\alpha(R' \to R) = 1\), so

\[ \pi(R)\, q(R \to R')\, e^{-\beta(c(R') - c(R))} = \frac{e^{-\beta c(R')}}{Z}\, q(R \to R') = \pi(R')\, q(R' \to R) \cdot 1, \]

using \(q(R \to R') = q(R' \to R)\). Detailed balance implies stationarity (sum both sides over \(R\)), and irreducibility on a finite space makes the stationary distribution unique (the standard Metropolis–Hastings argument that STOKE relies on [SSA13]). So the chain spends most of its time on low-cost programs; verified correctness is still established separately by Verify, never by the chain.

Solver-based synthesis

Theorem 13.3.11 (CEGIS is sound, and terminates on finite domains)

If Algorithm 13.3.6 returns \(\vec{h}\), then \(s \sqsupseteq t_{\vec{h}}\) on all of \(D\). If \(D\) is finite, it terminates after at most \(\lvert D \rvert\) iterations, and it returns none only if no instance of the template refines \(s\).

Proof

Soundness: \(\vec{h}\) is returned only when Verify finds no input of \(D\) where \(s(x)\) does not allow \(t_{\vec{h}}(x)\). Termination: each iteration that does not return adds an \(x\) with \(t_{\vec{h}}(x)\) not allowed; since \(\vec{h} = \mathrm{Synth}(E)\) is allowed on all of \(E\), \(x \notin E\). So \(E\) grows strictly, and \(E \subseteq D\). Completeness: if some \(\vec{h}^\ast\) is correct on \(D\), it is correct on every \(E \subseteq D\), so \(\mathrm{Synth}(E)\) never returns none (by its completeness), and the loop can end only by returning a verified \(\vec{h}\).

Learned rewrite rules

Proposition 13.3.12 (A verified sound precondition makes every instance valid; over-generalization is caught)

If \(P \Rightarrow \mathrm{WP}\) (Definition 13.3.7), every instance of the generalized rule allowed by \(P\) is a refinement. Conversely, if the generalized rule is invalid for some \((\vec{C}, N)\) allowed by \(P\), verification over widths \(\le N\) returns a counterexample.

Proof

The first claim is the definition of \(\mathrm{WP}\): an instance allowed by \(P\) lies in \(\mathrm{WP}\), where by definition it refines. For the second, the verifier checks the rule with \(\vec{C}\) as free variables at each width up to its bound; an invalid instance at width \(N\) is a satisfying assignment of the negated refinement condition at that width, which the solver (or enumeration) finds. The bound matters: a rule verified only for \(N \le 64\) says nothing about \(\texttt{i}128\) (Lesson 13.9 §4 on bitwidth independence).

5. Complexity

Technique	Time (worst)	Time (typical)	Space	Variables
Enumeration (Massalin, GSO, lab)	\(O\big(\prod_{j=1}^{L} \lvert I \rvert (a + k + j)^2 \cdot (\lvert T \rvert + 2^{Na} \text{ for survivors})\big)\)	seconds for \(L \le 4\)	\(O(L)\)	\(L\) length, \(a\) inputs, \(k = \lvert K \rvert\), \(\lvert I \rvert\) opcodes, \(N\) width
Bansal–Aiken database	\(O(P_L)\) once, then \(O(1)\) lookup per window + one SAT query per hit	offline hours, online fast	\(O(P_L)\) fingerprints	\(P_L\) programs of length \(\le L\)
STOKE (MCMC)	unbounded (a random walk); each step \(O(\lvert T \rvert \cdot \ell)\)	millions of proposals per minute	\(O(\ell)\)	\(\ell\) rewrite length, \(T\) tests
CEGIS (Souper)	\(\le \lvert D \rvert\) iterations, each two SMT queries (NP-hard)	a handful of iterations	\(O(\lvert E \rvert)\)	\(D\) input domain, \(E\) examples
Generalization (Alive-Infer, Hydra)	one verification per width and candidate; the predicate search is exponential in predicate size	seconds–minutes per rule	\(O(\lvert \mathit{Pos} \rvert + \lvert \mathit{Neg} \rvert)\)	examples

Justification. Instruction \(j\) of an enumerated program has \(\lvert I \rvert\) opcodes and at most \((a + k + j - 1)^2\) operand pairs, so the number of length-\(L\) programs is the product in the table — exponential in \(L\) with base growing in \(L\), the \(O(m n^{2n})\) of the GNU superoptimizer's README. Pathological family: any target whose shortest equivalent has length \(L\) forces the full product for all shorter lengths; measured on the lab tool: 8-bit signum, \(L = 4\), 80 852 083 candidates in about 8 s (box in §7), while \(L = 5\) would multiply that by roughly \(9 \cdot 13^2 \approx 1500\). CEGIS's worst case is \(\lvert D \rvert\) iterations when every candidate is wrong on exactly one new input; the worked example needed 9 of 65 536.

6. Variants and refinements

Enumerative superoptimization

• Pruning by equivalence classes: enumerate only one representative of each fingerprint per length (Bansal–Aiken's database; the "lens" algorithm of Phothilimthana et al. enumerates from both ends [PTBD16]). Trade-off: memory for the table.
• Branch elimination as the target application [GK92]; peephole databases harvested from real code [BA06]. Trade-off: rules only cover windows seen in training.

Stochastic superoptimization

• Two phases (synthesis with correctness-only cost, then optimization with performance) and restarts [SSA13]; floating-point STOKE trades bounded error for speed. Trade-off: no optimality guarantee.
• Cost-model learning (measured vs estimated latency). Trade-off: noise.

Solver-based synthesis

• Component-based synthesis [GJTV11]: holes choose components and their wiring, encoded in SMT. Trade-off: the component library bounds what can be found.
• Dataflow facts as synthesis targets: Souper also infers known bits, ranges and demanded bits for LLVM IR fragments, and compares them with LLVM's analyses to find imprecision [SCC+17].

Learned rewrite rules

• Alive-Infer learns weakest preconditions by predicate enumeration plus a learner over positive/negative examples [MN17]; Hydra generalizes Souper's results into rules with symbolic constants and preconditions and generates C++ [MR24]. Trade-off: the grammar of constant expressions and predicates limits what can be generalized.
• Rule inference for e-graphs (Ruler, Enumo) synthesizes whole rewrite systems from term enumeration; see Ch 17. Trade-off: rule-set size vs coverage.

7. In real compilers

Enumerative superoptimization

The GNU superoptimizer finds Massalin's signum

Reproduce (GNU superoptimizer 2.5, embecosm/gnu-superopt commit 3649aac; gcc 13.3.0; Linux):

git clone -q https://github.com/embecosm/gnu-superopt.git gso && git -C gso checkout -q 3649aac
make -C gso superopt-mc68020 superopt-i386 CC="gcc -std=gnu89 -fcommon -w" > /dev/null
./gso/superopt-mc68020 -fsgn -assembly -max-cost 4 | sed -n '1,2p;11,14p'
./gso/superopt-i386 -fsgn -assembly -max-cost 4 | sed -n '3,6p'

Output (complete):

Searching for { r = (signed_word) v0 > 0 ? 1 : ((signed_word) v0 < 0 ? -1 : 0); }
Superoptimizing at cost 1 2 3 4
3:  addl    d0,d0
    subxl   d1,d1
    negxl   d0
    addxl     d1,d1
1:  addl      %eax,%eax
    sbbl      %edx,%edx
    subl    %eax,%edx
    adcl      %eax,%edx

What to notice: result 3 for the 68020 is the classic four-instruction signum without branches: addl d0,d0 moves the sign bit into the carry/extend flag, subxl d1,d1 makes \(d_1 = -1\) or \(0\) from it, negxl d0 negates with borrow, and addxl d1,d1 combines. The x86 result is the same idea with sbb/adc. Both are found in milliseconds; GSO's README warns that its sequences are checked only by simulation on test values (the "When it breaks" note of §4).

What the compilers emit for signum, and the lab's superoptimizer

Reproduce (clang 23.1.2, gcc 13.3.0; ch13-superopt from the lab's reference solution on PATH):

echo 'int sgn(int x) { return (x > 0) - (x < 0); }' > sgn.c
echo "=== clang-23 -O2"; clang-23 --target=x86_64-unknown-linux-gnu -O2 -S -o - sgn.c | grep -P '^\t(?!\.)'
echo "=== gcc -O2";      gcc -O2 -S -o - sgn.c | grep -P '^\t(?!\.)'

Output (complete):

=== clang-23 -O2
    testl   %edi, %edi
    sets    %al
    setg    %cl
    subb    %al, %cl
    movsbl  %cl, %eax
    retq
=== gcc -O2
    endbr64
    xorl    %eax, %eax
    testl   %edi, %edi
    setg    %al
    shrl    $31, %edi
    subl    %edi, %eax
    ret

cat > sgn.ll <<'EOF'
define i8 @src(i8 %x) {
  %pos = icmp sgt i8 %x, 0
  %neg = icmp slt i8 %x, 0
  %p = zext i1 %pos to i8
  %n = sext i1 %neg to i8
  %r = or i8 %p, %n
  ret i8 %r
}
EOF
ch13-superopt --max-len=4 sgn.ll | sed -e 's/, [0-9.]* s$/, (time) s/'

Output (complete):

; ch13-superopt: 4 instructions (was 5), 80852083 candidates, (time) s
define i8 @opt(i8 %x) {
  %t0 = mul i8 %x, -1
  %t1 = lshr i8 %t0, 7
  %t2 = ashr i8 %x, 7
  %t3 = or i8 %t1, %t2
  ret i8 %t3
}

What to notice: clang and GCC emit 5–6 instructions using set<cc> (flags materialized as bytes), not the carry trick: their instruction selectors do not contain the superoptimized rule. The lab's flag-free IR search needs four instructions (mul x, -1 is its negation) and verifies the answer on all 257 inputs, poison included.

Stochastic superoptimization

STOKE's search: cost function and proposal masses (quoted)

Reproduce (STOKE sources at commit 98d8a0f; curl — STOKE itself needs an old Ubuntu and Haswell-era CPUs, so it was not run here):

URL=https://raw.githubusercontent.com/StanfordPL/stoke/98d8a0f028f2daf2052bfe607dbc32ec8d55ba9e/README.md
curl -sL $URL > stoke-README.md
grep -A6 '^A cost function is specified using' stoke-README.md
grep -- '^--.*_mass\|^--cost "correctness + latency"\|^--beta 1' stoke-README.md
grep '^- `src/search`' stoke-README.md

Output (complete):

A cost function is specified using the `--cost` command line argument.  It's an
expression composed using standard unsigned arithmetic operators.  As
variables, you can use several measurements of the current rewrite.  The most
important of these is `correctness`.  The value `correctness` is (by default)
the number of bits that differ in the outputs of the target versus the rewrite
summed across all testcases.  There are some tunable options for this, for
example, for floating point computations.  In all cases, lower cost is better.
--cost "correctness + latency" # Measure performance by summing instruction latencies
--global_swap_mass 0 # Proposal mass
--instruction_mass 1 # Proposal mass
--local_swap_mass 1 # Proposal mass
--opcode_mass 1 # Proposal mass
--operand_mass 1 # Proposal mass
--rotate_mass 0 # Proposal mass
--beta 1 # Search annealing constant
- `src/search`: An implementation of an MCMC-like algorithm for search.

What to notice: the cost is correctness (Hamming distance of live outputs over test cases) plus a performance term, exactly \(c = \mathrm{eq} + \mathrm{perf}\) of Algorithm 13.3.5; the _mass options weight the proposal kinds (opcode, operand, swap, instruction); --beta is \(\beta\) of Theorem 13.3.10.

Solver-based synthesis

Souper's division result, verified by Alive2

Reproduce (Souper sources at commit 963d4df via curl — Souper itself was not run here, its test file is quoted; alive-tv from Alive2 commit 01a5ec4 built against LLVM 23.1.2, see Lesson 13.9 §7):

curl -sL https://raw.githubusercontent.com/google/souper/963d4df436f3dc0b039cc0e47ada0577a26f5c4e/test/Infer/div_const.opt | sed -n '14,23p'
cat > souper515.ll <<'EOF'
define i16 @src(i16 %x) {
  %q = udiv i16 %x, 515
  ret i16 %q
}
define i16 @tgt(i16 %x) {
  %w = zext i16 %x to i32
  %m = mul i32 %w, 65155
  %s = lshr i32 %m, 25
  %q = trunc i32 %s to i16
  ret i16 %q
}
EOF
alive-tv souper515.ll | grep '^Transformation'

Output (complete):

%0:i16 = var
%1:i16 = udiv %0, 515
infer %1

%2:i32 = zext %0
%3:i32 = mul %2, 65155
%4:i32 = lshr %3, 25
%5:i16 = trunc %4
result %5
Transformation seems to be correct!

What to notice: the test asks Souper to infer a replacement for udiv i16 %0, 515, and the expected result is the multiply-and-shift found by CEGIS in §3: zext, mul 65155, lshr 25, trunc. Alive2 proves it for all inputs.

Learned rewrite rules

Generalizing a concrete rule and verifying it for every width with Alive2

Reproduce (the alive tool of Alive2 commit 01a5ec4, Z3 4.8.12; takes about a minute):

cat > gen.opt <<'EOF'
Name: found: (x << 3) >>u 3 => x & 31
%a = shl i8 %x, 3
%r = lshr %a, 3
  =>
%r = and %x, 31

Name: generalized: (x << y) >>u y => x & (-1 >>u y)
%a = shl %x, %y
%r = lshr %a, %y
  =>
%m = lshr -1, %y
%r = and %x, %m

Name: over-generalized: (x << y) >>s y => x
%a = shl %x, %y
%r = ashr %a, %y
  =>
%r = %x
EOF
stdbuf -o0 alive gen.opt 2>&1 | tr '\r' '\n' | grep -v '^$' | awk '
  { while (match($0, /^Done: [0-9]+/)) { n++; $0 = substr($0, RLENGTH + 1) } }
  $0 == "" { next }
  n { print "  (" n " type assignment" (n > 1 ? "s" : "") " checked)"; n = 0 }
  { print }'

Output (complete):

Processing gen.opt..
----------------------------------------
Name: found: (x << 3) >>u 3 => x & 31
  %a = shl i8 %x, 3
  %r = lshr i8 %a, 3
  ret %r
=>
  %r = and i8 %x, 31
  %a = shl i8 %x, 3
  ret %r
  (1 type assignment checked)
Transformation seems to be correct!
----------------------------------------
Name: generalized: (x << y) >>u y => x & (-1 >>u y)
  %a = shl %x, %y
  %r = lshr %a, %y
  ret %r
=>
  %m = lshr -1, %y
  %r = and %x, %m
  %a = shl %x, %y
  ret %r
  (64 type assignments checked)
Transformation seems to be correct!
----------------------------------------
Name: over-generalized: (x << y) >>s y => x
  %a = shl %x, %y
  %r = ashr %a, %y
  ret %r
=>
  %r = %x
  %a = shl %x, %y
  ret %r
  (1 type assignment checked)
ERROR: Value mismatch for i2 %r
Example:
i2 %x = #x2 (2, -2)
i2 %y = #x1 (1)
i2 %a = #x0 (0)
Source value: #x0 (0)
Target value: #x2 (2, -2)

What to notice: the concrete i8 rule is correct; the generalized rule, with the constant turned into a variable %y and the mask into lshr -1, %y, is proved for every integer type from i1 to i64 (Alive enumerates the 64 type assignments; the awk filter only condenses its progress lines); the over-generalized arithmetic-shift version passes at i1 and fails at i2. This is the verification step of Alive-Infer and Hydra (Algorithm 13.3.8).

8. Comparison

Technique	Power / precision	Speed (asymptotic · practical)	Output / error quality	Implementation effort	Typical use
Enumerative superoptimization	Optimal within \(I\), \(K\) and \(L\)	Exponential in \(L\) · \(L \le 4\)–5	Optimal, verified if a full check follows	Low (the lab tool: ~300 lines)	Finding short branch-free idioms; building peephole tables (GSO, Bansal–Aiken)
Stochastic superoptimization (STOKE)	Reaches long sequences; no optimality guarantee	Unbounded random walk · minutes–hours	Verified rewrites; quality depends on cost model	High (x86 semantics, verifier)	Hot kernels, research
Solver-based synthesis (Souper)	Complete for its templates and components	One SMT query per candidate · seconds–minutes per fragment	Verified; finds missing IR optimizations	High (SMT encodings of IR)	Offline discovery of LLVM InstCombine rules
Learned rewrite rules (Alive-Infer, Hydra)	Rules with symbolic constants and weakest-like preconditions	Verification per width · minutes	Generalized, verified rules, even code	High	Turning superoptimizer findings into compiler rules

Choose enumeration for very short sequences and exact optimality, and always verify. Choose stochastic search for longer straight-line kernels where good-enough is fine. Choose solver-based synthesis to systematically mine an IR (Souper on LLVM) for missed optimizations. Choose rule generalization when the output must become maintainable compiler rules, not a list of concrete improvements.

9. Assessment

Technique	Quiz questions	Drills	Flashcards	Exercises
Enumerative superoptimization	superopt-shortest, gso-signum	justification: enumeration is what the lab tool does; the rewrite-validity drill trains its verification step	tag enumerative-superopt	Lab Part C (★)
Stochastic superoptimization	stoke-accept, stoke-cost	justification: an MCMC trace depends on random draws; the quiz question computes one acceptance probability	tag stochastic-superopt	—
Solver-based synthesis	cegis-iterations, souper-magic	./course drill magic-division (the constants Souper synthesizes)	tag synthesis	—
Learned rewrite rules	generalize-rule, infer-precondition	./course drill rewrite-validity --difficulty hard	tag learned-rules	—

References

See the chapter references.