Correctnessimplementation

Translation Validation

Do not prove the optimizer correct — prove that *this* compilation preserved semantics. A checker runs alongside the compiler, compares the IR before and after each transformation, and reports the ones it cannot justify. Alive2 does this for LLVM, and it found bugs that had been shipping for years.

The question

Can I get some of the assurance of a verified compiler without rewriting the compiler in a proof assistant?

Source→Lexing→Tokens→Parsing→AST→Semantics→Typed→IR→Optimize→Codegen→Machine code→Link→Execute
What the program is here

A pair of IR functions — the input to a transformation and its output — plus a formal claim relating them: that every behavior of the target is a permitted behavior of the source. The representation under study is neither program but the *refinement relation* between them, encoded as a logical formula that an SMT solver either proves or supplies a counterexample to.

What this phase may assume or do

The checker is licensed to declare a transformation valid only when the target program refines the source: for every input on which the source is well-defined, the target produces one of the source’s permitted results, and the target introduces no new undefined behavior on such inputs. Refinement is deliberately one-directional — a transformation may reduce nondeterminism or exploit undefined behavior in the source, but never the reverse. Getting that direction backwards is the classic error, and it makes the checker reject every legal optimization that narrows behavior.

Key points

  • Translation validation checks that one particular compilation preserved semantics, rather than proving the optimizer correct for all inputs.
  • It is incremental, applies to the compiler you already have, and produces a concrete counterexample when it fails.
  • The property is refinement, not equality: the target may narrow nondeterminism and may exploit source-level undefined behavior.
  • The bug class that matters most is the reverse direction — a target that is undefined where the source was defined.
  • The check is discharged by an SMT solver, so loops and memory are the practical limits and a timeout is not a verdict.
  • Alive2 is the concrete example for LLVM, and much of what it found concerns undef and poison propagation rather than plain arithmetic.

Validate the compilation, not the compiler

Proving an optimizer correct is a large, slow, all-or-nothing project: every pass must be written in a form a proof assistant can reason about, and adding a pass means adding a proof. Translation validation asks a smaller question that pays out immediately. It does not ask "is this pass correct for all inputs". It asks "was this particular application of it, to this particular function, semantics-preserving".

That change of quantifier is the whole idea and it has three consequences worth stating separately. It is incremental: you can validate one pass today and another next month, and each is useful on its own. It applies to the compiler you already have, in the language it is already written in, with no restructuring. And when it fails, it hands you a concrete counterexample — an input on which the two functions differ — which is a bug report rather than a proof obligation.

What you give up is coverage. A verified compiler makes a statement about every program forever. A validator makes a statement about the compilations it actually checked. If it is run as part of the build, that is every compilation of your code, which is a genuinely useful guarantee; if it is run as a fuzzing harness over generated IR, it is the compilations somebody generated.

Three positions on the same axistypical
ApproachWhat is establishedCostWhat it misses
TestingThese programs behaved correctly this timeLow, ongoingEverything nobody tested — which is most program shapes
Translation validationThis compilation preserved semantics, with a counterexample when it did notModerate; solver time per function, and a formal IR semanticsCompilations that were not checked; passes the checker does not model
Verified compilerEvery compilation of every program preserves semantics, foreverVery high; the compiler must be written for the proofEverything outside the proof: frontend, runtime, specification, hardware

Refinement, and why the direction matters

implementationLLVM’s notion of "undefined" is finer-grained than the C standard’s: it distinguishes undef (an arbitrary value, possibly different at each use) from poison (a deferred error that taints its users) from full undefined behavior. Alive2 models all three, and a large share of the bugs it found are about their interaction. A validator for a different IR needs whatever that IR’s own model is, and getting it wrong produces a checker that is confidently and uselessly wrong.

The relation being checked is not equality of behavior. It is *refinement*: the target must exhibit only behaviors the source was permitted to exhibit. Two asymmetries fall out of that, and both are where people first get confused.

First, a transformation may legitimately reduce nondeterminism. If the source could return either of two values and the target always returns the first, that is a refinement and it is legal. Requiring equality would reject it. Second, and more importantly, undefined behavior in the source is a licence: if the source has undefined behavior on some input, the target may do anything at all on that input and still refine it. Every optimization that exploits [[undefined-behavior]] depends on this, and a checker that demanded equality would flag the entire optimizer.

