[mlir] Refactor how additional verification is specified in ODS

[rriddle]

Summary

Currently if an operation requires additional verification, it specifies an inline
code block (let verifier = "blah"). This is quite problematic for various reasons, e.g.
it requires defining C++ inside of Tablegen which is discouraged when possible, but mainly because
nearly all usages simply forward to a static function static LogicalResult verify(SomeOp op).
This commit adds support for a hasVerifier bit field that specifies if an additional verifier
is needed, and when set to 1 declares a LogicalResult verify() method for operations to
override. For migration purposes, the existing behavior is untouched. Upstream usages will
be replaced in a followup to keep this patch focused on the hasVerifier implementation.

One main user facing change is that what was once MyOp::verify is now MyOp::verifyInvariants.
This better matches the name this method is called everywhere else, and also frees up verify for
the user defined additional verification. The verify function when generated now (for additional
verification) is private to the operation class, which should also help avoid accidental usages after
this switch.

[Chia-hungDuan]

In D116789, I'm considering to use a trait to specify if an operation has an additional verifier. There are two kind of the these traits, indicating when it'll be run(before/after region verification). What do you think about this approach? Sorry that CL is pending now, will work on it ASAP.

[rriddle]

In D118742#3289006, @Chia-hungDuan wrote:

In D116789, I'm considering to use a trait to specify if an operation has an additional verifier. There are two kind of the these traits, indicating when it'll be run(before/after region verification). What do you think about this approach? Sorry that CL is pending now, will work on it ASAP.

Thanks for pinging that, commented on that patch.

[lattner]

This is great River, it reduces boilerplate etc. That said, I particularly like how this nudges people towards a consistent approach, rather than everyone making up their own similar-but-different patterns.

Thank you for doing this, do you think parser/printer could follow a similar approach?

[rriddle]

In D118742#3290661, @lattner wrote:

This is great River, it reduces boilerplate etc. That said, I particularly like how this nudges people towards a consistent approach, rather than everyone making up their own similar-but-different patterns.

Thank you for doing this, do you think parser/printer could follow a similar approach?

Yeah, I intend to fix parser/printers in a followup.

[mehdi_amini]

mlir/include/mlir/IR/OpDefinition.h

204

The comment can be misleading for this now.

mlir/lib/Target/SPIRV/Serialization/Serializer.cpp

89

shouldn't this be instead verify(module)?

flang/tools/tco/tco.cpp

