Lesson 12.8 — Translation validation: Pnueli, Necula, Alive and Alive2¶

Techniques: translation validation (Pnueli, Siegel and Singerman 1998): check each compilation instead of the compiler; Necula's validator for an optimizing compiler (2000): symbolic evaluation with an inferred simulation relation; Alive (Lopes et al. 2015): SMT-based verification of peephole rewrites for all bit widths; Alive2 (Lopes et al. 2021): bounded translation validation of whole LLVM functions with undef, poison and memory · Pebble implements: nothing to write — the lesson validates your pebble-strength with a 250-line validator (chapters/12-passes-and-testing/examples/tv.py) and with Alive2 · Drill: peephole-verify · Prerequisites: Lesson 12.3, Ch 9 Lesson 9.7 · Time: 4–5 hours

Every technique so far tests: it runs some programs and hopes to hit the bug. The lab's bug 5 (an nsw flag added where it is not justified) passed every differential test, because lli never shows poison. A proof would have caught it. Proving a whole optimizer correct is a research project (CompCert took years); translation validation proves something smaller and mechanical — this output refines this input — after every compilation, with an SMT solver doing the work. Alive2 does this for LLVM every day and has found hundreds of miscompilations in InstCombine and elsewhere [LLH+21].

1. Problem and motivation¶

Translation validation¶

Verifying a compiler means proving $\forall P.\ C(P) \sqsupseteq P$ — hard, and invalidated by every change. Pnueli, Siegel and Singerman [PSS98] proposed to leave the compiler alone and build a validator that, for each run, checks $C(P) \sqsupseteq P$ for the particular $P$, and either certifies it or raises an alarm. Their target was the SIGNAL-to-C translator; the idea applies to any compiler, and the validator is much simpler than the compiler.

Necula's validator¶

An optimizing compiler changes the control flow, reorders, merges and deletes computations, so the source and target programs do not correspond step by step. Necula [Nec00] validated GCC's optimizer (common subexpression elimination, loop unrolling, register allocation, scheduling) by symbolic evaluation of the two programs side by side, inferring a simulation relation — equalities between source and target variables at matching program points — from a few heuristics about the transformations, and proving the resulting verification conditions with a simple arithmetic decision procedure.

Alive¶

LLVM's InstCombine has thousands of peephole rewrites, each with subtle side conditions about flags, undef and poison. Lopes, Menendez, Nagarakatte and Regehr's Alive [LMNR15] expresses a rewrite in a small DSL, encodes "the target refines the source" as SMT queries over bit vectors for every feasible type, and returns either a proof or a concrete counterexample. It also infers the strongest nsw/nuw/exact flags a target may carry — the question of Theorem 12.3.10.

Alive2¶

