feat(verifier): check dominance by regehr · Pull Request #944 · opencompl/veir

regehr · 2026-06-28T19:09:14Z

ok this is a substantial tooling up of our verifier. the patch got bigger and messier than I wanted, but I think it's all good changes.
the main thing this does is attempts to make our verifier return the same verdict as MLIR's verifier, for a variety of interesting cases. so there are lots of new tests! and also there's a new test predicate VEIR_MLIR_SAME_VERDICT that insists that either mlir-opt and veir-opt both accept or both reject a test case.
I had to change a bunch of unrelated test cases-- these are ones that are rejected by upstream MLIR, and now are rejected by Veir.
the other goal of this patch is to hopefully set us up to de-axiomitize Veir/Dominance.lean. our goal is that this verifier acts as a dynamic checker for freshly parsed code, and after that all transformations must prove that their output is verified if their input is.

github-actions

VeIR Benchmarks

Details

Benchmark suite	Current: `4ee9633`	Previous: `a8086a5`	Ratio
`add-fold-worklist/create`	`1833000` ns (`± 104438`)	`2191000` ns (`± 116585`)	`0.84`
`add-fold-worklist/rewrite`	`3598000` ns (`± 112494`)	`4025500` ns (`± 99281`)	`0.89`
`add-fold-worklist-local/create`	`1832000` ns (`± 35506`)	`2104000` ns (`± 59879`)	`0.87`
`add-fold-worklist-local/rewrite`	`2914000` ns (`± 68372`)	`3305000` ns (`± 90508`)	`0.88`
`add-zero-worklist/create`	`1827000` ns (`± 40016`)	`2234000` ns (`± 109081`)	`0.82`
`add-zero-worklist/rewrite`	`2290000` ns (`± 22289`)	`2750000` ns (`± 105299`)	`0.83`
`add-zero-reuse-worklist/create`	`1504000` ns (`± 5495`)	`1842000` ns (`± 83972`)	`0.82`
`add-zero-reuse-worklist/rewrite`	`1843000` ns (`± 54784`)	`2160000` ns (`± 52555`)	`0.85`
`mul-two-worklist/create`	`1808000` ns (`± 50525`)	`2231000` ns (`± 55895`)	`0.81`
`mul-two-worklist/rewrite`	`5052000` ns (`± 70031`)	`5644500` ns (`± 283151`)	`0.90`
`add-fold-forwards/create`	`1869000` ns (`± 72871`)	`2202000` ns (`± 109662`)	`0.85`
`add-fold-forwards/rewrite`	`2664000` ns (`± 39480`)	`3032000` ns (`± 65213`)	`0.88`
`add-zero-forwards/create`	`1819000` ns (`± 21490`)	`2265000` ns (`± 96205`)	`0.80`
`add-zero-forwards/rewrite`	`1754000` ns (`± 17641`)	`1987500` ns (`± 93854`)	`0.88`
`add-zero-reuse-forwards/create`	`1536500` ns (`± 66860`)	`1832000` ns (`± 89057`)	`0.84`
`add-zero-reuse-forwards/rewrite`	`1425000` ns (`± 71827`)	`1542000` ns (`± 22638`)	`0.92`
`mul-two-forwards/create`	`1849000` ns (`± 62588`)	`2198000` ns (`± 41455`)	`0.84`
`mul-two-forwards/rewrite`	`3249000` ns (`± 35550`)	`3767000` ns (`± 172147`)	`0.86`
`add-zero-reuse-first/create`	`1536500` ns (`± 41607`)	`1855500` ns (`± 114257`)	`0.83`
`add-zero-reuse-first/rewrite`	`9000` ns (`± 1965`)	`8500` ns (`± 2543`)	`1.06`
`add-zero-lots-of-reuse-first/create`	`1534000` ns (`± 25225`)	`1789000` ns (`± 89329`)	`0.86`
`add-zero-lots-of-reuse-first/rewrite`	`759000` ns (`± 11803`)	`803000` ns (`± 57817`)	`0.95`

This comment was automatically generated by workflow using github-action-benchmark.

axelcool1234

My first skim of this PR. Will give another review round when I'm not busy :)

axelcool1234 · 2026-06-29T02:45:55Z

For the dominance analysis changes, LGTM :)

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

math-fehr

Very cool! I added a few comments, but otherwise the design seems great!
Quick question, it seems you are saying graph regions can sometimes have multiple blocks (like in a unregistered operation). Is this something from MLIR?

Also, for next time, it would probably have been easier for me if some parts of the PR (like the additions of verifiers about terminators, not necessarily dominance) would have been split. But no need for this time since I reviewed it!

math-fehr · 2026-07-11T20:57:35Z

@@ -0,0 +1,24 @@
+// RUN: not veir-opt %s 2>&1 | filecheck %s
+// RUN: VEIR_MLIR_SAME_VERDICT


Gavin added MLIR_INVALID, maybe we should use that instead of adding VEIR_MLIR_SAME_VERDICT?

math-fehr · 2026-07-12T01:17:53Z

+    "test.test"() ({
+    ^g0():
+      %a = "test.test"() : () -> i64
+    ^g1():
+      "test.test"(%a, %v) : (i64, i64) -> ()
+    }) : () -> ()


I do not understand why this test actually passes?
You mention in the comment that test.test is a graph region, but in that case graph regions only have a single block!
In general, any block that is part of a multi-block region should have a terminator

math-fehr · 2026-07-12T01:19:52Z

+// Dominance is only required in SSACFG regions. The body of an unregistered op
+// is a graph region, where a value defined in one block may be used in another