The direction is what makes the check useful rather than vacuous. Going the other way — the target may have undefined behavior where the source did not — is exactly the bug class that matters most, because it is how an optimizer turns a defined program into an exploitable one. Alive2 found several LLVM bugs of precisely this shape, where a pass introduced poison or undef propagation that the source did not have.

  • Target refines source: every target behavior on a defined input is a permitted source behavior. This is the property.
  • Source undefined on an input: the target is unconstrained there. Optimizations rely on this.
  • Target undefined where the source was defined: a bug, and the most consequential kind.
  • Target more deterministic than the source: legal, and a reason equality is the wrong relation.
  • Target less deterministic than the source: a bug, and one that ordinary testing almost never surfaces.

How a check actually runs

Both functions are translated into logical formulas over their inputs — memory as an array, arithmetic with explicit overflow and poison semantics, control flow encoded as path conditions. The checker then asks a solver whether there exists an input on which the source is well-defined and the target produces a behavior the source could not. If the solver says no, the transformation is validated for that function. If it says yes, it hands back the input, which is the counterexample.

The practical limits follow directly from that. Loops are the hard case, because encoding an unbounded loop as a formula requires either an invariant or a bound; Alive2 unrolls loops a fixed number of times, which makes its answer sound for the unrolled prefix and silent beyond it. Memory is the other hard case — modelling malloc, aliasing, and out-of-bounds access precisely is expensive, and the encoding choices there dominate solver time. And solver time is not bounded: a function that is too big simply times out, and a timeout is not a verdict.

The honest way to describe the result: translation validation as it exists today verifies most transformations on small, loop-free or loop-bounded functions, and times out on the rest. That is still enormously valuable, because it is applied over a large corpus continuously, and because a counterexample on a small function is a fixable bug report.

An Alive2-style check: does the target refine the source?
1define i32 @src(i32 %x) {
2  %a = mul nsw i32 %x, 2
3  %b = sdiv i32 %a, 2
4  ret i32 %b
5}
6 
7define i32 @tgt(i32 %x) {
8  ret i32 %x
9}
10 
11; Refinement holds: `mul nsw` means signed overflow is poison, so on
12; every input where @src is well-defined, %a is exactly 2*%x and the
13; division returns %x. Drop the `nsw` and the check fails, with the
14; counterexample x = INT_MIN/2 + 1 where the multiply wraps.

The entire legality of this rewrite lives in one three-character flag. That is the general shape of IR-level optimization: the flags carry the assumptions the frontend derived from the language, and a validator is checking the flags as much as the instructions — which is also why [[ir-design-tradeoffs]] treats "what metadata does an instruction carry" as a first-order design question.

Where it fits in a real toolchain

Two deployment shapes are worth distinguishing. The first is as a fuzzing harness: generate or collect IR, run a pass, validate, report. This is how Alive2 is mostly used against LLVM, and it is where its bug finds come from. It requires no changes to anyone’s build and it improves the compiler for everybody.

The second is as a build-time gate for a specific product: validate every function in your own build, and fail the build when a transformation cannot be justified. This is a much stronger local guarantee — the code you are shipping was checked — and much more expensive, since solver time is now on the critical path of every compile. It is the shape that makes sense in high-assurance settings where a slower build is an acceptable price.

A third, cheaper relative is worth naming: [[ir-verification]], which checks that the IR is *well-formed* after every pass rather than semantically equivalent. It catches a strictly weaker class — broken dominance, malformed phi nodes, type mismatches — at a fraction of the cost, and every serious compiler runs it in debug builds. It is not translation validation, but it is the first step toward the same discipline.

How it works

The steps, in the order the compiler takes them.

  • Capture the IR of a function before and after a transformation, in a form with a precise semantics.
  • Encode both as logical formulas over the function inputs: arithmetic with overflow and poison semantics, memory as an array, control flow as path conditions.
  • Bound the unbounded — unroll loops to a fixed depth, cap memory size — so the encoding is a finite formula.
  • Ask the solver whether an input exists on which the source is well-defined and the target exhibits a behavior the source could not.
  • If unsatisfiable, the transformation refines for this function; if satisfiable, the model is a counterexample input.
  • If the solver times out, record it as unchecked rather than as validated — the distinction is the difference between a tool and a rubber stamp.

