IRimplementation

IR Verification

A verifier is a function that rejects malformed IR. Its value is not that it finds bugs — it is that it finds them at the pass that caused them, instead of three passes later in a code generator that had every right to assume otherwise.

The question

Why does a compiler check its own intermediate representation, and what exactly is it checking?

Source→Lexing→Tokens→Parsing→AST→Semantics→Typed→IR→Optimize→Codegen→Machine code→Link→Execute

What the program is here

The IR immediately after a pass has rewritten it, being read by a function whose only job is to answer yes or no. The verifier exists to answer a question about the *compiler*, not the program: did the pass that just ran leave the representation in a state every downstream consumer is entitled to assume?

What this phase may assume or do

A verifier may reject only programs that violate a stated invariant of the representation, never programs it merely finds surprising — a verifier that rejects valid IR blocks legitimate transformations and will be disabled by the first person it inconveniences. The invariants it checks are exactly those every consumer is permitted to assume without checking: well-typed instructions, every use dominated by its definition, a phi operand per predecessor, a terminator on every block, and edges that agree with terminators.

Key points

A verifier rejects malformed IR, and its value is locality: it names the pass that caused the problem rather than the pass that first noticed.
The invariants are derived from what consumers assume without checking — phi arity, dominance of definitions over uses, type agreement, structural well-formedness, reachability.
"Every use dominated by its definition" is the correct condition, not "defined earlier in the listing" — a definition in one branch arm does not dominate a use in the other.
Run the verifier between passes, not once at the end; once at the end tells you the IR is broken but not who broke it.
A verifier proves well-formedness, not correctness. A pass that replaces add with sub passes every verifier ever written.

The three-passes-later problem

A pass introduces a phi node with two operands into a block with three predecessors. Nothing crashes. The next twelve passes read that phi, and most of them do not care about arity. Eventually the out-of-SSA pass walks the predecessors looking for each one's incoming value, finds nothing for the third, and substitutes a default — or the register allocator assigns a register based on a live range computed from an operand that was never there.

The program compiles. It produces a wrong answer on one input. Somebody bisects for two days and lands on a pass that is entirely innocent — the one that first *observed* the malformed IR, not the one that created it. This is the single most expensive failure pattern in compiler engineering, and the whole purpose of a verifier is to convert it into an immediate, local, obviously-attributable failure.

That is why the verifier runs *between passes*, not once at the end. Running it once at the end tells you the IR is broken; running it after every pass tells you which pass broke it, which is the only piece of information you actually needed.

What a verifier checks

The invariants are not arbitrary. Each one corresponds to an assumption that some consumer makes without checking, and the list is therefore derived from the consumers rather than invented.

Phi arity. A phi node has exactly one operand per predecessor of its block, and each operand is tagged with the predecessor it comes from. Every consumer that resolves phis into copies iterates the predecessors and expects to find a matching operand; a mismatch means a copy is placed for a nonexistent edge or omitted for a real one.

Use after definition, under dominance. Every use of a value is dominated by its definition. This is stronger than "defined somewhere earlier in the listing" and it is the correct condition: a definition in one arm of a branch does not dominate a use in the other arm, even though it appears earlier in the block ordering. Violating it means a register is read on a path where nothing wrote it.

Type agreement. Each instruction's operands match its signature, and each use of a value agrees with the type at its definition. In LLVM this is checked structurally; in an untyped IR the check does not exist and the failure surfaces at the code generator or, worse, at run time.

Structural well-formedness. Every block ends in exactly one terminator, every terminator's targets exist, the predecessor and successor lists agree with the terminators, and every block except the entry is reachable. AtlasLang enforces the last of these by construction: pruneUnreachable drops unreachable blocks after lowering, because the dominance computation assumes every block has a dominator and an orphan block breaks that assumption.

Each invariant, and the consumer that would otherwise be wrongtypical

