Lesson 13.9 — Verifying transformations: Alive2, bounded exhaustive checking, translation validation

Techniques: SMT-based verification of peephole rules (Alive 2015, Alive2 2021, Alive-FP 2016); bounded exhaustive checking at small bitwidths and its bitwidth-independence caveats; translation validation vs verified compilers (Pnueli et al. 1998, Necula 2000, CompCert) · Pebble implements: — · Lab: Part B, ch13-rewrite-check, a bounded exhaustive checker for rewrites over \(\texttt{i}N\), \(N \le 8\), with poison, UB and freeze, cross-checked with LLVM's own transformations and Alive2 · Prerequisites: Lesson 13.8 · Time: 4 hours

Lesson 13.8 made refinement precise. Checking it by hand for every rule of every compiler is hopeless: InstCombine alone has thousands of rules, and a single missing flag condition miscompiles. This lesson covers three ways to mechanize correctness. SMT-based verification encodes source and target as bit-vector formulas and asks a solver for an input where the target is not a refinement — Alive does this for InstCombine rules, and Alive2 for whole LLVM IR functions. Bounded exhaustive checking simply runs both programs on every input of a small width — what the lab's checker and the course drills do, and what LLVM's own unit tests do for division by constants — and the question is when small widths say anything about large ones. Translation validation checks each compiler run instead of the compiler, while a verified compiler proves the compiler correct once and for all.

1. Problem and motivation

Given a transformation (a rule with symbolic constants, or a concrete pair of functions), decide whether the target refines the source for all inputs, and if not, produce a counterexample. pebblec's peephole rules R1–R17 were validated this way while writing the course: each rule's lit test is a set of instances, and the lab's checker and Alive2 confirm the flag conditions (Lesson 13.8, Example 13.8.15 was found this way).

SMT-based verification

Lopes, Menendez, Nagarakatte and Regehr's Alive (PLDI 2015) is a DSL for InstCombine-style rules with preconditions; it encodes a rule for every feasible type assignment into SMT (Z3) queries for definedness, poison and value equality, found 8 bugs in the InstCombine rules it translated, and can emit C++ [LMNR15]. Alive-FP extended it to floating point and fast-math flags [MNG16]; Alive-Infer learns preconditions [MN17]. Alive2 (PLDI 2021) verifies arbitrary LLVM IR function pairs, with memory, loops (unrolled) and undef/poison, and runs over LLVM's test suite to report miscompilations; it found dozens of bugs, many due to undef [LLM+21]. The InstCombine contributor guide requires Alive2 proofs for new folds [LLVM-ICGuide].

Bounded exhaustive checking

Many peephole rules are about 8-, 16-, 32- and 64-bit integers and are "the same" at every width. Checking all \(2^{8k}\) inputs at 8 bits is a complete decision procedure for that width and needs no solver. LLVM's ConstantRange, KnownBits and division-by-constant unit tests enumerate all values of 4- to 12-bit integers; the course's drills and lab do the same. The catch is bitwidth independence: a rule proven at \(N = 8\) may fail at \(N = 1\) or \(N = 9\).

Translation validation and verified compilers

Pnueli, Siegel and Singerman proposed translation validation: instead of verifying a compiler, verify each translation it performs, by an independent checker [PSS98]; Necula built one for GCC's optimizer [Nec00]. Alive2's opt plugin and alive-tv are translation validators for LLVM. The alternative is a verified compiler: Leroy's CompCert is written and proven correct in Coq, so every compilation is correct by construction [Ler09]; Csmith's random testing found no wrong-code bug in its verified parts [YCER11].

2. Definitions and algorithms

SMT-based verification

Definition 13.9.1 (Bit-vector encoding of a straight-line function)

For a straight-line function \(f\) with integer arguments \(\vec{x}\) (bit-vector variables) and nondeterministic choices \(\vec{c}\) (freeze picks, undef uses), the encoding consists of three bit-vector formulas over \((\vec{x}, \vec{p}, \vec{c})\), where \(p_j\) is a Boolean "argument \(j\) is poison": \(\mathrm{val}_f\) (the returned bits), \(\mathrm{poison}_f\) (the result is poison) and \(\mathrm{ub}_f\) (the execution has immediate UB). Each instruction contributes its operation (bvadd, bvshl, …), its poison condition (the flag conditions of Definition 13.8.6 as bit-vector predicates, e.g. nsw on add as "the 9-bit sign-extended sum has two different top bits"), and its UB condition (a zero divisor).