How it breaks

What the engineer observes when it goes wrong — not what goes wrong internally.

  • The checker times out on every function above a few hundred instructions, so the parts of the codebase most likely to contain interaction bugs are exactly the parts that go unchecked.
  • A loop is unrolled to depth four and the bug requires five iterations, so the check passes and the bug ships with a green report attached.
  • The IR semantics used by the checker disagrees subtly with the compiler’s own, and the tool reports a stream of false counterexamples that nobody can reproduce in the compiler.
  • Refinement is implemented as equality, so every legal optimization that narrows nondeterminism is reported as a bug and the tool is abandoned in week two.
  • Timeouts are reported as passes, so coverage looks complete and is not.
  • Validation is run only on the fast path of the pipeline, so the passes that run at higher optimization levels — the ones with the interesting legality conditions — are never checked.

When it helps

  • Middle-end development: a new pass can be validated over a corpus before it is trusted, which finds legality mistakes far faster than waiting for a user program to hit them.
  • High-assurance builds where the specific binary being shipped needs evidence beyond "the tests passed".
  • Investigating a suspected miscompilation: running the validator over the failing translation unit often names the transformation directly.
  • Any IR with a written-down semantics, including your own. A small validator for a small IR is a very reasonable project, and forces the semantics to be written down at all.

When it hurts

  • Large functions and long-running loops, where the encoding blows up and the solver returns nothing useful within any acceptable time.
  • Compilers whose IR has no precise semantics, where the first task is writing one — which is most of the work and benefits the project in ways unrelated to validation.
  • Frontends. A validator compares two IR programs; it says nothing about whether the IR faithfully represented the source, which is where a large share of real compiler bugs live.
  • As a build gate on a large codebase, where solver time per function turns a two-minute build into an hour.

What it costs

Every one of these is paid by something.

  • Validation buys per-compilation evidence with counterexamples and costs solver time proportional to function size, which is why it is usually a background harness rather than a build step.
  • Bounding loops buys decidability and costs soundness beyond the bound: the tool reports success for a program it only partly examined, and the report does not say so unless it is written to.
  • A precise memory model buys real coverage of load/store optimizations and costs an enormous increase in formula size, so most validators trade some precision to stay tractable.
  • Writing a formal IR semantics buys the validator and costs a serious specification effort, plus the ongoing obligation to keep it in step with a compiler that changes weekly.
  • Deploying as a build gate buys assurance about the artifact you ship and pays in build latency on every commit, which competes directly with the fast feedback that keeps a team productive.

What else you could do

What a different compiler or language does instead, and when that is better.

  • A verified compiler proves the whole optimizer once rather than each compilation — stronger and far more expensive, and it constrains how the compiler may be written; see [[verified-compilers]].
  • Fuzzing with differential comparison finds wrong-code bugs without any formal semantics at all, at the cost of no guarantee and no counterexample beyond "these two differ" — [[compiler-fuzzing]].
  • Well-formedness verification after each pass — [[ir-verification]] — catches structural breakage cheaply and says nothing about semantics. Every compiler should have it; it is not a substitute.
  • Runtime checks in the generated code: bounds checks, overflow traps and sanitizers move the question to execution time, catching what static checking missed at the cost of runtime overhead.

See it for yourself

The flag, dump or tool that shows you this directly.

  • Alive2: alive-tv src.ll tgt.ll reports refinement or prints a counterexample. The online instance at alive2.llvm.org runs it in a browser, and opt -passes=instcombine plus alive-tv is the standard loop for checking one pass.
  • Alive2 also runs as an opt plugin over a whole test suite, which is how it is used against LLVM’s own regression corpus.
  • The cheap relative, available everywhere: opt -verify and Clang’s -mllvm -verify-each, which run LLVM’s well-formedness verifier after every pass.
  • The IR semantics being checked against is written down: LLVM’s LangRef sections on undef, poison and freeze are the specification a validator encodes, and reading them explains most of what Alive2 reports.
  • Our own compiler runs the weak form: SSA well-formedness and phi arity are asserted after construction in scripts/compilers-sim.test.ts, which is [[ir-verification]] rather than validation, and the difference is worth feeling directly.