compileFIR(const mlir::PassPipelineCLParser &passPipeline) {
   fir::support::loadDialects(context);
   fir::support::registerLLVMTranslation(context);
   auto owningRef = mlir::parseSourceFile(sourceMgr, &context);
 
   if (!owningRef) {
     errs() << "Error can't load file " << inputFilename << '\n';
     return mlir::failure();
   }
-  if (mlir::failed(owningRef->verify())) {
+  if (mlir::failed(owningRef->verifyInvariants())) {
     errs() << "Error verifying FIR module\n";
     return mlir::failure();
   }
 
   std::error_code ec;
   ToolOutputFile out(outputFilename, ec, sys::fs::OF_None);
 
   // run passes

mlir/docs/OpDefinitions.md

 
 ### Custom verifier code
 
 Verification code will be automatically generated for
 [constraints](#constraints) specified on various entities of the op. To perform
 _additional_ verification, you can use
 
 ```tablegen
-let verifier = [{
-  ...
-}];
+let hasVerifier = 1;
 ```
 
-Code placed in `verifier` will be called after the auto-generated verification
-code. The order of trait verification excluding those of `verifier` should not
-be relied upon.
+This will generate a `LogicalResult verify()` method declaration on the op class
+that can be defined with any additional verification constraints. This method
+will be invoked after the auto-generated verification code. The order of trait
+verification excluding those of `hasVerifier` should not be relied upon.
 
 ### Declarative Assembly Format
 
 The custom assembly form of the operation may be specified in a declarative
 string that matches the operations operands, attributes, etc. With the ability
 to express additional information that needs to be parsed to build the
 operation:
 

mlir/include/mlir/Dialect/Affine/IR/AffineOps.h

public:
 
   static StringRef getSrcMapAttrName() { return "src_map"; }
   static StringRef getDstMapAttrName() { return "dst_map"; }
   static StringRef getTagMapAttrName() { return "tag_map"; }
 
   static StringRef getOperationName() { return "affine.dma_start"; }
   static ParseResult parse(OpAsmParser &parser, OperationState &result);
   void print(OpAsmPrinter &p);
-  LogicalResult verify();
+  LogicalResult verifyInvariants();
   LogicalResult fold(ArrayRef<Attribute> cstOperands,
                      SmallVectorImpl<OpFoldResult> &results);
 
   /// Returns true if this DMA operation is strided, returns false otherwise.
   bool isStrided() {
     return getNumOperands() !=
            getTagMemRefOperandIndex() + 1 + getTagMap().getNumInputs() + 1;
   }
public:
   }
 
   /// Returns the number of elements transferred by the associated DMA op.
   Value getNumElements() { return getOperand(1 + getTagMap().getNumInputs()); }
 
   static StringRef getTagMapAttrName() { return "tag_map"; }
   static ParseResult parse(OpAsmParser &parser, OperationState &result);
   void print(OpAsmPrinter &p);
-  LogicalResult verify();
+  LogicalResult verifyInvariants();
   LogicalResult fold(ArrayRef<Attribute> cstOperands,
                      SmallVectorImpl<OpFoldResult> &results);
 };
 
 /// Returns true if the given Value can be used as a dimension id in the region
 /// of the closest surrounding op that has the trait `AffineScope`.
 bool isValidDim(Value value);
 

mlir/include/mlir/IR/OpBase.td

class Op<Dialect dialect, string mnemonic, list<Trait> props = []> {
   code parser = ?;
 
   // Custom printer.
   code printer = ?;
 
   // Custom assembly format.
   string assemblyFormat = ?;
 
-  // Custom verifier.
+  // A bit indicating if the operation has additional invariants that need to
+  // verified (aside from those verified by other ODS constructs). If set to `1`,
+  // an additional `LogicalResult verify()` declaration will be generated on the
+  // operation class. The operation should implement this method and verify the
+  // additional necessary invariants.
+  bit hasVerifier = 0;
+  // A custom code block corresponding to the extra verification code of the
+  // operation.
+  // NOTE: This field is deprecated in favor of `hasVerifier` and is slated for
+  // deletion.
   code verifier = ?;
 
   // Whether this op has associated canonicalization patterns.
   bit hasCanonicalizer = 0;
 
   // Whether this op has a static "canonicalize" method to perform "match and
   // rewrite patterns".
   bit hasCanonicalizeMethod = 0;

mlir/include/mlir/IR/OpDefinition.h

public:
   /// This hook returns any canonicalization pattern rewrites that the operation
   /// supports, for use by the canonicalization pass.
   static void getCanonicalizationPatterns(RewritePatternSet &results,
                                           MLIRContext *context) {}
 
 protected:
   /// If the concrete type didn't implement a custom verifier hook, just fall
   /// back to this one which accepts everything.
-  LogicalResult verify() { return success(); }
+  LogicalResult verifyInvariants() { return success(); }
 
   /// Parse the custom form of an operation. Unless overridden, this method will
   /// first try to get an operation parser from the op's dialect. Otherwise the
   /// custom assembly form of an op is always rejected. Op implementations
   /// should implement this to return failure. On success, they should fill in
   /// result with the fields to use.
   static ParseResult parse(OpAsmParser &parser, OperationState &result);
 

 /// This provides public APIs that all operations should have.  The template
 /// argument 'ConcreteType' should be the concrete type by CRTP and the others
 /// are base classes by the policy pattern.
 template <typename ConcreteType, template <typename T> class... Traits>
 class Op : public OpState, public Traits<ConcreteType>... {
 public:
   /// Inherit getOperation from `OpState`.
   using OpState::getOperation;
+  using OpState::verifyInvariants;
 
   /// Return if this operation contains the provided trait.
   template <template <typename T> class Trait>
   static constexpr bool hasTrait() {
     return llvm::is_one_of<Trait<ConcreteType>, Traits<ConcreteType>...>::value;
   }
 
   /// Create a deep copy of this operation.
getPrintAssemblyFnImpl() {
     return &printAssembly;
   }
   static void printAssembly(Operation *op, OpAsmPrinter &p,
                             StringRef defaultDialect) {
     OpState::printOpName(op, p, defaultDialect);
     return cast<ConcreteType>(op).print(p);
   }
   /// Implementation of `VerifyInvariantsFn` OperationName hook.
+  static LogicalResult verifyInvariants(Operation *op) {
+    static_assert(hasNoDataMembers(),
+                  "Op class shouldn't define new data members");
+    return failure(
+        failed(op_definition_impl::verifyTraits<VerifiableTraitsTupleT>(op)) ||
+        failed(cast<ConcreteType>(op).verifyInvariants()));
+  }
   static OperationName::VerifyInvariantsFn getVerifyInvariantsFn() {
-    return &verifyInvariants;
+    return static_cast<LogicalResult (*)(Operation *)>(&verifyInvariants);
   }
 
   static constexpr bool hasNoDataMembers() {
     // Checking that the derived class does not define any member by comparing
     // its size to an ad-hoc EmptyOp.
     class EmptyOp : public Op<EmptyOp, Traits...> {};
     return sizeof(ConcreteType) == sizeof(EmptyOp);
   }
 
-  static LogicalResult verifyInvariants(Operation *op) {
-    static_assert(hasNoDataMembers(),
-                  "Op class shouldn't define new data members");
-    return failure(
-        failed(op_definition_impl::verifyTraits<VerifiableTraitsTupleT>(op)) ||
-        failed(cast<ConcreteType>(op).verify()));
-  }
-
   /// Allow access to internal implementation methods.
   friend RegisteredOperationName;
 };
 
 /// This class represents the base of an operation interface. See the definition
 /// of `detail::Interface` for requirements on the `Traits` type.
 template <typename ConcreteType, typename Traits>
 class OpInterface

mlir/include/mlir/Parser.h

assert(op->getNumRegions() == 1 && llvm::hasSingleElement(op->getRegion(0)) &&
          "expected generated operation to have a single region with a single "
          "block");
   Block *opBlock = &op->getRegion(0).front();
   opBlock->getOperations().splice(opBlock->begin(),
                                   parsedBlock->getOperations());
 
   // After splicing, verify just this operation to ensure it can properly
   // contain the operations inside of it.
-  if (failed(op.verify()))
+  if (failed(op.verifyInvariants()))
     return OwningOpRef<ContainerOpT>();
   return opRef;
 }
 } // namespace detail
 
 /// This parses the file specified by the indicated SourceMgr and appends parsed
 /// operations to the given block. If the block is non-empty, the operations are
 /// placed before the current terminator. If parsing is successful, success is