Definition 13.9.2 (Refinement query)

\(t\) refines \(s\) (Definition 13.8.2) iff the formula

\[ \exists \vec{x}, \vec{p}, \vec{c}_t .\ \forall \vec{c}_s .\ \neg \mathrm{ub}_s \land \big( \mathrm{ub}_t \lor (\neg \mathrm{poison}_s \land (\mathrm{poison}_t \lor \mathrm{val}_s \ne \mathrm{val}_t)) \big) \]

is unsatisfiable; a model is a counterexample. Without nondeterminism in the source the \(\forall\) disappears and the query is a quantifier-free bit-vector (QF_BV) satisfiability problem. (Alive2 separates the query into three checks — UB, poison, value — to report which failed.)

Algorithm 13.9.3 (Alive-style verification of a rule)

• Input: a rule \(L \to R\) with precondition \(P\), symbolic constants \(\vec{C}\) and type variables.
• Output: valid, or a counterexample (types, constants, inputs, the failing check).
• Precondition: an SMT solver complete for QF_BV (and for the \(\exists\forall\) fragment when there is nondeterminism).
• Postcondition: valid means every instance with \(P\) true, at every enumerated type assignment, is a refinement (Theorem 13.9.9).
• Invariant: every type assignment already processed is either valid or has produced a counterexample.

function Verify(L → R, P):
    for each assignment τ of widths to the type variables (Alive: all widths 1..64 that type-check):
        φ_s ← Encode(L, τ);  φ_t ← Encode(R, τ)                  # Definition 13.9.1
        for check in [ub, poison, value]:                           # Definition 13.9.2, split
            q ← P(C) ∧ ¬ub_s ∧ (check-specific failure of refinement)
            if Solve(q) = sat(model):
                return counterexample(τ, model, check)
    return valid

Bounded exhaustive checking

Definition 13.9.4 (Width-generic rule and bitwidth independence)

A rule is width-generic if its patterns and constant expressions are defined for every width \(N \ge 1\) (constants given as expressions in \(N\), like \(0\), \(1\), \(-1\), \(N - 1\), rather than as fixed bit patterns). Its validity set is \(\{N \mid\) every instance at width \(N\) is a refinement\(\}\). The rule is bitwidth independent if its validity set is either empty or all of \(\mathbb{N}_{\ge 1}\).

Definition 13.9.5 (Bounded exhaustive check)

A bounded exhaustive check of \(s \Rightarrow t\) at width assignment \(\tau\) evaluates both functions on every input — each argument ranges over \(2^{w}\) bit patterns plus poison (minus poison for noundef arguments) — and on every assignment of the source's and target's nondeterministic choices, and applies Definition 13.8.4.

Algorithm 13.9.6 (Refinement by enumeration)

• Input: straight-line functions \(s\) (source) and \(t\) (target) with the same signature; small widths.
• Output: valid, or the first counterexample in enumeration order with its reason.
• Precondition: \(\prod_j (2^{w_j} + 1) \cdot 2^{F_s + F_t}\) is small enough to enumerate (\(F\) = total width of freeze choices).
• Postcondition: valid iff \(s \sqsupseteq t\) at these widths (Theorem 13.9.10).
• Invariant: every input enumerated so far satisfies Definition 13.8.4.

function Refines(s, t):
    for x in Inputs(s):                       # odometer, last argument fastest; each 0 .. 2^w − 1, then poison
        S ← { Run(s, x, c) | c ∈ Choices(s) }  # outcome set: values, poison, UB
        if UB ∈ S: continue                   # anything is allowed
        for c in Choices(t):
            o ← Run(t, x, c)
            if o = UB:                              return invalid(x, "target has undefined behavior where source does not")
            if o = poison and poison ∉ S:          return invalid(x, "target is more poisonous than source")
            if o is a value, poison ∉ S, o ∉ S:    return invalid(x, "value mismatch")
    return valid

