17  Verification

Verification is the mechanism that turns MLIR from a printable syntax tree into a trustworthy intermediate representation. Every operation is expected to satisfy structural and semantic invariants before analyses and lowering passes rely on it. Parsing proves that a string can be decoded; verification proves that the decoded operation means something valid in its declared dialect.

17.1 What MLIR Verifies

Generic IR verification checks the facts shared by all operations: operands and results exist with well-formed types, uses respect SSA visibility, regions own valid blocks, successor operands agree with destination block arguments, and parent/child ownership is coherent. Operation-specific verification then checks the dialect contract.

%out = arith.addi %lhs, %rhs : i32

For this small operation, the dialect verifies type and operation-specific constraints. For a structured loop, verification also relates the loop bounds, step, body arguments, yield operands, and result types. For an operation with an axis attribute, it may check that the axis is in range for the input rank. These cross-field facts cannot be recovered from grammar alone.

17.2 Verification Is Layered

An operation definition can express simple invariants declaratively in ODS: operand classes, result counts, traits, region counts, attribute kinds, and type relationships. MLIR generates checks for these constraints. A handwritten verifier handles conditions that require inspecting several fields or nested IR: uniqueness of an axis list, agreement between a function signature and all returns, dominance-sensitive region rules, or semantic restrictions on a dialect attribute.

This division matters for dialect authors. Put stable, local facts in the declaration so builders and documentation share them. Put nonlocal semantic conditions in a verifier with a clear diagnostic. Do not defer a simple type constraint to a later optimization pass; malformed input should fail at the boundary where it is created or parsed.

17.3 A Verifier Is Not An Optimizer

Verification rejects IR that violates the dialect’s contract. It does not prove that the program is fast, free of undefined source-language behavior, or globally optimal. It also does not establish every property a specialized analysis may need. For example, a verifier can establish that a memref load has well-typed indices, but it cannot generally prove at compile time that a dynamic index is within bounds.

Likewise, a verifier must not silently repair malformed IR. A transformation that sees an invalid attribute should diagnose or fail, rather than normalize it without recording the semantic decision. Repair belongs in an explicit canonicalization or legalization pass with documented preconditions.

17.4 Verification During Transformations

Run verification after constructing nontrivial IR and after structural rewrites, especially while developing a pass. The most useful workflow is to verify close to the mutation that caused an error. A bad rewrite can otherwise survive until a later lowering pass fails with an apparently unrelated type or dominance diagnostic.

Patterns should return failure when their preconditions are not met. They should not create a partially rewritten operation and hope a verifier catches it. Within a PatternRewriter, build replacement operations first, replace uses only when the new form is valid, then erase dead old operations. For CFG edits, update branch operands and block arguments as one conceptual change.

17.5 Reading Diagnostics

A good MLIR verifier diagnostic identifies the offending operation and field, then explains the required relationship. When debugging, print generic form if custom assembly hides an attribute or result type; run the verifier on a reduced test case; and inspect the operation definition rather than guessing from the printed form. The location attached to an operation helps connect generated IR back to source or a transformation stage.

Verification failures are design feedback. If a pass frequently needs to bypass a rule, either its rewrite is incomplete or the dialect’s stated contract no longer models valid programs. Do not weaken verification simply to make a test pass: downstream analyses depend on those invariants.