mlir/lib/Dialect/Affine/IR/AffineOps.cpp

ParseResult AffineDmaStartOp::parse(OpAsmParser &parser,
   if (srcMapOperands.size() != srcMapAttr.getValue().getNumInputs() ||
       dstMapOperands.size() != dstMapAttr.getValue().getNumInputs() ||
       tagMapOperands.size() != tagMapAttr.getValue().getNumInputs())
     return parser.emitError(parser.getNameLoc(),
                             "memref operand count not equal to map.numInputs");
   return success();
 }
 
-LogicalResult AffineDmaStartOp::verify() {
+LogicalResult AffineDmaStartOp::verifyInvariants() {
   if (!getOperand(getSrcMemRefOperandIndex()).getType().isa<MemRefType>())
     return emitOpError("expected DMA source to be of memref type");
   if (!getOperand(getDstMemRefOperandIndex()).getType().isa<MemRefType>())
     return emitOpError("expected DMA destination to be of memref type");
   if (!getOperand(getTagMemRefOperandIndex()).getType().isa<MemRefType>())
     return emitOpError("expected DMA tag to be of memref type");
 
   unsigned numInputsAllMaps = getSrcMap().getNumInputs() +
return parser.emitError(parser.getNameLoc(),
                             "expected tag to be of memref type");
 
   if (tagMapOperands.size() != tagMapAttr.getValue().getNumInputs())
     return parser.emitError(parser.getNameLoc(),
                             "tag memref operand count != to map.numInputs");
   return success();
 }
 
-LogicalResult AffineDmaWaitOp::verify() {
+LogicalResult AffineDmaWaitOp::verifyInvariants() {
   if (!getOperand(0).getType().isa<MemRefType>())
     return emitOpError("expected DMA tag to be of memref type");
   Region *scope = getAffineScope(*this);
   for (auto idx : getTagIndices()) {
     if (!idx.getType().isIndex())
       return emitOpError("index to dma_wait must have 'index' type");
     if (!isValidAffineIndexOperand(idx, scope))
       return emitOpError("index must be a dimension or symbol identifier");

mlir/lib/Target/SPIRV/Serialization/Serializer.cpp

 
 Serializer::Serializer(spirv::ModuleOp module,
                        const SerializationOptions &options)
     : module(module), mlirBuilder(module.getContext()), options(options) {}
 
 LogicalResult Serializer::serialize() {
   LLVM_DEBUG(llvm::dbgs() << "+++ starting serialization +++\n");
 
-  if (failed(module.verify()))
+  if (failed(module.verifyInvariants()))
     return failure();
 
   // TODO: handle the other sections
   processCapability();
   processExtension();
   processMemoryModel();
   processDebugInfo();
 

mlir/test/lib/Dialect/Test/TestDialect.cpp

void StringAttrPrettyNameOp::getAsmResultNames(
   auto value = getNames();
   for (size_t i = 0, e = value.size(); i != e; ++i)
     if (auto str = value[i].dyn_cast<StringAttr>())
       if (!str.getValue().empty())
         setNameFn(getResult(i), str.getValue());
 }
 
 //===----------------------------------------------------------------------===//
+// ResultTypeWithTraitOp
+//===----------------------------------------------------------------------===//
+
+LogicalResult ResultTypeWithTraitOp::verify() {
+  if ((*this)->getResultTypes()[0].hasTrait<TypeTrait::TestTypeTrait>())
+    return success();
+  return emitError("result type should have trait 'TestTypeTrait'");
+}
+
+//===----------------------------------------------------------------------===//
+// AttrWithTraitOp
+//===----------------------------------------------------------------------===//
+
+LogicalResult AttrWithTraitOp::verify() {
+  if (getAttr().hasTrait<AttributeTrait::TestAttrTrait>())
+    return success();
+  return emitError("'attr' attribute should have trait 'TestAttrTrait'");
+}
+
+//===----------------------------------------------------------------------===//
 // RegionIfOp
 //===----------------------------------------------------------------------===//
 
 static void print(OpAsmPrinter &p, RegionIfOp op) {
   p << " ";
   p.printOperands(op.getOperands());
   p << ": " << op.getOperandTypes();
   p.printArrowTypeList(op.getResultTypes());

mlir/test/lib/Dialect/Test/TestOps.td

let extraClassDeclaration = [{
     void getAsmResultNames(::llvm::function_ref<void(::mlir::Value, ::llvm::StringRef)> setNameFn) {}
   }];
   let assemblyFormat = "regions attr-dict-with-keyword";
 }
 
 // This operation requires its return type to have the trait 'TestTypeTrait'.
 def ResultTypeWithTraitOp : TEST_Op<"result_type_with_trait", []> {
   let results = (outs AnyType);
-
-  let verifier = [{
-    if((*this)->getResultTypes()[0].hasTrait<TypeTrait::TestTypeTrait>())
-      return success();
-    return this->emitError("result type should have trait 'TestTypeTrait'");
-  }];
+  let hasVerifier = 1;
 }
 
 // This operation requires its "attr" attribute to have the
 // trait 'TestAttrTrait'.
 def AttrWithTraitOp : TEST_Op<"attr_with_trait", []> {
   let arguments = (ins AnyAttr:$attr);
-
-  let verifier = [{
-    if (this->getAttr().hasTrait<AttributeTrait::TestAttrTrait>())
-      return success();
-    return this->emitError("'attr' attribute should have trait 'TestAttrTrait'");
-  }];
+  let hasVerifier = 1;
 }
 
-
 //===----------------------------------------------------------------------===//
 // Test Locations
 //===----------------------------------------------------------------------===//
 
 def TestLocationSrcOp : TEST_Op<"loc_src"> {
   let arguments = (ins I32:$input);
   let results = (outs I32:$output);
 }

mlir/test/mlir-tblgen/op-decl-and-defs.td

 // CHECK:   ::mlir::Attribute removeAttr2Attr();
 // CHECK:   static void build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, Value val);
 // CHECK:   static void build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, int integer = 0);
 // CHECK:   static void build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::Type r, ::mlir::TypeRange s, ::mlir::Value a, ::mlir::ValueRange b, ::mlir::IntegerAttr attr1, /*optional*/::mlir::FloatAttr attr2, unsigned someRegionsCount)
 // CHECK:   static void build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::Type r, ::mlir::TypeRange s, ::mlir::Value a, ::mlir::ValueRange b, uint32_t attr1, /*optional*/::mlir::FloatAttr attr2, unsigned someRegionsCount)
 // CHECK:   static void build(::mlir::OpBuilder &, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes, unsigned numRegions)
 // CHECK:   static ::mlir::ParseResult parse(::mlir::OpAsmParser &parser, ::mlir::OperationState &result);
 // CHECK:   void print(::mlir::OpAsmPrinter &p);
-// CHECK:   ::mlir::LogicalResult verify();
+// CHECK:   ::mlir::LogicalResult verifyInvariants();
 // CHECK:   static void getCanonicalizationPatterns(::mlir::RewritePatternSet &results, ::mlir::MLIRContext *context);
 // CHECK:   ::mlir::LogicalResult fold(::llvm::ArrayRef<::mlir::Attribute> operands, ::llvm::SmallVectorImpl<::mlir::OpFoldResult> &results);
 // CHECK:   // Display a graph for debugging purposes.
 // CHECK:   void displayGraph();
 // CHECK: };
 
 // DEFS-LABEL: NS::AOp definitions
 

mlir/tools/mlir-tblgen/OpDefinitionsGen.cpp

if (traitName == "::mlir::OpTrait::AttrSizedOperandSegments") {
       body << formatv(
           checkAttrSizedValueSegmentsCode, attrName, op.getNumResults(),
           "result", emitHelper.getAttr(attrName), emitHelper.emitErrorPrefix());
     }
   }
 }
 
 void OpEmitter::genVerifier() {
-  auto *method = opClass.addMethod("::mlir::LogicalResult", "verify");
-  ERROR_IF_PRUNED(method, "verify", op);
+  auto *method = opClass.addMethod("::mlir::LogicalResult", "verifyInvariants");
+  ERROR_IF_PRUNED(method, "verifyInvariants", op);
   auto &body = method->body();
 
   OpOrAdaptorHelper emitHelper(op, /*isOp=*/true);
   genNativeTraitAttrVerifier(body, emitHelper);
 
   auto *valueInit = def.getValueInit("verifier");
   StringInit *stringInit = dyn_cast<StringInit>(valueInit);
-  bool hasCustomVerify = stringInit && !stringInit->getValue().empty();
+  bool hasCustomVerifyCodeBlock = stringInit && !stringInit->getValue().empty();
   populateSubstitutions(emitHelper, verifyCtx);
 
   genAttributeVerifier(emitHelper, verifyCtx, body, staticVerifierEmitter);
   genOperandResultVerifier(body, op.getOperands(), "operand");
   genOperandResultVerifier(body, op.getResults(), "result");
 
   for (auto &trait : op.getTraits()) {
     if (auto *t = dyn_cast<tblgen::PredTrait>(&trait)) {
       body << tgfmt("  if (!($0))\n    "
                     "return emitOpError(\"failed to verify that $1\");\n",
                     &verifyCtx, tgfmt(t->getPredTemplate(), &verifyCtx),
                     t->getSummary());
     }
   }
 
   genRegionVerifier(body);
   genSuccessorVerifier(body);
 
-  if (hasCustomVerify) {
+  if (def.getValueAsBit("hasVerifier")) {
+    auto *method = opClass.declareMethod<Method::Private>(
+        "::mlir::LogicalResult", "verify");
+    ERROR_IF_PRUNED(method, "verify", op);
+    body << "  return verify();\n";
+
+  } else if (hasCustomVerifyCodeBlock) {
     FmtContext fctx;
     fctx.addSubst("cppClass", opClass.getClassName());
     auto printer = stringInit->getValue().ltrim().rtrim(" \t\v\f\r");
     body << "  " << tgfmt(printer, &fctx);
   } else {
     body << "  return ::mlir::success();\n";
   }
 }