[FR] Verifier Pass

[hsqStephenZhang]

Motivation

In the current implementation of Koopa IR, it is relatively easy to inadvertently violate IR invariants, leading to "broken" IR states that are difficult to diagnose. Common scenarios include:

1. Inconsistent Use-Def Chains: Modifying instructions via kind_mut() without manually synchronizing the corresponding used_by information.
2. Structural Desynchronization: Instructions existing in the Layout (execution order) but missing from the DataFlowGraph (data storage), or vice-versa.
3. SSA Violations: Moving instructions such that a value is used before its definition point (dominance violation).

Currently, these issues are often handled silently or trigger obscure panics deep within the codegen or later optimization passes. This makes debugging significantly harder, as the root cause (the pass that broke the IR) is disconnected from the symptoms. As an educational framework, Koopa should empower users to identify exactly when and where their IR became invalid.

Proposal

We propose introducing a Verifier abstraction and a VerifierManager to ensure IR integrity throughout the compilation pipeline.

1. The Verifier Trait

A core trait that allows for both global (Program) and local (Function) level checks. To provide high-quality error messages, Verifiers will be granted access to certain internal fields (via pub(crate) visibility or extension traits).

pub trait Verifier {
  /// Returns the human-readable name of the verifier for error reporting.
  fn name(&self) -> &str;

  /// Performs integrity checks on the entire IR program.
  fn verify_program(&self, _program: &Program) {}

  /// Performs integrity checks on a specific function.
  fn verify_function(&self, _func: Function, _data: &FunctionData) {}
}

2. Built-in Verifiers

Koopa will ship with a set of standard verifiers:

• UseDefVerifier: Ensures every Value in the DFG has a perfectly synchronized used_by set.
• CfgVerifier: Validates basic block termination and layout-DFG consistency.
• DominanceVerifier: (Planned) Validates SSA dominance properties.

3. Verification Management & Pass Integration

To provide maximum flexibility, we propose two ways to run verifiers:

• Explicit Pass Wrapping: Provide VerifierModulePass<V> and VerifierFunctionPass<V> so verifiers can be treated as standard passes and manually registered at specific points in the PassManager.
• Automatic Verification (The VerifierManager): A dedicated manager that can be configured to run a suite of verifiers automatically after each optimization pass.

Why a dedicated Manager?
While manual registration works, it is redundant and error-prone for users to re-add a "VerifyPass" after every single optimization. A VerifierManager integrated into the PassManager execution loop allows for a "Verify-Each" mode (similar to LLVM's -verify-each), ensuring that the IR is validated at every step of the transformation.

Benefits

1. Fail-Fast Debugging: Catch IR corruption immediately after the problematic pass, rather than during codegen.
2. Educational Clarity: Detailed error messages help students understand the subtle invariants of SSA and IR structures.
3. Extensibility: Users can easily define and register custom verifiers for their own specific optimization constraints.

[MaxXSoft]

Great job! I think this is a good start, the Verifier abstraction can solve many problems that users may encounter when modifying the IR structure.

A few more points to be clarified:

Interface of Verifier

• Mixing program and function verifier into one trait, with both retaining default empty implementations, may not be a good idea.
• Verify functions should have a certain return type instead of unit, in order to generate detailed error reports, otherwise it may only panic or print strings.

A potentially more reasonable interface design:

pub trait Verifier {
  /// Returns the human-readable name of the verifier for error reporting.
  fn name(&self) -> &str;
}

pub trait ProgramVerifier: Verifier {
  /// Performs integrity checks on the entire IR program.
  fn verify(&self, _program: &Program) -> ???;   // Or maybe `Result<???>`?
  // What's the exact type of `???` still needs further discussion.
}

pub trait FunctionVerifier: Verifier {
  /// Performs integrity checks on a specific function.
  fn verify(&self, _func: Function, _data: &FunctionData) -> ???;
}

Visibility

Internal verifiers can of course read pub(crate), but how can third-party verifiers do so? Therefore, anything that needs to be read by a verifier should ultimately be exposed as pub. Fundamentally, this issue boils down to the design of the crate's interface.

This part may require further discussion.

[MaxXSoft]

Furthermore, the design of the VerifierManager remains to be clarified.

This component could be implemented in a very simple manner, or it could be quite complex.

[hsqStephenZhang]

Thanks for the detailed reply.

A few comments:

1. This new interface design is better.
2. The visibility issue is conceptually problematic, but not necessarily in practice. Most pub(in crate::ir) methods are intended for constructing things rather than accessing them, so the accessing should be fine. Moreover, we could expose the limitations of the current visibility design by implementing some verifiers outside the source tree, which would naturally reveal any visibility-related issues.
3. The VerifierManager could simply invoke all verifiers sequentially.
4. The return type should look like Result<(), VerifyErrors> to be able to accumulate the errors. Could borrow cranelift's design https://github.com/bytecodealliance/wasmtime/blob/1f4f816f7c4019842122d7191a411541169a8e00/cranelift/codegen/src/verifier/mod.rs#L177.

Just thought of another question, should we use FxHashMap to get deterministic output? Or the printed IR is unstable.

[MaxXSoft]

One issue with exposing internal fields is that some internal implementations may not be stable. If there are explicit external dependencies, subsequently modifying such APIs becomes difficult. In this scenario, the outdated out-of-tree verifier would trigger some compilation errors, while the in-tree verifier would remain unaffected.

Another approach is to use a compile-time reflection crate to provide a "read field by name" interface. If the field does not exist, it returns None, like a hash map. But I have no idea what a verifier could possibly do after reading a non-existent field, if we simply want to enable some old out-of-tree verifiers to compile.

Just thought of another question, should we use FxHashMap to get deterministic output? Or the printed IR is unstable.

Yes, I think FxHashMap and deterministic output are helpful.