Plausible wrong readings

Stated the way a confident engineer states them.

  • "Translation validation proves the compiler correct." It proves something about the compilations it checked. Two different quantifiers, and the difference is the whole reason it is affordable.
  • "If the validator passes, the code is correct." It says the transformation preserved the IR’s semantics. If the frontend lowered your source wrongly in the first place, both sides are equally wrong and the check is green.
  • "A timeout means it is probably fine." A timeout means nothing was checked. A tool that conflates the two is worse than no tool, because it produces confidence without evidence.
  • "The relation is that the two programs are equivalent." It is refinement, and it is one-directional. Equality would reject every optimization that narrows behavior or exploits undefined behavior.

Misconceptions

The claim, and what is actually true.

Translation validation and verified compilation are two names for the same thing.
One checks the instance, the other proves the general case. The first is incremental and applies to an existing compiler; the second requires the compiler to be built for it.
If a transformation is correct in general, validating individual applications is redundant.
Most compiler bugs are not in the abstract transformation but in its implementation — a stale analysis result, a missed side condition, an unmaintained dominator tree. Validating the instance catches exactly those.

Go deeper

The same idea at increasing depth. Stop wherever it stops being useful.

overview

Rather than proving the whole optimizer correct, translation validation checks one compilation at a time: here is the code before a transformation and here it is after, does the second do only things the first was allowed to do. A solver answers, and when the answer is no it hands you an input where they differ. It is cheaper than verification, it works on the compiler you already have, and it only tells you about the compilations you actually checked.

practical

For LLVM, alive-tv src.ll tgt.ll is the tool, and the standard loop is: dump IR, run one pass, dump again, validate. Read the counterexample carefully — a surprising number of them turn on nsw, nuw or poison rather than on the arithmetic you were looking at. If you maintain your own IR, start with the weaker version: run a well-formedness verifier after every pass. It catches a different class, it costs almost nothing, and it is the step that makes the stronger tool conceivable later.

advanced

The structural reason this catches what unit tests do not is that it re-establishes the relation rather than trusting accumulated facts. A compiler pass is correct relative to analysis results it did not compute — alias information, dominance, loop invariance — and the usual failure is that one of those became stale while remaining plausible. A unit test on the pass supplies fresh, consistent analyses and passes. A validator on the real compilation sees the actual pair of programs and does not care where the facts came from. That is also why bounding loops is the technique’s sharpest limitation rather than an implementation detail: the transformations most likely to rely on subtle invariants are exactly the loop transformations the bound cannot reach.

How much this depends on

Nothing in this domain is true of every compiler. These say how much.

implementationAlive2 targets LLVM IR and encodes LLVM’s specific model of undef, poison and freeze. There is no equivalent for GCC’s GIMPLE in general use, and none for most other IRs. A validator for a different compiler is a new project, not a configuration, and the semantics it encodes must be re-derived from that IR’s own rules.
simplifiedWe describe the check as one solver query per function pair. Real validators split the query, apply syntactic fast paths for the many cases where the two functions are identical, bound memory sizes, and unroll loops to a configurable depth. Each of those is a soundness or completeness compromise made to stay inside a time budget, and a serious tool reports which ones it applied.
typicalThe claim that validators time out on large functions describes SMT-based tools as they stand today, LLVM-oriented ones included. Approaches based on simulation relations and invariant inference scale differently and fail differently — they handle loops better and require more from the compiler, typically extra hints emitted by each pass about the correspondence it maintained.

If you were asked this in an interview

  • Why is the relation refinement rather than equality?
  • What does a validator tell you when it times out, and what should the tool report?
  • A pass is proven correct on paper. Why validate individual compilations anyway?

Connections

Domains that do not exist yet
  • Testing & Reliability Engineering — Property checking with SMT solvers, and the difference between bounded and unbounded verification
    Bounded model checking, counterexample extraction and the honest reporting of timeouts are general verification concerns that apply well beyond compilers. What is compiler-specific is that the property is refinement over an IR semantics, and that undefined behavior makes the relation one-directional.