It is not actually true that the body of an unregistered op is a graph region.
Because graph regions have only a single block, this means that whenever any operation has a region with multiple blocks, the region needs to be a SSACFG region.

math-fehr · 2026-07-12T01:33:18Z

+  -- In a graph region every dominator (including the block itself) properly
+  -- dominates the block; in an SSACFG region a block does not properly dominate
+  -- itself.


Where does this rule come from?
My understanding is that "properly dominates" means dominates and not equal?

math-fehr · 2026-07-12T01:40:06Z

-    true
-  else
-    let some idom := block.getIDom? dfCtx irCtx | return false
-    idom ≠ block && dominatesWithinRegion dominator idom dfCtx irCtx
+    return true
+  -- In a graph region there is no block ordering, so every block dominates every
+  -- other block in the region.
+  if let some region := (block.get! irCtx).parent then
+    if !region.hasSSADominanceByKind irCtx then
+      return true
+  let some idom := block.getIDom? dfCtx irCtx | return false
+  return idom ≠ block && dominatesWithinRegion dominator idom dfCtx irCtx


There can only be a single block in a graph region, so this function should probably be unchanged?

math-fehr · 2026-07-12T01:46:08Z

+    match dominator.block! irCtx with
+    | some block =>
+      match (block.get! irCtx).parent with
+      | some region => !region.hasSSADominanceByKind irCtx
+      | none => false
+    | none => false


Should this code be factored somewhere? You also use the exact same one earlier

math-fehr · 2026-07-12T01:51:30Z

+  if op.getNumSuccessors ctx.raw opIn ≠ 0 && operation.next.isSome then
+    throw "operation with block successors must terminate its parent block"


Only terminators can have successors. So maybe there is a stronger check to be made somewhere about this?

math-fehr · 2026-07-12T01:54:47Z

+    | none => pure ()
+    | some useRegion =>
+      let instrName := String.fromUTF8! (op.getOpType ctx.raw opIn).name
+      for i in [0:op.getNumOperands ctx.raw opIn] do


Suggested change

for i in [0:op.getNumOperands ctx.raw opIn] do

for i in 0...op.getNumOperands ctx.raw opIn do

I believe this is the standard notation for ranges (unless it is ..).
This avoids allocating a list

math-fehr · 2026-07-12T02:02:30Z

+  -- A consequence, shared with MLIR, is that a use hidden in a *non-entry* block
+  -- of a graph region with no intra-region control-flow edges is unreachable and
+  -- therefore not checked, even if it captures a value that does not dominate the
+  -- graph-owning operation. (A capture used in the graph region's *entry* block
+  -- is still checked, because the entry block is always reachable.)


I would argue that if an operation is unreachable, then its operands are dominated by the value definitions. This is because dominance is defined as "all path that goes to A goes first to B", but here since there is no path, it is trivially correct!

This has the same effect (that we don't need to check unreachable blocks), but the reasoning is different (and will be reflected in the proof).

math-fehr · 2026-07-12T02:05:05Z

+    let some dfCtx := fixpointSolve top #[DominanceAnalysis] ctx.raw
+      | throw "dominance analysis did not terminate"
+    ctx.raw.forOpsDepM fun op opIn =>
+      op.verifyOperandDominance ctx dfCtx opIn


This will actually break if we have any operation that wasn't deallocated, nor inserted in the module.
We can keep it as-is here, but we'll have to fix it at some point (hopefully after I add walkers to walk the IR a bit more nicely).

regehr added 10 commits June 27, 2026 17:00

first version

9bd8095

more checks matching upstream MLIR and also tests

6cf5ddd

more workin

e3dc900

docs

80d9809

work

b008928

work

e5a35ec

more tests

66709c0

Merge remote-tracking branch 'origin/main' into regehr/dominance-checker

6b40104

better testing

73c84e3

rename test predicate

9c9abb5

regehr requested review from axelcool1234, math-fehr and tobiasgrosser June 28, 2026 19:09

regehr self-assigned this Jun 28, 2026

github-actions Bot reviewed Jun 28, 2026

View reviewed changes

axelcool1234 reviewed Jun 28, 2026

View reviewed changes

Comment thread Veir/IR/Dominance.lean

Comment thread Veir/IR/Dominance.lean

add a quote from the MLIR docs

8072c62

regehr and others added 2 commits June 30, 2026 08:18

Merge remote-tracking branch 'origin/main' into regehr/dominance-checker

41ff357

Merge remote-tracking branch 'origin/main' into regehr/dominance-checker

4ee9633

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

math-fehr reviewed Jul 12, 2026

View reviewed changes

		@@ -0,0 +1,24 @@
		// RUN: not veir-opt %s 2>&1 \| filecheck %s
		// RUN: VEIR_MLIR_SAME_VERDICT

		// Dominance is only required in SSACFG regions. The body of an unregistered op
		// is a graph region, where a value defined in one block may be used in another

		if op.getNumSuccessors ctx.raw opIn ≠ 0 && operation.next.isSome then
		throw "operation with block successors must terminate its parent block"

	for i in [0:op.getNumOperands ctx.raw opIn] do
	for i in 0...op.getNumOperands ctx.raw opIn do

Uh oh!

Conversation

regehr commented Jun 28, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

VeIR Benchmarks

Uh oh!

axelcool1234 left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

axelcool1234 commented Jun 29, 2026

Uh oh!

math-fehr left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

regehr commented Jun 28, 2026 •

edited

Loading

github-actions Bot left a comment •

edited

Loading