From 9bd809547c31a328c0b09e936e3d5b1715fb359a Mon Sep 17 00:00:00 2001 From: John Regehr Date: Sat, 27 Jun 2026 17:00:27 -0600 Subject: [PATCH 01/10] first version --- UnitTest/DataFlowFramework/Dominance.lean | 12 ++--- Veir/IR/Dominance.lean | 8 +-- Veir/Pass.lean | 2 +- Veir/Verifier.lean | 59 ++++++++++++++++++++++- VeirInterpret.lean | 2 +- VeirOpt.lean | 2 +- 6 files changed, 70 insertions(+), 15 deletions(-) diff --git a/UnitTest/DataFlowFramework/Dominance.lean b/UnitTest/DataFlowFramework/Dominance.lean index 298a28343..e8cc13375 100644 --- a/UnitTest/DataFlowFramework/Dominance.lean +++ b/UnitTest/DataFlowFramework/Dominance.lean @@ -36,9 +36,9 @@ private def compareExpectedDominator | return #[s!"dominators {expected.name}: missing block label {expectedDom}"] let shouldProperlyDom := expectedDom ≠ expected.name let mut report := #[] - if !expectedBlock.dominates block dfCtx irCtx then + if !expectedBlock.dominatesByAnalysis block dfCtx irCtx then report := report.push s!"dominators {expected.name}: missing expected dominator {expectedDom}" - if expectedBlock.properlyDominates block dfCtx irCtx ≠ shouldProperlyDom then + if expectedBlock.properlyDominatesByAnalysis block dfCtx irCtx ≠ shouldProperlyDom then report := report.push s!"dominators {expected.name}: unexpected properlyDominates result for {expectedDom}" return report @@ -56,8 +56,8 @@ private def compareObservedDominator (expected : ExpectedBlockDominators) (dfCtx : DataFlowContext) (irCtx : IRContext OpCode) : MismatchReport := Id.run do - let observedByRelation := observedBlock.dominates block dfCtx irCtx - let observedProperly := observedBlock.properlyDominates block dfCtx irCtx + let observedByRelation := observedBlock.dominatesByAnalysis block dfCtx irCtx + let observedProperly := observedBlock.properlyDominatesByAnalysis block dfCtx irCtx let mut report := #[] if observedProperly ≠ (observedByRelation && observedBlock ≠ block) then report := report.push @@ -173,8 +173,8 @@ private def compareOperationDominance let some dominated := getNamedOperation? recovered expected.dominated irCtx | return #[s!"op dominance {expected.dominator}->{expected.dominated}: missing dominated op"] - let observedDominates := dominator.dominates dominated dfCtx irCtx - let observedProperly := dominator.properlyDominates dominated dfCtx irCtx + let observedDominates := dominator.dominatesByAnalysis dominated dfCtx irCtx + let observedProperly := dominator.properlyDominatesByAnalysis dominated dfCtx irCtx let mut report := #[] if observedDominates ≠ expected.dominates then report := report.push diff --git a/Veir/IR/Dominance.lean b/Veir/IR/Dominance.lean index ff95fa532..b0321565a 100644 --- a/Veir/IR/Dominance.lean +++ b/Veir/IR/Dominance.lean @@ -144,7 +144,7 @@ def immediateDominator? /-- Dominance query between two blocks, where a block dominates itself. -/ -def dominates +def dominatesByAnalysis [FactSpec .dominator] (dominator block : BlockPtr) (dfCtx : DataFlowContext) @@ -154,7 +154,7 @@ def dominates /-- Dominance query between two blocks, where a block does not dominate itself. -/ -def properlyDominates +def properlyDominatesByAnalysis [FactSpec .dominator] (dominator block : BlockPtr) (dfCtx : DataFlowContext) @@ -169,7 +169,7 @@ namespace OperationPtr /-- Dominance query between two operations, where an operation dominates itself. -/ -def dominates +def dominatesByAnalysis (dominator op : OperationPtr) (dfCtx : DataFlowContext) (irCtx : IRContext OpCode) : Bool := @@ -178,7 +178,7 @@ def dominates /-- Dominance query between two operations, where an operation does not dominate itself. -/ -def properlyDominates +def properlyDominatesByAnalysis (dominator op : OperationPtr) (dfCtx : DataFlowContext) (irCtx : IRContext OpCode) : Bool := diff --git a/Veir/Pass.lean b/Veir/Pass.lean index 488b6537d..4ce5f9b9a 100644 --- a/Veir/Pass.lean +++ b/Veir/Pass.lean @@ -67,7 +67,7 @@ def run (pipeline : PassPipeline OpCode) if h : moduleOp.InBounds currentCtx.raw then let ctx' ← try pass.run currentCtx moduleOp h catch errMsg => throw s!"pass '{pass.name}' failed: {errMsg}" - if let .error errMsg := ctx'.verify then + if let .error errMsg := WfIRContext.verify ctx' (some moduleOp) then throw s!"verification failed after pass '{pass.name}': {errMsg}" currentCtx := ctx' else diff --git a/Veir/Verifier.lean b/Veir/Verifier.lean index d106bccbb..7034a3278 100644 --- a/Veir/Verifier.lean +++ b/Veir/Verifier.lean @@ -1,6 +1,7 @@ module public import Veir.IR.Basic +public import Veir.IR.Dominance public import Veir.IR.Fields public import Veir.Properties public import Veir.GlobalOpInfo @@ -883,12 +884,63 @@ def BlockPtr.verifyTerminator (block : BlockPtr) (ctx : WfIRContext OpCode) if !(lastOp.getOpType! ctx.raw).isTerminator then throw "Expected the last operation of a block to be a terminator" +def ValuePtr.dominatesBeforeOp? + (value : ValuePtr) (useOp : OperationPtr) + (dfCtx : DataFlowContext) (ctx : IRContext OpCode) : Bool := + match value with + | .opResult result => + OperationPtr.properlyDominatesByAnalysis result.op useOp dfCtx ctx + | .blockArgument arg => + match (useOp.get! ctx).parent with + | some useBlock => BlockPtr.dominatesByAnalysis arg.block useBlock dfCtx ctx + | none => false + +def OperationPtr.verifyOperandDominance + (op : OperationPtr) (ctx : WfIRContext OpCode) + (dfCtx : DataFlowContext) (opIn : op.InBounds ctx.raw) : + Except String PUnit := do + -- The SSA dominance constraint only applies inside SSACFG regions and, as in + -- LLVM/MLIR, only to uses in blocks reachable from the region entry. Operands + -- used in graph regions or in unreachable code impose no dominance requirement; + -- the analysis records no dominator fact for unreachable blocks (whereas the + -- entry block has a fact with no immediate dominator). + let shouldCheck : Bool := Id.run do + let some useBlock := (op.get ctx.raw opIn).parent | return false + let some region := (useBlock.get! ctx.raw).parent | return false + let .SSACFG := region.getRegionKind ctx | return false + return (useBlock.getDominatorFact? dfCtx ctx.raw).isSome + if shouldCheck then + let instrName := String.fromUTF8! (op.getOpType ctx.raw opIn).name + for i in [0:op.getNumOperands ctx.raw opIn] do + let value := op.getOperand! ctx.raw i + if !value.dominatesBeforeOp? op dfCtx ctx.raw then + throw s!"{instrName}: operand {i} ({reprStr value}) does not dominate its use in operation {reprStr op}" + +/-- + Dynamically check the SSA dominance condition used by `ctx.Dom`: every ordinary operation + operand must dominate the point immediately before the operation that uses it. + + This is intentionally an executable checker. It does not yet provide a Lean proof of + `ctx.Dom`, but its algorithm is structured to match that property. +-/ +def WfIRContext.verifyDominance + (ctx : WfIRContext OpCode) (top : OperationPtr) : Except String Unit := do + if _ : top.InBounds ctx.raw then + 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 + else + throw s!"dominance root operation is not in bounds: {reprStr top}" + public section /-- - Verify that all operations in the IRContext satisfy their local invariants. + Verify that all operations in the IRContext satisfy their local invariants. If `top?` is + provided, also run the dynamic SSA dominance checker rooted at that operation. -/ -def WfIRContext.verify (ctx : WfIRContext OpCode) : Except String Unit := do +def WfIRContext.verify (ctx : WfIRContext OpCode) + (top? : Option OperationPtr := none) : Except String Unit := do ctx.raw.forOpsDepM (fun op opIn => do op.verifyLocalInvariants ctx opIn if let .riscv _ := op.getOpType ctx.raw opIn then @@ -902,6 +954,9 @@ def WfIRContext.verify (ctx : WfIRContext OpCode) : Except String Unit := do if region.getRegionKind ctx = .SSACFG then block.verifyTerminator ctx blockIn | none => pure ()) + match top? with + | some top => ctx.verifyDominance top + | none => pure () /-- Assert that all operations in the IRContext satisfy their local invariants. diff --git a/VeirInterpret.lean b/VeirInterpret.lean index a8480db4f..9dfa45235 100644 --- a/VeirInterpret.lean +++ b/VeirInterpret.lean @@ -95,7 +95,7 @@ def main (args : List String) : IO Unit := do | [filename] => match ← parseOperation filename with | .ok (ctx, op) => - match ctx.verify with + match WfIRContext.verify ctx (some op) with | .ok _ => let rawCtx : IRContext OpCode := ctx let mainOp ← resolveEntryPoint rawCtx op diff --git a/VeirOpt.lean b/VeirOpt.lean index 3cd256079..9c910e6c7 100644 --- a/VeirOpt.lean +++ b/VeirOpt.lean @@ -132,7 +132,7 @@ def main (args : List String) : IO Unit := do IO.eprintln errMsg IO.Process.exit 1 | .ok (ctx, op) => - match ctx.verify with + match WfIRContext.verify ctx (some op) with | .error errMsg => IO.eprintln s!"Error verifying input program: {errMsg}" IO.Process.exit 1 From 6cf5dddf04e7940fdc81f722a625429d3000da55 Mon Sep 17 00:00:00 2001 From: John Regehr Date: Sat, 27 Jun 2026 17:55:39 -0600 Subject: [PATCH 02/10] more checks matching upstream MLIR and also tests --- Test/Passes/CastsReconciliation/basic.mlir | 9 --- Test/Passes/CastsReconciliation/error.mlir | 2 - Test/Passes/DCE/basic.mlir | 3 - Test/Verifier/dominance_back_edge.mlir | 23 ++++++++ Test/Verifier/dominance_block_argument.mlir | 18 ++++++ Test/Verifier/dominance_cross_block.mlir | 19 +++++++ Test/Verifier/dominance_graph_region_ok.mlir | 17 ++++++ Test/Verifier/dominance_sibling_branch.mlir | 19 +++++++ Test/Verifier/dominance_unreachable_ok.mlir | 19 +++++++ Test/Verifier/entry_block_predecessor.mlir | 17 ++++++ Test/Verifier/graph_region_multi_block.mlir | 14 +++++ Test/Verifier/ssa_single_assignment.mlir | 15 +++++ Test/Verifier/ssa_undefined_value.mlir | 13 +++++ Veir/Verifier.lean | 58 +++++++++++++++++++- 14 files changed, 231 insertions(+), 15 deletions(-) create mode 100644 Test/Verifier/dominance_back_edge.mlir create mode 100644 Test/Verifier/dominance_block_argument.mlir create mode 100644 Test/Verifier/dominance_cross_block.mlir create mode 100644 Test/Verifier/dominance_graph_region_ok.mlir create mode 100644 Test/Verifier/dominance_sibling_branch.mlir create mode 100644 Test/Verifier/dominance_unreachable_ok.mlir create mode 100644 Test/Verifier/entry_block_predecessor.mlir create mode 100644 Test/Verifier/graph_region_multi_block.mlir create mode 100644 Test/Verifier/ssa_single_assignment.mlir create mode 100644 Test/Verifier/ssa_undefined_value.mlir diff --git a/Test/Passes/CastsReconciliation/basic.mlir b/Test/Passes/CastsReconciliation/basic.mlir index 8a89e9d7c..dda423d01 100644 --- a/Test/Passes/CastsReconciliation/basic.mlir +++ b/Test/Passes/CastsReconciliation/basic.mlir @@ -2,7 +2,6 @@ "builtin.module"() ({ - ^1(): "func.func"() <{function_type = (i64) -> ()}> ({ ^1(%0 : i64): %1 = "builtin.unrealized_conversion_cast"(%0) : (i64) -> i64 @@ -11,7 +10,6 @@ "func.return"() : () -> () }) : () -> () - ^2(): "func.func"() <{function_type = (i64) -> ()}> ({ ^1(%0 : i64): %1 = "builtin.unrealized_conversion_cast"(%0) : (i64) -> !riscv.reg @@ -21,7 +19,6 @@ "func.return"() : () -> () }) : () -> () - ^3(): "func.func"() <{function_type = (i64) -> ()}> ({ ^1(%0 : i64): // the remaining cast is unused @@ -33,7 +30,6 @@ "func.return"() : () -> () }) : () -> () - ^4(): "func.func"() <{function_type = (i64) -> ()}> ({ ^1(%0 : i64): // the remaining cast is used @@ -48,7 +44,6 @@ "func.return"() : () -> () }) : () -> () - ^5(): "func.func"() <{function_type = (i64) -> ()}> ({ ^1(%0 : i64): // identity cast and pairs of casts @@ -61,7 +56,6 @@ "func.return"() : () -> () }) : () -> () - ^6(): "func.func"() <{function_type = (i64) -> ()}> ({ ^1(%0 : i64): // pairs of casts @@ -75,7 +69,6 @@ "func.return"() : () -> () }) : () -> () - ^7(): "func.func"() <{function_type = (!riscv.reg) -> ()}> ({ ^1(%0 : !riscv.reg): // identity cast on block argument @@ -86,7 +79,6 @@ "func.return"() : () -> () }) : () -> () - ^8(): "func.func"() <{function_type = (i8) -> ()}> ({ ^1(%0 : i8): %1 = "builtin.unrealized_conversion_cast"(%0) : (i8) -> i8 @@ -95,7 +87,6 @@ "func.return"() : () -> () }) : () -> () - ^9(): "func.func"() <{function_type = (i64) -> ()}> ({ ^1(%0 : i64): // pairs of casts diff --git a/Test/Passes/CastsReconciliation/error.mlir b/Test/Passes/CastsReconciliation/error.mlir index 4ce38a3c5..ceb2ce1da 100644 --- a/Test/Passes/CastsReconciliation/error.mlir +++ b/Test/Passes/CastsReconciliation/error.mlir @@ -2,7 +2,6 @@ "builtin.module"() ({ - ^1(): "func.func"() <{function_type = (i64) -> ()}> ({ ^1(%0 : i64): %1 = "builtin.unrealized_conversion_cast"(%0) : (i64) -> i8 @@ -14,7 +13,6 @@ "func.return"() : () -> () }) : () -> () - ^2(): "func.func"() <{function_type = (i64) -> ()}> ({ ^1(%0 : i64): %1 = "builtin.unrealized_conversion_cast"(%0) : (i64) -> !riscv.reg diff --git a/Test/Passes/DCE/basic.mlir b/Test/Passes/DCE/basic.mlir index d2970c801..51ce7a6e1 100644 --- a/Test/Passes/DCE/basic.mlir +++ b/Test/Passes/DCE/basic.mlir @@ -5,7 +5,6 @@ "builtin.module"() ({ // An operation that returns one unused result - ^4(): "func.func"() <{function_type = (i64) -> ()}> ({ ^6(%1 : i64): %2 = "llvm.add"(%1, %1) : (i64, i64) -> i64 @@ -18,7 +17,6 @@ }) : () -> () // A chain of operations that is eventually unused - ^5(): "func.func"() <{function_type = () -> ()}> ({ ^6(): %1 = "arith.constant"() <{ "value" = 1 : i64 }> : () -> i64 @@ -34,7 +32,6 @@ }) : () -> () // A chain of operations that is eventually used - ^6(): "func.func"() <{function_type = () -> ()}> ({ ^6(): %1 = "arith.constant"() <{ "value" = 1 : i64 }> : () -> i64 diff --git a/Test/Verifier/dominance_back_edge.mlir b/Test/Verifier/dominance_back_edge.mlir new file mode 100644 index 000000000..becbb2977 --- /dev/null +++ b/Test/Verifier/dominance_back_edge.mlir @@ -0,0 +1,23 @@ +// RUN: not veir-opt %s 2>&1 | filecheck %s + +// %x is defined in the loop body but used in the loop header. The header is +// reachable from ^entry without going through ^body, so ^body does not dominate +// the header and the use of %x there is invalid. + +"builtin.module"() ({ + "func.func"() <{function_type = () -> i32, sym_name = "main"}> ({ + ^entry(): + "cf.br"() [^header] : () -> () + ^body(): + %x = "arith.constant"() <{"value" = 5 : i32}> : () -> i32 + "cf.br"() [^header] : () -> () + ^header(): + %y = "arith.addi"(%x, %x) : (i32, i32) -> i32 + %c = "arith.constant"() <{"value" = 1 : i1}> : () -> i1 + "cf.cond_br"(%c) [^body, ^exit] <{"branch_weights" = array, "operandSegmentSizes" = array}> : (i1) -> () + ^exit(): + "func.return"(%y) : (i32) -> () + }) : () -> () +}) : () -> () + +// CHECK: arith.addi: operand 0 {{.*}} does not dominate its use diff --git a/Test/Verifier/dominance_block_argument.mlir b/Test/Verifier/dominance_block_argument.mlir new file mode 100644 index 000000000..72694a066 --- /dev/null +++ b/Test/Verifier/dominance_block_argument.mlir @@ -0,0 +1,18 @@ +// RUN: not veir-opt %s 2>&1 | filecheck %s + +// Block arguments are subject to the same dominance rule as op results. %arg is +// an argument of ^a, but it is used in ^b, and ^a does not dominate ^b (^b is +// also reachable directly from ^entry). + +"builtin.module"() ({ + "func.func"() <{function_type = (i1) -> i1, sym_name = "main"}> ({ + ^entry(%c : i1): + "cf.cond_br"(%c, %c) [^a, ^b] <{"branch_weights" = array, "operandSegmentSizes" = array}> : (i1, i1) -> () + ^a(%arg : i1): + "cf.br"() [^b] : () -> () + ^b: + "func.return"(%arg) : (i1) -> () + }) : () -> () +}) : () -> () + +// CHECK: func.return: operand 0 {{.*}} does not dominate its use diff --git a/Test/Verifier/dominance_cross_block.mlir b/Test/Verifier/dominance_cross_block.mlir new file mode 100644 index 000000000..92f56ef33 --- /dev/null +++ b/Test/Verifier/dominance_cross_block.mlir @@ -0,0 +1,19 @@ +// RUN: not veir-opt %s 2>&1 | filecheck %s + +// %x is defined in ^a but used in ^b. ^a does not dominate ^b, because ^b is +// also reachable directly from ^entry, so this violates SSA dominance even +// though every name is assigned exactly once and every use is defined. + +"builtin.module"() ({ + "func.func"() <{function_type = (i1) -> i32, sym_name = "main"}> ({ + ^entry(%c : i1): + "cf.cond_br"(%c) [^a, ^b] <{"branch_weights" = array, "operandSegmentSizes" = array}> : (i1) -> () + ^a: + %x = "arith.constant"() <{"value" = 42 : i32}> : () -> i32 + "cf.br"() [^b] : () -> () + ^b: + "func.return"(%x) : (i32) -> () + }) : () -> () +}) : () -> () + +// CHECK: func.return: operand 0 {{.*}} does not dominate its use diff --git a/Test/Verifier/dominance_graph_region_ok.mlir b/Test/Verifier/dominance_graph_region_ok.mlir new file mode 100644 index 000000000..45d2e5dde --- /dev/null +++ b/Test/Verifier/dominance_graph_region_ok.mlir @@ -0,0 +1,17 @@ +// RUN: veir-opt %s | filecheck %s + +// 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 +// block that it does not dominate, so this program verifies. + +"builtin.module"() ({ + "test.test"() ({ + ^bb0: + %v = "test.test"() : () -> i32 + ^bb1: + "test.test"(%v) : (i32) -> () + }) : () -> () +}) : () -> () + +// CHECK: %[[V:.*]] = "test.test"() : () -> i32 +// CHECK: "test.test"(%[[V]]) : (i32) -> () diff --git a/Test/Verifier/dominance_sibling_branch.mlir b/Test/Verifier/dominance_sibling_branch.mlir new file mode 100644 index 000000000..f039802ea --- /dev/null +++ b/Test/Verifier/dominance_sibling_branch.mlir @@ -0,0 +1,19 @@ +// RUN: not veir-opt %s 2>&1 | filecheck %s + +// %x is defined in ^then and used in the sibling block ^else. Neither branch of +// the conditional dominates the other, so the use in ^else is not dominated by +// its definition. + +"builtin.module"() ({ + "func.func"() <{function_type = (i1) -> i32, sym_name = "main"}> ({ + ^entry(%c : i1): + "cf.cond_br"(%c) [^then, ^else] <{"branch_weights" = array, "operandSegmentSizes" = array}> : (i1) -> () + ^then: + %x = "arith.constant"() <{"value" = 7 : i32}> : () -> i32 + "func.return"(%x) : (i32) -> () + ^else: + "func.return"(%x) : (i32) -> () + }) : () -> () +}) : () -> () + +// CHECK: func.return: operand 0 {{.*}} does not dominate its use diff --git a/Test/Verifier/dominance_unreachable_ok.mlir b/Test/Verifier/dominance_unreachable_ok.mlir new file mode 100644 index 000000000..d0267fcdb --- /dev/null +++ b/Test/Verifier/dominance_unreachable_ok.mlir @@ -0,0 +1,19 @@ +// RUN: veir-opt %s | filecheck %s + +// Like LLVM/MLIR, the dominance check is skipped for unreachable blocks. ^dead +// has no predecessors (^entry returns), so its use of %v imposes no dominance +// requirement and the program verifies. + +"builtin.module"() ({ + "func.func"() <{function_type = () -> i32, sym_name = "main"}> ({ + ^entry(): + %v = "arith.constant"() <{"value" = 0 : i32}> : () -> i32 + "func.return"(%v) : (i32) -> () + ^dead(): + "func.return"(%v) : (i32) -> () + }) : () -> () +}) : () -> () + +// CHECK: %[[V:.*]] = "arith.constant"() <{"value" = 0 : i32}> : () -> i32 +// CHECK-NEXT: "func.return"(%[[V]]) : (i32) -> () +// CHECK: "func.return"(%[[V]]) : (i32) -> () diff --git a/Test/Verifier/entry_block_predecessor.mlir b/Test/Verifier/entry_block_predecessor.mlir new file mode 100644 index 000000000..2f8b7b73f --- /dev/null +++ b/Test/Verifier/entry_block_predecessor.mlir @@ -0,0 +1,17 @@ +// RUN: not veir-opt %s 2>&1 | filecheck %s + +// The entry block of a region may not have predecessors. Here ^bb1 branches back +// to the entry block ^bb0, which would mean the region is re-entered through its +// entry block and breaks the assumption that the entry block dominates the rest +// of the region. + +"builtin.module"() ({ + "func.func"() <{function_type = () -> (), sym_name = "main"}> ({ + ^bb0(): + "cf.br"() [^bb1] : () -> () + ^bb1(): + "cf.br"() [^bb0] : () -> () + }) : () -> () +}) : () -> () + +// CHECK: entry block of a region may not have predecessors diff --git a/Test/Verifier/graph_region_multi_block.mlir b/Test/Verifier/graph_region_multi_block.mlir new file mode 100644 index 000000000..8b7aeae1b --- /dev/null +++ b/Test/Verifier/graph_region_multi_block.mlir @@ -0,0 +1,14 @@ +// RUN: not veir-opt %s 2>&1 | filecheck %s + +// builtin.module is a registered op with a graph region, so its region may have +// at most one block. (Unregistered ops and the test dialect are exempt and may +// use multi-block graph regions.) + +"builtin.module"() ({ +^bb0: + "func.func"() <{function_type = () -> (), sym_name = "a"}> ({ ^e0: "func.return"() : () -> () }) : () -> () +^bb1: + "func.func"() <{function_type = () -> (), sym_name = "b"}> ({ ^e1: "func.return"() : () -> () }) : () -> () +}) : () -> () + +// CHECK: expects graph region 0 to have 0 or 1 blocks diff --git a/Test/Verifier/ssa_single_assignment.mlir b/Test/Verifier/ssa_single_assignment.mlir new file mode 100644 index 000000000..ec30e11f3 --- /dev/null +++ b/Test/Verifier/ssa_single_assignment.mlir @@ -0,0 +1,15 @@ +// RUN: not veir-opt %s 2>&1 | filecheck %s + +// SSA requires that each name is assigned exactly once. Defining %a twice is +// rejected by the parser, before verification runs. + +"builtin.module"() ({ + "func.func"() <{function_type = () -> i32, sym_name = "main"}> ({ + ^bb0(): + %a = "arith.constant"() <{"value" = 0 : i32}> : () -> i32 + %a = "arith.constant"() <{"value" = 1 : i32}> : () -> i32 + "func.return"(%a) : (i32) -> () + }) : () -> () +}) : () -> () + +// CHECK: value %a has already been defined diff --git a/Test/Verifier/ssa_undefined_value.mlir b/Test/Verifier/ssa_undefined_value.mlir new file mode 100644 index 000000000..96db0de67 --- /dev/null +++ b/Test/Verifier/ssa_undefined_value.mlir @@ -0,0 +1,13 @@ +// RUN: not veir-opt %s 2>&1 | filecheck %s + +// Every used SSA name must be defined somewhere. A use of a name that is never +// assigned is rejected by the parser, before verification runs. + +"builtin.module"() ({ + "func.func"() <{function_type = () -> i32, sym_name = "main"}> ({ + ^bb0(): + "func.return"(%missing) : (i32) -> () + }) : () -> () +}) : () -> () + +// CHECK: use of undefined value %missing diff --git a/Veir/Verifier.lean b/Veir/Verifier.lean index 7034a3278..dc8d0a242 100644 --- a/Veir/Verifier.lean +++ b/Veir/Verifier.lean @@ -871,6 +871,59 @@ def OperationPtr.verifyTerminatorPosition (op : OperationPtr) (ctx : WfIRContext if operation.opType.isTerminator && operation.next.isSome then throw "Expected a terminator to be the last operation of its block" +/-- + Verify that no operation branches to the entry block of a region. The entry + block of a region may not have predecessors: it is the unique block that the + region is entered through, and dominance assumes it dominates every other block + in the region. +-/ +def OperationPtr.verifyDoesNotBranchToEntryBlock (op : OperationPtr) (ctx : WfIRContext OpCode) + (opIn : op.InBounds ctx.raw) : Except String PUnit := do + for succ in op.getSuccessors ctx.raw opIn do + match (succ.get! ctx.raw).parent with + | some region => + if (region.get! ctx.raw).firstBlock = some succ then + throw "entry block of a region may not have predecessors" + | none => pure () + +/-- + Verify that every successor of an operation lies in the same region as the + operation itself. Control flow may not branch out of its enclosing region. + + This cannot be expressed in the textual format (block labels are region-scoped, + so the parser already rejects a reference to a block in another region), but it + guards against passes that build malformed cross-region control flow. +-/ +def OperationPtr.verifySuccessorsInSameRegion (op : OperationPtr) (ctx : WfIRContext OpCode) + (opIn : op.InBounds ctx.raw) : Except String PUnit := do + match (op.get ctx.raw opIn).parent with + | none => pure () + | some block => + let blockRegion := (block.get! ctx.raw).parent + for succ in op.getSuccessors ctx.raw opIn do + if (succ.get! ctx.raw).parent ≠ blockRegion then + throw "branching to a block of a different region" + +/-- + Verify that graph regions of registered operations contain at most one block. + Like MLIR, this restriction limits the cases transforms must handle; it applies + only to registered operations, so unregistered ops and the test dialect may + still use multi-block graph regions. +-/ +def OperationPtr.verifyGraphRegionBlockCount (op : OperationPtr) (ctx : WfIRContext OpCode) + (opIn : op.InBounds ctx.raw) : Except String PUnit := do + let opCode := op.getOpType ctx.raw opIn + match opCode with + | .builtin .unregistered | .test .test => pure () + | _ => + for i in [0:op.getNumRegions ctx.raw opIn] do + if opCode.getRegionKind i = .Graph then + match (op.getRegion! ctx.raw i |>.get! ctx.raw).firstBlock with + | some b => + if (b.get! ctx.raw).next.isSome then + throw s!"expects graph region {i} to have 0 or 1 blocks" + | none => pure () + /-- Check that a block is non-empty and its last operation is a terminator. @@ -947,7 +1000,10 @@ def WfIRContext.verify (ctx : WfIRContext OpCode) op.verifyRISCVRegisterTypes ctx opIn match (op.get ctx.raw opIn).parent with | some _ => op.verifyTerminatorPosition ctx opIn - | none => pure ()) + | none => pure () + op.verifyDoesNotBranchToEntryBlock ctx opIn + op.verifySuccessorsInSameRegion ctx opIn + op.verifyGraphRegionBlockCount ctx opIn) ctx.raw.forBlocksDepM (fun block blockIn => do match (block.get ctx.raw blockIn).parent with | some region => From e3dc900c046f6f898ccc5de5800a1b0f9d7bb979 Mon Sep 17 00:00:00 2001 From: John Regehr Date: Sat, 27 Jun 2026 20:06:24 -0600 Subject: [PATCH 03/10] more workin --- Test/Verifier/isolation_from_above.mlir | 19 +++++++ Test/Verifier/isolation_nested_region_ok.mlir | 19 +++++++ Veir/GlobalOpInfo.lean | 13 +++++ Veir/Verifier.lean | 56 ++++++++++++++++++- 4 files changed, 106 insertions(+), 1 deletion(-) create mode 100644 Test/Verifier/isolation_from_above.mlir create mode 100644 Test/Verifier/isolation_nested_region_ok.mlir diff --git a/Test/Verifier/isolation_from_above.mlir b/Test/Verifier/isolation_from_above.mlir new file mode 100644 index 000000000..3fe491306 --- /dev/null +++ b/Test/Verifier/isolation_from_above.mlir @@ -0,0 +1,19 @@ +// RUN: not veir-opt %s 2>&1 | filecheck %s + +// func.func is isolated from above: the body of @inner may not reference %k, +// which is defined in the enclosing function @outer. + +"builtin.module"() ({ + "func.func"() <{function_type = () -> (), sym_name = "outer"}> ({ + ^bb0(): + %k = "arith.constant"() <{"value" = 1 : i64}> : () -> i64 + "func.func"() <{function_type = () -> (), sym_name = "inner"}> ({ + ^bb1(): + "test.test"(%k) : (i64) -> () + "func.return"() : () -> () + }) : () -> () + "func.return"() : () -> () + }) : () -> () +}) : () -> () + +// CHECK: uses a value defined outside the isolated region diff --git a/Test/Verifier/isolation_nested_region_ok.mlir b/Test/Verifier/isolation_nested_region_ok.mlir new file mode 100644 index 000000000..aee65b827 --- /dev/null +++ b/Test/Verifier/isolation_nested_region_ok.mlir @@ -0,0 +1,19 @@ +// RUN: veir-opt %s | filecheck %s + +// A non-isolated nested region (the body of an unregistered test.test op) may +// reference values from an enclosing region. Only IsolatedFromAbove ops, such as +// func.func, form a barrier, so this program verifies. + +"builtin.module"() ({ + "func.func"() <{function_type = (i64) -> (), sym_name = "f"}> ({ + ^bb0(%a : i64): + "test.test"() ({ + ^bb1(): + "test.test"(%a) : (i64) -> () + }) : () -> () + "func.return"() : () -> () + }) : () -> () +}) : () -> () + +// CHECK: ^{{.*}}(%[[A:.*]] : i64): +// CHECK: "test.test"(%[[A]]) : (i64) -> () diff --git a/Veir/GlobalOpInfo.lean b/Veir/GlobalOpInfo.lean index 2714e4273..e47ebcad8 100644 --- a/Veir/GlobalOpInfo.lean +++ b/Veir/GlobalOpInfo.lean @@ -368,6 +368,19 @@ def OpCode.getRegionKind (opCode : OpCode) (_index : Nat) : RegionKind := | .test .test => .Graph | _ => .SSACFG +/-- + Whether this operation defines `IsolatedFromAbove` regions: operations nested + inside its regions may not reference SSA values defined outside the operation. + This mirrors MLIR, where symbol-table ops like modules and functions are + isolated from above. +-/ +def OpCode.isIsolatedFromAbove (opCode : OpCode) : Bool := + match opCode with + | .builtin .module + | .func .func + | .llvm .func => true + | _ => false + /-- Does this OpCode count as an MLIR basic block terminator? -/ diff --git a/Veir/Verifier.lean b/Veir/Verifier.lean index dc8d0a242..c2ed3fa0e 100644 --- a/Veir/Verifier.lean +++ b/Veir/Verifier.lean @@ -904,6 +904,59 @@ def OperationPtr.verifySuccessorsInSameRegion (op : OperationPtr) (ctx : WfIRCon if (succ.get! ctx.raw).parent ≠ blockRegion then throw "branching to a block of a different region" +/-- + Starting from `region` (the region containing a use) and walking outward, decide + whether an `IsolatedFromAbove` barrier is crossed before reaching `defRegion` + (the region containing the used value's definition). Reaching `defRegion` first + means the use is in scope; crossing a barrier first means the value escapes it. +-/ +private partial def regionEscapesIsolation + (defRegion region : RegionPtr) (ctx : WfIRContext OpCode) : Bool := + if region = defRegion then + false + else + match (region.get! ctx.raw).parent with + | none => false + | some parentOp => + if (parentOp.getOpType! ctx.raw).isIsolatedFromAbove then + true + else + match (parentOp.get! ctx.raw).parent with + | none => false + | some parentBlock => + match (parentBlock.get! ctx.raw).parent with + | none => false + | some parentRegion => regionEscapesIsolation defRegion parentRegion ctx + +/-- + Verify the `IsolatedFromAbove` property: an operation nested inside an isolated + region may not use a value defined outside the nearest enclosing isolated + operation. +-/ +def OperationPtr.verifyOperandIsolation (op : OperationPtr) (ctx : WfIRContext OpCode) + (opIn : op.InBounds ctx.raw) : Except String PUnit := do + match (op.get ctx.raw opIn).parent with + | none => pure () + | some useBlock => + match (useBlock.get! ctx.raw).parent with + | none => pure () + | some useRegion => + let instrName := String.fromUTF8! (op.getOpType ctx.raw opIn).name + for i in [0:op.getNumOperands ctx.raw opIn] do + let value := op.getOperand! ctx.raw i + let defBlock? : Option BlockPtr := + match value with + | .opResult result => (result.op.get! ctx.raw).parent + | .blockArgument arg => some arg.block + match defBlock? with + | none => pure () + | some defBlock => + match (defBlock.get! ctx.raw).parent with + | none => pure () + | some defRegion => + if regionEscapesIsolation defRegion useRegion ctx then + throw s!"{instrName}: operand {i} ({reprStr value}) uses a value defined outside the isolated region that encloses its use" + /-- Verify that graph regions of registered operations contain at most one block. Like MLIR, this restriction limits the cases transforms must handle; it applies @@ -1003,7 +1056,8 @@ def WfIRContext.verify (ctx : WfIRContext OpCode) | none => pure () op.verifyDoesNotBranchToEntryBlock ctx opIn op.verifySuccessorsInSameRegion ctx opIn - op.verifyGraphRegionBlockCount ctx opIn) + op.verifyGraphRegionBlockCount ctx opIn + op.verifyOperandIsolation ctx opIn) ctx.raw.forBlocksDepM (fun block blockIn => do match (block.get ctx.raw blockIn).parent with | some region => From 80d98098b0a4620f8b20b7ee30d7bc34fdd01a16 Mon Sep 17 00:00:00 2001 From: John Regehr Date: Sat, 27 Jun 2026 20:12:22 -0600 Subject: [PATCH 04/10] docs --- Veir/Dominance.lean | 8 +++++++ Veir/Verifier.lean | 52 +++++++++++++++++++++++++++++++++++++++++---- 2 files changed, 56 insertions(+), 4 deletions(-) diff --git a/Veir/Dominance.lean b/Veir/Dominance.lean index 9ec6c198b..58f40c80b 100644 --- a/Veir/Dominance.lean +++ b/Veir/Dominance.lean @@ -119,6 +119,14 @@ SSA dominance. /-- A predicate that states that the values in the IR context are used in operations that are dominated by the operation or block that defines them. + + `WfIRContext.verifyDominance` (in `Veir/Verifier.lean`) is the executable decision + procedure for this predicate: it visits every in-bounds operation and every operand, + and for each checks `value.dominatesIp (InsertPoint.before op) ctx` via the dominance + analysis. A successful run is intended to witness exactly `ctx.Dom`; the checker is + written so that each step matches a clause of this definition. (`ctx.Dom` assumes + SSACFG regions, and the checker restricts itself to SSACFG, reachable blocks + accordingly.) -/ def WfIRContext.Dom (ctx : WfIRContext OpInfo) : Prop := ∀ {op : OperationPtr} (_opInBounds : op.InBounds ctx.raw) {value : ValuePtr}, diff --git a/Veir/Verifier.lean b/Veir/Verifier.lean index c2ed3fa0e..e1a341ba2 100644 --- a/Veir/Verifier.lean +++ b/Veir/Verifier.lean @@ -990,6 +990,27 @@ def BlockPtr.verifyTerminator (block : BlockPtr) (ctx : WfIRContext OpCode) if !(lastOp.getOpType! ctx.raw).isTerminator then throw "Expected the last operation of a block to be a terminator" +/-- + Decide the per-operand condition of `WfIRContext.Dom` (see `Veir/Dominance.lean`): + whether `value` dominates the program point immediately before `useOp`, i.e. the + proposition `value.dominatesIp (InsertPoint.before useOp) ctx`. + + The two `ValuePtr` cases mirror the two ways a value is defined: + + * `.opResult result` — the result is available immediately after `result.op`, so + it dominates the point before `useOp` exactly when `result.op` *strictly* + dominates `useOp` (mirroring `OperationPtr.dominatesIp_before`, which relates + `dominatesIp (.before _)` to `strictlyDominates`). `properlyDominatesByAnalysis` + decides precisely that strict-dominance fact. + + * `.blockArgument arg` — a block argument is live from the top of `arg.block`, so + it dominates the point before `useOp` exactly when `arg.block` dominates + `useOp`'s block (reflexively — the same block counts, since the argument + precedes every operation in it). `dominatesByAnalysis` decides that. + + So `dominatesBeforeOp? value useOp = true` is exactly the clause `ctx.Dom` + demands of the `(value, useOp)` pair. +-/ def ValuePtr.dominatesBeforeOp? (value : ValuePtr) (useOp : OperationPtr) (dfCtx : DataFlowContext) (ctx : IRContext OpCode) : Bool := @@ -1017,17 +1038,40 @@ def OperationPtr.verifyOperandDominance return (useBlock.getDominatorFact? dfCtx ctx.raw).isSome if shouldCheck then let instrName := String.fromUTF8! (op.getOpType ctx.raw opIn).name + -- The inner `∀ value ∈ op.getOperands!` of `ctx.Dom`: these indices enumerate + -- exactly `op.getOperands!`, and `dominatesBeforeOp?` decides the required + -- `value.dominatesIp (InsertPoint.before op) ctx` for each one. for i in [0:op.getNumOperands ctx.raw opIn] do let value := op.getOperand! ctx.raw i if !value.dominatesBeforeOp? op dfCtx ctx.raw then throw s!"{instrName}: operand {i} ({reprStr value}) does not dominate its use in operation {reprStr op}" /-- - Dynamically check the SSA dominance condition used by `ctx.Dom`: every ordinary operation - operand must dominate the point immediately before the operation that uses it. + Executable decision procedure for `WfIRContext.Dom` (defined in `Veir/Dominance.lean`). + + `ctx.Dom` is: + + ∀ (op) (_ : op.InBounds ctx.raw) (value), + value ∈ op.getOperands! ctx.raw → + value.dominatesIp (InsertPoint.before op) ctx + + and this checker discharges that proposition clause for clause: + + * `forOpsDepM` visits every in-bounds operation — the outer `∀ op`. + * `verifyOperandDominance` iterates `op`'s operands — the inner + `∀ value ∈ op.getOperands!`. + * `ValuePtr.dominatesBeforeOp?` decides `value.dominatesIp (InsertPoint.before op) ctx` + for each operand (see its docstring for the `opResult`/`blockArgument` cases). + + Therefore `verifyDominance ctx top = .ok ()` means every operand of every operation + dominates its use, i.e. `ctx.Dom` holds. The restriction in `verifyOperandDominance` + to SSACFG, reachable blocks matches the scope of `ctx.Dom`: that predicate is stated + for SSACFG regions (graph regions impose no dominance), and dominance over + unreachable code is vacuous. - This is intentionally an executable checker. It does not yet provide a Lean proof of - `ctx.Dom`, but its algorithm is structured to match that property. + This is still an executable checker, not a Lean proof of `ctx.Dom`; it is written so + that each step lines up with a clause of the definition, which is what makes the + implication "the check succeeds ⇒ `ctx.Dom`" clear. -/ def WfIRContext.verifyDominance (ctx : WfIRContext OpCode) (top : OperationPtr) : Except String Unit := do From b0089285ae5a69a0ebd6ed6231c7e436a6108e6c Mon Sep 17 00:00:00 2001 From: John Regehr Date: Sat, 27 Jun 2026 20:32:36 -0600 Subject: [PATCH 05/10] work --- Veir/Dominance.lean | 7 ++++--- Veir/IR/Dominance.lean | 28 +++++++++++++++++++++++++++- Veir/Verifier.lean | 28 ++++++++++++++++------------ 3 files changed, 47 insertions(+), 16 deletions(-) diff --git a/Veir/Dominance.lean b/Veir/Dominance.lean index 58f40c80b..f1d11e28d 100644 --- a/Veir/Dominance.lean +++ b/Veir/Dominance.lean @@ -124,9 +124,10 @@ SSA dominance. procedure for this predicate: it visits every in-bounds operation and every operand, and for each checks `value.dominatesIp (InsertPoint.before op) ctx` via the dominance analysis. A successful run is intended to witness exactly `ctx.Dom`; the checker is - written so that each step matches a clause of this definition. (`ctx.Dom` assumes - SSACFG regions, and the checker restricts itself to SSACFG, reachable blocks - accordingly.) + written so that each step matches a clause of this definition for reachable SSACFG + blocks. For graph regions, the executable checker follows MLIR's region-aware + dominance rule: same-block order is ignored inside the graph region, but values + captured from enclosing regions must still dominate the graph-owning operation. -/ def WfIRContext.Dom (ctx : WfIRContext OpInfo) : Prop := ∀ {op : OperationPtr} (_opInBounds : op.InBounds ctx.raw) {value : ValuePtr}, diff --git a/Veir/IR/Dominance.lean b/Veir/IR/Dominance.lean index b0321565a..b0f829315 100644 --- a/Veir/IR/Dominance.lean +++ b/Veir/IR/Dominance.lean @@ -26,6 +26,20 @@ private partial def normalizeInsertPoint let parentOp ← (parentRegion.get! irCtx).parent normalizeInsertPoint region (.before parentOp) irCtx +/-- +Whether this region has MLIR-style SSA dominance. In graph regions, operations +in the same block may use each other without respecting source order, but values +defined outside the graph region must still dominate the operation that owns the +graph region. +-/ +private def RegionPtr.hasSSADominanceByKind + (region : RegionPtr) (irCtx : IRContext OpCode) : Bool := + match (region.get! irCtx).parent with + | some parentOp => + let parent := parentOp.get! irCtx + parent.opType.getRegionKind (parent.regions.idxOf region) = .SSACFG + | none => true + /-- Check dominance between two blocks that are already known to lie in the same region. @@ -70,6 +84,10 @@ to lie in the same block. private def dominatesWithinBlock (dominator point : InsertPoint) (irCtx : IRContext OpCode) : Bool := Id.run do + let some block := dominator.block! irCtx | return false + let some region := (block.get! irCtx).parent | return false + if !region.hasSSADominanceByKind irCtx then + return true if dominator = point then return true match dominator, point with @@ -123,7 +141,15 @@ private def properlyDominates (point : InsertPoint) (dfCtx : DataFlowContext) (irCtx : IRContext OpCode) : Bool := - dominator ≠ point && dominator.dominates point dfCtx irCtx + if dominator = point then + match dominator.block! irCtx with + | some block => + match (block.get! irCtx).parent with + | some region => !region.hasSSADominanceByKind irCtx + | none => false + | none => false + else + dominator.dominates point dfCtx irCtx end InsertPoint diff --git a/Veir/Verifier.lean b/Veir/Verifier.lean index e1a341ba2..9c7b3ccd5 100644 --- a/Veir/Verifier.lean +++ b/Veir/Verifier.lean @@ -862,14 +862,19 @@ def RegionPtr.getRegionKind (region : RegionPtr) (ctx : WfIRContext OpCode) : Re | none => .SSACFG /-- - Verify that a terminator only ever appears as the last operation of its block: - an operation that is a terminator must not be followed by another operation. + Verify operation/block control-flow position rules: a terminator only ever + appears as the last operation of its block, and any operation with block + successors must also terminate its parent block. The second rule matches + MLIR's generic verifier and catches malformed successor-bearing unknown/test + ops even when they are not registered terminators. -/ def OperationPtr.verifyTerminatorPosition (op : OperationPtr) (ctx : WfIRContext OpCode) (opIn : op.InBounds ctx.raw) : Except String PUnit := do let operation := op.get ctx.raw opIn if operation.opType.isTerminator && operation.next.isSome then throw "Expected a terminator to be the last operation of its block" + if op.getNumSuccessors ctx.raw opIn ≠ 0 && operation.next.isSome then + throw "operation with block successors must terminate its parent block" /-- Verify that no operation branches to the entry block of a region. The entry @@ -1026,15 +1031,14 @@ def OperationPtr.verifyOperandDominance (op : OperationPtr) (ctx : WfIRContext OpCode) (dfCtx : DataFlowContext) (opIn : op.InBounds ctx.raw) : Except String PUnit := do - -- The SSA dominance constraint only applies inside SSACFG regions and, as in - -- LLVM/MLIR, only to uses in blocks reachable from the region entry. Operands - -- used in graph regions or in unreachable code impose no dominance requirement; - -- the analysis records no dominator fact for unreachable blocks (whereas the + -- As in LLVM/MLIR, dominance is only checked in blocks reachable from the + -- region entry. Graph regions still need an operand check: their same-block + -- operation order is non-SSA, but captured values from enclosing SSACFG + -- regions must dominate the operation that owns the graph region. The + -- analysis records no dominator fact for unreachable blocks (whereas the -- entry block has a fact with no immediate dominator). let shouldCheck : Bool := Id.run do let some useBlock := (op.get ctx.raw opIn).parent | return false - let some region := (useBlock.get! ctx.raw).parent | return false - let .SSACFG := region.getRegionKind ctx | return false return (useBlock.getDominatorFact? dfCtx ctx.raw).isSome if shouldCheck then let instrName := String.fromUTF8! (op.getOpType ctx.raw opIn).name @@ -1064,10 +1068,10 @@ def OperationPtr.verifyOperandDominance for each operand (see its docstring for the `opResult`/`blockArgument` cases). Therefore `verifyDominance ctx top = .ok ()` means every operand of every operation - dominates its use, i.e. `ctx.Dom` holds. The restriction in `verifyOperandDominance` - to SSACFG, reachable blocks matches the scope of `ctx.Dom`: that predicate is stated - for SSACFG regions (graph regions impose no dominance), and dominance over - unreachable code is vacuous. + in a reachable block dominates its use according to the region-aware dominance + relation used by MLIR: SSACFG regions enforce control-flow and same-block order, + graph regions ignore same-block order, and values captured by nested graph regions + must still dominate the enclosing operation in the parent region. This is still an executable checker, not a Lean proof of `ctx.Dom`; it is written so that each step lines up with a clause of the definition, which is what makes the From e5a35ece2bc735bcf0dcab7cf7e8f5e19b479f39 Mon Sep 17 00:00:00 2001 From: John Regehr Date: Sat, 27 Jun 2026 22:01:46 -0600 Subject: [PATCH 06/10] work --- UnitTest/DataFlowFramework/Dominance.lean | 152 +++++++++++++--------- Veir/IR/Dominance.lean | 12 +- Veir/Verifier.lean | 13 +- 3 files changed, 107 insertions(+), 70 deletions(-) diff --git a/UnitTest/DataFlowFramework/Dominance.lean b/UnitTest/DataFlowFramework/Dominance.lean index e8cc13375..3038732f7 100644 --- a/UnitTest/DataFlowFramework/Dominance.lean +++ b/UnitTest/DataFlowFramework/Dominance.lean @@ -19,6 +19,24 @@ private structure ExpectedOperationDominance where dominates : Bool properDom : Bool +/-- +Whether `block` lies in a graph region. In graph regions there is no SSA source +order, so dominance is reflexive even for the proper variant: a block (or op) +properly dominates itself, and a dominator properly dominates every block it +dominates, including itself. +-/ +private def blockInGraphRegion (block : BlockPtr) (irCtx : IRContext OpCode) : Bool := + match (block.get! irCtx).parent with + | some region => + match (region.get! irCtx).parent with + | some parentOp => + let parent := parentOp.get! irCtx + match parent.opType.getRegionKind (parent.regions.idxOf region) with + | .Graph => true + | .SSACFG => false + | none => false + | none => false + /-- Compare one expected dominator label against the observed dominance information. @@ -34,7 +52,10 @@ private def compareExpectedDominator (irCtx : IRContext OpCode) : MismatchReport := Id.run do let some expectedBlock := recovered.blocks[expectedDom]? | return #[s!"dominators {expected.name}: missing block label {expectedDom}"] - let shouldProperlyDom := expectedDom ≠ expected.name + -- 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. + let shouldProperlyDom := blockInGraphRegion block irCtx || expectedDom ≠ expected.name let mut report := #[] if !expectedBlock.dominatesByAnalysis block dfCtx irCtx then report := report.push s!"dominators {expected.name}: missing expected dominator {expectedDom}" @@ -56,15 +77,18 @@ private def compareObservedDominator (expected : ExpectedBlockDominators) (dfCtx : DataFlowContext) (irCtx : IRContext OpCode) : MismatchReport := Id.run do + let inGraph := blockInGraphRegion block irCtx let observedByRelation := observedBlock.dominatesByAnalysis block dfCtx irCtx let observedProperly := observedBlock.properlyDominatesByAnalysis block dfCtx irCtx let mut report := #[] - if observedProperly ≠ (observedByRelation && observedBlock ≠ block) then + -- In a graph region proper dominance coincides with dominance (self included); + -- in an SSACFG region a block does not properly dominate itself. + if observedProperly ≠ (observedByRelation && (inGraph || observedBlock ≠ block)) then report := report.push s!"dominators {expected.name}: dominates/properlyDominates disagree on {observedName}" if observedByRelation && !expected.doms.contains observedName then report := report.push s!"dominators {expected.name}: unexpected dominator {observedName}" - if observedProperly && (!expected.doms.contains observedName || observedName = expected.name) then + if observedProperly && (!expected.doms.contains observedName || (!inGraph && observedName = expected.name)) then report := report.push s!"dominators {expected.name}: unexpected proper dominator {observedName}" report @@ -252,14 +276,14 @@ def runOperationDominance -/ def testDomLoop : String := run - "\"builtin.module\"() ({\n\ -^bb0:\n\ - \"test.test\"() [^bb1] : () -> ()\n\ -^bb1:\n\ - \"test.test\"() [^bb2] : () -> ()\n\ -^bb2:\n\ - \"test.test\"() [^bb1] : () -> ()\n\ -}) : () -> ()" + r#""func.func"() <{function_type = () -> (), sym_name = "f"}> ({ +^bb0: + "test.test"() [^bb1] : () -> () +^bb1: + "test.test"() [^bb2] : () -> () +^bb2: + "test.test"() [^bb1] : () -> () +}) : () -> ()"# #[ { name := "bb0", doms := { "bb0" }, immediateDom := "bb0" } , { name := "bb1", doms := { "bb0", "bb1" }, immediateDom := "bb0" } , { name := "bb2", doms := { "bb0", "bb1", "bb2" }, immediateDom := "bb1" } @@ -279,16 +303,16 @@ def testDomLoop : String := -/ def testDomDiamond : String := run - "\"builtin.module\"() ({\n\ -^bb0:\n\ - \"test.test\"() [^bb1, ^bb2] : () -> ()\n\ -^bb1:\n\ - \"test.test\"() [^bb3] : () -> ()\n\ -^bb2:\n\ - \"test.test\"() [^bb3] : () -> ()\n\ -^bb3:\n\ - \"test.test\"() : () -> ()\n\ -}) : () -> ()" + r#""func.func"() <{function_type = () -> (), sym_name = "f"}> ({ +^bb0: + "test.test"() [^bb1, ^bb2] : () -> () +^bb1: + "test.test"() [^bb3] : () -> () +^bb2: + "test.test"() [^bb3] : () -> () +^bb3: + "test.test"() : () -> () +}) : () -> ()"# #[ { name := "bb0", doms := { "bb0" }, immediateDom := "bb0" } , { name := "bb1", doms := { "bb0", "bb1" }, immediateDom := "bb0" } , { name := "bb2", doms := { "bb0", "bb2" }, immediateDom := "bb0" } @@ -315,16 +339,16 @@ def testDomDiamond : String := -/ def testDomLine : String := run - "\"builtin.module\"() ({\n\ -^bb0:\n\ - \"test.test\"() [^bb1] : () -> ()\n\ -^bb1:\n\ - \"test.test\"() [^bb2] : () -> ()\n\ -^bb2:\n\ - \"test.test\"() [^bb3] : () -> ()\n\ -^bb3:\n\ - \"test.test\"() : () -> ()\n\ -}) : () -> ()" + r#""func.func"() <{function_type = () -> (), sym_name = "f"}> ({ +^bb0: + "test.test"() [^bb1] : () -> () +^bb1: + "test.test"() [^bb2] : () -> () +^bb2: + "test.test"() [^bb3] : () -> () +^bb3: + "test.test"() : () -> () +}) : () -> ()"# #[ { name := "bb0", doms := { "bb0" }, immediateDom := "bb0" } , { name := "bb1", doms := { "bb0", "bb1" }, immediateDom := "bb0" } , { name := "bb2", doms := { "bb0", "bb1", "bb2" }, immediateDom := "bb1" } @@ -351,24 +375,24 @@ def testDomLine : String := -/ def testDomIfLoopIf : String := run - "\"builtin.module\"() ({\n\ -^bb0:\n\ - \"test.test\"() [^bb1, ^bb2] : () -> ()\n\ -^bb1:\n\ - \"test.test\"() [^bb5] : () -> ()\n\ -^bb2:\n\ - \"test.test\"() [^bb3, ^bb4] : () -> ()\n\ -^bb3:\n\ - \"test.test\"() [^bb6] : () -> ()\n\ -^bb4:\n\ - \"test.test\"() [^bb6] : () -> ()\n\ -^bb5:\n\ - \"test.test\"() [^bb1, ^bb7] : () -> ()\n\ -^bb6:\n\ - \"test.test\"() [^bb7] : () -> ()\n\ -^bb7:\n\ - \"test.test\"() : () -> ()\n\ -}) : () -> ()" + r#""func.func"() <{function_type = () -> (), sym_name = "f"}> ({ +^bb0: + "test.test"() [^bb1, ^bb2] : () -> () +^bb1: + "test.test"() [^bb5] : () -> () +^bb2: + "test.test"() [^bb3, ^bb4] : () -> () +^bb3: + "test.test"() [^bb6] : () -> () +^bb4: + "test.test"() [^bb6] : () -> () +^bb5: + "test.test"() [^bb1, ^bb7] : () -> () +^bb6: + "test.test"() [^bb7] : () -> () +^bb7: + "test.test"() : () -> () +}) : () -> ()"# #[ { name := "bb0", doms := { "bb0" }, immediateDom := "bb0" } , { name := "bb1", doms := { "bb0", "bb1" }, immediateDom := "bb0" } , { name := "bb2", doms := { "bb0", "bb2" }, immediateDom := "bb0" } @@ -424,7 +448,7 @@ def testDomNestedRegions : String := └───────┘ -/ def testDomDiamondNestedJoin : String := - run r#""builtin.module"() ({ + run r#""func.func"() <{function_type = () -> (), sym_name = "f"}> ({ ^bb0: "test.test"() [^bb1, ^bb2] : () -> () ^bb1: @@ -488,7 +512,7 @@ def testDomTwoLevelNested : String := └────────┘ -/ def testDomDiamondLoop: String := - run r#""builtin.module"() ({ + run r#""func.func"() <{function_type = () -> (), sym_name = "f"}> ({ ^bb0: "test.test"() [^bb1, ^bb2] : () -> () ^bb1: @@ -522,12 +546,15 @@ def testOpDomNestedRegions : String := %siblingInner = "test.test"() : () -> i32 }) : () -> i32 }) : () -> ()"# - #[ { dominator := "outer", dominated := "outer", dominates := true, properDom := false } + #[ -- `outer` and `otherOuter` share the module's graph region, so source order + -- is ignored: each properly dominates itself and `otherOuter` dominates + -- `inner` (nested in `outer`) despite appearing later. + { dominator := "outer", dominated := "outer", dominates := true, properDom := true } , { dominator := "outer", dominated := "inner", dominates := true, properDom := true } , { dominator := "outer", dominated := "otherOuter", dominates := true, properDom := true } , { dominator := "outer", dominated := "siblingInner", dominates := true, properDom := true } , { dominator := "inner", dominated := "siblingInner", dominates := false, properDom := false } - , { dominator := "otherOuter", dominated := "inner", dominates := false, properDom := false } + , { dominator := "otherOuter", dominated := "inner", dominates := true, properDom := true } , { dominator := "otherOuter", dominated := "siblingInner", dominates := true, properDom := true } ] @@ -548,28 +575,23 @@ def testOpDomTwoLevelNested : String := #[ { dominator := "top", dominated := "middle", dominates := true, properDom := true } , { dominator := "top", dominated := "leaf", dominates := true, properDom := true } , { dominator := "middle", dominated := "leaf", dominates := true, properDom := true } - , { dominator := "leaf", dominated := "leaf", dominates := true, properDom := false } + , { dominator := "leaf", dominated := "leaf", dominates := true, properDom := true } ] /- Test: operation dominance across two blocks in the same nested region. -/ def testOpDomSameRegionTwoBlocks : String := - runOperationDominance r#""builtin.module"() ({ -^bb0: - %outer = "test.test"() ({ - ^bb1: - %entry = "test.test"() : () -> i32 - "test.test"() [^bb2] : () -> () - ^bb2: - %exit = "test.test"() : () -> i32 - }) : () -> i32 + runOperationDominance r#""func.func"() <{function_type = () -> (), sym_name = "f"}> ({ +^bb1: + %entry = "test.test"() : () -> i32 + "test.test"() [^bb2] : () -> () +^bb2: + %exit = "test.test"() : () -> i32 }) : () -> ()"# #[ { dominator := "entry", dominated := "entry", dominates := true, properDom := false } , { dominator := "entry", dominated := "exit", dominates := true, properDom := true } , { dominator := "exit", dominated := "entry", dominates := false, properDom := false } - , { dominator := "outer", dominated := "entry", dominates := true, properDom := true } - , { dominator := "outer", dominated := "exit", dominates := true, properDom := true } ] /-- info: "ok" diff --git a/Veir/IR/Dominance.lean b/Veir/IR/Dominance.lean index b0f829315..1a2f22642 100644 --- a/Veir/IR/Dominance.lean +++ b/Veir/IR/Dominance.lean @@ -52,10 +52,14 @@ private partial def BlockPtr.dominatesWithinRegion (dfCtx : DataFlowContext) (irCtx : IRContext OpCode) : Bool := Id.run do if dominator = block then - 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 /-- diff --git a/Veir/Verifier.lean b/Veir/Verifier.lean index 9c7b3ccd5..e38626ba6 100644 --- a/Veir/Verifier.lean +++ b/Veir/Verifier.lean @@ -1039,7 +1039,18 @@ def OperationPtr.verifyOperandDominance -- entry block has a fact with no immediate dominator). let shouldCheck : Bool := Id.run do let some useBlock := (op.get ctx.raw opIn).parent | return false - return (useBlock.getDominatorFact? dfCtx ctx.raw).isSome + -- Reachable blocks carry a dominator fact and are always checked. + if (useBlock.getDominatorFact? dfCtx ctx.raw).isSome then + return true + -- A non-entry block of a graph region has no dominator fact of its own, but + -- its operations are still live when the graph region is. Fall back to the + -- region's entry block, which carries the fact whenever the region is live. + -- (Unreachable SSACFG blocks have no fact and are correctly skipped.) + let some region := (useBlock.get! ctx.raw).parent | return false + if region.getRegionKind ctx = .SSACFG then + return false + let some entry := (region.get! ctx.raw).firstBlock | return false + return (entry.getDominatorFact? dfCtx ctx.raw).isSome if shouldCheck then let instrName := String.fromUTF8! (op.getOpType ctx.raw opIn).name -- The inner `∀ value ∈ op.getOperands!` of `ctx.Dom`: these indices enumerate From 66709c05cceb4736815764dbdd6841a96b3cbf5b Mon Sep 17 00:00:00 2001 From: John Regehr Date: Sat, 27 Jun 2026 22:15:39 -0600 Subject: [PATCH 07/10] more tests --- Test/Verifier/dominance_graph_capture.mlir | 26 +++++++++++++++++++ ...ominance_graph_capture_block_argument.mlir | 23 ++++++++++++++++ .../dominance_graph_capture_result.mlir | 24 +++++++++++++++++ Test/Verifier/dominance_graph_intra_ok.mlir | 21 +++++++++++++++ .../successor_nonterminator_not_last.mlir | 18 +++++++++++++ 5 files changed, 112 insertions(+) create mode 100644 Test/Verifier/dominance_graph_capture.mlir create mode 100644 Test/Verifier/dominance_graph_capture_block_argument.mlir create mode 100644 Test/Verifier/dominance_graph_capture_result.mlir create mode 100644 Test/Verifier/dominance_graph_intra_ok.mlir create mode 100644 Test/Verifier/successor_nonterminator_not_last.mlir diff --git a/Test/Verifier/dominance_graph_capture.mlir b/Test/Verifier/dominance_graph_capture.mlir new file mode 100644 index 000000000..413044ee6 --- /dev/null +++ b/Test/Verifier/dominance_graph_capture.mlir @@ -0,0 +1,26 @@ +// RUN: not veir-opt %s 2>&1 | filecheck %s + +// A graph region captures %x from ^A, but ^A does not dominate ^B (the block +// that owns the graph region), so %x does not dominate its use. The use is in a +// NON-entry block (^g1) of the multi-block graph region, which must still be +// checked. + +"builtin.module"() ({ + "func.func"() <{function_type = (i1) -> (), sym_name = "m"}> ({ + ^entry(%c : i1): + "cf.cond_br"(%c) [^A, ^B] <{"branch_weights" = array, "operandSegmentSizes" = array}> : (i1) -> () + ^A(): + %x = "test.test"() : () -> i64 + "cf.br"() [^B] : () -> () + ^B(): + "test.test"() ({ + ^g0(): + "test.test"() : () -> () + ^g1(): + "test.test"(%x) : (i64) -> () + }) : () -> () + "func.return"() : () -> () + }) : () -> () +}) : () -> () + +// CHECK: does not dominate its use diff --git a/Test/Verifier/dominance_graph_capture_block_argument.mlir b/Test/Verifier/dominance_graph_capture_block_argument.mlir new file mode 100644 index 000000000..8eb04b978 --- /dev/null +++ b/Test/Verifier/dominance_graph_capture_block_argument.mlir @@ -0,0 +1,23 @@ +// RUN: not veir-opt %s 2>&1 | filecheck %s + +// The block argument %arg is only available along the path through ^b. Hiding +// its use inside a nested graph region in sibling block ^a must not bypass the +// enclosing SSACFG dominance requirement. + +"builtin.module"() ({ + "func.func"() <{function_type = (i1) -> (), sym_name = "main"}> ({ + ^entry(%c : i1): + %v = "arith.constant"() <{"value" = 5 : i32}> : () -> i32 + "cf.cond_br"(%c, %v) [^b, ^a] <{"branch_weights" = array, "operandSegmentSizes" = array}> : (i1, i32) -> () + ^b(%arg : i32): + "cf.br"() [^a] : () -> () + ^a: + "test.test"() ({ + ^inner: + "test.test"(%arg) : (i32) -> () + }) : () -> () + "func.return"() : () -> () + }) : () -> () +}) : () -> () + +// CHECK: test.test: operand 0 {{.*}} does not dominate its use diff --git a/Test/Verifier/dominance_graph_capture_result.mlir b/Test/Verifier/dominance_graph_capture_result.mlir new file mode 100644 index 000000000..6c9f52e1a --- /dev/null +++ b/Test/Verifier/dominance_graph_capture_result.mlir @@ -0,0 +1,24 @@ +// RUN: not veir-opt %s 2>&1 | filecheck %s + +// The use of %x is inside a graph region, where same-block operation order does +// not matter. But %x is defined in sibling CFG block ^b, and ^b does not +// dominate the graph-owning operation in ^a because ^a is reachable directly +// from ^entry. + +"builtin.module"() ({ + "func.func"() <{function_type = (i1) -> (), sym_name = "main"}> ({ + ^entry(%c : i1): + "cf.cond_br"(%c) [^b, ^a] <{"branch_weights" = array, "operandSegmentSizes" = array}> : (i1) -> () + ^b: + %x = "arith.constant"() <{"value" = 5 : i32}> : () -> i32 + "cf.br"() [^a] : () -> () + ^a: + "test.test"() ({ + ^inner: + "test.test"(%x) : (i32) -> () + }) : () -> () + "func.return"() : () -> () + }) : () -> () +}) : () -> () + +// CHECK: test.test: operand 0 {{.*}} does not dominate its use diff --git a/Test/Verifier/dominance_graph_intra_ok.mlir b/Test/Verifier/dominance_graph_intra_ok.mlir new file mode 100644 index 000000000..b0332fc76 --- /dev/null +++ b/Test/Verifier/dominance_graph_intra_ok.mlir @@ -0,0 +1,21 @@ +// RUN: veir-opt %s | filecheck %s + +// Inside a multi-block graph region there is no block ordering, so %a (defined in +// ^g0) may be used in the sibling block ^g1. The captured value %v dominates the +// graph-owning operation, so it is also a legal use. The program verifies. + +"builtin.module"() ({ + "func.func"() <{function_type = () -> (), sym_name = "m"}> ({ + ^entry(): + %v = "test.test"() : () -> i64 + "test.test"() ({ + ^g0(): + %a = "test.test"() : () -> i64 + ^g1(): + "test.test"(%a, %v) : (i64, i64) -> () + }) : () -> () + "func.return"() : () -> () + }) : () -> () +}) : () -> () + +// CHECK: "test.test"(%{{.*}}, %{{.*}}) : (i64, i64) -> () diff --git a/Test/Verifier/successor_nonterminator_not_last.mlir b/Test/Verifier/successor_nonterminator_not_last.mlir new file mode 100644 index 000000000..7e955664a --- /dev/null +++ b/Test/Verifier/successor_nonterminator_not_last.mlir @@ -0,0 +1,18 @@ +// RUN: not veir-opt %s 2>&1 | filecheck %s + +// MLIR's generic verifier requires any operation with block successors to +// terminate its parent block, even if the operation is not a registered +// terminator. Otherwise non-terminator ops can smuggle CFG edges that ordinary +// terminator-based analyses do not see. + +"builtin.module"() ({ + "func.func"() <{function_type = () -> (), sym_name = "main"}> ({ + ^entry: + "test.test"() [^side] : () -> () + "func.return"() : () -> () + ^side: + "func.return"() : () -> () + }) : () -> () +}) : () -> () + +// CHECK: operation with block successors must terminate its parent block From 73c84e34fb00338c700c893bdeefe5a306e8bba4 Mon Sep 17 00:00:00 2001 From: John Regehr Date: Sun, 28 Jun 2026 09:51:27 -0600 Subject: [PATCH 08/10] better testing --- Test/Verifier/dominance_back_edge.mlir | 1 + Test/Verifier/dominance_block_argument.mlir | 1 + Test/Verifier/dominance_cross_block.mlir | 1 + Test/Verifier/dominance_graph_capture.mlir | 16 +++++--- ...ominance_graph_capture_block_argument.mlir | 1 + .../dominance_graph_capture_result.mlir | 1 + Test/Verifier/dominance_graph_intra_ok.mlir | 1 + Test/Verifier/dominance_graph_region_ok.mlir | 1 + Test/Verifier/dominance_sibling_branch.mlir | 1 + Test/Verifier/dominance_unreachable_ok.mlir | 1 + Test/Verifier/entry_block_predecessor.mlir | 1 + Test/Verifier/graph_region_multi_block.mlir | 1 + Test/Verifier/isolation_from_above.mlir | 1 + Test/Verifier/isolation_nested_region_ok.mlir | 1 + Test/Verifier/ssa_single_assignment.mlir | 1 + Test/Verifier/ssa_undefined_value.mlir | 1 + .../successor_nonterminator_not_last.mlir | 1 + Test/lit.cfg | 7 ++++ Veir/Dominance.lean | 3 +- Veir/Verifier.lean | 38 +++++++++---------- 20 files changed, 53 insertions(+), 27 deletions(-) diff --git a/Test/Verifier/dominance_back_edge.mlir b/Test/Verifier/dominance_back_edge.mlir index becbb2977..b93197ced 100644 --- a/Test/Verifier/dominance_back_edge.mlir +++ b/Test/Verifier/dominance_back_edge.mlir @@ -1,4 +1,5 @@ // RUN: not veir-opt %s 2>&1 | filecheck %s +// RUN: MLIR_AGREE // %x is defined in the loop body but used in the loop header. The header is // reachable from ^entry without going through ^body, so ^body does not dominate diff --git a/Test/Verifier/dominance_block_argument.mlir b/Test/Verifier/dominance_block_argument.mlir index 72694a066..a8de5b70a 100644 --- a/Test/Verifier/dominance_block_argument.mlir +++ b/Test/Verifier/dominance_block_argument.mlir @@ -1,4 +1,5 @@ // RUN: not veir-opt %s 2>&1 | filecheck %s +// RUN: MLIR_AGREE // Block arguments are subject to the same dominance rule as op results. %arg is // an argument of ^a, but it is used in ^b, and ^a does not dominate ^b (^b is diff --git a/Test/Verifier/dominance_cross_block.mlir b/Test/Verifier/dominance_cross_block.mlir index 92f56ef33..6782cb048 100644 --- a/Test/Verifier/dominance_cross_block.mlir +++ b/Test/Verifier/dominance_cross_block.mlir @@ -1,4 +1,5 @@ // RUN: not veir-opt %s 2>&1 | filecheck %s +// RUN: MLIR_AGREE // %x is defined in ^a but used in ^b. ^a does not dominate ^b, because ^b is // also reachable directly from ^entry, so this violates SSA dominance even diff --git a/Test/Verifier/dominance_graph_capture.mlir b/Test/Verifier/dominance_graph_capture.mlir index 413044ee6..4db66720e 100644 --- a/Test/Verifier/dominance_graph_capture.mlir +++ b/Test/Verifier/dominance_graph_capture.mlir @@ -1,9 +1,13 @@ -// RUN: not veir-opt %s 2>&1 | filecheck %s +// RUN: veir-opt %s | filecheck %s +// RUN: MLIR_AGREE -// A graph region captures %x from ^A, but ^A does not dominate ^B (the block -// that owns the graph region), so %x does not dominate its use. The use is in a -// NON-entry block (^g1) of the multi-block graph region, which must still be -// checked. +// A graph region captures %x from ^A, and ^A does not dominate ^B (the block +// that owns the graph region). The capture is used in a NON-entry block (^g1) +// of the multi-block graph region. Like MLIR, dominance is only checked in +// blocks reachable from their region's entry; ^g1 has no intra-region control +// flow into it, so it is unreachable and the use is not checked. The program +// therefore verifies. (A capture used in the graph region's entry block ^g0 is +// still checked -- see dominance_graph_capture_result.mlir.) "builtin.module"() ({ "func.func"() <{function_type = (i1) -> (), sym_name = "m"}> ({ @@ -23,4 +27,4 @@ }) : () -> () }) : () -> () -// CHECK: does not dominate its use +// CHECK: "test.test"(%{{.*}}) : (i64) -> () diff --git a/Test/Verifier/dominance_graph_capture_block_argument.mlir b/Test/Verifier/dominance_graph_capture_block_argument.mlir index 8eb04b978..a10f7bbef 100644 --- a/Test/Verifier/dominance_graph_capture_block_argument.mlir +++ b/Test/Verifier/dominance_graph_capture_block_argument.mlir @@ -1,4 +1,5 @@ // RUN: not veir-opt %s 2>&1 | filecheck %s +// RUN: MLIR_AGREE // The block argument %arg is only available along the path through ^b. Hiding // its use inside a nested graph region in sibling block ^a must not bypass the diff --git a/Test/Verifier/dominance_graph_capture_result.mlir b/Test/Verifier/dominance_graph_capture_result.mlir index 6c9f52e1a..dcb0b0d17 100644 --- a/Test/Verifier/dominance_graph_capture_result.mlir +++ b/Test/Verifier/dominance_graph_capture_result.mlir @@ -1,4 +1,5 @@ // RUN: not veir-opt %s 2>&1 | filecheck %s +// RUN: MLIR_AGREE // The use of %x is inside a graph region, where same-block operation order does // not matter. But %x is defined in sibling CFG block ^b, and ^b does not diff --git a/Test/Verifier/dominance_graph_intra_ok.mlir b/Test/Verifier/dominance_graph_intra_ok.mlir index b0332fc76..620f1b167 100644 --- a/Test/Verifier/dominance_graph_intra_ok.mlir +++ b/Test/Verifier/dominance_graph_intra_ok.mlir @@ -1,4 +1,5 @@ // RUN: veir-opt %s | filecheck %s +// RUN: MLIR_AGREE // Inside a multi-block graph region there is no block ordering, so %a (defined in // ^g0) may be used in the sibling block ^g1. The captured value %v dominates the diff --git a/Test/Verifier/dominance_graph_region_ok.mlir b/Test/Verifier/dominance_graph_region_ok.mlir index 45d2e5dde..316104e69 100644 --- a/Test/Verifier/dominance_graph_region_ok.mlir +++ b/Test/Verifier/dominance_graph_region_ok.mlir @@ -1,4 +1,5 @@ // RUN: veir-opt %s | filecheck %s +// RUN: MLIR_AGREE // 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 diff --git a/Test/Verifier/dominance_sibling_branch.mlir b/Test/Verifier/dominance_sibling_branch.mlir index f039802ea..6593c0901 100644 --- a/Test/Verifier/dominance_sibling_branch.mlir +++ b/Test/Verifier/dominance_sibling_branch.mlir @@ -1,4 +1,5 @@ // RUN: not veir-opt %s 2>&1 | filecheck %s +// RUN: MLIR_AGREE // %x is defined in ^then and used in the sibling block ^else. Neither branch of // the conditional dominates the other, so the use in ^else is not dominated by diff --git a/Test/Verifier/dominance_unreachable_ok.mlir b/Test/Verifier/dominance_unreachable_ok.mlir index d0267fcdb..83636a82c 100644 --- a/Test/Verifier/dominance_unreachable_ok.mlir +++ b/Test/Verifier/dominance_unreachable_ok.mlir @@ -1,4 +1,5 @@ // RUN: veir-opt %s | filecheck %s +// RUN: MLIR_AGREE // Like LLVM/MLIR, the dominance check is skipped for unreachable blocks. ^dead // has no predecessors (^entry returns), so its use of %v imposes no dominance diff --git a/Test/Verifier/entry_block_predecessor.mlir b/Test/Verifier/entry_block_predecessor.mlir index 2f8b7b73f..4c5e39ce5 100644 --- a/Test/Verifier/entry_block_predecessor.mlir +++ b/Test/Verifier/entry_block_predecessor.mlir @@ -1,4 +1,5 @@ // RUN: not veir-opt %s 2>&1 | filecheck %s +// RUN: MLIR_AGREE // The entry block of a region may not have predecessors. Here ^bb1 branches back // to the entry block ^bb0, which would mean the region is re-entered through its diff --git a/Test/Verifier/graph_region_multi_block.mlir b/Test/Verifier/graph_region_multi_block.mlir index 8b7aeae1b..f977f9eda 100644 --- a/Test/Verifier/graph_region_multi_block.mlir +++ b/Test/Verifier/graph_region_multi_block.mlir @@ -1,4 +1,5 @@ // RUN: not veir-opt %s 2>&1 | filecheck %s +// RUN: MLIR_AGREE // builtin.module is a registered op with a graph region, so its region may have // at most one block. (Unregistered ops and the test dialect are exempt and may diff --git a/Test/Verifier/isolation_from_above.mlir b/Test/Verifier/isolation_from_above.mlir index 3fe491306..589c74ca1 100644 --- a/Test/Verifier/isolation_from_above.mlir +++ b/Test/Verifier/isolation_from_above.mlir @@ -1,4 +1,5 @@ // RUN: not veir-opt %s 2>&1 | filecheck %s +// RUN: MLIR_AGREE // func.func is isolated from above: the body of @inner may not reference %k, // which is defined in the enclosing function @outer. diff --git a/Test/Verifier/isolation_nested_region_ok.mlir b/Test/Verifier/isolation_nested_region_ok.mlir index aee65b827..8770d925a 100644 --- a/Test/Verifier/isolation_nested_region_ok.mlir +++ b/Test/Verifier/isolation_nested_region_ok.mlir @@ -1,4 +1,5 @@ // RUN: veir-opt %s | filecheck %s +// RUN: MLIR_AGREE // A non-isolated nested region (the body of an unregistered test.test op) may // reference values from an enclosing region. Only IsolatedFromAbove ops, such as diff --git a/Test/Verifier/ssa_single_assignment.mlir b/Test/Verifier/ssa_single_assignment.mlir index ec30e11f3..f2b21930e 100644 --- a/Test/Verifier/ssa_single_assignment.mlir +++ b/Test/Verifier/ssa_single_assignment.mlir @@ -1,4 +1,5 @@ // RUN: not veir-opt %s 2>&1 | filecheck %s +// RUN: MLIR_AGREE // SSA requires that each name is assigned exactly once. Defining %a twice is // rejected by the parser, before verification runs. diff --git a/Test/Verifier/ssa_undefined_value.mlir b/Test/Verifier/ssa_undefined_value.mlir index 96db0de67..215e9a8f5 100644 --- a/Test/Verifier/ssa_undefined_value.mlir +++ b/Test/Verifier/ssa_undefined_value.mlir @@ -1,4 +1,5 @@ // RUN: not veir-opt %s 2>&1 | filecheck %s +// RUN: MLIR_AGREE // Every used SSA name must be defined somewhere. A use of a name that is never // assigned is rejected by the parser, before verification runs. diff --git a/Test/Verifier/successor_nonterminator_not_last.mlir b/Test/Verifier/successor_nonterminator_not_last.mlir index 7e955664a..e1d89917d 100644 --- a/Test/Verifier/successor_nonterminator_not_last.mlir +++ b/Test/Verifier/successor_nonterminator_not_last.mlir @@ -1,4 +1,5 @@ // RUN: not veir-opt %s 2>&1 | filecheck %s +// RUN: MLIR_AGREE // MLIR's generic verifier requires any operation with block successors to // terminate its parent block, even if the operation is not a registered diff --git a/Test/lit.cfg b/Test/lit.cfg index b51ee0b8f..7d889e38f 100644 --- a/Test/lit.cfg +++ b/Test/lit.cfg @@ -55,12 +55,19 @@ if mlir_opt: # messages. We'd rather test the error message of `veir-opt`. config.substitutions.append(("MLIR_INVALID", "not mlir-opt --mlir-print-op-generic --mlir-print-local-scope %s")) + # Assert that veir-opt and mlir-opt reach the same accept/reject verdict on + # %s. Backed by a helper script so we can compare exit codes (lit's internal + # shell cannot). Only the verdict is compared, not the diagnostic text. + config.substitutions.append(("MLIR_AGREE", + f"bash {veir_root}/Test/Tools/mlir_agree.sh {veir_root}/.lake/build/bin/veir-opt{exe_suffix} {mlir_opt} %s")) else: print(f"'mlir-opt' version {version_short} ({version}) detected, but only {mlir_versions_supported} supported. Skipping MLIR compatibility tests") config.substitutions.append(("MLIR_ROUNDTRIP", "true")) config.substitutions.append(("MLIR_UNREGISTERED_ROUNDTRIP", "true")) config.substitutions.append(("MLIR_INVALID", "true")) + config.substitutions.append(("MLIR_AGREE", "true")) else: config.substitutions.append(("MLIR_ROUNDTRIP", "true")) config.substitutions.append(("MLIR_UNREGISTERED_ROUNDTRIP", "true")) config.substitutions.append(("MLIR_INVALID", "true")) + config.substitutions.append(("MLIR_AGREE", "true")) diff --git a/Veir/Dominance.lean b/Veir/Dominance.lean index f1d11e28d..8f87f98dd 100644 --- a/Veir/Dominance.lean +++ b/Veir/Dominance.lean @@ -127,7 +127,8 @@ SSA dominance. written so that each step matches a clause of this definition for reachable SSACFG blocks. For graph regions, the executable checker follows MLIR's region-aware dominance rule: same-block order is ignored inside the graph region, but values - captured from enclosing regions must still dominate the graph-owning operation. + captured into its entry block must still dominate the graph-owning operation. As in + MLIR, the check is skipped for blocks that are unreachable from their region's entry. -/ def WfIRContext.Dom (ctx : WfIRContext OpInfo) : Prop := ∀ {op : OperationPtr} (_opInBounds : op.InBounds ctx.raw) {value : ValuePtr}, diff --git a/Veir/Verifier.lean b/Veir/Verifier.lean index e38626ba6..98e735675 100644 --- a/Veir/Verifier.lean +++ b/Veir/Verifier.lean @@ -1031,26 +1031,22 @@ def OperationPtr.verifyOperandDominance (op : OperationPtr) (ctx : WfIRContext OpCode) (dfCtx : DataFlowContext) (opIn : op.InBounds ctx.raw) : Except String PUnit := do - -- As in LLVM/MLIR, dominance is only checked in blocks reachable from the - -- region entry. Graph regions still need an operand check: their same-block - -- operation order is non-SSA, but captured values from enclosing SSACFG - -- regions must dominate the operation that owns the graph region. The - -- analysis records no dominator fact for unreachable blocks (whereas the - -- entry block has a fact with no immediate dominator). + -- As in LLVM/MLIR, dominance is only checked in blocks reachable from their + -- region's entry. This matches MLIR's verifier, which gates the operand + -- dominance check on `DominanceInfo::isReachableFromEntry(block)` + -- (`mlir/lib/IR/Verifier.cpp`): the region's entry block is always reachable, + -- and every other block is reachable iff the region's dominator tree says so. + -- A block carries a dominator fact in exactly those cases, so fact presence is + -- the executable form of `isReachableFromEntry`. + -- + -- 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.) let shouldCheck : Bool := Id.run do let some useBlock := (op.get ctx.raw opIn).parent | return false - -- Reachable blocks carry a dominator fact and are always checked. - if (useBlock.getDominatorFact? dfCtx ctx.raw).isSome then - return true - -- A non-entry block of a graph region has no dominator fact of its own, but - -- its operations are still live when the graph region is. Fall back to the - -- region's entry block, which carries the fact whenever the region is live. - -- (Unreachable SSACFG blocks have no fact and are correctly skipped.) - let some region := (useBlock.get! ctx.raw).parent | return false - if region.getRegionKind ctx = .SSACFG then - return false - let some entry := (region.get! ctx.raw).firstBlock | return false - return (entry.getDominatorFact? dfCtx ctx.raw).isSome + return (useBlock.getDominatorFact? dfCtx ctx.raw).isSome if shouldCheck then let instrName := String.fromUTF8! (op.getOpType ctx.raw opIn).name -- The inner `∀ value ∈ op.getOperands!` of `ctx.Dom`: these indices enumerate @@ -1081,8 +1077,10 @@ def OperationPtr.verifyOperandDominance Therefore `verifyDominance ctx top = .ok ()` means every operand of every operation in a reachable block dominates its use according to the region-aware dominance relation used by MLIR: SSACFG regions enforce control-flow and same-block order, - graph regions ignore same-block order, and values captured by nested graph regions - must still dominate the enclosing operation in the parent region. + graph regions ignore same-block order, and values captured into the *entry* block of + a graph region must still dominate the enclosing operation in the parent region. As in + MLIR, blocks that are not reachable from their region's entry are not checked, so a + capture used in a non-entry, edgeless graph-region block is left unverified. This is still an executable checker, not a Lean proof of `ctx.Dom`; it is written so that each step lines up with a clause of the definition, which is what makes the From 9c9abb5c10cffc959914b42d1dc6736a4bf77796 Mon Sep 17 00:00:00 2001 From: John Regehr Date: Sun, 28 Jun 2026 13:04:39 -0600 Subject: [PATCH 09/10] rename test predicate --- Test/Tools/veir_mlir_same_verdict.sh | 39 +++++++++++++++++++ Test/Verifier/dominance_back_edge.mlir | 2 +- Test/Verifier/dominance_block_argument.mlir | 2 +- Test/Verifier/dominance_cross_block.mlir | 2 +- Test/Verifier/dominance_graph_capture.mlir | 2 +- ...ominance_graph_capture_block_argument.mlir | 2 +- .../dominance_graph_capture_result.mlir | 2 +- Test/Verifier/dominance_graph_intra_ok.mlir | 2 +- Test/Verifier/dominance_graph_region_ok.mlir | 2 +- Test/Verifier/dominance_sibling_branch.mlir | 2 +- Test/Verifier/dominance_unreachable_ok.mlir | 2 +- Test/Verifier/entry_block_predecessor.mlir | 2 +- Test/Verifier/graph_region_multi_block.mlir | 2 +- Test/Verifier/isolation_from_above.mlir | 2 +- Test/Verifier/isolation_nested_region_ok.mlir | 2 +- Test/Verifier/ssa_single_assignment.mlir | 2 +- Test/Verifier/ssa_undefined_value.mlir | 2 +- .../successor_nonterminator_not_last.mlir | 2 +- Test/lit.cfg | 8 ++-- 19 files changed, 60 insertions(+), 21 deletions(-) create mode 100755 Test/Tools/veir_mlir_same_verdict.sh diff --git a/Test/Tools/veir_mlir_same_verdict.sh b/Test/Tools/veir_mlir_same_verdict.sh new file mode 100755 index 000000000..d7d369102 --- /dev/null +++ b/Test/Tools/veir_mlir_same_verdict.sh @@ -0,0 +1,39 @@ +#!/usr/bin/env bash +# +# Check that veir-opt and mlir-opt reach the same accept/reject verdict on a +# single test file. Used by the `VEIR_MLIR_SAME_VERDICT` lit substitution (see Test/lit.cfg). +# +# Usage: veir_mlir_same_verdict.sh +# +# Exits 0 iff both tools verify the input (both accept) or both reject it (parse +# or verification failure). Only the verdict is compared, not the diagnostic +# text, which is not stable across mlir-opt versions. +# +# veir-opt natively accepts unregistered ops such as `test.test`; mlir-opt needs +# `--allow-unregistered-dialect` to do the same, so the two invocations differ +# only by that flag. + +set -u + +if [ "$#" -ne 3 ]; then + echo "veir_mlir_same_verdict.sh: expected 3 arguments, got $#" >&2 + exit 2 +fi + +veir="$1" +mlir="$2" +file="$3" + +"$veir" "$file" >/dev/null 2>&1 +[ $? -eq 0 ] && veir_verdict=accept || veir_verdict=reject + +"$mlir" --allow-unregistered-dialect "$file" >/dev/null 2>&1 +[ $? -eq 0 ] && mlir_verdict=accept || mlir_verdict=reject + +if [ "$veir_verdict" = "$mlir_verdict" ]; then + echo "VEIR_MLIR_SAME_VERDICT: veir-opt and mlir-opt agree ($veir_verdict) on $file" + exit 0 +fi + +echo "VEIR_MLIR_SAME_VERDICT: DISAGREEMENT on $file: veir-opt=$veir_verdict mlir-opt=$mlir_verdict" >&2 +exit 1 diff --git a/Test/Verifier/dominance_back_edge.mlir b/Test/Verifier/dominance_back_edge.mlir index b93197ced..b3a5617a3 100644 --- a/Test/Verifier/dominance_back_edge.mlir +++ b/Test/Verifier/dominance_back_edge.mlir @@ -1,5 +1,5 @@ // RUN: not veir-opt %s 2>&1 | filecheck %s -// RUN: MLIR_AGREE +// RUN: VEIR_MLIR_SAME_VERDICT // %x is defined in the loop body but used in the loop header. The header is // reachable from ^entry without going through ^body, so ^body does not dominate diff --git a/Test/Verifier/dominance_block_argument.mlir b/Test/Verifier/dominance_block_argument.mlir index a8de5b70a..86016c3f9 100644 --- a/Test/Verifier/dominance_block_argument.mlir +++ b/Test/Verifier/dominance_block_argument.mlir @@ -1,5 +1,5 @@ // RUN: not veir-opt %s 2>&1 | filecheck %s -// RUN: MLIR_AGREE +// RUN: VEIR_MLIR_SAME_VERDICT // Block arguments are subject to the same dominance rule as op results. %arg is // an argument of ^a, but it is used in ^b, and ^a does not dominate ^b (^b is diff --git a/Test/Verifier/dominance_cross_block.mlir b/Test/Verifier/dominance_cross_block.mlir index 6782cb048..1959d5bc1 100644 --- a/Test/Verifier/dominance_cross_block.mlir +++ b/Test/Verifier/dominance_cross_block.mlir @@ -1,5 +1,5 @@ // RUN: not veir-opt %s 2>&1 | filecheck %s -// RUN: MLIR_AGREE +// RUN: VEIR_MLIR_SAME_VERDICT // %x is defined in ^a but used in ^b. ^a does not dominate ^b, because ^b is // also reachable directly from ^entry, so this violates SSA dominance even diff --git a/Test/Verifier/dominance_graph_capture.mlir b/Test/Verifier/dominance_graph_capture.mlir index 4db66720e..9d1b49937 100644 --- a/Test/Verifier/dominance_graph_capture.mlir +++ b/Test/Verifier/dominance_graph_capture.mlir @@ -1,5 +1,5 @@ // RUN: veir-opt %s | filecheck %s -// RUN: MLIR_AGREE +// RUN: VEIR_MLIR_SAME_VERDICT // A graph region captures %x from ^A, and ^A does not dominate ^B (the block // that owns the graph region). The capture is used in a NON-entry block (^g1) diff --git a/Test/Verifier/dominance_graph_capture_block_argument.mlir b/Test/Verifier/dominance_graph_capture_block_argument.mlir index a10f7bbef..3841a3e7c 100644 --- a/Test/Verifier/dominance_graph_capture_block_argument.mlir +++ b/Test/Verifier/dominance_graph_capture_block_argument.mlir @@ -1,5 +1,5 @@ // RUN: not veir-opt %s 2>&1 | filecheck %s -// RUN: MLIR_AGREE +// RUN: VEIR_MLIR_SAME_VERDICT // The block argument %arg is only available along the path through ^b. Hiding // its use inside a nested graph region in sibling block ^a must not bypass the diff --git a/Test/Verifier/dominance_graph_capture_result.mlir b/Test/Verifier/dominance_graph_capture_result.mlir index dcb0b0d17..3193f9426 100644 --- a/Test/Verifier/dominance_graph_capture_result.mlir +++ b/Test/Verifier/dominance_graph_capture_result.mlir @@ -1,5 +1,5 @@ // RUN: not veir-opt %s 2>&1 | filecheck %s -// RUN: MLIR_AGREE +// RUN: VEIR_MLIR_SAME_VERDICT // The use of %x is inside a graph region, where same-block operation order does // not matter. But %x is defined in sibling CFG block ^b, and ^b does not diff --git a/Test/Verifier/dominance_graph_intra_ok.mlir b/Test/Verifier/dominance_graph_intra_ok.mlir index 620f1b167..51c7df7f1 100644 --- a/Test/Verifier/dominance_graph_intra_ok.mlir +++ b/Test/Verifier/dominance_graph_intra_ok.mlir @@ -1,5 +1,5 @@ // RUN: veir-opt %s | filecheck %s -// RUN: MLIR_AGREE +// RUN: VEIR_MLIR_SAME_VERDICT // Inside a multi-block graph region there is no block ordering, so %a (defined in // ^g0) may be used in the sibling block ^g1. The captured value %v dominates the diff --git a/Test/Verifier/dominance_graph_region_ok.mlir b/Test/Verifier/dominance_graph_region_ok.mlir index 316104e69..bd73ce5ad 100644 --- a/Test/Verifier/dominance_graph_region_ok.mlir +++ b/Test/Verifier/dominance_graph_region_ok.mlir @@ -1,5 +1,5 @@ // RUN: veir-opt %s | filecheck %s -// RUN: MLIR_AGREE +// 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 diff --git a/Test/Verifier/dominance_sibling_branch.mlir b/Test/Verifier/dominance_sibling_branch.mlir index 6593c0901..b16c121fb 100644 --- a/Test/Verifier/dominance_sibling_branch.mlir +++ b/Test/Verifier/dominance_sibling_branch.mlir @@ -1,5 +1,5 @@ // RUN: not veir-opt %s 2>&1 | filecheck %s -// RUN: MLIR_AGREE +// RUN: VEIR_MLIR_SAME_VERDICT // %x is defined in ^then and used in the sibling block ^else. Neither branch of // the conditional dominates the other, so the use in ^else is not dominated by diff --git a/Test/Verifier/dominance_unreachable_ok.mlir b/Test/Verifier/dominance_unreachable_ok.mlir index 83636a82c..65eadc71c 100644 --- a/Test/Verifier/dominance_unreachable_ok.mlir +++ b/Test/Verifier/dominance_unreachable_ok.mlir @@ -1,5 +1,5 @@ // RUN: veir-opt %s | filecheck %s -// RUN: MLIR_AGREE +// RUN: VEIR_MLIR_SAME_VERDICT // Like LLVM/MLIR, the dominance check is skipped for unreachable blocks. ^dead // has no predecessors (^entry returns), so its use of %v imposes no dominance diff --git a/Test/Verifier/entry_block_predecessor.mlir b/Test/Verifier/entry_block_predecessor.mlir index 4c5e39ce5..70b1103a6 100644 --- a/Test/Verifier/entry_block_predecessor.mlir +++ b/Test/Verifier/entry_block_predecessor.mlir @@ -1,5 +1,5 @@ // RUN: not veir-opt %s 2>&1 | filecheck %s -// RUN: MLIR_AGREE +// RUN: VEIR_MLIR_SAME_VERDICT // The entry block of a region may not have predecessors. Here ^bb1 branches back // to the entry block ^bb0, which would mean the region is re-entered through its diff --git a/Test/Verifier/graph_region_multi_block.mlir b/Test/Verifier/graph_region_multi_block.mlir index f977f9eda..f5bda60a1 100644 --- a/Test/Verifier/graph_region_multi_block.mlir +++ b/Test/Verifier/graph_region_multi_block.mlir @@ -1,5 +1,5 @@ // RUN: not veir-opt %s 2>&1 | filecheck %s -// RUN: MLIR_AGREE +// RUN: VEIR_MLIR_SAME_VERDICT // builtin.module is a registered op with a graph region, so its region may have // at most one block. (Unregistered ops and the test dialect are exempt and may diff --git a/Test/Verifier/isolation_from_above.mlir b/Test/Verifier/isolation_from_above.mlir index 589c74ca1..4a6eddf0e 100644 --- a/Test/Verifier/isolation_from_above.mlir +++ b/Test/Verifier/isolation_from_above.mlir @@ -1,5 +1,5 @@ // RUN: not veir-opt %s 2>&1 | filecheck %s -// RUN: MLIR_AGREE +// RUN: VEIR_MLIR_SAME_VERDICT // func.func is isolated from above: the body of @inner may not reference %k, // which is defined in the enclosing function @outer. diff --git a/Test/Verifier/isolation_nested_region_ok.mlir b/Test/Verifier/isolation_nested_region_ok.mlir index 8770d925a..79564c6e4 100644 --- a/Test/Verifier/isolation_nested_region_ok.mlir +++ b/Test/Verifier/isolation_nested_region_ok.mlir @@ -1,5 +1,5 @@ // RUN: veir-opt %s | filecheck %s -// RUN: MLIR_AGREE +// RUN: VEIR_MLIR_SAME_VERDICT // A non-isolated nested region (the body of an unregistered test.test op) may // reference values from an enclosing region. Only IsolatedFromAbove ops, such as diff --git a/Test/Verifier/ssa_single_assignment.mlir b/Test/Verifier/ssa_single_assignment.mlir index f2b21930e..a797bf94a 100644 --- a/Test/Verifier/ssa_single_assignment.mlir +++ b/Test/Verifier/ssa_single_assignment.mlir @@ -1,5 +1,5 @@ // RUN: not veir-opt %s 2>&1 | filecheck %s -// RUN: MLIR_AGREE +// RUN: VEIR_MLIR_SAME_VERDICT // SSA requires that each name is assigned exactly once. Defining %a twice is // rejected by the parser, before verification runs. diff --git a/Test/Verifier/ssa_undefined_value.mlir b/Test/Verifier/ssa_undefined_value.mlir index 215e9a8f5..5674f26c1 100644 --- a/Test/Verifier/ssa_undefined_value.mlir +++ b/Test/Verifier/ssa_undefined_value.mlir @@ -1,5 +1,5 @@ // RUN: not veir-opt %s 2>&1 | filecheck %s -// RUN: MLIR_AGREE +// RUN: VEIR_MLIR_SAME_VERDICT // Every used SSA name must be defined somewhere. A use of a name that is never // assigned is rejected by the parser, before verification runs. diff --git a/Test/Verifier/successor_nonterminator_not_last.mlir b/Test/Verifier/successor_nonterminator_not_last.mlir index e1d89917d..5208a6f3f 100644 --- a/Test/Verifier/successor_nonterminator_not_last.mlir +++ b/Test/Verifier/successor_nonterminator_not_last.mlir @@ -1,5 +1,5 @@ // RUN: not veir-opt %s 2>&1 | filecheck %s -// RUN: MLIR_AGREE +// RUN: VEIR_MLIR_SAME_VERDICT // MLIR's generic verifier requires any operation with block successors to // terminate its parent block, even if the operation is not a registered diff --git a/Test/lit.cfg b/Test/lit.cfg index 7d889e38f..c4d1dfc63 100644 --- a/Test/lit.cfg +++ b/Test/lit.cfg @@ -58,16 +58,16 @@ if mlir_opt: # Assert that veir-opt and mlir-opt reach the same accept/reject verdict on # %s. Backed by a helper script so we can compare exit codes (lit's internal # shell cannot). Only the verdict is compared, not the diagnostic text. - config.substitutions.append(("MLIR_AGREE", - f"bash {veir_root}/Test/Tools/mlir_agree.sh {veir_root}/.lake/build/bin/veir-opt{exe_suffix} {mlir_opt} %s")) + config.substitutions.append(("VEIR_MLIR_SAME_VERDICT", + f"bash {veir_root}/Test/Tools/veir_mlir_same_verdict.sh {veir_root}/.lake/build/bin/veir-opt{exe_suffix} {mlir_opt} %s")) else: print(f"'mlir-opt' version {version_short} ({version}) detected, but only {mlir_versions_supported} supported. Skipping MLIR compatibility tests") config.substitutions.append(("MLIR_ROUNDTRIP", "true")) config.substitutions.append(("MLIR_UNREGISTERED_ROUNDTRIP", "true")) config.substitutions.append(("MLIR_INVALID", "true")) - config.substitutions.append(("MLIR_AGREE", "true")) + config.substitutions.append(("VEIR_MLIR_SAME_VERDICT", "true")) else: config.substitutions.append(("MLIR_ROUNDTRIP", "true")) config.substitutions.append(("MLIR_UNREGISTERED_ROUNDTRIP", "true")) config.substitutions.append(("MLIR_INVALID", "true")) - config.substitutions.append(("MLIR_AGREE", "true")) + config.substitutions.append(("VEIR_MLIR_SAME_VERDICT", "true")) From 8072c629d1bb5e242da663b5aa9edb2d685564af Mon Sep 17 00:00:00 2001 From: John Regehr Date: Sun, 28 Jun 2026 16:14:40 -0600 Subject: [PATCH 10/10] add a quote from the MLIR docs --- Veir/IR/Dominance.lean | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/Veir/IR/Dominance.lean b/Veir/IR/Dominance.lean index 1a2f22642..730a3bae4 100644 --- a/Veir/IR/Dominance.lean +++ b/Veir/IR/Dominance.lean @@ -138,6 +138,13 @@ private def dominates /-- Proper dominance query between two insertion points. +From the MLIR documentation: "If A and B are in the same block and A +properly dominates B within the block, or if the block that contains A +properly dominates the block that contains B. In an SSACFG region, +Operation A dominates Operation B in the same block if A preceeds +B. In a Graph region, all operations in a block properly dominate all +operations in the same block." + An insertion point does not properly dominate itself. Otherwise this is the same query as `InsertPoint.dominates`. -/ private def properlyDominates