Alive checks rewrite rules; bugs also live in whole passes. Alive2 [LLH+21] validates LLVM IR functions before and after a pass (translation validation in Pnueli's sense), with a formal semantics for undef, poison, freeze, memory and calls, and bounded handling of loops (unrolled up to a limit). It runs as alive-tv, as an opt/clang plugin and over LLVM's own test suite.

2. Definitions and algorithms¶

Definition 12.8.1 (Outcomes of straight-line IR)

For a function $f$ over integer arguments and an argument vector $\vec{a}$ in which each component is a bit vector or poison, the outcome $\llbracket f \rrbracket(\vec{a})$ is $\mathsf{UB}$ if execution performs immediate undefined behavior (division by zero, sdiv INT_MIN, -1, branching on poison, ...), otherwise the returned value, which is a bit vector or poison (Definition 12.3.1 gives the operations).

Definition 12.8.2 (Refinement)

A target $t$ refines a source $s$, written $t \sqsupseteq s$, if for every argument vector $\vec{a}$: $\llbracket s \rrbracket(\vec{a}) = \mathsf{UB}$, or ($\llbracket t \rrbracket(\vec{a}) \ne \mathsf{UB}$ and ($\llbracket s \rrbracket(\vec{a}) = \mathrm{poison}$ or $\llbracket t \rrbracket(\vec{a}) = \llbracket s \rrbracket(\vec{a})$)). With undef, "the value" becomes a set of values and the condition becomes inclusion: every value the target can produce must be one the source can produce.

Translation validation¶

Definition 12.8.3 (Validator)

A validator is a procedure $V(S, T) \in \{\mathsf{valid}, \mathsf{invalid}(\vec{a}), \mathsf{unknown}\}$. It is sound if $V(S, T) = \mathsf{valid} \Rightarrow T \sqsupseteq S$, and its counterexamples are genuine if $\mathsf{invalid}(\vec{a})$ implies that $\vec{a}$ violates Definition 12.8.2.

Algorithm 12.8.4 (Translation validation of one compiler run, SMT encoding for straight-line code)

Input: source $S$ and target $T = C(S)$, loop-free, same signature.
Output: $\mathsf{valid}$, or a counterexample $\vec{a}$.
Precondition: every operation has a bit-vector encoding (Definition 12.3.1).
Postcondition: $\mathsf{valid}$ iff $T \sqsupseteq S$ (Theorem 12.8.9).
Invariant: after encoding instruction $v$, $(\mathit{val}_v, \mathit{poi}_v)$ are SMT terms for its value and poison bit, and $\mathit{ub}$ is the disjunction of the UB conditions of the instructions encoded so far.

function Validate(S, T):
    for each argument a: val_a ← fresh bit vector; poi_a ← fresh boolean       # shared by S and T
    (vS, pS, ubS) ← Encode(S); (vT, pT, ubT) ← Encode(T)
    φ ← ¬ubS ∧ (ubT ∨ (¬pS ∧ (pT ∨ vS ≠ vT)))       # "some input violates refinement"
    if SMT(φ) = unsat: return valid
    return invalid(model of φ restricted to the arguments)

function Encode(F):
    ub ← false
    for each instruction v = op(x, y) in order:
        val_v ← bvop(val_x, val_y)
        poi_v ← poi_x ∨ poi_y ∨ FlagViolation(op, flags, val_x, val_y)   # nsw, nuw, exact, shift ≥ width
        if op is a division or remainder: ub ← ub ∨ poi_y ∨ val_y = 0 ∨ (signed ∧ val_x = INT_MIN ∧ val_y = −1)
    return (val_ret, poi_ret, ub)

Necula's validator¶

Definition 12.8.5 (Simulation relation)

Let $S$ and $T$ be programs with control points $p$ (source) and $q$ (target). A simulation relation is a set of pairs of points $(p, q)$, each with a formula $\rho_{p,q}$ over the variables of both programs (typically equalities $x_S = e(y_T)$ and facts about memory), containing the entries and the exits, such that for every source path from $p$ to the next related point $p'$ there is a target path from $q$ to a related $q'$ with $\rho_{p,q} \land \text{(path conditions)} \Rightarrow \rho_{p',q'}$ after symbolically executing both paths.

Algorithm 12.8.6 (Necula-style validation by symbolic evaluation, after [Nec00])

Input: $S$, $T$ (the compiler's input and output for one function).
Output: $\mathsf{valid}$ or $\mathsf{unknown}$ (with the failing condition).
Precondition: loops of $S$ correspond to loops of $T$ (the checked transformations preserve loop structure, possibly unrolled).
Postcondition: $\mathsf{valid}$ only if every verification condition was proved (Theorem 12.8.10).
Invariant: the relation built so far contains the entry pair and every pair reached by the symbolic evaluation.

function NeculaValidate(S, T):
    R ← {(entry_S, entry_T) with ρ = "arguments equal, memories equal"}
    worklist ← [(entry_S, entry_T)]
    while worklist ≠ []:
        (p, q) ← pop(worklist)
        for each branch outcome b of the source path from p to its next cut point p' (loop header or exit):
            find the target path from q with the corresponding branch condition to a cut point q'   # branches are
                                                               # matched by comparing their symbolic conditions
            σS, σT ← symbolic states after executing the two paths from ρ_{p,q}
            if (p', q') ∉ R: guess ρ_{p',q'} from σS, σT (equal symbolic values ⇒ equal variables); add; push
            VC ← ρ_{p,q} ∧ cond_S ∧ cond_T ⇒ ρ_{p',q'}(σS, σT) ∧ (cond_S ⇔ cond_T)
            if not Prove(VC): return unknown(VC)       # arithmetic + uninterpreted-function reasoning
    return valid

Alive¶

Algorithm 12.8.7 (Alive: verifying a rewrite rule for all types, after [LMNR15])

Input: a rule src => tgt over typed variables and constants, with an optional precondition.
Output: "correct" for every feasible type assignment, or a counterexample with types.
Precondition: finitely many feasible type assignments (Alive bounds widths, e.g. up to 64 bits).
Postcondition: "correct" iff for every feasible typing, under the precondition, tgt refines src (including undef: target values must be possible source values).
Invariant: each checked typing contributed one closed SMT query.

function Alive(rule):
    for each type assignment τ satisfying the rule's typing constraints (widths 1..64 bits):
        encode src and tgt under τ as in Algorithm 12.8.4, constants C as fresh variables
        φ ← Pre(C) ∧ ∃ inputs, src-undefs ∀ tgt-undefs: ¬ubS ∧ (ubT ∨ (¬pS ∧ (pT ∨ vS ≠ vT)))
        if SMT(φ) = sat: return counterexample(τ, model)
    return correct

Flag inference: for each nsw/nuw/exact position in tgt, ask whether the rule stays correct with the flag added; keep the flags for which it does.

Alive2¶

Algorithm 12.8.8 (Alive2: bounded translation validation of functions, after [LLH+21])

Input: LLVM IR functions src and tgt (or a module and a pass pipeline, validated per function); unroll bounds $k_S, k_T$.
Output: "correct", a counterexample, or "failed to prove" (timeout, unsupported feature, approximation).
Precondition: the functions are not inter-procedurally transformed (Alive2 checks one function at a time).
Postcondition: "correct" means: for all inputs and all executions that stay within the unroll bounds, tgt refines src (Definition 12.8.2 extended to memory and to executions that do not return).
Invariant: each loop body is copied at most $k$ times; paths that would need more iterations are cut off (they neither prove nor refute).

function Alive2(src, tgt, kS, kT):
    S ← Unroll(src, kS); T ← Unroll(tgt, kT)          # loops become DAGs of k copies
    encode S and T symbolically: values, poison, undef (as quantified variables), memory as SMT arrays of blocks,
        calls to unknown functions as uninterpreted functions with shared behavior
    check, in order: preconditions of both are consistent; the source can return (else "doesn't reach a return");
        ¬UB(S) ⇒ ¬UB(T); return values refine; final memories refine
    report the first violated check with a model, or correct

3. Worked example¶

The running example is the Chapter 12 strength reduction sdiv x, 4 ⇒ the biased shift sequence (Algorithm 12.3.4), and the wrong alternative ashr x, 2, at width i4 (values $-8..7$), where exhaustion replaces the SMT solver (the drill's oracle). Definition 12.8.2 is checked input by input:

$x$	`sdiv x, 4`	biased sequence	refines?	`ashr x, 2`	refines?
−8	−2	−2	✓	−2	✓
−7	−1	−1	✓	−2	✗
−6	−1	−1	✓	−2	✗
−5	−1	−1	✓	−2	✗
−4	−1	−1	✓	−1	✓
−3	0	0	✓	−1	✗
−2	0	0	✓	−1	✗
−1	0	0	✓	−1	✗
0 … 7	$\lfloor x/4 \rfloor$	same	✓	same	✓
poison	poison	poison	✓ (source poison)	poison	✓

No input makes the source UB (the divisor is the constant 4). The biased sequence refines on all 17 inputs; ashr fails on the six negative non-multiples of 4, exactly Theorem 12.3.9(1). For the flag question, Algorithm 12.8.4 on mul nsw i4 %x, -8 ⇒ shl nsw i4 %x, 3 gives $\varphi$ satisfiable with $x = 1$: the source is $-8$ (defined), the target poison (Theorem 12.3.10). An SMT solver answers the same questions for $i32$, where exhaustion needs $2^{32}$ cases.

Try it

./course drill peephole-verify --seed 5 --difficulty hard --solution checks five rewrites from this chapter by exhaustion and prints a witness for every invalid one.

4. Invariants and correctness¶

Theorem 12.8.9 (The SMT encoding is exact for straight-line code)

For loop-free $S, T$ whose operations are those of Definition 12.3.1, $\varphi$ of Algorithm 12.8.4 is satisfiable iff $T \not\sqsupseteq S$, and every model restricted to the arguments is a genuine counterexample.

Proof

By induction on the instructions, $(\mathit{val}_v, \mathit{poi}_v)$ under an assignment of the argument variables equals the value and poison bit of $v$ on those arguments whenever no UB occurred before $v$, and $\mathit{ub}$ is true iff some encoded instruction has UB: each case of Encode transcribes Definition 12.3.1 (bit-vector operations are exactly modular arithmetic; the flag conditions are the definitions of nsw, nuw, exact; a poison or zero divisor is UB). Poison operands propagate by the disjunction. Hence for arguments $\vec{a}$, $\varphi(\vec{a})$ holds iff the source has no UB, and the target has UB, or the source is not poison and the target is poison or different — the negation of Definition 12.8.2 at $\vec{a}$. So $\varphi$ is satisfiable iff some $\vec{a}$ violates refinement, and a model is such an $\vec{a}$. ∎

Theorem 12.8.10 (Soundness of simulation-based validation, after [Nec00])

If Algorithm 12.8.6 returns $\mathsf{valid}$, then for every input on which the source terminates, the target terminates with the same observable result.

Proof sketch (full proof: [Nec00, §2], [PSS98, §3])

Induction on the number of cut points passed by the source execution. Initially $\rho_{\mathrm{entry}}$ holds. If the source is at $p$ and the target at $q$ with $\rho_{p,q}$ true, the source follows some path to $p'$ with its condition true; the proved VC says the corresponding target path has an equivalent condition, hence is the one the target takes, and that $\rho_{p',q'}$ holds after both. At the exits, $\rho$ includes equality of return values and memory. Since the relation is checked for every source path between cut points, the target cannot diverge from the source's control flow in a way the source did not. The argument needs the VC prover to be sound; incompleteness only produces $\mathsf{unknown}$. ∎

Theorem 12.8.11 (Per-run validation composes)

If a sound validator returns $\mathsf{valid}$ for every pass run of a pipeline on $P$, the pipeline's output refines $P$.

Proof

Each run satisfies $P_{i} \sqsupseteq P_{i-1}$ by soundness (Definition 12.8.3); refinement is transitive (Theorem 12.2.11's proof), so $P_k \sqsupseteq P_0$. Note what is not claimed: nothing about other programs — the compiler may still be wrong on inputs nobody validated. ∎

Proposition 12.8.12 (Bounded validation is sound only for bounded executions)

Alive2's "correct" (Algorithm 12.8.8) guarantees refinement for executions that complete within the unroll bounds; a transformation that is wrong only for executions needing more iterations is not detected, and a source whose loops always need more than $k_S$ iterations yields no verdict ("doesn't reach a return").

Proof

After unrolling, the encoded programs represent exactly the executions of at most $k$ iterations per loop, and the refinement check (Theorem 12.8.9, extended to memory) quantifies over those executions only. An execution with more iterations is not represented, so a violation that occurs only there is not a model of the query. If no execution of the source reaches a return within the bound, the source's "returns" condition is unsatisfiable and Alive2 reports that instead of a verdict (§7 shows both cases). ∎

Testing cannot see poison, validation can

The lab's bug 5 (add ⇒ add nsw after folding) produces the same bits in every lli run, so differential testing misses it (Proposition 12.5.12). The validator of Algorithm 12.8.4 finds x = INT_MAX - 1 in milliseconds (§7): the target is poison where the source is defined.

5. Complexity¶

Let $I$ be the number of instructions, $w$ the bit width, $k$ the unroll bound, and $T_{\mathrm{SMT}}$ the solver time.

Technique	Time (worst)	Time (typical)	Space	Notes
Translation validation (SMT, straight-line)	NP-hard: satisfiability of bit-vector formulas of size $O(I \cdot w^2)$ after bit-blasting multiplication	milliseconds for peepholes; the lab's validator, 4 functions in under a second	the formula	decidable (finite widths)
Necula's validator	per pair of paths, one VC; exponential number of paths between cut points in the worst case	seconds per GCC function in [Nec00]	symbolic states per path	cut points at loop headers keep paths short
Alive	$\sum_{\tau}$ one SMT query per feasible typing, with quantifiers for undef	seconds per rule	—	multiplication/division at 64 bits dominate
Alive2	paths $\times$ unroll: formula size $O(k \cdot I)$ per loop, memory as arrays	ms to minutes; timeouts are common (§7)	the formulas	"failed to prove" is a result

Justification. Bit-vector satisfiability with multiplication is NP-complete for fixed width (it encodes circuit satisfiability), and bit-blasting an $w$-bit multiplier yields $O(w^2)$ gates. Pathological family: mul/udiv chains of 64-bit values — each multiplier doubles the circuit, and solvers time out quickly; Alive2 reports "failed to prove" rather than a verdict. In this lesson's §7, a 5-times unrolled loop took 16 s with Ubuntu's Z3 4.8.12, and a branchy pair with shl/add timed out even at 60 s — scale is the practical limit of the method.

Translation validation¶

Credible compilation (Rinard and Marinov, 1999): the compiler emits a proof with each transformation, which a checker validates. Trade-off: the compiler must be modified.
Verified validators (CompCert's validators for register allocation and scheduling, written and proved in Coq). Trade-off: a mechanized proof of the validator itself.

Necula's validator¶

Inference of the relation from compiler hints instead of heuristics. Trade-off: couples validator and compiler.
Equality saturation-based validation (Tate et al., 2009; Stepp et al., 2011): compare programs through an e-graph of equivalent terms. Trade-off: memory for the e-graph.

Alive¶

Alive-FP and Alive-Infer (preconditions synthesized automatically) [LLH+21]. Trade-off: more solver work.
Flag inference (Algorithm 12.8.7): strengthen the target's flags as far as correctness allows.

Alive2¶

opt and clang plugins, alive-tv -passes=... validate every pass of a real pipeline, and a nightly run over llvm/test/Transforms reports unsound tests [Alive2].
Unroll bounds and SMT timeouts trade coverage for time (Proposition 12.8.12).

7. In real compilers¶

Translation validation¶

The course's chapters/12-passes-and-testing/examples/tv.py implements Algorithm 12.8.4 with Z3 for single-block functions; Alive2's alive-tv is the production tool (below); CompCert validates parts of its own pipeline.

Validating runs of pebble-strength and pebble-lab-fold

Reproduce (opt 23.1.2, the course build with the reference solution, z3-solver 5.1.0 via uv; $SOL is that build: SOL=$PWD/build/ci-solutions-linux from the repository root, ci-solutions-macos on macOS):

cat > f.ll <<'EOF'
define i32 @mul8(i32 %x) {
  %r = mul nsw i32 %x, 8
  ret i32 %r
}
define i32 @sdiv4(i32 %x) {
  %r = sdiv i32 %x, 4
  ret i32 %r
}
define i8 @top(i8 %x) {
  %r = mul nsw i8 %x, -128
  ret i8 %r
}
define i32 @fold(i32 %x) {
  %a = add i32 %x, 5
  %b = sub i32 %a, 2
  ret i32 %b
}
EOF
TV="uv run --with z3-solver python chapters/12-passes-and-testing/examples/tv.py"
$TV run --load-pass-plugin $SOL/lib/PebblePasses.so --passes pebble-strength f.ll
$TV run --load-pass-plugin $SOL/lib/Ch12LabPasses.so --passes 'pebble-lab-fold<bug=5>' f.ll

Output:

@mul8: verified
@sdiv4: verified
@top: verified
@fold: verified
@mul8: verified
@sdiv4: verified
@top: verified
@fold: NOT verified: %x = 2147483646: target is poison

What to notice: Pnueli's scheme [PSS98] on two real runs: the reference pebble-strength output refines its input for all $2^{32}$ (or $2^8$) inputs, including the nsw case at $k = N-1$ where the pass must drop the flag (Theorem 12.3.10). The lab's bug 5 is caught with a concrete witness — the bug that differential testing missed (§3 of Lesson 12.5). The exact counterexample value can differ between Z3 versions; any value it prints is genuine (Theorem 12.8.9).

Necula's validator¶

Necula's validator for GCC 2.7 [Nec00] is not distributed; its approach — symbolic evaluation of both programs with a relation at control-flow joins — is what Alive2 does for acyclic control flow (AliveToolkit/alive2, smt/ and tools/transform.cpp, class TransformVerify) [Alive2].

Symbolic evaluation across different control flow

Reproduce (alive-tv from Alive2 commit 01a5ec45 (2026-08-17) built against LLVM 23.1.2 and Z3 4.8.12 — build commands for macOS and Linux in the chapter's tools outside the course toolchain; a newer Alive2 commit needs a matching newer LLVM):

cat > sel.srctgt.ll <<'EOF'
define i32 @src(i32 %x, i1 %c) {
entry:
  br i1 %c, label %t, label %e
t:
  %a = add i32 %x, 1
  br label %j
e:
  %b = add i32 %x, 2
  br label %j
j:
  %r = phi i32 [ %a, %t ], [ %b, %e ]
  ret i32 %r
}
define i32 @tgt(i32 %x, i1 %c) {
entry:
  %d = select i1 %c, i32 1, i32 2
  %r = add i32 %x, %d
  ret i32 %r
}
EOF
alive-tv sel.srctgt.ll | tail -2

Output:

Transformation seems to be correct!

What to notice: the source has four blocks and a phi, the target one block and a select — no step-by-step correspondence. Symbolic evaluation turns both into one term per path condition ($c$: $x + 1$; $\neg c$: $x + 2$), which is Algorithm 12.8.6's relation at the exit, proved for all inputs (and for poison $c$, which is UB in the source's branch).

Alive¶

The Alive DSL lives on in Alive2's alive tool (AliveToolkit/alive2, tools/alive.cpp) [Alive2]; InstCombine patches routinely link Alive2 proofs.

Alive proves one nsw rewrite and refutes the other

Reproduce (the alive tool from the same Alive2 build):

cat > rule.opt <<'EOF'
Name: mul nsw by 64 is shl nsw 6
%r = mul nsw i8 %x, 64
  =>
%r = shl nsw i8 %x, 6

Name: mul nsw by 128 is shl nsw 7
%r = mul nsw i8 %x, 128
  =>
%r = shl nsw i8 %x, 7

Name: mul nsw by 128 is shl 7
%r = mul nsw i8 %x, 128
  =>
%r = shl i8 %x, 7
EOF
alive rule.opt 2>&1 | grep -E '^Name|correct|ERROR|i8 %x =|Source value|Target value'

Output:

Name: mul nsw by 64 is shl nsw 6
Transformation seems to be correct!
Name: mul nsw by 128 is shl nsw 7
ERROR: Target is more poisonous than source for i8 %r
i8 %x = #x01 (1)
Source value: #x80 (128, -128)
Target value: poison
Name: mul nsw by 128 is shl 7
Transformation seems to be correct!

What to notice: Theorem 12.3.10 checked by a solver: with $k = 6 = N - 2$ the flag may stay; with $k = 7 = N - 1$ it may not, and the counterexample is exactly the proof's $x = 1$; dropping the flag makes the third rule correct.

Alive2¶

AliveToolkit/alive2 — tools/alive-tv.cpp (the standalone validator), tv/tv.cpp (the opt/clang plugin), ir/ (the IR semantics), smt/ (the SMT layer) [Alive2].

Alive2 validates an instcombine run and bounds a loop

Reproduce (the same Alive2 build):

cat > f.ll <<'EOF'
define i32 @mul8(i32 %x) {
  %r = mul nsw i32 %x, 8
  ret i32 %r
}
define i32 @sdiv4(i32 %x) {
  %r = sdiv i32 %x, 4
  ret i32 %r
}
define i8 @top(i8 %x) {
  %r = mul nsw i8 %x, -128
  ret i8 %r
}
define i32 @fold(i32 %x) {
  %a = add i32 %x, 5
  %b = sub i32 %a, 2
  ret i32 %b
}
EOF
alive-tv -passes=instcombine f.ll | sed -n '/^Summary/,$p'
cat > loop.srctgt.ll <<'EOF'
define i32 @src(i32 %x) {
entry:
  br label %loop
loop:
  %i = phi i32 [ 0, %entry ], [ %i.next, %loop ]
  %s = phi i32 [ 0, %entry ], [ %s.next, %loop ]
  %s.next = add i32 %s, %x
  %i.next = add i32 %i, 1
  %c = icmp ult i32 %i.next, 4
  br i1 %c, label %loop, label %exit
exit:
  ret i32 %s.next
}
define i32 @tgt(i32 %x) {
  %r = shl i32 %x, 2
  ret i32 %r
}
EOF
for u in 2 5; do echo "src-unroll=$u: $(alive-tv --src-unroll=$u --smt-to=120000 loop.srctgt.ll | grep -E 'correct|ERROR')"; done

Output:

Summary:
  4 correct transformations
  0 incorrect transformations
  0 failed-to-prove transformations
  0 Alive2 errors
src-unroll=2: ERROR: The source program doesn't reach a return instruction.
src-unroll=5: Transformation seems to be correct!

What to notice: alive-tv -passes=instcombine runs the pass itself and validates each function (Algorithm 12.8.8 on a real run). For the loop, Proposition 12.8.12 in action: with 2 unrolled iterations the source never returns and Alive2 gives no verdict; with 5 (the loop runs 4 times) it proves the closed form $4x$ — in about 16 s, a reminder of §5.

8. Comparison¶

Technique	Power / precision	Speed	Output / error quality	Implementation effort	Typical use
Translation validation	Proves each run correct (sound, Theorem 12.8.11); says nothing about unvalidated programs	Solver time per run; ms for peepholes	A concrete counterexample input	Medium: a semantics + an encoding (the course's is ~250 lines)	Checking a pass on its test corpus, bug hunting
Necula's validator	Handles control-flow-changing optimizations via inferred simulation relations; incomplete (unknown)	Seconds per function (2000-era GCC)	The failing verification condition	High	GCC's optimizer in [Nec00]; ideas reused in later validators
Alive	Proves rewrite rules for all feasible types, with undef/poison; infers flags	Seconds per rule	Counterexample with types and values	Low per rule (the DSL)	InstCombine rewrites, flag questions
Alive2	Whole functions, memory, undef/poison, bounded loops (Prop. 12.8.12)	ms to minutes; timeouts	Counterexample, or "failed to prove"	Very low to use	Validating LLVM passes and tests daily; reviewing patches

Choose translation validation when a pass is small enough for a semantics you can encode and you want certainty for its test inputs — it is the only technique here that catches poison-only bugs. Choose Necula-style relations when transformations change control flow and you control the validator. Choose Alive when the question is a rewrite rule or a flag; Alive2 when you have LLVM IR and a pass: it is the de-facto standard for LLVM miscompilation reports.

9. Assessment¶

Quiz: tv-refine (mapping), tv-sound, tv-poison-bug, necula-relation, necula-unknown, alive-flag (number), alive2-unroll.
Drill: ./course drill peephole-verify (exhaustive refinement checks with counterexamples).
Flashcards: tags tv-pnueli, tv-necula, alive, alive2.
Try it: run tv.py run on your own pebble-strength (--load-pass-plugin build/<preset>/lib/PebblePasses.so) and on the lab plugin with bug=1 and bug=2; which counterexample does each produce?

References¶

See the chapter references.

Lesson 12.8 — Translation validation: Pnueli, Necula, Alive and Alive2¶

1. Problem and motivation¶

Translation validation¶

Necula's validator¶

Alive¶

Alive2¶

2. Definitions and algorithms¶

Translation validation¶

Necula's validator¶

Alive¶

Alive2¶

3. Worked example¶

4. Invariants and correctness¶

5. Complexity¶

6. Variants and refinements¶

Translation validation¶

Necula's validator¶

Alive¶

Alive2¶

7. In real compilers¶

Translation validation¶

Necula's validator¶

Alive¶

Alive2¶

8. Comparison¶

9. Assessment¶

References¶