Lesson 24.7 — What's next: MLIR, verified compilation, translation validation at scale

Techniques: MLIR dialect conversion — an IR made of dialects (sets of operations with their own verifiers), lowered progressively by legality-driven rewriting: a ConversionTarget says which operations are legal, patterns rewrite illegal ones, and the driver (OperationLegalizer) keeps going until everything is legal or nothing applies; CompCert (verified compilation) — a compiler whose every pass carries a machine-checked proof that the output simulates the input, composed into one theorem about the whole pipeline (transf_c_program_correct); translation validation at scale (Alive2) — instead of proving the compiler, check each run: encode source and target functions as SMT formulas and ask whether the target refines the source, which is what alive-tv does to your -O1 output below.

This course built one compiler, one way. This closing lesson shows the three directions in which the field has moved past that way: representing programs at several levels of abstraction at once (MLIR), proving the pipeline instead of testing it (CompCert), and checking each compilation with a solver when proving the compiler is out of reach (Alive2). Each is presented with the depth contract's full treatment, but the honest scope is a map: the exercises point to the lessons of this course that each direction generalizes (Ch 12's translation validation, Ch 13's Alive-style rule checking, Ch 11's lowering as a conversion), and the "Where to go from here" section of the chapter README says what to read next. mlir-opt and Coq are not in this container; the MLIR and CompCert boxes quote the pinned sources and LLVM's own test files. The Alive2 box is a real run of alive-tv (built by the Ch 12 author at commit 01a5ec45) on pebblec's IR.

1. Problem and motivation

MLIR dialect conversion

pebblec has two IRs: PIR, which knows about assert and checked arithmetic, and LLVM IR, which knows about i64 and br. Every real compiler has more: Clang has the AST, Swift has SIL, Rust has HIR, THIR and MIR, Flang had nothing between the parse tree and LLVM until MLIR. Each IR needs a parser, a printer, a verifier, a pass manager, and every optimization written for it is unavailable to the others. MLIR [LAB+21] makes one IR infrastructure host all of them: an operation is a generic record (name, operands, results, attributes, regions) and a dialect is a namespace of operations with their own verifier and folder. arith.addi, scf.for, llvm.add and a hypothetical pebble.assert are all operations in one module, at the same time. Lowering then is not a rewrite of one data structure into another but a conversion within the same one: mark pebble.* illegal and llvm.* legal, provide patterns, and let a driver rewrite until the module is legal. Pebble's Lesson 11.2 lowering scheme (PIR statement → LLVM instructions) is a set of conversion patterns; the "one function at a time, all statements" order of Algorithm 11.2.3 is the driver's job.

CompCert (verified compilation)

Chapter 12 tested pebblec with a fuzzer and validated single runs; Ch 24's Exercise E2 runs a differential fuzzer for hours and finds nothing. That is evidence, not proof: the fuzzer's generator (Lab L1) produces programs from a grammar a page long, and the bug that is not in that grammar is not found. CompCert [Ler09] is the demonstration that a proof is possible for a realistic compiler: C (a deterministic subset with a formal semantics) to PowerPC, ARM, x86, RISC-V assembly, through twenty passes, each with a Coq proof that the pass's output has no behavior the input does not allow. The proofs compose into one theorem, checked by Coq, and the compiler is extracted from the Coq definitions — the executable is the proved function. Csmith, the fuzzer of Yang et al. [YCER11] that found hundreds of bugs in GCC and LLVM, found none in the verified parts of CompCert.

Translation validation at scale (Alive2)

LLVM will not be rewritten in Coq. The alternative that scales is Ch 12's translation validation, made precise enough for real IR and fast enough to run over the whole test suite: Alive2 [LLH+21] gives LLVM IR a formal semantics (including undef, poison, memory, and the exact meaning of each nsw/nuw/exact flag), encodes a source and a target function into SMT, and asks the solver for an input on which the target's behavior is not one the source allows (Definition 12.8.2). Run over LLVM's test/Transforms directory, it has found dozens of miscompilations in InstCombine alone, several of them decade-old. Its tool alive-tv takes two .ll files; the box below runs it on the IR your own pipeline produces.

2. Definitions and algorithms

MLIR dialect conversion

Definition 24.7.1 (Operation, dialect, conversion target, legality)

An operation \(o\) has a name dialect.op, operands and results (SSA values with types), attributes, and zero or more regions, each a list of blocks of operations (so operations nest: func.func holds a region holding scf.for holding a region ...). A dialect \(D\) is a set of operation names with a verifier. A conversion target \(T\) assigns to each operation name (or whole dialect) a legality action \(\in \{\mathrm{Legal}, \mathrm{Dynamic}(\phi), \mathrm{Illegal}\}\): every instance is legal; an instance is legal iff the predicate \(\phi(o)\) holds; no instance is legal. An operation may be recursively legal: then everything nested in it is legal too. A conversion pattern \(P\) matches an operation and rewrites it, receiving operands already remapped through a type converter (an adaptor), and may fail. Partial conversion leaves untouched any operation that is neither illegal nor reachable by a pattern; full conversion fails unless every operation is legal at the end ("Modes of Conversion" in [MLIR-DialectConversion]).