Invariant	Who assumes it	What happens if it is violated
One phi operand per predecessor	Out-of-SSA, register allocation, any phi-aware pass	A copy is emitted on a nonexistent edge or missed on a real one; a value is undefined on one path
Every use dominated by its definition	Register allocation, liveness, code generation	A register is read on a path where nothing wrote it; the value is whatever was there before
Operand types match the instruction signature	Instruction selection, every arithmetic transformation	A 32-bit value is used as 64-bit; results are correct until they cross a threshold
Exactly one terminator per block	The CFG builder, every graph traversal	Fallthrough into an unrelated block, which works until block ordering changes
Edges agree with terminators	Dominance, loop detection, phi resolution	Dominance is computed over a graph that does not match the code, silently
Every block reachable from entry	Dominance, which assumes every block has a dominator	The dominator computation produces undefined results for the orphan and anything below it

AtlasLang checks exactly these, and you can run them

simplifiedAtlasLang verifies by test suite over a fixed set of example programs; LLVM verifies by an in-process VerifierPass that can be scheduled after every pass and is enabled by default in debug builds. The difference matters: a test suite checks the programs you thought of, and an in-process verifier checks every program anyone ever compiles. For a teaching compiler with a fixed example set the first is adequate; for a production compiler it is not.

This domain's compiler is verified by a test suite rather than by an in-process verifier function, and the suite asserts precisely the invariants above. scripts/compilers-sim.test.ts contains a test that walks every example program, converts it to SSA, and asserts that every phi's operand blocks — sorted — equal that block's predecessor list, sorted. Not a subset, not a superset: equal. Another asserts that no register is ever defined twice, which is the SSA invariant itself. Another asserts that no phi survives out-of-SSA into the machine representation, because a phi reaching code generation is a phi nobody will lower.

The suite goes further than a verifier can, in one respect that is worth noticing. It checks the parallel-copy sequencer by *simulating* the sequence of moves and comparing the final register state — not by comparing against an expected list of moves. A hand-written expectation can itself be wrong, and a wrong sequence that matches a wrong expectation passes. Running the moves and checking the state cannot.

