From 8e21e0af6c7181b2ca94cdb60c40414f90f0881a Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Sun, 22 Feb 2026 23:23:01 +0000 Subject: [PATCH 1/2] Complete the syntax for the integer fragment of the arith dialect This PR only stablished syntax, but no semantics yet. It is pulled out of PR #219. We also increase the max recursion limit as the generation of the opcode inductive requires a deeper limit. Co-authored-by: Alexander Viand --- Test/Arith/identity.mlir | 68 +++++++++-- Veir/OpCode.lean | 30 ++++- Veir/Verifier.lean | 236 ++++++++++++++++++++++++++++++++++++++- 3 files changed, 317 insertions(+), 17 deletions(-) diff --git a/Test/Arith/identity.mlir b/Test/Arith/identity.mlir index 88264b78..dadab8bf 100644 --- a/Test/Arith/identity.mlir +++ b/Test/Arith/identity.mlir @@ -1,19 +1,65 @@ // RUN: veir-opt %s | filecheck %s "builtin.module"() ({ -^bb0(): - %5 = "arith.constant"() <{ value = 13 : i32 }> : () -> i32 +^4(): + %5 = "arith.constant"() <{ "value" = 13 : i32 }> : () -> i32 %6 = "arith.addi"(%5, %5) : (i32, i32) -> i32 - %7 = "arith.subi"(%5, %5) : (i32, i32) -> i32 - %8 = "arith.muli"(%5, %5) : (i32, i32) -> i32 - %9 = "arith.andi"(%5, %5) : (i32, i32) -> i32 + %7 = "arith.addui_extended"(%5, %5) : (i32, i32) -> i32 + %8 = "arith.andi"(%5, %5) : (i32, i32) -> i32 + %9 = "arith.ceildivsi"(%5, %5) : (i32, i32) -> i32 + %10 = "arith.ceildivui"(%5, %5) : (i32, i32) -> i32 + %11 = "arith.cmpi"(%5, %5) : (i32, i32) -> i1 + %12 = "arith.divsi"(%5, %5) : (i32, i32) -> i32 + %13 = "arith.divui"(%5, %5) : (i32, i32) -> i32 + %14 = "arith.extui"(%5) : (i32) -> i32 + %15 = "arith.floordivsi"(%5, %5) : (i32, i32) -> i32 + %16 = "arith.maxsi"(%5, %5) : (i32, i32) -> i32 + %17 = "arith.maxui"(%5, %5) : (i32, i32) -> i32 + %18 = "arith.minsi"(%5, %5) : (i32, i32) -> i32 + %19 = "arith.minui"(%5, %5) : (i32, i32) -> i32 + %20 = "arith.muli"(%5, %5) : (i32, i32) -> i32 + %21 = "arith.mulsi_extended"(%5, %5) : (i32, i32) -> i32 + %22 = "arith.mului_extended"(%5, %5) : (i32, i32) -> i32 + %23 = "arith.ori"(%5, %5) : (i32, i32) -> i32 + %24 = "arith.remsi"(%5, %5) : (i32, i32) -> i32 + %25 = "arith.remui"(%5, %5) : (i32, i32) -> i32 + %26 = "arith.select"(%11, %5, %5) : (i1, i32, i32) -> i32 + %27 = "arith.shli"(%5, %5) : (i32, i32) -> i32 + %28 = "arith.shrsi"(%5, %5) : (i32, i32) -> i32 + %29 = "arith.shrui"(%5, %5) : (i32, i32) -> i32 + %30 = "arith.subi"(%5, %5) : (i32, i32) -> i32 + %31 = "arith.trunci"(%5) : (i32) -> i32 + %32 = "arith.xori"(%5, %5) : (i32, i32) -> i32 }) : () -> () // CHECK: "builtin.module"() ({ // CHECK-NEXT: ^4(): -// CHECK-NEXT: %5 = "arith.constant"() <{"value" = 13 : i32}> : () -> i32 -// CHECK-NEXT: %6 = "arith.addi"(%5, %5) : (i32, i32) -> i32 -// CHECK-NEXT: %7 = "arith.subi"(%5, %5) : (i32, i32) -> i32 -// CHECK-NEXT: %8 = "arith.muli"(%5, %5) : (i32, i32) -> i32 -// CHECK-NEXT: %9 = "arith.andi"(%5, %5) : (i32, i32) -> i32 -// CHECK-NEXT: }) : () -> () +// CHECK-NEXT: %5 = "arith.constant"() <{"value" = 13 : i32}> : () -> i32 +// CHECK-NEXT: %6 = "arith.addi"(%5, %5) : (i32, i32) -> i32 +// CHECK-NEXT: %7 = "arith.addui_extended"(%5, %5) : (i32, i32) -> i32 +// CHECK-NEXT: %8 = "arith.andi"(%5, %5) : (i32, i32) -> i32 +// CHECK-NEXT: %9 = "arith.ceildivsi"(%5, %5) : (i32, i32) -> i32 +// CHECK-NEXT: %10 = "arith.ceildivui"(%5, %5) : (i32, i32) -> i32 +// CHECK-NEXT: %11 = "arith.cmpi"(%5, %5) : (i32, i32) -> i1 +// CHECK-NEXT: %12 = "arith.divsi"(%5, %5) : (i32, i32) -> i32 +// CHECK-NEXT: %13 = "arith.divui"(%5, %5) : (i32, i32) -> i32 +// CHECK-NEXT: %14 = "arith.extui"(%5) : (i32) -> i32 +// CHECK-NEXT: %15 = "arith.floordivsi"(%5, %5) : (i32, i32) -> i32 +// CHECK-NEXT: %16 = "arith.maxsi"(%5, %5) : (i32, i32) -> i32 +// CHECK-NEXT: %17 = "arith.maxui"(%5, %5) : (i32, i32) -> i32 +// CHECK-NEXT: %18 = "arith.minsi"(%5, %5) : (i32, i32) -> i32 +// CHECK-NEXT: %19 = "arith.minui"(%5, %5) : (i32, i32) -> i32 +// CHECK-NEXT: %20 = "arith.muli"(%5, %5) : (i32, i32) -> i32 +// CHECK-NEXT: %21 = "arith.mulsi_extended"(%5, %5) : (i32, i32) -> i32 +// CHECK-NEXT: %22 = "arith.mului_extended"(%5, %5) : (i32, i32) -> i32 +// CHECK-NEXT: %23 = "arith.ori"(%5, %5) : (i32, i32) -> i32 +// CHECK-NEXT: %24 = "arith.remsi"(%5, %5) : (i32, i32) -> i32 +// CHECK-NEXT: %25 = "arith.remui"(%5, %5) : (i32, i32) -> i32 +// CHECK-NEXT: %26 = "arith.select"(%11, %5, %5) : (i1, i32, i32) -> i32 +// CHECK-NEXT: %27 = "arith.shli"(%5, %5) : (i32, i32) -> i32 +// CHECK-NEXT: %28 = "arith.shrsi"(%5, %5) : (i32, i32) -> i32 +// CHECK-NEXT: %29 = "arith.shrui"(%5, %5) : (i32, i32) -> i32 +// CHECK-NEXT: %30 = "arith.subi"(%5, %5) : (i32, i32) -> i32 +// CHECK-NEXT: %31 = "arith.trunci"(%5) : (i32) -> i32 +// CHECK-NEXT: %32 = "arith.xori"(%5, %5) : (i32, i32) -> i32 +// CHECK-NEXT: }) : () -> () \ No newline at end of file diff --git a/Veir/OpCode.lean b/Veir/OpCode.lean index 48d07ac0..dd2ad357 100644 --- a/Veir/OpCode.lean +++ b/Veir/OpCode.lean @@ -17,11 +17,34 @@ namespace Veir @[opcodes] inductive Arith where -| constant | addi -| subi -| muli +| addui_extended | andi +| ceildivsi +| ceildivui +| cmpi +| constant +| divsi +| divui +| extui +| floordivsi +| maxsi +| maxui +| minsi +| minui +| muli +| mulsi_extended +| mului_extended +| ori +| remsi +| remui +| select +| shli +| shrsi +| shrui +| subi +| trunci +| xori @[opcodes] inductive Builtin where @@ -152,6 +175,7 @@ public section An operation code (OpCode) identifies the type of an operation. Each OpCode corresponds to a specific operation. -/ +set_option maxRecDepth 100000 #generate_op_codes end diff --git a/Veir/Verifier.lean b/Veir/Verifier.lean index d1b3184b..9e9bf4df 100644 --- a/Veir/Verifier.lean +++ b/Veir/Verifier.lean @@ -16,6 +16,66 @@ def OperationPtr.verifyLocalInvariants (op : OperationPtr) (ctx : IRContext) (op match op.getOpType ctx opIn with | .builtin_unregistered => pure () /- ARITH -/ + | .arith_addi => do + if op.getNumOperands ctx opIn ≠ 2 then + throw "Expected 2 operands" + if op.getNumResults ctx opIn ≠ 1 then + throw "Expected 1 result" + if op.getNumRegions ctx opIn ≠ 0 then + throw "Expected 0 regions" + if op.getNumSuccessors ctx opIn ≠ 0 then + throw "Expected 0 successors" + pure () + | .arith_addui_extended => do + if op.getNumOperands ctx opIn ≠ 2 then + throw "Expected 2 operands" + if op.getNumResults ctx opIn ≠ 1 then + throw "Expected 1 result" + if op.getNumRegions ctx opIn ≠ 0 then + throw "Expected 0 regions" + if op.getNumSuccessors ctx opIn ≠ 0 then + throw "Expected 0 successors" + pure () + | .arith_andi => do + if op.getNumOperands ctx opIn ≠ 2 then + throw "Expected 2 operands" + if op.getNumResults ctx opIn ≠ 1 then + throw "Expected 1 result" + if op.getNumRegions ctx opIn ≠ 0 then + throw "Expected 0 regions" + if op.getNumSuccessors ctx opIn ≠ 0 then + throw "Expected 0 successors" + pure () + | .arith_ceildivsi => do + if op.getNumOperands ctx opIn ≠ 2 then + throw "Expected 2 operands" + if op.getNumResults ctx opIn ≠ 1 then + throw "Expected 1 result" + if op.getNumRegions ctx opIn ≠ 0 then + throw "Expected 0 regions" + if op.getNumSuccessors ctx opIn ≠ 0 then + throw "Expected 0 successors" + pure () + | .arith_ceildivui => do + if op.getNumOperands ctx opIn ≠ 2 then + throw "Expected 2 operands" + if op.getNumResults ctx opIn ≠ 1 then + throw "Expected 1 result" + if op.getNumRegions ctx opIn ≠ 0 then + throw "Expected 0 regions" + if op.getNumSuccessors ctx opIn ≠ 0 then + throw "Expected 0 successors" + pure () + | .arith_cmpi => do + if op.getNumOperands ctx opIn ≠ 2 then + throw "Expected 2 operands" + if op.getNumResults ctx opIn ≠ 1 then + throw "Expected 1 result" + if op.getNumRegions ctx opIn ≠ 0 then + throw "Expected 0 regions" + if op.getNumSuccessors ctx opIn ≠ 0 then + throw "Expected 0 successors" + pure () | .arith_constant => do if op.getNumOperands ctx opIn ≠ 0 then throw "Expected 0 operands" @@ -26,7 +86,7 @@ def OperationPtr.verifyLocalInvariants (op : OperationPtr) (ctx : IRContext) (op if op.getNumSuccessors ctx opIn ≠ 0 then throw "Expected 0 successors" pure () - | .arith_addi => do + | .arith_divsi => do if op.getNumOperands ctx opIn ≠ 2 then throw "Expected 2 operands" if op.getNumResults ctx opIn ≠ 1 then @@ -36,7 +96,67 @@ def OperationPtr.verifyLocalInvariants (op : OperationPtr) (ctx : IRContext) (op if op.getNumSuccessors ctx opIn ≠ 0 then throw "Expected 0 successors" pure () - | .arith_subi => do + | .arith_divui => do + if op.getNumOperands ctx opIn ≠ 2 then + throw "Expected 2 operands" + if op.getNumResults ctx opIn ≠ 1 then + throw "Expected 1 result" + if op.getNumRegions ctx opIn ≠ 0 then + throw "Expected 0 regions" + if op.getNumSuccessors ctx opIn ≠ 0 then + throw "Expected 0 successors" + pure () + | .arith_extui => do + if op.getNumOperands ctx opIn ≠ 1 then + throw "Expected 1 operand" + if op.getNumResults ctx opIn ≠ 1 then + throw "Expected 1 result" + if op.getNumRegions ctx opIn ≠ 0 then + throw "Expected 0 regions" + if op.getNumSuccessors ctx opIn ≠ 0 then + throw "Expected 0 successors" + pure () + | .arith_floordivsi => do + if op.getNumOperands ctx opIn ≠ 2 then + throw "Expected 2 operands" + if op.getNumResults ctx opIn ≠ 1 then + throw "Expected 1 result" + if op.getNumRegions ctx opIn ≠ 0 then + throw "Expected 0 regions" + if op.getNumSuccessors ctx opIn ≠ 0 then + throw "Expected 0 successors" + pure () + | .arith_maxsi => do + if op.getNumOperands ctx opIn ≠ 2 then + throw "Expected 2 operands" + if op.getNumResults ctx opIn ≠ 1 then + throw "Expected 1 result" + if op.getNumRegions ctx opIn ≠ 0 then + throw "Expected 0 regions" + if op.getNumSuccessors ctx opIn ≠ 0 then + throw "Expected 0 successors" + pure () + | .arith_maxui => do + if op.getNumOperands ctx opIn ≠ 2 then + throw "Expected 2 operands" + if op.getNumResults ctx opIn ≠ 1 then + throw "Expected 1 result" + if op.getNumRegions ctx opIn ≠ 0 then + throw "Expected 0 regions" + if op.getNumSuccessors ctx opIn ≠ 0 then + throw "Expected 0 successors" + pure () + | .arith_minsi => do + if op.getNumOperands ctx opIn ≠ 2 then + throw "Expected 2 operands" + if op.getNumResults ctx opIn ≠ 1 then + throw "Expected 1 result" + if op.getNumRegions ctx opIn ≠ 0 then + throw "Expected 0 regions" + if op.getNumSuccessors ctx opIn ≠ 0 then + throw "Expected 0 successors" + pure () + | .arith_minui => do if op.getNumOperands ctx opIn ≠ 2 then throw "Expected 2 operands" if op.getNumResults ctx opIn ≠ 1 then @@ -56,7 +176,117 @@ def OperationPtr.verifyLocalInvariants (op : OperationPtr) (ctx : IRContext) (op if op.getNumSuccessors ctx opIn ≠ 0 then throw "Expected 0 successors" pure () - | .arith_andi => do + | .arith_mulsi_extended => do + if op.getNumOperands ctx opIn ≠ 2 then + throw "Expected 2 operands" + if op.getNumResults ctx opIn ≠ 1 then + throw "Expected 1 result" + if op.getNumRegions ctx opIn ≠ 0 then + throw "Expected 0 regions" + if op.getNumSuccessors ctx opIn ≠ 0 then + throw "Expected 0 successors" + pure () + | .arith_mului_extended => do + if op.getNumOperands ctx opIn ≠ 2 then + throw "Expected 2 operands" + if op.getNumResults ctx opIn ≠ 1 then + throw "Expected 1 result" + if op.getNumRegions ctx opIn ≠ 0 then + throw "Expected 0 regions" + if op.getNumSuccessors ctx opIn ≠ 0 then + throw "Expected 0 successors" + pure () + | .arith_ori => do + if op.getNumOperands ctx opIn ≠ 2 then + throw "Expected 2 operands" + if op.getNumResults ctx opIn ≠ 1 then + throw "Expected 1 result" + if op.getNumRegions ctx opIn ≠ 0 then + throw "Expected 0 regions" + if op.getNumSuccessors ctx opIn ≠ 0 then + throw "Expected 0 successors" + pure () + | .arith_remsi => do + if op.getNumOperands ctx opIn ≠ 2 then + throw "Expected 2 operands" + if op.getNumResults ctx opIn ≠ 1 then + throw "Expected 1 result" + if op.getNumRegions ctx opIn ≠ 0 then + throw "Expected 0 regions" + if op.getNumSuccessors ctx opIn ≠ 0 then + throw "Expected 0 successors" + pure () + | .arith_remui => do + if op.getNumOperands ctx opIn ≠ 2 then + throw "Expected 2 operands" + if op.getNumResults ctx opIn ≠ 1 then + throw "Expected 1 result" + if op.getNumRegions ctx opIn ≠ 0 then + throw "Expected 0 regions" + if op.getNumSuccessors ctx opIn ≠ 0 then + throw "Expected 0 successors" + pure () + | .arith_select => do + if op.getNumOperands ctx opIn ≠ 3 then + throw "Expected 3 operands" + if op.getNumResults ctx opIn ≠ 1 then + throw "Expected 1 result" + if op.getNumRegions ctx opIn ≠ 0 then + throw "Expected 0 regions" + if op.getNumSuccessors ctx opIn ≠ 0 then + throw "Expected 0 successors" + pure () + | .arith_shli => do + if op.getNumOperands ctx opIn ≠ 2 then + throw "Expected 2 operands" + if op.getNumResults ctx opIn ≠ 1 then + throw "Expected 1 result" + if op.getNumRegions ctx opIn ≠ 0 then + throw "Expected 0 regions" + if op.getNumSuccessors ctx opIn ≠ 0 then + throw "Expected 0 successors" + pure () + | .arith_shrsi => do + if op.getNumOperands ctx opIn ≠ 2 then + throw "Expected 2 operands" + if op.getNumResults ctx opIn ≠ 1 then + throw "Expected 1 result" + if op.getNumRegions ctx opIn ≠ 0 then + throw "Expected 0 regions" + if op.getNumSuccessors ctx opIn ≠ 0 then + throw "Expected 0 successors" + pure () + | .arith_shrui => do + if op.getNumOperands ctx opIn ≠ 2 then + throw "Expected 2 operands" + if op.getNumResults ctx opIn ≠ 1 then + throw "Expected 1 result" + if op.getNumRegions ctx opIn ≠ 0 then + throw "Expected 0 regions" + if op.getNumSuccessors ctx opIn ≠ 0 then + throw "Expected 0 successors" + pure () + | .arith_subi => do + if op.getNumOperands ctx opIn ≠ 2 then + throw "Expected 2 operands" + if op.getNumResults ctx opIn ≠ 1 then + throw "Expected 1 result" + if op.getNumRegions ctx opIn ≠ 0 then + throw "Expected 0 regions" + if op.getNumSuccessors ctx opIn ≠ 0 then + throw "Expected 0 successors" + pure () + | .arith_trunci => do + if op.getNumOperands ctx opIn ≠ 1 then + throw "Expected 1 operand" + if op.getNumResults ctx opIn ≠ 1 then + throw "Expected 1 result" + if op.getNumRegions ctx opIn ≠ 0 then + throw "Expected 0 regions" + if op.getNumSuccessors ctx opIn ≠ 0 then + throw "Expected 0 successors" + pure () + | .arith_xori => do if op.getNumOperands ctx opIn ≠ 2 then throw "Expected 2 operands" if op.getNumResults ctx opIn ≠ 1 then From 96088115ff1d4b9f688666373ae566d5aa7894f3 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Mon, 23 Feb 2026 00:05:54 +0000 Subject: [PATCH 2/2] Address comments --- Test/Arith/identity.mlir | 14 +++++++------- Veir/Verifier.lean | 12 ++++++------ 2 files changed, 13 insertions(+), 13 deletions(-) diff --git a/Test/Arith/identity.mlir b/Test/Arith/identity.mlir index dadab8bf..3b47a167 100644 --- a/Test/Arith/identity.mlir +++ b/Test/Arith/identity.mlir @@ -4,7 +4,7 @@ ^4(): %5 = "arith.constant"() <{ "value" = 13 : i32 }> : () -> i32 %6 = "arith.addi"(%5, %5) : (i32, i32) -> i32 - %7 = "arith.addui_extended"(%5, %5) : (i32, i32) -> i32 + %70, %71 = "arith.addui_extended"(%5, %5) : (i32, i32) -> (i32, i32) %8 = "arith.andi"(%5, %5) : (i32, i32) -> i32 %9 = "arith.ceildivsi"(%5, %5) : (i32, i32) -> i32 %10 = "arith.ceildivui"(%5, %5) : (i32, i32) -> i32 @@ -18,8 +18,8 @@ %18 = "arith.minsi"(%5, %5) : (i32, i32) -> i32 %19 = "arith.minui"(%5, %5) : (i32, i32) -> i32 %20 = "arith.muli"(%5, %5) : (i32, i32) -> i32 - %21 = "arith.mulsi_extended"(%5, %5) : (i32, i32) -> i32 - %22 = "arith.mului_extended"(%5, %5) : (i32, i32) -> i32 + %210, %211 = "arith.mulsi_extended"(%5, %5) : (i32, i32) -> (i32, i32) + %220, %221 = "arith.mului_extended"(%5, %5) : (i32, i32) -> (i32, i32) %23 = "arith.ori"(%5, %5) : (i32, i32) -> i32 %24 = "arith.remsi"(%5, %5) : (i32, i32) -> i32 %25 = "arith.remui"(%5, %5) : (i32, i32) -> i32 @@ -36,7 +36,7 @@ // CHECK-NEXT: ^4(): // CHECK-NEXT: %5 = "arith.constant"() <{"value" = 13 : i32}> : () -> i32 // CHECK-NEXT: %6 = "arith.addi"(%5, %5) : (i32, i32) -> i32 -// CHECK-NEXT: %7 = "arith.addui_extended"(%5, %5) : (i32, i32) -> i32 +// CHECK-NEXT: %7_0, %7_1 = "arith.addui_extended"(%5, %5) : (i32, i32) -> (i32, i32) // CHECK-NEXT: %8 = "arith.andi"(%5, %5) : (i32, i32) -> i32 // CHECK-NEXT: %9 = "arith.ceildivsi"(%5, %5) : (i32, i32) -> i32 // CHECK-NEXT: %10 = "arith.ceildivui"(%5, %5) : (i32, i32) -> i32 @@ -50,8 +50,8 @@ // CHECK-NEXT: %18 = "arith.minsi"(%5, %5) : (i32, i32) -> i32 // CHECK-NEXT: %19 = "arith.minui"(%5, %5) : (i32, i32) -> i32 // CHECK-NEXT: %20 = "arith.muli"(%5, %5) : (i32, i32) -> i32 -// CHECK-NEXT: %21 = "arith.mulsi_extended"(%5, %5) : (i32, i32) -> i32 -// CHECK-NEXT: %22 = "arith.mului_extended"(%5, %5) : (i32, i32) -> i32 +// CHECK-NEXT: %21_0, %21_1 = "arith.mulsi_extended"(%5, %5) : (i32, i32) -> (i32, i32) +// CHECK-NEXT: %22_0, %22_1 = "arith.mului_extended"(%5, %5) : (i32, i32) -> (i32, i32) // CHECK-NEXT: %23 = "arith.ori"(%5, %5) : (i32, i32) -> i32 // CHECK-NEXT: %24 = "arith.remsi"(%5, %5) : (i32, i32) -> i32 // CHECK-NEXT: %25 = "arith.remui"(%5, %5) : (i32, i32) -> i32 @@ -62,4 +62,4 @@ // CHECK-NEXT: %30 = "arith.subi"(%5, %5) : (i32, i32) -> i32 // CHECK-NEXT: %31 = "arith.trunci"(%5) : (i32) -> i32 // CHECK-NEXT: %32 = "arith.xori"(%5, %5) : (i32, i32) -> i32 -// CHECK-NEXT: }) : () -> () \ No newline at end of file +// CHECK-NEXT: }) : () -> () diff --git a/Veir/Verifier.lean b/Veir/Verifier.lean index 9e9bf4df..ec1f4e5d 100644 --- a/Veir/Verifier.lean +++ b/Veir/Verifier.lean @@ -29,8 +29,8 @@ def OperationPtr.verifyLocalInvariants (op : OperationPtr) (ctx : IRContext) (op | .arith_addui_extended => do if op.getNumOperands ctx opIn ≠ 2 then throw "Expected 2 operands" - if op.getNumResults ctx opIn ≠ 1 then - throw "Expected 1 result" + if op.getNumResults ctx opIn ≠ 2 then + throw "Expected 2 results" if op.getNumRegions ctx opIn ≠ 0 then throw "Expected 0 regions" if op.getNumSuccessors ctx opIn ≠ 0 then @@ -179,8 +179,8 @@ def OperationPtr.verifyLocalInvariants (op : OperationPtr) (ctx : IRContext) (op | .arith_mulsi_extended => do if op.getNumOperands ctx opIn ≠ 2 then throw "Expected 2 operands" - if op.getNumResults ctx opIn ≠ 1 then - throw "Expected 1 result" + if op.getNumResults ctx opIn ≠ 2 then + throw "Expected 2 result" if op.getNumRegions ctx opIn ≠ 0 then throw "Expected 0 regions" if op.getNumSuccessors ctx opIn ≠ 0 then @@ -189,8 +189,8 @@ def OperationPtr.verifyLocalInvariants (op : OperationPtr) (ctx : IRContext) (op | .arith_mului_extended => do if op.getNumOperands ctx opIn ≠ 2 then throw "Expected 2 operands" - if op.getNumResults ctx opIn ≠ 1 then - throw "Expected 1 result" + if op.getNumResults ctx opIn ≠ 2 then + throw "Expected 2 result" if op.getNumRegions ctx opIn ≠ 0 then throw "Expected 0 regions" if op.getNumSuccessors ctx opIn ≠ 0 then