Algorithm 24.7.2 (Dialect conversion, after OperationLegalizer and applyPartialConversion)

• Input: a root operation \(R\), a target \(T\), a set of patterns \(\mathcal{P}\) with benefits, a type converter; the mode (partial or full).
• Output: the rewritten \(R\), or failure.
• Precondition: \(R\) verifies; every pattern is semantics-preserving on remapped operands.
• Postcondition: on success in full mode every remaining operation is legal for \(T\); in partial mode every operation that was Illegal has been replaced, and the others are legal or untouched (Theorem 24.7.7).
• Invariant: the IR seen by patterns is the original IR plus recorded, not yet applied, changes; a rolled-back pattern leaves no trace.

function ApplyConversion(R, T, P, mode):
    W ← all operations under R in preorder                  # an op before the ops in its regions
    for o in W: if not legalize(o):
        if mode = full or T.isIllegal(o): fail
    finalize: materialize pending type conversions, replace all uses, erase replaced ops
    return success

function legalize(o):                                        # OperationLegalizer::legalize
    if o is ignored: return true
    if T.isLegal(o):
        if recursively legal: mark every op nested in o ignored
        return true
    if legalizeWithFold(o) succeeds and its results are legal: return true
    for P in patterns for o, by decreasing benefit and legalization-graph cost:
        apply P under a recording rewriter
        if every newly created op legalizes (recursively): commit; return true
        else rollback
    return false

Cost: each operation is legalized at most once per pattern that creates it; the rollback makes the worst case exponential in the pattern-application depth, bounded in practice by a depth limit.

CompCert (verified compilation)

Definition 24.7.3 (Semantics, behaviors, refinement of behaviors)

A semantics \(L\) (CompCert's Smallstep.semantics) is a set of states, a step relation \(s \xrightarrow{t} s'\) labelled by a trace \(t\) of observable events (calls to external functions, volatile accesses), a set of initial states and a final-state predicate with a return code. A program behavior (Behaviors.program_behavior) is one of: terminates with trace \(t\) and code \(r\); diverges silently after trace \(t\); reacts with an infinite trace; goes wrong after \(t\) (a stuck state: undefined behavior). \(\mathrm{beh}_1\) improves to \(\mathrm{beh}_2\) (behavior_improves) iff they are equal, or \(\mathrm{beh}_1\) goes wrong after a trace \(t\) and \(\mathrm{beh}_2\) has \(t\) as a prefix. A compiled program \(P_2\) refines \(P_1\), \(L_1 \sqsupseteq L_2\) in the chapter's notation, when every behavior of \(L_2\) is improved from some behavior of \(L_1\): what the target does is what the source does, except where the source had undefined behavior. This is Definition 12.8.2 lifted from straight-line code to whole programs with traces.

Definition 24.7.4 (Forward simulation with a well-founded measure)

A forward simulation from \(L_1\) to \(L_2\) (Smallstep.fsim_properties) is a relation \(\sim \subseteq I \times \mathrm{state}(L_1) \times \mathrm{state}(L_2)\) indexed by a type \(I\) with a well-founded order \(\prec\), such that:

