diff --git a/Test/Parsing/forward-reference-missing-block.mlir b/Test/Parsing/forward-reference-missing-block.mlir new file mode 100644 index 000000000..06d893d10 --- /dev/null +++ b/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: ^ diff --git a/Test/Parsing/forward-reference.mlir b/Test/Parsing/forward-reference.mlir new file mode 100644 index 000000000..c628462c9 --- /dev/null +++ b/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: }) : () -> () diff --git a/UnitTest/MlirParser.lean b/UnitTest/MlirParser.lean index 82696426d..96522d5ba 100644 --- a/UnitTest/MlirParser.lean +++ b/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 + }) : () -> () +}) : () -> ()"# diff --git a/Veir/Parser/DecidableInBounds.lean b/Veir/Parser/DecidableInBounds.lean index 82fc1f052..b0faf2bc0 100644 --- a/Veir/Parser/DecidableInBounds.lean +++ b/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)) := diff --git a/Veir/Parser/MlirParser.lean b/Veir/Parser/MlirParser.lean index b398215b6..6197dc397 100644 --- a/Veir/Parser/MlirParser.lean +++ b/Veir/Parser/MlirParser.lean @@ -35,6 +35,29 @@ def BlockEntry.block : BlockEntry → BlockPtr | .Defined block _ => block | .ForwardDeclared block _ => block +/-- + Bookkeeping for an SSA value that has been referenced before it is defined + (a "forward reference"). For each referenced result index, we hold a detached + single-result placeholder operation whose result stands in for the eventual + definition. When the definition is finally parsed, all uses of each + placeholder result are replaced by the real value (via `Rewriter.replaceValue`) + and the placeholder operation is erased, keeping the module well-formed by + construction. + + This mirrors MLIR's `createForwardRefPlaceholder`, which likewise uses a throwaway + operation result (not a distinct kind of SSA value) as the placeholder. +-/ +structure ForwardValue where + /-- Map from each referenced result index to its placeholder operation and first-use location. -/ + placeholders : Std.HashMap Nat (OperationPtr × Location) + /-- Location of the first use, used for error reporting if the value is never defined. -/ + loc : Location + /-- The nesting depth of the scope in which this value was first referenced. + A forward reference can only be resolved by a definition in the same scope, + matching MLIR's SSA scoping rules. -/ + scopeDepth : Nat + deriving Inhabited + structure MlirParserState where /-- The current IR context. -/ ctx : WfIRContext OpCode @@ -46,6 +69,13 @@ structure MlirParserState where Each scope sees all values defined in parent scopes (those that appear earlier in the array). -/ definitionsPerScope : Array (Std.HashSet ByteArray) + /-- + Values that have been referenced but not yet defined, keyed by name. + These are resolved and removed when the corresponding definition is parsed; + any that remain when their enclosing region finishes parsing are reported as + uses of undefined values. + -/ + forwardValues : Std.HashMap ByteArray ForwardValue /-- The blocks that have been encountered during parsing, along with whether they have been defined or only forward declared. @@ -62,6 +92,7 @@ def MlirParserState.fromContext (ctx : WfIRContext OpCode) allowUnregisteredDialect values := Std.HashMap.emptyWithCapacity 128 definitionsPerScope := #[Std.HashSet.emptyWithCapacity 2] + forwardValues := Std.HashMap.emptyWithCapacity 1 blocks := Std.HashMap.emptyWithCapacity 1 } @@ -125,28 +156,6 @@ def inChildScope {α : Type} (m : MlirParserM α) : MlirParserM α := do return result -/-- - Register an array of parsed values with the given name in the current scope. - This is used to keep track of values that have been defined during parsing. --/ -def registerValueDefs (name : ByteArray) (pos : Location) (values : Array ValuePtr) : MlirParserM Unit := do - if let some (_, existingPos) := (← get).values[name]? then - let error := ParserError.mk s!"value %{String.fromUTF8! name} has already been defined" pos [] - let error := error.addNote existingPos "previously defined here" - throw error - modify fun s => - { s with - values := s.values.insert name (values, pos) - definitionsPerScope := s.definitionsPerScope.modify (s.definitionsPerScope.size - 1) (·.insert name) - } - -/-- - Register a single value with the given name in current scope. - This is used to keep track of values that have been defined during parsing. --/ -def registerValueDef (name : ByteArray) (pos : Location) (value : ValuePtr) : MlirParserM Unit := - registerValueDefs name pos #[value] - /-- Set the current IR context. This should be called whenever any modifications have been made to the context @@ -184,6 +193,93 @@ def modifyContextM' (f : WfIRContext OpCode → MlirParserM (α × WfIRContext O def modifyContextM (f : WfIRContext OpCode → MlirParserM (WfIRContext OpCode)) : MlirParserM Unit := modifyContextM' (fun ctx => do pure ((), ← f ctx)) +/-- + The operation code used for forward-reference placeholders. + As in MLIR (`createForwardRefPlaceholder`), we use a throwaway operation result + (specifically a `builtin.unrealized_conversion_cast`) to stand in for a value that + is referenced before it is defined. This avoids introducing a distinct kind of SSA + value: a placeholder is just an ordinary operation result. +-/ +def placeholderOpCode : OpCode := .builtin .unrealized_conversion_cast + +/-- + Create a detached, single-result placeholder operation of the given type. + Its result is used to stand in for a value that has been referenced but not yet + defined. The operation is not inserted into any block; once the real definition is + parsed, `resolveForwardValue` replaces all uses of this result with the real value + and erases this operation. +-/ +def createForwardRefPlaceholder (ty : TypeAttr) (loc : Location) : MlirParserM OperationPtr := + modifyContextM' fun ctx => do + match WfRewriter.createOp ctx placeholderOpCode #[ty] #[] #[] #[] + (default : propertiesOf placeholderOpCode) none with + | none => throwAt loc "internal error: failed to create forward-reference placeholder" + | some (ctx', op) => pure (op, ctx') + +/-- + Resolve a forward-referenced value now that its real definition has been parsed. + For each result index that was referenced, replace all uses of the placeholder result + with the corresponding real value and erase the placeholder operation. +-/ +def resolveForwardValue (name : ByteArray) (pos : Location) (fwd : ForwardValue) + (values : Array ValuePtr) : MlirParserM Unit := do + for (index, (placeholderOp, useLoc)) in fwd.placeholders do + let some realValue := values[index]? + | throw (({ msg := s!"definition of value %{String.fromUTF8! name} provides {values.size} results, but result #{index} was used", + pos := some pos } : ParserError).addNote useLoc "value used here") + let placeholderValue : ValuePtr := placeholderOp.getResult 0 + /- The value has a single type, so the definition must match every use. -/ + let ⟨ctx, _⟩ ← getContext + let usedType := placeholderValue.getType! ctx + let definedType := realValue.getType! ctx + if usedType ≠ definedType then + throw (({ msg := s!"definition of value %{String.fromUTF8! name}#{index} has type {definedType} but was used with type {usedType}", + pos := some pos } : ParserError).addNote useLoc "value used here") + /- Rewire all uses of the placeholder to the real value, then erase the placeholder. -/ + modifyContextM fun ctx => do + let ⟨hOldIn⟩ ← checkValueInBounds placeholderValue ctx.raw + let ⟨hNewIn⟩ ← checkValueInBounds realValue ctx.raw + let ⟨hNe⟩ ← checkValuesNe placeholderValue realValue + pure (WfRewriter.replaceValue ctx placeholderValue realValue hNe hOldIn hNewIn) + modifyContextM fun ctx => do + let ⟨hOpIn⟩ ← checkOpInBounds placeholderOp ctx.raw + let ⟨hNoRegions⟩ ← checkOpNoRegions placeholderOp ctx.raw + let ⟨hNoUses⟩ ← checkOpNoUses placeholderOp ctx.raw + pure (WfRewriter.eraseOp ctx placeholderOp hNoRegions (by simpa using hNoUses) hOpIn) + modify fun s => { s with forwardValues := s.forwardValues.erase name } + +/-- + Register an array of parsed values with the given name in the current scope. + This is used to keep track of values that have been defined during parsing. + If the name was forward-referenced earlier in the same scope, the placeholders + created for it are resolved to the newly-parsed values. +-/ +def registerValueDefs (name : ByteArray) (pos : Location) (values : Array ValuePtr) : MlirParserM Unit := do + let state ← get + let currentDepth := state.definitionsPerScope.size - 1 + /- If this name was forward-referenced in the current scope, resolve it. A forward + reference in an enclosing scope is left alone: it cannot be satisfied by a + definition nested inside it, and will be reported when its own region finishes. -/ + if let some fwd := state.forwardValues[name]? then + if fwd.scopeDepth = currentDepth then + resolveForwardValue name pos fwd values + if let some (_, existingPos) := (← get).values[name]? then + let error := ParserError.mk s!"value %{String.fromUTF8! name} has already been defined" pos [] + let error := error.addNote existingPos "previously defined here" + throw error + modify fun s => + { s with + values := s.values.insert name (values, pos) + definitionsPerScope := s.definitionsPerScope.modify (s.definitionsPerScope.size - 1) (·.insert name) + } + +/-- + Register a single value with the given name in current scope. + This is used to keep track of values that have been defined during parsing. +-/ +def registerValueDef (name : ByteArray) (pos : Location) (value : ValuePtr) : MlirParserM Unit := + registerValueDefs name pos #[value] + /-- Create a block at the given insert point and register its name in the parsing context. If a block was already declared with the given name, use that block instead, and @@ -347,13 +443,52 @@ def parseBlockOperand : MlirParserM BlockPtr := do def parseBlockOperands : MlirParserM (Array BlockPtr) := do return (← parseOptionalDelimitedList .square parseBlockOperand).getD #[] +/-- + Resolve a reference to a value that has not yet been defined by creating (or reusing) + a placeholder operation whose result stands in for the eventual definition. + The placeholder is recorded in `forwardValues` and resolved once the definition is parsed. +-/ +def resolveForwardOperand (operand : UnresolvedOperand) (expectedType : TypeAttr) : MlirParserM ValuePtr := do + let idx := operand.indexD + match (← get).forwardValues[operand.name]? with + | some fwd => + match fwd.placeholders[idx]? with + | some (placeholderOp, useLoc) => + /- The same result index was referenced before: reuse its placeholder and + check the type is consistent with the previous use. -/ + let placeholderValue : ValuePtr := placeholderOp.getResult 0 + let ⟨ctx, _⟩ ← getContext + let parsedType := placeholderValue.getType! ctx + if parsedType ≠ expectedType then + throw (({ msg := s!"type mismatch for value {operand}: expected {expectedType}, got {parsedType}", + pos := some operand.pos } : ParserError).addNote useLoc "value first used here") + return placeholderValue + | none => + /- A new result index of an already forward-referenced value. -/ + let placeholderOp ← createForwardRefPlaceholder expectedType operand.pos + modify fun s => { s with + forwardValues := s.forwardValues.insert operand.name + { fwd with placeholders := fwd.placeholders.insert idx (placeholderOp, operand.pos) } } + return placeholderOp.getResult 0 + | none => + /- First reference of a not-yet-defined value. -/ + let placeholderOp ← createForwardRefPlaceholder expectedType operand.pos + modify fun s => { s with + forwardValues := s.forwardValues.insert operand.name + { placeholders := (Std.HashMap.emptyWithCapacity 1).insert idx (placeholderOp, operand.pos), + loc := operand.pos, + scopeDepth := s.definitionsPerScope.size - 1 } } + return placeholderOp.getResult 0 + /-- Resolve an operand to an SSA value of the expected type. - Throw an error if the value is not defined or if the type does not match. + If the value has not yet been defined, a forward-reference placeholder is created; + it will be resolved when the definition is parsed, or reported as an error if the + value is never defined within its region. -/ def resolveOperand (operand : UnresolvedOperand) (expectedType : TypeAttr) : MlirParserM ValuePtr := do let some (values, defPos) := (← getValues? operand.name) - | throwAt operand.pos s!"use of undefined value %{operand.nameString}" + | resolveForwardOperand operand expectedType let some value := values[operand.indexD]? | throw (({ msg := s!"invalid result index {operand.indexD} for %{operand.nameString}", pos := some operand.pos } : ParserError).addNote defPos "value defined here") @@ -600,6 +735,12 @@ partial def parseRegion : MlirParserM RegionPtr := do if let .ForwardDeclared _ forwardLoc := entry then throwAt forwardLoc s!"block %{String.fromUTF8! blockName} was used but never defined" + /- Check that all values forward referenced in this region were eventually defined. -/ + let currentDepth := (← getThe MlirParserState).definitionsPerScope.size - 1 + for (valueName, fwd) in (← getThe MlirParserState).forwardValues do + if fwd.scopeDepth = currentDepth then + throwAt fwd.loc s!"use of undefined value %{String.fromUTF8! valueName}" + /- Restore the previous block parsing state. -/ modifyThe MlirParserState fun s => {s with blocks := oldBlocks} return region