feat(parser): support forward references to SSA values

Test/Parsing/forward-reference-missing-block.mlir

@@ -0,0 +1,10 @@
+// RUN: not veir-opt %s 2>&1 | filecheck %s --strict-whitespace
+
+"builtin.module"() ({
+^entry:
+  "test.test"()[^missing] : () -> ()
+}) : () -> ()
+
+// CHECK:forward-reference-missing-block.mlir:5:17: error: block %missing was used but never defined
+// CHECK-NEXT:  "test.test"()[^missing] : () -> ()
+// CHECK-NEXT:                ^

Test/Parsing/forward-reference.mlir

@@ -0,0 +1,27 @@
+// RUN: veir-opt %s --allow-unregistered-dialect | filecheck %s
+
+// A value may be used in a block that appears, in file order, before the block
+// that defines it, as long as the definition dominates the use in the CFG. The
+// parser resolves such forward references rather than rejecting them.
+
+"builtin.module"() ({
+^bb0:
+  "test.test"()[^bb2] : () -> ()
+^bb1:
+  "test.test"(%v) : (i32) -> ()
+  "test.test"()[^bb1] : () -> ()
+^bb2:
+  %v = "test.test"() : () -> i32
+  "test.test"()[^bb1] : () -> ()
+}) : () -> ()
+
+// CHECK:      "builtin.module"() ({
+// CHECK-NEXT:   ^{{.*}}():
+// CHECK-NEXT:     "test.test"() [^[[DEF:.*]]] : () -> ()
+// CHECK-NEXT:   ^[[USE:.*]]():
+// CHECK-NEXT:     "test.test"(%[[V:.*]]) : (i32) -> ()
+// CHECK-NEXT:     "test.test"() [^[[USE]]] : () -> ()
+// CHECK-NEXT:   ^[[DEF]]():
+// CHECK-NEXT:     %[[V]] = "test.test"() : () -> i32
+// CHECK-NEXT:     "test.test"() [^[[USE]]] : () -> ()
+// CHECK-NEXT: }) : () -> ()

UnitTest/MlirParser.lean

@@ -280,3 +280,94 @@ def testParseOp (s : String) : IO Unit :=
 ^bb1:
   %a = "test.test"() : () -> i32
 }) : () -> ()"#
+
+/-!
+## Forward references to SSA values
+
+The parser accepts textual forward references to SSA values by creating a placeholder
+for the not-yet-defined value and resolving it once the definition is parsed. Dominance
+is not checked by the parser.
+-/
+
+/--
+  info: "builtin.module"() ({
+  ^4():
+    "test.test"() [^5] : () -> ()
+  ^5():
+    "test.test"(%10) : (i32) -> ()
+  ^9():
+    %10 = "test.test"() : () -> i32
+}) : () -> ()
+-/
+#guard_msgs in
+#eval! testParseOp r#""builtin.module"() ({
+^bb0:
+  "test.test"() [^bb1] : () -> ()
+^bb1:
+  "test.test"(%v) : (i32) -> ()
+^bb2:
+  %v = "test.test"() : () -> i32
+}) : () -> ()"#
+
+/--
+  info: "builtin.module"() ({
+  ^4():
+    %6 = "test.test"(%7) : (i32) -> i32
+    %7 = "test.test"() : () -> i32
+}) : () -> ()
+-/
+#guard_msgs in
+#eval! testParseOp r#""builtin.module"() ({
+  %b = "test.test"(%a) : (i32) -> i32
+  %a = "test.test"() : () -> i32
+}) : () -> ()"#
+
+/--
+  info: "builtin.module"() ({
+  ^4():
+    "test.test"() [^5] : () -> ()
+  ^5():
+    %8 = "test.test"(%10#1) : (i64) -> i32
+  ^9():
+    %10:2 = "test.test"() : () -> (i32, i64)
+}) : () -> ()
+-/
+#guard_msgs in
+#eval! testParseOp r#""builtin.module"() ({
+^bb0:
+  "test.test"() [^bb1] : () -> ()
+^bb1:
+  %b = "test.test"(%a#1) : (i64) -> i32
+^bb2:
+  %a:2 = "test.test"() : () -> (i32, i64)
+}) : () -> ()"#
+
+/--
+  error: definition of value %a#0 has type i64 but was used with type i32
+-/
+#guard_msgs in
+#eval! testParseOp r#""builtin.module"() ({
+  %b = "test.test"(%a) : (i32) -> i32
+  %a = "test.test"() : () -> i64
+}) : () -> ()"#
+
+/--
+  error: type mismatch for value %a: expected i64, got i32
+-/
+#guard_msgs in
+#eval! testParseOp r#""builtin.module"() ({
+  %b = "test.test"(%a) : (i32) -> i32
+  %c = "test.test"(%a) : (i64) -> i32
+  %a = "test.test"() : () -> i32
+}) : () -> ()"#
+
+/--
+  error: use of undefined value %a
+-/
+#guard_msgs in
+#eval! testParseOp r#""builtin.module"() ({
+  "test.test"(%a) : (i32) -> ()
+  "test.test"() ({
+    %a = "test.test"() : () -> i32
+  }) : () -> ()
+}) : () -> ()"#

Veir/Parser/DecidableInBounds.lean

@@ -66,6 +66,24 @@ def checkValueInBounds (value : ValuePtr) (ctx : IRContext OpInfo) :
   if h : value.InBounds ctx then pure ⟨h⟩
   else throwString s!"internal error: value is not in bounds"
 
+/-- Check that two values are distinct. -/
+def checkValuesNe (v₁ v₂ : ValuePtr) :
+    m (PLift (v₁ ≠ v₂)) :=
+  if h : v₁ ≠ v₂ then pure ⟨h⟩
+  else throwString s!"internal error: values are unexpectedly equal"
+
+/-- Check that an operation has no regions. -/
+def checkOpNoRegions (op : OperationPtr) (ctx : IRContext OpInfo) :
+    m (PLift (op.getNumRegions! ctx = 0)) :=
+  if h : op.getNumRegions! ctx = 0 then pure ⟨h⟩
+  else throwString s!"internal error: operation unexpectedly has regions"
+
+/-- Check that an operation has no uses. -/
+def checkOpNoUses (op : OperationPtr) (ctx : IRContext OpInfo) :
+    m (PLift (op.hasUses! ctx = false)) :=
+  if h : op.hasUses! ctx = false then pure ⟨h⟩
+  else throwString s!"internal error: operation unexpectedly has uses"
+
 /-- Check that a region is in bounds. -/
 def checkRegionInBounds (region : RegionPtr) (ctx : IRContext OpInfo) :
     m (PLift (region.InBounds ctx)) :=