Run them with npm test, which runs every scripts/*.test.ts under the Node test runner. Break something in src/compilers/sim/ir.ts first — delete the if (!phi.sources.some(...)) guard that prevents a duplicate phi operand, say — and watch which test names the failure. That is what a verifier buys, demonstrated on a compiler small enough to break on purpose.

The phi-arity invariant, as asserted in scripts/compilers-sim.test.ts

1for (const b of ssa.blocks) {
2  for (const i of b.instrs) {
3    if (i.op !== 'phi') continue
4    const blocks = i.sources.map((s) => s.block).sort()
5    assert.deepEqual(blocks, [...b.preds].sort(),
6      `${ex.id}/${fn.name}/${b.id}: phi operands do not match predecessors`)
7  }
8}

The comparison is deepEqual over sorted lists, so a phi with a duplicate operand for one predecessor and none for another fails — even though the count matches. Checking the count alone is the version of this test that passes while the bug ships.

What verification is not

A verifier does not prove the compiler is correct. It proves the IR is well-formed. A pass can produce perfectly well-formed IR that computes the wrong thing — replace an add with a sub and every invariant still holds. Detecting *that* needs a different technique: differential testing against another compiler, translation validation of each transformation, or a formally verified compiler where the proof is the artifact. Those are [[differential-testing]], [[translation-validation]] and [[verified-compilers]], and they are strictly more expensive.

The verifier is worth its cost anyway, because malformed IR is where a large fraction of real pass bugs land, and because the cost is small: a linear walk over the function checking local properties, cheap enough to run after every pass in a debug build and to disable in a release build.

The other thing a verifier is not is optional-in-spirit. An invariant that is documented but unchecked is a comment, and comments are violated. The invariants that survive in a codebase are the ones that fail a build.

How it works

The steps, in the order the compiler takes them.

Walk every block and assert it has exactly one terminator whose targets all exist.
Recompute predecessor and successor lists from the terminators and assert they match the stored ones.
For every phi, assert the set of operand-source blocks equals the set of predecessors — as sets, so a duplicate cannot mask a missing one.
Compute dominance, then assert every use of a value is dominated by that value's definition.
For every instruction, assert operand types match its signature and each value's type agrees at definition and use.
Assert every block is reachable from the entry, since dominance is undefined for blocks that are not.
Schedule the whole check to run after every pass in debug builds, and behind a flag in release builds.

How it breaks

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

Without verification: a wrong answer appears at run time, bisection lands on an innocent pass, and two days are spent before anyone looks at the pass that actually created the malformed IR.
With a verifier that only counts phi operands rather than matching them to predecessors: a phi with two operands for one predecessor and none for another passes, and one path reads an undefined value.
With a verifier that checks "defined earlier" rather than "dominates": IR where a value defined in the then arm is used in the else arm passes, and a register is read on a path where nothing wrote it.
With verification disabled in the configuration everyone actually uses: the invariants drift, and by the time somebody turns it on, hundreds of pre-existing failures make it unusable and it gets turned off again.
With a verifier that rejects legal IR: a legitimate transformation is blocked, and the pass author disables the verifier rather than arguing with it.

When it helps

Developing a new pass. The verifier catches the mistakes a new pass makes — stale edge lists, unmaintained phi operands, uses that escaped their dominance region — at the moment they happen.
Accepting hand-written IR. Any tool that reads textual IR from a user needs a verifier, because the user has no other feedback and a malformed input would otherwise crash somewhere unrelated.
Bisecting a miscompilation. Enabling verification after every pass turns "something is wrong" into "pass 43 is wrong" in one run.

When it hurts

In release builds on large programs, where a full verification after each of a hundred and fifty passes is a measurable fraction of compile time. This is why it is a debug-build default and a release-build flag.
When the invariants are wrong. A verifier that encodes an over-strict rule becomes an obstacle, and the failure mode is not a false alarm — it is that everyone learns to turn it off.

What it costs

Every one of these is paid by something.

Verification buys immediate, locally attributable failure and pays compile time proportional to program size times pass count — which is why it is on in debug builds and behind a flag in release ones.
Stronger invariants buy fewer representable bugs and pay at every construction site, which must now satisfy them — an IR forbidding critical edges makes out-of-SSA trivial and forces every edge-splitting decision earlier.
A test-suite verifier is cheap to write and only checks the programs you thought of; an in-process verifier checks everything anyone compiles and costs a maintained pass.

What else you could do

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

Make the invariant unrepresentable instead of checked. Block parameters instead of phi nodes make phi arity a structural property of the jump — there is no way to write the wrong number of arguments and have it parse.
Property-based testing over generated programs, which finds violations the fixed example set does not contain, at the cost of needing a generator that produces valid and interesting programs — [[compiler-fuzzing]].
Translation validation, which checks that each transformation preserved *meaning* rather than well-formedness. Strictly stronger and strictly more expensive — [[translation-validation]].
A formally verified compiler such as CompCert, where the proof replaces the check entirely for the parts that are proved. The strongest guarantee available and an enormous investment — [[verified-compilers]].

See it for yourself

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

opt -passes=verify file.ll runs the LLVM verifier over a module and reports the first invariant violated, with the offending instruction printed.
llvm-as < file.ll > /dev/null parses and verifies textual IR — the fastest way to check whether a hand-written .ll file is well-formed.
opt -passes='default<O2>' -verify-each file.ll runs the verifier after every pass in the pipeline, which is the configuration that names the guilty pass.
clang -mllvm -verify-machineinstrs extends verification to the machine-level IR, where a different set of invariants applies.
For this domain's compiler: npm test runs scripts/compilers-sim.test.ts under the Node test runner. The SSA, phi-arity, dominance and parallel-copy invariants are all asserted there, and breaking one in src/compilers/sim/ir.ts shows you exactly what a verifier failure reads like.

Plausible wrong readings

Stated the way a confident engineer states them.

"The verifier proves the compiler is correct." It proves the IR is well-formed. A pass that computes the wrong value while maintaining every invariant passes cleanly.
"If the verifier passes, the program will run correctly." The verifier says nothing about the program. It says the compiler has not corrupted its own data structure.
"Verification is a testing technique." It is a runtime assertion over a data structure, and it runs on every compilation in a debug build — it catches things no test case anticipated.
"We can turn it on later." Later, the invariants have already been violated in places that depend on the violation, and turning it on produces hundreds of failures nobody has time to triage.

Misconceptions

The claim, and what is actually true.

A verifier slows the compiler down too much to be worth it.

It costs a linear walk per pass and it is a build-mode decision, not an all-or-nothing one. The comparison is against days of bisecting a miscompilation, which is the alternative it is competing with.

Checking phi operand *count* is the same as checking arity.

A phi with two operands for one predecessor and none for another has the right count and is malformed. AtlasLang's test compares sorted lists of source blocks against sorted predecessors, precisely to catch this.

Well-formed IR means the pass did the right thing.

Well-formed IR means the pass did not corrupt the data structure. Whether it preserved the program's meaning is a separate and much harder question.

Go deeper

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

overview

A compiler checks its own intermediate representation after each transformation. The checks are simple — every block ends in a jump, every merge point has one incoming value per incoming edge, every value is defined before it is used on every path — and their purpose is to make a broken pass fail immediately instead of corrupting something that fails much later.

practical

If you are debugging a miscompilation in an LLVM-based toolchain, run the pipeline with -verify-each before doing anything else. If a pass is producing malformed IR, that one flag names it, and the remaining work is reading one pass instead of bisecting a hundred and fifty. If verification passes cleanly, you have learned something too: the bug is semantic rather than structural, and differential testing against another optimization level or another compiler is the next tool.

advanced

The design question behind verification is which invariants to *enforce* rather than check. Every checked invariant is a runtime cost and a possible false rejection; every enforced invariant is a constraint on the representation that makes the violation unwriteable. Block parameters make phi arity structural. An IR that forbids critical edges makes phi resolution total. Sealed-block SSA construction makes "use before def" unconstructible. The mature version of this lesson is not "write a verifier" but "notice which of your checks could have been a type", and the checks that remain are the ones that genuinely could not.

How much this depends on

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

implementationLLVM enables its verifier by default in assertions-enabled builds and disables it in release builds; -verify-each schedules it after every pass. GCC has -fchecking, which enables analogous internal consistency checks. Cranelift enables its verifier when the enable_verifier setting is on, which is the default in debug configurations. Every project makes this a build-mode decision, and the defaults differ.

typicalThe invariant list here is the one common to SSA-based, block-structured IRs. A stack-based IR checks operand-stack depth at every merge point instead; a sea-of-nodes IR checks effect-edge chains and node-input arity. The principle transfers exactly; the specific checks do not.

If you were asked this in an interview

What does an IR verifier check, and why check it after every pass instead of once at the end?
A phi node has the right number of operands but the compiler still produces wrong code. What check was missing?
Give me an invariant you would rather enforce structurally than verify, and say how.

Connections

DSAdirected-graph dfs

Securityfuzzing

Domains that do not exist yet

Testing & Reliability Engineering — Invariant checking and assertions as a development-time technique
A verifier is an invariant assertion over a data structure, and the general practice — where to assert, what it costs, why assertions that are disabled in production still pay for themselves — is owned there.
Programming Languages & Runtime Internals — Runtime assertions and heap verification in a garbage collector
A GC verifier walking the heap to check that every reference points at a live object is the same technique on a different data structure, and the reasoning about when to enable it is identical.