function Run(f, x, c):                       # Definitions 9.7.1-9.7.4 and 13.8.1
    env ← x;  k ← 0
    for i in f:
        if i is freeze: env[i] ← env[op] if env[op] ≠ poison else c[k]; k ← k + 1
        else: env[i] ← Eval(i, env)          # may return UB: stop with UB
    return env[returned value]

This is the lab's ch13-rewrite-check (Part B) and the oracle of the drill rewrite-validity.

Translation validation and verified compilers

Definition 13.9.7 (Translation validator and verified compiler)

A translation validator for a compiler \(C\) is a program \(V\) with \(V(p, C(p)) = \mathit{true} \Rightarrow p \sqsupseteq C(p)\) (sound; it may answer "don't know"). A verified compiler is a compiler \(C\) with a machine-checked proof that for every source \(p\) with \(C(p) = \mathit{OK}(q)\), \(q\) refines \(p\) (for CompCert: a backward simulation from the assembly semantics of \(q\) to the C semantics of \(p\)) [Ler09].

Algorithm 13.9.8 (Translation validation of an optimization pipeline)

• Input: a module \(M\) and a pass pipeline \(\Pi = \pi_1, \dots, \pi_k\).
• Output: the optimized module, and for each pass and function a verdict: correct, incorrect (with a counterexample) or unknown (timeout, unsupported feature).
• Precondition: a sound refinement checker for pairs of functions (Alive2's alive-tv).
• Postcondition: if every verdict is correct, the final module refines \(M\) (Theorem 13.8.3, transitivity).
• Invariant: \(M_j\) refines \(M\) whenever all verdicts up to pass \(j\) are correct.

function ValidatePipeline(M, Π):
    M_0 ← M
    for j in 1..k:
        M_j ← π_j(M_{j−1})
        for f in functions changed by π_j:
            verdict[j, f] ← Check(M_{j−1}.f, M_j.f)            # alive-tv, per function
            if verdict[j, f] = incorrect: report(π_j, f, counterexample)
    return M_k, verdict

3. Worked example

Running example: the rule R11 add nsw x, x \(\Rightarrow\) shl nsw x, 1, its variant with nuw on the target, and the mask rule and x, 255 \(\Rightarrow\) x.

SMT-based verification

Encoding at \(N = 8\) (Definition 13.9.1), the query of the box in §7:

component	formula
\(\mathrm{val}_s\)	bvadd x x
\(\mathrm{poison}_s\)	top two bits of the 9-bit bvadd (sext x) (sext x) differ (signed overflow)
\(\mathrm{val}_t\)	bvshl x #x01
\(\mathrm{poison}_t\) (nsw)	bvashr of the result by 1 \(\ne x\) (a shifted-out bit differs from the sign)
\(\mathrm{poison}_t\) (nuw)	bvlshr of the result by 1 \(\ne x\) (a set bit shifted out)
query	\(\neg\mathrm{poison}_s \land (\mathrm{poison}_t \lor \mathrm{val}_s \ne \mathrm{val}_t)\) (no UB here)

Z3 answers unsat for nsw (valid) and sat with \(x\) = #xc0 (\(-64\)) for nuw: \(-64 + -64 = -128\) has no signed overflow, but shl shifts out a set bit.

Bounded exhaustive checking

Algorithm 13.9.6 on add nsw x, x \(\Rightarrow\) shl nuw x, 1 at \(\texttt{i}8\): inputs in the order \(0, 1, \dots, 255\), poison:

input \(x\) (signed)	source	target	allowed?
0 … 63	\(2x\)	\(2x\) (no set bit shifted out)	yes
64 … 127	poison (signed overflow)	—	yes (source poison)
\(-128\) … \(-65\) (128 … 191)	poison	—	yes
\(-64\) (192)	\(-128\)	poison (bit 7 of 192 is shifted out)	no: the first counterexample

The lab's checker prints input: %x = -64, source: -128, target: poison (tests/ch13/lab/rewrite-check.test). For and x, 255 \(\Rightarrow\) x: at \(\texttt{i}8\) all 257 inputs pass (255 is all ones); at \(\texttt{i}9\) the first failure is \(x = 256\) (printed as \(-256\)): source 0, target 256 — the box in §7.

Translation validation and verified compilers

Algorithm 13.9.8 with \(\Pi\) = instcombine on @f(x, y) = -((x & y) + (x | y)) written as ~s + 1 with nsw adds: InstCombine produces sub nsw 0, (add nsw x, y) (it used \((x \& y) + (x | y) = x + y\) and \(\sim s + 1 = -s\)); alive-tv in.ll out.ll reports 1 correct transformation (box in §7). The flags are the interesting part: InstCombine kept nsw on both new instructions, and the validator confirms that this is justified.

Try it

./course drill rewrite-validity --seed 5 --difficulty hard --solution runs Algorithm 13.9.6 and lists how many of the inputs are counterexamples; lab Part B asks you to build the same algorithm on real LLVM IR.

4. Invariants and correctness

SMT-based verification

Theorem 13.9.9 (The refinement query is sound and complete for a fixed width)

For fixed widths, the formula of Definition 13.9.2 is unsatisfiable iff \(s \sqsupseteq t\) (Definition 13.8.2), provided the encodings are faithful (each formula holds exactly for the executions of Definition 13.8.1).

Proof

Fix the widths; faithfulness means that for every \((\vec{x}, \vec{p})\) and choices, the three formulas are true exactly for the corresponding execution's outcome. Satisfiable implies not a refinement: take a model \((\vec{x}, \vec{p}, \vec{c}_t)\). Because the body holds for every source choice \(\vec{c}_s\): no source execution on this input has UB, so \(\mathsf{UB} \notin \mathcal{B}(s)\); and either the target execution with \(\vec{c}_t\) has UB, or no source execution is poison and the target outcome (poison, or a value different from every source value) is not in \(\mathcal{B}(s)\). Either way the target outcome is not in \(\overline{\mathcal{B}(s, \vec{x})}\) (Definition 13.8.2). Not a refinement implies satisfiable: if some input \(\vec{x}\) and target choice \(\vec{c}_t\) give an outcome \(o \notin \overline{\mathcal{B}(s, \vec{x})}\), then UB is not a source behavior, and \(o\) is UB, or poison is not a source behavior and \(o\) is poison or a value no source execution returns; so \((\vec{x}, \vec{c}_t)\) satisfies the body for every \(\vec{c}_s\). Z3 decides QF_BV and, by quantifier instantiation, the \(\exists\forall\) bit-vector fragment that Alive2 uses for nondeterminism [LLM+21].

Bounded exhaustive checking

Theorem 13.9.10 (Enumeration decides refinement at fixed widths)

Algorithm 13.9.6 terminates and returns valid iff \(s \sqsupseteq t\) at the given widths; when it returns a counterexample, the input and the reason are correct.

Proof

Termination: the sets of inputs and of choices are finite, and each run is a straight-line execution. Soundness of invalid: each return reports an input \(x\) and a target outcome \(o\) from a real target execution, with \(\mathsf{UB} \notin S\) and \(o \notin \overline{S}\) by the three tests, where \(S\) is exactly \(\mathcal{B}(s, x)\) (all source choices were run): Definition 13.8.4 fails. Completeness: if refinement fails, some input \(x\) and target choice give an outcome outside \(\overline{\mathcal{B}(s, x)}\); the loops reach that pair, and one of the three tests fires (they partition the ways to be outside the closure). Invariant: an input is passed only after all target choices were accepted.

Proposition 13.9.11 (Bitwidth independence: a positive case and three caveats)

(a) A width-generic rule built only from and, or, xor and the constants \(0\) and \(-1\) (all ones), without flags, is bitwidth independent; so it is valid for all \(N\) iff it is valid at \(N = 1\). (b) R11 add nsw x, x \(\Rightarrow\) shl nsw x, 1 is valid at every \(N \ge 2\) and invalid at \(N = 1\). (c) and x, 255 \(\Rightarrow\) x is valid for \(N \le 8\) (where 255 is \(-1\)) and invalid for every \(N \ge 9\). (d) Hence no fixed finite set of checked widths implies validity for all widths in general.

Proof

(a) The bitwise operations act on each bit position independently with the same Boolean function, the constants \(0\) and \(-1\) have the same bit (0 resp. 1) in every position, and poison propagates identically at every width (P-Op); so the rule at width \(N\) is \(N\) copies of the rule at width 1, and fails at \(N\) iff it fails at 1 (a failing bit position at width \(N\) is a failing instance at width 1, and conversely replicate the width-1 counterexample in every position). (b) At \(N \ge 2\): shl nsw x, 1 computes \(2x \bmod 2^N\) and is poison iff \(2x\) (signed) leaves \([-2^{N-1}, 2^{N-1})\), exactly when add nsw x, x is poison; values agree. At \(N = 1\) the shift amount \(1 \ge N\) makes shl poison for every input, while add nsw i1 0, 0 = 0 is defined (Alive's counterexample in §7). (c) At \(N \le 8\) the constant \(255 \bmod 2^N\) is all ones. At \(N \ge 9\), \(x = 256\) gives \(256 \mathbin{\&} 255 = 0 \ne 256\). (d) Take the rule family and x, 2^M - 1 \(\Rightarrow\) x: valid exactly for \(N \le M\); checking widths up to \(M\) says nothing about \(M + 1\).

When it breaks. A bounded check is a proof for the widths checked and a test for all others. The rules most exposed are those with literal constants (whose meaning depends on \(N\)), shift amounts related to \(N\), and flags whose conditions involve \(2^{N-1}\). Alive therefore checks every feasible width up to 64, and Alive-FP handles FP formats with their own caveats (a half-precision proof does not transfer to double: rounding boundaries move) [MNG16].

Translation validation and verified compilers

Theorem 13.9.12 (Validated runs are correct; verified compilers are correct on every run)

(a) If every verdict of Algorithm 13.9.8 is correct, the output module refines the input. (b) If CompCert's main theorem holds (a Coq proof), then every successful CompCert compilation of a C program without undefined behavior yields assembly whose behaviors are behaviors of the C program.

Proof sketch (full proof of (b): [Ler09, §3]; CompCert driver/Compiler.v, transf_c_program_correct)

(a) Each verdict establishes \(M_{j-1}.f \sqsupseteq M_j.f\) for the changed functions; unchanged functions are trivially refined; refinement of each function lifts to the module (calls are contexts, Theorem 13.8.11 generalized to calls in [LLM+21]), and Theorem 13.8.3 chains the passes. (b) CompCert composes, for each of its roughly 20 passes, a machine-checked simulation proof into a backward simulation from the target's semantics to the source's; a backward simulation implies that every behavior of the compiled program is a behavior of the source (or the source has UB). The trusted base is the Coq kernel, the formal semantics of C and assembly, and the unverified parts (parsing, printing, assembling). Translation validation's trusted base is the validator (and its SMT solver) instead, and it can answer unknown.

5. Complexity

Technique	Time (worst)	Time (typical)	Space	Variables
SMT-based verification	QF_BV satisfiability is NEXPTIME-complete in the bit-vector widths given in binary (NP-complete for widths in unary); \(\exists\forall\) is harder	seconds for peepholes; multiplication and division at 64 bits can time out	solver-dependent	widths, pattern size
Bounded exhaustive checking	\(O\big(\prod_j (2^{w_j} + 1) \cdot 2^{F_s + F_t} \cdot n\big)\)	\(< 0.1\) s for two i8 arguments	\(O(2^{F_s})\)	\(w_j\) argument widths, \(F\) freeze bits, \(n\) instructions
Translation validation	one refinement query per changed function per pass	minutes for a large module with timeouts	—	—
Verified compiler	proof effort once (person-years)	generated code comparable to gcc -O1 [Ler09]	—	—

Justification. Enumeration: each input needs \(2^{F_s}\) source runs and \(2^{F_t}\) target runs (at most), each linear in \(n\). SMT: bit-blasting a \(w\)-bit multiplication produces \(\Theta(w^2)\) clauses, and hard instances are exponential in the number of variables; Alive2's paper reports timeouts on large multiplications and divisions [LLM+21]. Pathological family: a rule over three i32 arguments has \((2^{32}+1)^3 \approx 8 \cdot 10^{28}\) inputs — beyond any enumeration, while an SMT solver proves (x & y) + (x | y) = x + y at 32 bits instantly. Conversely, udiv i64 %x, %d rules can make Z3 time out while 8-bit enumeration takes milliseconds: the two techniques are complementary.

6. Variants and refinements

SMT-based verification

• Alive → C++ generation [LMNR15]: verified rules become compiler code. Trade-off: only rules expressible in the DSL.
• Alive2's translation of memory, loops (bounded unrolling) and calls [LLM+21]. Trade-off: incompleteness (loops) and timeouts.
• Verified DSLs for back ends: Crocus verifies Cranelift ISLE lowering rules with SMT (VanHattum et al., ASPLOS 2024). Trade-off: rule annotations.

Bounded exhaustive checking

• Exhaustive unit tests of analyses (LLVM ConstantRangeTest, KnownBitsTest, DivisionByConstantTest at 4–12 bits). Trade-off: small widths only.
• Small-scope hypothesis (Jackson's Alloy): most bugs have small counterexamples. Trade-off: a heuristic, not a proof (Proposition 13.9.11).
• Width-generic proofs (e.g., by induction over bit positions for bitwise rules, or SMT with symbolic width) close the gap for some rule classes.

Translation validation and verified compilers

• Necula's validator for GCC by symbolic simulation of loop-free regions [Nec00]; Alive2 opt plugin runs after every pass of opt [LLM+21]. Trade-off: false alarms and timeouts.
• Verified compilers: CompCert (C to assembly) [Ler09]; CakeML (ML); Vellvm (verified LLVM IR semantics and passes). Trade-off: optimizations are limited to what was proven.
• Differential testing (Csmith [YCER11], YARPGen) as the empirical complement: Ch 12.

7. In real compilers

SMT-based verification

alive-tv finds the flag bug in a constant fold

Reproduce (alive-tv from Alive2 commit 01a5ec4, built with cmake -DBUILD_TV=1 -DLLVM_DIR=/opt/llvm-23/lib/cmake/llvm against LLVM 23.1.2 and Z3 4.8.12; later Alive2 commits need an LLVM newer than 23.1.2):

cat > flags.ll <<'EOF'
define i8 @src(i8 %x) {
  %a = add nsw i8 %x, 100
  %r = add nsw i8 %a, 100
  ret i8 %r
}
define i8 @tgt(i8 %x) {
  %r = add nsw i8 %x, -56
  ret i8 %r
}
EOF
alive-tv flags.ll | sed -n '/^Transformation/,$p'

Output (complete):

Transformation doesn't verify!

ERROR: Target is more poisonous than source

Example:
i8 %x = #x98 (152, -104)

Source:
i8 %a = #xfc (252, -4)
i8 %r = #x60 (96)

Target:
i8 %r = poison
Source value: #x60 (96)
Target value: poison

What to notice: Alive2 reports which of the three checks failed ("Target is more poisonous than source"), a model for the input (\(x = -104\); every \(x \in [-128, -73]\) is a counterexample, and the lab's checker reports the first in its order, \(-128\)), and the source's intermediate values: exactly the failure Theorem 13.8.14 (b) predicts.

The refinement query in SMT-LIB, solved by Z3

Reproduce (z3 4.8.12; any OS):

cat > q.smt2 <<'EOF'
; add nsw i8 %x, %x  =>  shl nsw i8 %x, 1 (query 1)  and  =>  shl nuw i8 %x, 1 (query 2)
(declare-const x (_ BitVec 8))
(define-fun sum9 () (_ BitVec 9) (bvadd ((_ sign_extend 1) x) ((_ sign_extend 1) x)))
(define-fun src_poison () Bool (not (= ((_ extract 8 8) sum9) ((_ extract 7 7) sum9))))
(define-fun src_val () (_ BitVec 8) (bvadd x x))
(define-fun tgt_val () (_ BitVec 8) (bvshl x #x01))
(define-fun tgt_poison_nsw () Bool (not (= (bvashr tgt_val #x01) x)))
(define-fun tgt_poison_nuw () Bool (not (= (bvlshr tgt_val #x01) x)))
(push)
(assert (and (not src_poison) (or tgt_poison_nsw (not (= src_val tgt_val)))))
(check-sat)
(pop)
(push)
(assert (and (not src_poison) (or tgt_poison_nuw (not (= src_val tgt_val)))))
(check-sat)
(get-value (x))
(pop)
EOF
z3 q.smt2

Output (complete):

unsat
sat
((x #xc0))

What to notice: the encoding of §3 by hand: the first query (target shl nsw) is unsat — no input makes the target fail, so R11 is valid at i8 — and the second (target shl nuw) is sat with \(x\) = #xc0 \(= -64\), the counterexample the bounded check found (Theorem 13.9.9).

Bounded exhaustive checking

Bitwidth caveats: small widths prove and refute

Reproduce (the lab's reference ch13-rewrite-check; alive of Alive2 commit 01a5ec4):

for w in 8 9; do
  cat > mask$w.ll <<EOF
define i$w @src(i$w %x) {
  %r = and i$w %x, 255
  ret i$w %r
}
define i$w @tgt(i$w %x) {
  ret i$w %x
}
EOF
  echo "=== i$w"; ch13-rewrite-check mask$w.ll
done
cat > i1.opt <<'EOF'
Name: add-self-to-shl
%r = add nsw %x, %x
  =>
%r = shl nsw %x, 1
EOF
echo "=== alive, all widths"; alive i1.opt | sed -n '/^ERROR/,/^Target value/p'

Output (complete):

=== i8
valid: @tgt refines @src (257 inputs)
=== i9
invalid: value mismatch
input: %x = -256
source: 0
target: -256
=== alive, all widths
ERROR: Target is more poisonous than source for i1 %r

NOTE: The counterexample is unique.

Example:
i1 %x = #x0 (0)
Source value: #x0 (0)
Target value: poison

What to notice: and x, 255 \(\Rightarrow\) x is valid at i8 and invalid at i9 (Proposition 13.9.11 (c)); Alive's DSL tool, which tries every width for a width-generic rule, finds R11's failure at i1 (Proposition 13.9.11 (b)) — the reason exercise E2 restricts R11 to widths \(\ge 2\).

LLVM tests its division magic numbers exhaustively

Reproduce (LLVM 23.1.2 sources; curl):

curl -sL https://raw.githubusercontent.com/llvm/llvm-project/llvmorg-23.1.2/llvm/unittests/Support/DivisionByConstantTest.cpp \
  | sed -n '/^TEST(SignedDivisionByConstantTest, Test) {/,/^      EnumerateAPInts(Bits, \[Divisor, Magics, Bits\]/p'

Output (complete):

TEST(SignedDivisionByConstantTest, Test) {
  for (unsigned Bits = 1; Bits <= 32; ++Bits) {
    if (Bits < 3)
      continue; // Not supported by `SignedDivisionByConstantInfo::get()`.
    if (Bits > 12)
      continue; // Unreasonably slow.
    EnumerateAPInts(Bits, [Bits](const APInt &Divisor) {
      if (Divisor.isZero())
        return; // Division by zero is undefined behavior.
      SignedDivisionByConstantInfo Magics;
      if (!(Divisor.isOne() || Divisor.isAllOnes()))
        Magics = SignedDivisionByConstantInfo::get(Divisor);
      EnumerateAPInts(Bits, [Divisor, Magics, Bits](const APInt &Numerator) {

What to notice: the signed-division test enumerates every divisor and every dividend for widths 3 to 12 and compares the magic-number sequence with APInt::sdiv — a bounded exhaustive check of the algorithm of Lesson 13.7 (llvm/unittests/Support/DivisionByConstantTest.cpp), accepting that it proves nothing directly about 32 and 64 bits.

Alive2 on floating point: signed zeros

Reproduce (alive-tv, Alive2 commit 01a5ec4):

cat > fp.ll <<'EOF'
define double @src(double %x) {
  %r = fadd double %x, 0.0
  ret double %r
}
define double @tgt(double %x) {
  ret double %x
}
EOF
sed 's/fadd double/fadd nsz double/' fp.ll > fpnsz.ll
echo "=== fadd x, 0.0 => x";     alive-tv fp.ll | sed -n '/^Transformation/p;/^ERROR/,/^Target value/p'
echo "=== fadd nsz x, 0.0 => x"; alive-tv fpnsz.ll | grep '^Transformation'

Output (complete):

=== fadd x, 0.0 => x
Transformation doesn't verify!
ERROR: Value mismatch

Example:
double %x = #x8000000000000000 (-0.0)

Source:
double %r = #x0000000000000000 (+0.0)

Target:
Source value: #x0000000000000000 (+0.0)
Target value: #x8000000000000000 (-0.0)
=== fadd nsz x, 0.0 => x
Transformation seems to be correct!

What to notice: Alive2's FP encoding (the successor of Alive-FP [MNG16]) finds \(x = -0.0\) for x + 0.0 → x and proves the rewrite once nsz is present, exactly Proposition 13.8.16 (b).

Translation validation and verified compilers

Translation validation of one instcombine run

Reproduce (opt 23.1.2, alive-tv; any OS):

cat > in.ll <<'EOF'
define i8 @f(i8 %x, i8 %y) {
  %a = and i8 %x, %y
  %o = or i8 %x, %y
  %s = add nsw i8 %a, %o
  %n = xor i8 %s, -1
  %r = add nsw i8 %n, 1
  ret i8 %r
}
EOF
opt -passes=instcombine -S in.ll -o out.ll
sed -n '/^define/,/^}/p' out.ll
alive-tv in.ll out.ll | sed -n '/^Transformation/p;/^Summary/,$p'

Output (complete):

define i8 @f(i8 %x, i8 %y) {
  %s = add nsw i8 %x, %y
  %r = sub nsw i8 0, %s
  ret i8 %r
}
Transformation seems to be correct!
Summary:
  1 correct transformations
  0 incorrect transformations
  0 failed-to-prove transformations
  0 Alive2 errors

What to notice: InstCombine rewrote four instructions into two, keeping nsw on both; alive-tv in.ll out.ll validates this particular run (Algorithm 13.9.8 with one pass). Alive2 also ships an opt plugin that does this after every pass of a pipeline.

CompCert's correctness theorem

Reproduce (CompCert 3.15 sources; curl):

curl -sL https://raw.githubusercontent.com/AbsInt/CompCert/v3.15/driver/Compiler.v | grep -A3 '^Theorem transf_c_program_correct:'

Output (complete):

Theorem transf_c_program_correct:
  forall p tp,
  transf_c_program p = OK tp ->
  backward_simulation (Csem.semantics p) (Asm.semantics tp).

What to notice: the whole compiler's correctness is one Coq theorem: if compilation succeeds (= OK tp), there is a backward simulation from the assembly semantics to the C semantics — Theorem 13.9.12 (b); the value-numbering pass of Lesson 13.1 contributes one link of that chain (backend/CSEproof.v).

8. Comparison

Technique	Power / precision	Speed (asymptotic · practical)	Output / error quality	Implementation effort	Typical use
SMT-based verification (Alive, Alive2, Alive-FP)	Complete for fixed widths, all widths up to 64; memory and FP supported; loops bounded	NP-hard · seconds, timeouts on wide mul/div	Counterexample with the failing check	Very high (semantics in SMT)	Proving InstCombine rules; validating LLVM's test suite
Bounded exhaustive checking	Complete at small widths only; a test beyond them	Exponential in total input bits · instant at 8 bits	First counterexample in a fixed order	Low (an interpreter)	Unit tests of analyses; drills; the lab's checker; quick rule screening
Translation validation and verified compilers	TV: per run, may say unknown; CompCert: all runs, fewer optimizations	TV: per pass per function; CompCert: normal compile	TV: counterexamples; CompCert: no bugs in verified parts [YCER11]	TV high; verified compiler very high	Alive2 over LLVM; CompCert in safety-critical code

Choose SMT verification for every rule that goes into a production compiler (the LLVM guide requires Alive2 proofs). Choose bounded exhaustive checking when you need an independent, trivially trustworthy oracle at small widths — and then argue bitwidth independence or check with SMT. Choose translation validation to find bugs in an existing optimizer on real inputs; choose a verified compiler when every compilation must be correct and a smaller optimizer is acceptable.

9. Assessment

Technique	Quiz questions	Drills	Flashcards	Exercises
SMT-based verification	smt-query, alive-checks	./course drill rewrite-validity (the same question, answered by enumeration)	tag smt	—
Bounded exhaustive checking	bounded-width, bounded-inputs	./course drill rewrite-validity	tag bounded	Lab Part B (ch13-rewrite-check)
Translation validation and verified compilers	tv-vs-verified, compcert-theorem	justification: a translation validator is Algorithm 13.9.6 applied per pass; the drill covers the check itself	tag translation-validation	Lab Part B cross-check with instcombine (rewrite-check-llvm.test)

References

See the chapter references.