1. (initial) every initial \(s_1\) matches some initial \(s_2\): \(\exists i, s_2.\ s_1 \sim_i s_2\);
2. (final) if \(s_1 \sim_i s_2\) and \(s_1\) is final with code \(r\), then \(s_2\) is final with \(r\);
3. (step) if \(s_1 \xrightarrow{t} s_1'\) and \(s_1 \sim_i s_2\), then there are \(i'\), \(s_2'\) with \(s_1' \sim_{i'} s_2'\) and either \(s_2 \xrightarrow{t}{}^{+} s_2'\) (one or more steps), or \(s_2 \xrightarrow{t}{}^{*} s_2'\) (zero or more) and \(i' \prec i\).

The measure forbids the target from stuttering forever while the source runs: a pass that deletes instructions (dead code, constant propagation) matches a source step with zero target steps only finitely often in a row. forward_simulation_star, _plus, _step, _opt are the special cases (Inlining's proof uses forward_simulation_star).

Translation validation at scale (Alive2)

Algorithm 24.7.5 (Validating one -O1 run of your pipeline, function by function)

• Input: P.pbl; the course plugin; alive-tv.
• Output: a verdict per (function, stage): correct, incorrect with a counterexample, or failed-to-prove.
• Precondition: pebblec --emit=llvm -O0 accepts P.pbl; each stage is a function-level pipeline (no inlining, no function deletion), so that every function of the input is defined in the output.
• Postcondition: a correct verdict for \((f, S)\) is a proof of refinement of \(f\) by \(S(f)\) under the assumptions of Proposition 24.7.6; an incorrect verdict comes with an input that is a witness unless it exercises one of those assumptions.
• Invariant: each stage is validated against its own input, so a bug is attributed to one stage.

function ValidateRun(P):
    pebblec --emit=llvm -O0 P.pbl -o P0.ll
    prev ← P0.ll
    for S in the function-level stages of designCoursePipeline (pebble-o1<print> lists them):
        opt -load-pass-plugin=PebblePasses.so -passes='<S>' prev -S -o P_S.ll
        for f defined in prev:
            alive-tv --func=f --disable-undef-input prev P_S.ll     # read the Summary line
            on failed-to-prove: retry with --smt-to=60000 or --src-unroll=k --tgt-unroll=k
        prev ← P_S.ll
    stop before the first interprocedural stage (pebble-inline)

Cost: one SMT query per (function, stage), seconds each for the straight-line code the generator of Lab L1 produces; minutes for loops, since Alive2 bounds them by unrolling.

Why stop at inlining: after it a callee may be gone, and Alive2 treats a call to a function it does not inline as an unknown call whose result in the source is unconstrained — the target, which computed the value, is then "less defined" and the tool reports a false alarm (the second box in §7).

Proposition 24.7.6 (What an Alive2 verdict means)

alive-tv reports correct for \((f_S, f_T)\) iff, for every input and every choice of undef/nondeterminism in the source that the options allow, every behavior of \(f_T\) is a behavior of \(f_S\) or \(f_S\) has undefined behavior on that input (refinement, Definition 12.8.2), under the assumptions: loops are unrolled to the given bound; memory is modelled with the tool's finite block model; calls to functions without bodies are the same unknown function on both sides. A correct verdict is therefore a proof of refinement for the inputs and unrolling depth covered, and an incorrect verdict comes with a concrete input that is a witness — unless it exercises one of the assumptions (an unknown call, as in the box).

Proof

Alive2 encodes each function as a formula over symbolic inputs (Ch 12, Theorem 12.8.9 for straight-line code; Alive2's translation extends it with a memory model and with undef/poison as explicit non-determinism). The query it discharges is the negation of refinement: an input on which the target has a behavior (value, memory state, UB, non-termination within the unrolled bound) that the source does not allow. The encoding is exact for the fragment it models [LLH+21, §3–4], so an unsatisfiable query is a proof of refinement within the model: bounded loops, finite memory blocks, and unknown calls modelled by one uninterpreted function shared by both sides. A satisfiable query yields a model, printed as the counterexample; when the model assigns a behavior to an unknown call rather than a value to an input, the "witness" is an artifact of the modelling assumption rather than of the program.

3. Worked example

MLIR dialect conversion

The LLVM test mlir/test/Conversion/ArithToLLVM/arith-to-llvm.mlir runs mlir-opt -pass-pipeline="builtin.module(func.func(convert-arith-to-llvm))" and checks:

func.func @vector_ops(%arg0: vector<4xf32>, %arg1: vector<4xi1>, %arg2: vector<4xi64>, %arg3: vector<4xi64>) -> vector<4xf32> {
// CHECK-NEXT:  %0 = llvm.mlir.constant(dense<4.200000e+01> : vector<4xf32>) : vector<4xf32>
  %0 = arith.constant dense<42.> : vector<4xf32>
// CHECK-NEXT:  %1 = llvm.fadd %arg0, %0 : vector<4xf32>
  %1 = arith.addf %arg0, %0 : vector<4xf32>
// CHECK-NEXT:  %2 = llvm.sdiv %arg2, %arg2 : vector<4xi64>
  %3 = arith.divsi %arg2, %arg2 : vector<4xi64>

Trace of Algorithm 24.7.2 with target \(T\) = "llvm dialect legal, arith dialect illegal" (the pass's ConvertArithToLLVMPass constructs exactly this and calls populateArithToLLVMConversionPatterns then applyPartialConversion):

Worklist op (preorder)	isLegal?	Action	New ops, legalized recursively
func.func @vector_ops	not in \(T\), not Illegal → partial mode leaves it (it stays func.func; a later convert-func-to-llvm handles it)	—	—
arith.constant dense<42.>	Illegal	pattern ConstantOpLowering	llvm.mlir.constant — Legal
arith.addf %arg0, %0	Illegal	pattern AddFOpLowering: operands remapped: %0 ↦ the new llvm.mlir.constant	llvm.fadd — Legal
arith.divsi	Illegal	DivSIOpLowering	llvm.sdiv — Legal
func.return	left (partial)	—	—

The result is the mixed-dialect module the CHECK lines describe: func.func around llvm.* operations. That mixture is the point: nothing forces the whole module to change level at once. The same test also runs --convert-to-llvm="filter-dialects=arith", the generic driver that gathers the patterns of every dialect implementing ConvertToLLVMPatternInterface. In Pebble terms, PIR's assert c, kind @l:c (PIR spec §5) would be a pebble.assert op with one Illegal action and one pattern producing llvm.cond_br + a call to pebble_trap, the exact rewrite of Algorithm 11.2.3's statement case for assert.

CompCert (verified compilation)

driver/Compiler.v composes the RTL passes (CompCert 3.15):

Definition transf_rtl_program (f: RTL.program) : res Asm.program :=
   OK f
   @@ print (print_RTL 0)
   @@ total_if Compopts.optim_tailcalls (time "Tail calls" Tailcall.transf_program)
   @@ print (print_RTL 1)
  @@@ time "Inlining" Inlining.transf_program
   @@ print (print_RTL 2)
   @@ time "Renumbering" Renumber.transf_program
   @@ print (print_RTL 3)
   @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program)
   @@ print (print_RTL 4)
   @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program)
   @@ print (print_RTL 5)
  @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program)
   @@ print (print_RTL 6)
  @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program)
   @@ print (print_RTL 7)
  @@@ time "Unused globals" Unusedglob.transform_program
   @@ print (print_RTL 8)
  @@@ time "Register allocation" Allocation.transf_program
   @@ print print_LTL
   @@ time "Branch tunneling" Tunneling.tunnel_program
  @@@ time "CFG linearization" Linearize.transf_program
   @@ time "Label cleanup" CleanupLabels.transf_program
  @@@ partial_if Compopts.debug (time "Debugging info for local variables" Debugvar.transf_program)
  @@@ time "Mach generation" Stacking.transf_program
   @@ print print_Mach
  @@@ time "Asm generation" Asmgen.transf_program.

@@ composes a total pass, @@@ a partial one that may fail (res); the pipeline is Lesson 24.1's staged design written as a function, with the same order the course pipeline uses (inline, then constant propagation and CSE, then dead-code, then allocation), and with no fixed-point iteration: a round would need a termination proof, so each pass runs once. For each pass there is a match_prog relation and a proof file; for inlining, backend/Inliningproof.v defines match_states between an RTL state of the source and one of the inlined program (an inlined call's frames are merged into the caller's) and ends with

Theorem transf_program_correct:
  forward_simulation (semantics prog) (semantics tprog).
Proof.
  eapply forward_simulation_star.

forward_simulation_star is Definition 24.7.4 with a measure: a source Icall to an inlined function is matched by zero target steps (the measure decreases), and a source step inside the inlined body by one or more target steps.

Translation validation at scale (Alive2)

tv.pbl:

fn f(a: int, b: int) -> int {
    let s = a &+ b;
    let t = (s &* 8) / 2;
    return t &- (b & 7);
}
fn main() -> int { print(f(3, 4)); return 0; }

Steps 1–3 of Algorithm 24.7.5 with \(S\) = the function-level passes of the canonicalize and early-scalar stages plus pebble-strength and pebble-reassociate: the box in §7 shows the run and the verdict Transformation seems to be correct! for f. What the solver had to check: that mul i64 %s, 8 → shl i64 %s, 3 agrees on all \(2^{64}\) inputs (it does; no nsw on either side), that sdiv i64 %x, 2 → (x + (x >>s 63) >>u 63) >>a 1 agrees, including on INT_MIN (it does: the source's / is checked by PIR's assert, but the divisor 2 makes both checks br i1 false, which pebble-constfold and pebble-sccp prove and simplifycfg did not yet remove — the trap blocks are still there in both), and that the reordering of the and/sub is sound. Step 4's warning is the second box: after pebble-o1 inlines f into pebble_main, validating pebble_main reports "Source is more defined than target" with i64 %#0 = function did not return! — the source's call @f is unknown to the tool, so it may not return, while the target prints 24. Not a bug; the tool's assumption.

4. Invariants and correctness

MLIR dialect conversion

Theorem 24.7.7 (Full conversion is sound and, with monotone patterns, terminates)

Let every pattern in \(\mathcal{P}\) be semantics-preserving (its output operations have the meaning of the input on the remapped operands) and let each pattern's output be strictly closer to legal in the legalization graph (computeLegalizationGraphBenefit's ordering: the minimal number of pattern applications to reach only-legal operations decreases). Then Algorithm 24.7.2 in full mode terminates, and if it succeeds the resulting module (i) contains only operations legal for \(T\) and (ii) has the semantics of the input.

Proof

Termination: each legalize(o) either succeeds without changes, or applies a pattern whose newly created operations have a strictly smaller distance to legality and are legalized recursively; by induction on that distance the recursion is finite; on failure the rollback restores the previous state and the next pattern is tried, and there are finitely many. The worklist is finite and no operation is re-added except by creation, which is charged to the pattern that created it. (i) In full mode the driver fails unless every operation on the worklist, including every created one, was found legal or ignored under a recursively legal op; the ignored ones are legal by definition. (ii) Every committed change is a pattern application or a fold, semantics-preserving by hypothesis (folds are the dialect's own, verified per operation); rolled-back changes leave no trace, since the rewriter replays them in reverse (RewriterState undo in ConversionPatternRewriterImpl). The type materializations at finalization are identity conversions by the type converter's contract.

Invariant kept by the framework: during a conversion, operations are not erased and uses are not replaced immediately ("Immediate vs. Delayed IR Modification" in [MLIR-DialectConversion]); the rewriter records the intent and applies it at finalization, so that rollback is possible and patterns see the original operands through the adaptor.

CompCert (verified compilation)

Theorem 24.7.8 (Semantic preservation, after Compiler.transf_c_program_correct)

If transf_c_program p = OK tp, then backward_simulation (Csem.semantics p) (Asm.semantics tp): every behavior of the compiled program tp is improved from a behavior of the source p (backward_simulation_behavior_improves). In particular, if p has no undefined behavior, tp has exactly p's behaviors, trace for trace.

Proof

(Sketch of the Coq proof's structure.) Each pass \(k\) proves forward_simulation between its input and output semantics (Definition 24.7.4); compose_forward_simulations chains them into forward_simulation (Cstrategy.semantics p) (Asm.semantics tp) (cstrategy_semantic_preservation), where Cstrategy is C with a fixed evaluation order for the nondeterministic parts of C's semantics. forward_simulation_behavior_improves turns a forward simulation into behavior improvement in the forward direction: every source behavior is matched by some target behavior. To conclude about every target behavior one needs the converse, and forward_to_backward_simulation gives it when the source semantics is receptive and the target determinate (Asm.semantics_determinate): a deterministic target has only one behavior per input, which the forward simulation already showed is a source behavior. Finally c_semantic_preservation composes with the backward simulation from nondeterministic Csem to Cstrategy, since choosing an evaluation order is itself a refinement. The statement is checked by Coq; the executable compiler is extracted from the same definitions of transf_c_program, so there is no gap between what was proved and what runs — except the unverified parts, which Leroy lists: the parser (validated), the assembler and linker, and the formal semantics themselves.

Why forward and not backward directly: a forward simulation is proved by case analysis on source steps, which are the ones the pass author understands (what does Icall do after inlining?); a backward simulation would need case analysis on target steps, including target states that correspond to no source state. Determinism of the target lets one prove the easy direction and get the strong one.

Translation validation at scale (Alive2)

Proposition 24.7.6 is the invariant; its assumptions are the reason Algorithm 24.7.5 validates per function and per function-level stage. The theorem behind it is Ch 12's Theorem 12.8.9 (soundness of the SMT encoding) extended by Alive2's memory model and by the undef/poison semantics of Ch 13 Lesson 8.

5. Complexity

Technique	Compile time	Proof / check effort	Trust base
Dialect conversion	per pattern application; rollback can repeat work	none (a framework)	the patterns' correctness, by test
CompCert	ordinary (no iteration; -O1-class code)	~100 000 lines of Coq for 20 passes; years	Coq's kernel, the semantics, the extraction, the assembler
Alive2	none in the compiler; SMT per (function, run)	none for the user; seconds–minutes per function	Alive2's encoding of LLVM semantics and the SMT solver

6. Variants and refinements

• Greedy rewriting (applyPatternsGreedily, the canonicalize pass) is the other MLIR driver: no target, no legality, apply every matching pattern until a fixed point — Lesson 24.1's canonicalization loop with no phase ordering, relying on patterns that strictly simplify. Canonicalizer.cpp builds a GreedyRewriteConfig and calls it; Ch 13's peephole is that driver specialized to one dialect.
• One-shot bufferization, transform dialect, PDL: MLIR's later additions make the schedule of conversions itself an IR (transform.apply_patterns), so that a pipeline is data, as Lesson 24.1's PipelineDesign is.
• CompCert's partial verification of register allocation (Rideau & Leroy 2010): the allocator is untrusted OCaml, and a verified validator checks each allocation — translation validation inside a verified compiler, the same idea as Alive2 with a proof of the validator instead of a solver.
• Bounded translation validation is what Alive2 does for loops (--src-unroll); unbounded validation needs invariants (Lesson 12.8's discussion), and the research line "Alive2 → Alive-loops → LLVM's own -verify-each" is open.
• Alive2 as a plugin: opt -load-pass-plugin=tv.so -passes='tv,instcombine,tv' validates each pass of a pipeline against its predecessor, which is Algorithm 24.7.5 automated; LLVM's own buildbots run it over the InstCombine tests.

7. In real compilers

MLIR dialect conversion

A dialect conversion as LLVM's own test states it (quoted; no mlir-opt in this container)

Reproduce (LLVM 23.1.2 sources at tag llvmorg-23.1.2; the lines are quoted from the test file and the pass, not produced by running mlir-opt here):

curl -sL https://raw.githubusercontent.com/llvm/llvm-project/llvmorg-23.1.2/mlir/test/Conversion/ArithToLLVM/arith-to-llvm.mlir | sed -n '1,16p'
curl -sL https://raw.githubusercontent.com/llvm/llvm-project/llvmorg-23.1.2/mlir/lib/Conversion/ArithToLLVM/ArithToLLVM.cpp | grep -n 'applyPartialConversion\|populateArithToLLVMConversionPatterns\|struct ArithToLLVMConversionPass'

Output (the test's RUN lines and first checks; the pass's three key lines):

// RUN: mlir-opt -pass-pipeline="builtin.module(func.func(convert-arith-to-llvm))" %s -split-input-file | FileCheck %s

// Same below, but using the `ConvertToLLVMPatternInterface` entry point
// and the generic `convert-to-llvm` pass.
// RUN: mlir-opt --convert-to-llvm="filter-dialects=arith" --split-input-file %s | FileCheck %s
// RUN: mlir-opt --convert-to-llvm="filter-dialects=arith allow-pattern-rollback=0" --split-input-file %s | FileCheck %s

// CHECK-LABEL: @vector_ops
func.func @vector_ops(%arg0: vector<4xf32>, %arg1: vector<4xi1>, %arg2: vector<4xi64>, %arg3: vector<4xi64>) -> vector<4xf32> {
// CHECK-NEXT:  %0 = llvm.mlir.constant(dense<4.200000e+01> : vector<4xf32>) : vector<4xf32>
  %0 = arith.constant dense<42.> : vector<4xf32>
// CHECK-NEXT:  %1 = llvm.fadd %arg0, %0 : vector<4xf32>
  %1 = arith.addf %arg0, %0 : vector<4xf32>
// CHECK-NEXT:  %2 = llvm.sdiv %arg2, %arg2 : vector<4xi64>
  %3 = arith.divsi %arg2, %arg2 : vector<4xi64>

705:struct ArithToLLVMConversionPass
719:    arith::populateArithToLLVMConversionPatterns(converter, patterns);
721:    if (failed(applyPartialConversion(getOperation(), target,
748:    arith::populateArithToLLVMConversionPatterns(typeConverter, patterns);
764:void mlir::arith::populateArithToLLVMConversionPatterns(

What to notice: the test runs inside func.func (builtin.module(func.func(...))), so the function operation itself is never on the conversion's worklist; the CHECK-NEXT lines are the trace of Algorithm 24.7.2 in §3, one llvm.* operation per arith.* one; and the third RUN line, allow-pattern-rollback=0, is the framework's newer mode without the rollback of step 2.4 — the same patterns must then succeed first time. The pass body is three calls: build a target, populate patterns, applyPartialConversion.

MLIR (LLVM 23.1.2)

mlir/docs/DialectConversion.md — "Modes of Conversion" (partial, full, analysis; quoted in Definition 24.7.1), "Conversion Target" (Legal, Dynamic, Illegal; recursive legality) [MLIR-DialectConversion]; mlir/lib/Transforms/Utils/DialectConversion.cpp — OperationLegalizer::legalize (Algorithm 24.7.2 step 2), legalizeWithFold, legalizeWithPattern, legalizePatternResult, computeLegalizationGraphBenefit; mlir/include/mlir/Transforms/DialectConversion.h — ConversionTarget, enum class LegalizationAction, applyPartialConversion, applyFullConversion, applyAnalysisConversion; mlir/lib/Conversion/ArithToLLVM/ArithToLLVM.cpp — ArithToLLVMConversionPass::runOnOperation (builds the target, calls populateArithToLLVMConversionPatterns, then applyPartialConversion); mlir/test/Conversion/ArithToLLVM/arith-to-llvm.mlir (the worked example). No mlir-opt in this container: the test file's RUN and CHECK lines are quoted as the expected behavior.

• Flang (flang/lib/Optimizer/CodeGen/CodeGen.cpp): FIR → LLVM dialect by one large applyFullConversion; IREE, CIRCT, Triton: whole compilers as stacks of conversions.
• Swift's SIL and Rust's MIR are single-level IRs with their own infrastructure — the situation MLIR was built to end. ClangIR (clang/lib/CIR, 2024–) is Clang moving in MLIR's direction.

Find where LLVM does it. In mlir/lib/Transforms/Utils/DialectConversion.cpp, find OperationLegalizer::legalize. Question: in what order does it try (a) the target's legality check, (b) folding, (c) patterns, and what does it do to the operations nested in a recursively legal operation? (Quiz find-operation-legalizer.)

CompCert (verified compilation)

CompCert's simulation record and one pass's proof, as the Coq sources state them (quoted; no Coq in this container)

Reproduce (CompCert 3.15 sources at tag v3.15; quoted, not checked by running coqc here):

curl -sL https://raw.githubusercontent.com/AbsInt/CompCert/v3.15/common/Smallstep.v | sed -n '/^Record fsim_properties/,/^  }\./p'
curl -sL https://raw.githubusercontent.com/AbsInt/CompCert/v3.15/backend/Inliningproof.v | grep -n -A3 '^Theorem transf_program_correct'
curl -sL https://raw.githubusercontent.com/AbsInt/CompCert/v3.15/driver/Compiler.v | grep -n -A3 '^Theorem transf_c_program_correct'

Output (complete for the record; the two theorems with their first proof lines):

Record fsim_properties (L1 L2: semantics) (index: Type)
                       (order: index -> index -> Prop)
                       (match_states: index -> state L1 -> state L2 -> Prop) : Prop := {
    fsim_order_wf: well_founded order;
    fsim_match_initial_states:
      forall s1, initial_state L1 s1 ->
      exists i, exists s2, initial_state L2 s2 /\ match_states i s1 s2;
    fsim_match_final_states:
      forall i s1 s2 r,
      match_states i s1 s2 -> final_state L1 s1 r -> final_state L2 s2 r;
    fsim_simulation:
      forall s1 t s1', Step L1 s1 t s1' ->
      forall i s2, match_states i s1 s2 ->
      exists i', exists s2',
         (Plus L2 s2 t s2' \/ (Star L2 s2 t s2' /\ order i' i))
      /\ match_states i' s1' s2';
    fsim_public_preserved:
      forall id, Senv.public_symbol (symbolenv L2) id = Senv.public_symbol (symbolenv L1) id
  }.

1321:Theorem transf_program_correct:
1322-  forward_simulation (semantics prog) (semantics tprog).
1323-Proof.
1324-  eapply forward_simulation_star.

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

What to notice: fsim_simulation is Definition 24.7.4 clause 3 verbatim: Plus (one or more target steps) or Star with order i' i (zero or more, and the index decreases, fsim_order_wf). Inlining's proof picks forward_simulation_star, the special case with a measure, because an inlined call is a source step matched by no target step. The main theorem is stated for the partial function transf_c_program (= OK tp) and concludes a backward simulation from nondeterministic Csem, which Theorem 24.7.8's proof sketch traces back to the forward simulations.

CompCert 3.15

driver/Compiler.v — transf_rtl_program, transf_cminor_program, transf_c_program (the pass list above), Theorem transf_c_program_correct (Theorem 24.7.8), cstrategy_semantic_preservation, c_semantic_preservation, transf_c_program_match [CompCert-Compiler]; common/Smallstep.v — Record fsim_properties (Definition 24.7.4, with fsim_order_wf, fsim_match_initial_states, fsim_match_final_states, fsim_simulation), forward_simulation_star/_plus/_step/_opt, compose_forward_simulations, forward_to_backward_simulation, Record determinate, Record receptive [CompCert-Smallstep]; common/Behaviors.v — program_behavior, behavior_improves, forward_simulation_behavior_improves, backward_simulation_behavior_improves; backend/Inliningproof.v — match_states, Theorem transf_program_correct by forward_simulation_star. No Coq in this container: quoted from the tagged sources.

• CakeML (HOL4): a verified compiler for an ML dialect, down to machine code including the garbage collector; seL4's C code is compiled by GCC and validated against the proof's semantics (Sewell, Myreen & Klein 2013) — translation validation of an unverified compiler's runs, per binary.
• Vellvm / VeLLVM-2 give LLVM IR a Coq semantics; Alive2 gives it an executable one.

Find where CompCert does it. In common/Smallstep.v, find fsim_properties. Question: in the fsim_simulation clause, what are the two alternatives for the target's steps when the source takes one step, and what role does order play in the second?

Translation validation at scale (Alive2)

alive-tv on your pipeline's output: correct for f, and the false alarm after inlining

Reproduce (pebblec from a solution build, opt 23.1.2, alive-tv at commit 01a5ec45 built against LLVM 23.1.2, x86-64; tv.pbl is the program of §3):

pebblec --emit=llvm -O0 tv.pbl -o tv-O0.ll
opt -load-pass-plugin=build/ch24-sol/lib/PebblePasses.so \
    -passes='function(pebble-mem2reg,pebble-constfold,pebble-peephole,pebble-lvn,pebble-strength,pebble-reassociate,pebble-dce)' \
    -S tv-O0.ll -o tv-opt.ll
sed -n '/define.*@f/,/^}/p' tv-opt.ll
alive-tv --func=f --disable-undef-input tv-O0.ll tv-opt.ll | tail -7
opt -load-pass-plugin=build/ch24-sol/lib/PebblePasses.so -passes='pebble-o1' -S tv-O0.ll -o tv-o1.ll
grep -c '^define' tv-o1.ll
alive-tv --func=pebble_main --disable-undef-input tv-O0.ll tv-o1.ll | grep -v '^$' | sed -n '/^define/,/^}/p;/^Transformation/,/did not return/p'

Output (the function f after the stage, the first verdict's tail, and the second run abridged to the two pebble_mains (source, then target) and the error):

define internal i64 @f(i64 %a, i64 %b) {
entry:
  br label %bb0

bb0:                                              ; preds = %entry
  %0 = add i64 %a, %b
  %1 = shl i64 %0, 3
  br i1 false, label %trap.div_by_zero, label %assert.ok

assert.ok:                                        ; preds = %bb0
  br i1 false, label %trap.overflow, label %assert.ok1

trap.div_by_zero:                                 ; preds = %bb0
  call void @pebble_trap(i32 2, ptr @.str, i32 3, i32 13)
  unreachable

assert.ok1:                                       ; preds = %assert.ok
  %2 = ashr i64 %1, 63
  %3 = lshr i64 %2, 63
  %4 = add i64 %1, %3
  %5 = ashr i64 %4, 1
  %6 = and i64 %b, 7
  %7 = sub i64 %5, %6
  ret i64 %7

trap.overflow:                                    ; preds = %assert.ok
  call void @pebble_trap(i32 1, ptr @.str, i32 3, i32 13)
  unreachable
}

Transformation seems to be correct!

Summary:
  1 correct transformations
  0 incorrect transformations
  0 failed-to-prove transformations
  0 Alive2 errors

1
define i64 @pebble_main() {
entry:
  %_0 = alloca i64 8, align 8
  br label %bb0
bb0:
  %#0 = call i64 @f(i64 3, i64 4)
  store i64 %#0, ptr %_0, align 8
  %#1 = load i64, ptr %_0, align 8
  call void @pebble_print_int(i64 %#1)
  call void @pebble_print_newline()
  ret i64 0
}
define i64 @pebble_main() {
entry:
  call void @pebble_print_int(i64 24)
  call void @pebble_print_newline()
  ret i64 0
}
Transformation doesn't verify!
ERROR: Source is more defined than target
Example:
Source:
ptr %_0 = pointer(local, block_id=0, offset=0) / Address=#x8000000000000000
  >> Jump to %bb0
i64 %#0 = function did not return!

What to notice: the first run is a proof that seven of your passes, in sequence, refine f on all \(2^{128}\) inputs, including the sdiv-by-2 strength reduction and the folded trap conditions. The second run is the false alarm of Algorithm 24.7.5: f was inlined and its body is gone, Alive2 models the source's call @f as an unknown function ("function did not return!" is one of its allowed behaviors), and so the target, which always prints 24, is more defined. The counterexample names no input, which is the tell. The differential fuzzer (E2) is the check that covers the interprocedural stages; Alive2 covers the intraprocedural ones exhaustively.

Alive2 (commit 01a5ec45, built against LLVM 23.1.2)

tools/alive-tv.cpp — the driver: parses both modules, pairs functions by name (or --func), calls Verifier::compareFunctions [Alive2]; llvm_util/llvm2alive.cpp — the translation of LLVM IR into Alive2's IR (the assume i1 0 after a noreturn call in the box's dump is its rendering of unreachable); ir/memory.cpp — the block-based memory model that made the @.str mismatch in a first attempt (validating an llvm-extracted function against a module whose global has an initializer reports "Mismatch in memory": always validate whole modules against whole modules).

Find where Alive2 does it. In tools/alive-tv.cpp, find the loop over the source module's functions. Question: how does it choose the target function to compare against each source function, and what does it do when --func is given?

8. Comparison

Technique	Power / precision	Speed	Output / error quality	Implementation effort	Typical use
MLIR dialect conversion	legality-driven rewriting to a target dialect (Theorem 24.7.7)	pattern-driven; worklist with rollback	mixed-dialect IR at every stage	a framework: high once, low per lowering	Flang, IREE, CIRCT, Triton
CompCert (verified compilation)	a machine-checked proof for every compilation (Theorem 24.7.8)	the compiler runs normally; proofs are static	no miscompilation, by construction	very high (proof engineering)	safety-critical C
Alive2 (translation validation)	per-run refinement check, bounded loops (Proposition 24.7.6)	SMT time, seconds to minutes per function	counterexamples with inputs (the box)	none for the user; the tool exists	LLVM's own test suite, your pebble-o1 output
Differential fuzzing (E2, Ch 12)	whatever the generator reaches	thousands of programs per hour	a failing program, minimized	low (Lab L1)	every compiler's CI

9. Assessment

• Quiz: conversion-mode-outcome (mapping: which ops remain under partial conversion), legality-actions (mapping), find-operation-legalizer (text), compcert-pass-kind (mapping: @@ vs @@@), fsim-measure-case (single), alive-verdict-meaning (single), alive-false-alarm (single). Tags mlir, compcert, alive2. The exam is cumulative: ../quiz.md also draws on every earlier chapter.
• Drills: none. The three techniques are a framework, a proof, and a tool; the drill-able core of each is already a drill elsewhere: pass-order (Lesson 24.1) for the conversion worklist's order, Ch 12's peephole-verify drill for the refinement query, and Ch 13's rewrite-validity drill for the encoding.
• Flashcards: tags mlir, compcert, alive2.
• Exercises: E2's optional last step runs Algorithm 24.7.5 over the fuzzer's corpus (fuzz.py --keep DIR keeps the generated programs; a shell loop over them with alive-tv --func=<fn> records the verdicts); the ★ list in the README ("Where to go from here") has the two larger projects: PIR as an MLIR dialect, and a simulation argument for one of your passes.

Pitfall

"Alive2 said correct, so the pass is correct." It said that this input pair refines, for the unrolling bound, under the tool's memory model, treating unknown calls as the same unknown on both sides. A pass that is wrong only on a loop with 9 iterations, or only when a callee is not nounwind, passes every alive-tv run that does not exercise that case. Proposition 24.7.6's assumptions are the fine print; the fuzzer and the proof are the other two legs.

References

See the chapter references.