[mlir] Support verification order (3/3)

[Chia-hungDuan]

Summary

In this CL, update the function name of verifier according to the
behavior. If a verifier needs to access the region then it'll be updated
to verifyRegions.

[rriddle]

mlir/include/mlir/Interfaces/InferTypeOpInterface.td

67–68

mlir/lib/Dialect/LLVMIR/IR/LLVMDialect.cpp

1774

Some of the checks here are not related to regions. We should really keep the checks contained to where they should be checked (I would keep everything non-region in the main hasVerifier). hasRegionVerifier should really only contain region related verification code.

mlir/lib/Dialect/OpenMP/IR/OpenMPDialect.cpp

1267

Same comment here and throughout.

mlir/lib/IR/Operation.cpp

1091–1095

If it should be well formed (i.e. if you are guaranteed to be able to assume it), we should just remove the assert. It feels like a legacy assert at this point.

mlir/test/Dialect/Tensor/invalid.mlir

379

Missing newline here?

[Chia-hungDuan]

Address review comment and quickly went through the verifiers on Ops and updated some of them.

[Chia-hungDuan]

mlir/lib/Dialect/LLVMIR/IR/LLVMDialect.cpp

1774

Supported both hasVerifier and hasRegionVerifier and split the verifier based on if it touches the region

mlir/lib/IR/Operation.cpp

1091–1095

Ideally no one should just use this except the trait. Removed.

mlir/test/Dialect/Tensor/invalid.mlir

379

Not sure what happened here, upload a new one and see if this is still happening.

[Chia-hungDuan]

Fix verification label in linalg op interface

[jpienaar]

Nice thanks

mlir/include/mlir/IR/OpBase.td

2068–2069

This probably becomes more interesting with SameOperandsAndResultType moving to to interfaces (and I still need to do some work there to make it OpTraitList), A little bit of artifact of this file being a collection of all attributes.

mlir/lib/Dialect/LLVMIR/IR/LLVMDialect.cpp

2138

I'm a little bit hesitant to have this duplicated at every decl site.

mlir/test/Dialect/GPU/invalid.mlir

29 ↗

(On Diff #411954)

Ooc why this change?

mlir/test/Dialect/LLVMIR/global.mlir

175

Having the SSA id in the error message is unfortunate, especially as not guaranteed to be stable (so makes it easy to create a flaky test here, e.g., every run could have a different id returned)

mlir/test/Dialect/SCF/invalid.mlir

292 ↗

(On Diff #411954)

So here yield would fail first to verify parent relationship and change error else?

[rriddle]

mlir/lib/Dialect/LLVMIR/IR/LLVMDialect.cpp

2138

Yeah, can we just drop this? Feels like this should be gleaned from the ODS documentation (which I know right now is a mess).

mlir/lib/Dialect/SPIRV/IR/SPIRVOps.cpp

4126 ↗

(On Diff #411954)

Can we signal this in the op definition? i.e. by removing the hasVerifier or by adding hasVerifier = ?(if the hasVerifier was set in a base class).

[Chia-hungDuan]

Address review comments and rebase

mlir/include/mlir/IR/OpBase.td

2068–2069

Yep, it may be a problem for describing dependency between these traits and interfaces. Not sure if we can do it in pure string rather than a tblgen def

mlir/lib/Dialect/LLVMIR/IR/LLVMDialect.cpp

2138

All removed.
Added more descriptions in the doc.

mlir/lib/Dialect/SPIRV/IR/SPIRVOps.cpp

4126 ↗

(On Diff #411954)

disable them in the derived class by adding let hasVerifier = 0

mlir/test/Dialect/GPU/invalid.mlir

29 ↗

(On Diff #411954)

return expects its parent to be builtin.func so that we won't get the expected error. In fact, there are many cases like this, most of the ops are well-defined, i.e., they specify the restriction of terminator, the restriction of parent op, .etc. As a result, some tests case we may not be able to verify the fact they want without using ops from other dialects(like test dialect)

mlir/test/Dialect/LLVMIR/global.mlir

175

You're right. Removed the later of "block with no terminator"

mlir/test/Dialect/SCF/invalid.mlir

292 ↗

(On Diff #411954)

Yes, like the case above. yield has assigned its parent

[rriddle]

mlir/lib/Dialect/GPU/IR/GPUDialect.cpp

278 ↗

(On Diff #414270)

Can we remove this?

[Chia-hungDuan]

Address review comment

mlir/lib/Dialect/GPU/IR/GPUDialect.cpp

278 ↗

(On Diff #414270)

Sorry, a leftover.

mlir/include/mlir/Dialect/LLVMIR/LLVMOps.td

let extraClassDeclaration = [{
     /// op with the initializer value.
     Block *getInitializerBlock() {
       return getInitializerRegion().empty() ?
         nullptr : &getInitializerRegion().front();
     }
   }];
 
   let hasCustomAssemblyFormat = 1;
-  let hasVerifier = 1;
+  let hasRegionVerifier = 1;
 }
 
 def LLVM_GlobalCtorsOp : LLVM_Op<"mlir.global_ctors", [
                            DeclareOpInterfaceMethods<SymbolUserOpInterface>]> {
   let arguments = (ins FlatSymbolRefArrayAttr
                    : $ctors, I32ArrayAttr
                    : $priorities);
   let summary = "LLVM dialect global_ctors.";

mlir/include/mlir/Dialect/OpenMP/OpenMPOps.td

let description = [{
     similar to a compare-exchange loop based atomic update.
   }];
 
   let arguments = (ins OpenMP_PointerLikeType:$x,
                        DefaultValuedAttr<I64Attr, "0">:$hint,
                        OptionalAttr<MemoryOrderKindAttr>:$memory_order);
   let regions = (region SizedRegion<1>:$region);
   let hasCustomAssemblyFormat = 1;
-  let hasVerifier = 1;
+  let hasRegionVerifier = 1;
 }
 
 def AtomicCaptureOp : OpenMP_Op<"atomic.capture",
     [SingleBlockImplicitTerminator<"TerminatorOp">]> {
   let summary = "performs an atomic capture";
   let description = [{
     This operation performs an atomic capture.
 

mlir/include/mlir/Dialect/Tensor/IR/TensorOps.td

def Tensor_GenerateOp : Tensor_Op<"generate",
 
   let builders = [
     // Build op and populate its body per callback function.
     OpBuilder<(ins "Type":$resultTy, "ValueRange":$dynamicExtents,
       "function_ref<void(OpBuilder &, Location, ValueRange)>")>,
   ];
 
   let hasCanonicalizer = 1;
-  let hasVerifier = 1;
+  let hasRegionVerifier = 1;
 }
 
 //===----------------------------------------------------------------------===//
 // InsertOp
 //===----------------------------------------------------------------------===//
 
 def Tensor_InsertOp : Tensor_Op<"insert",
     [NoSideEffect,

mlir/include/mlir/IR/OpBase.td

 def AutomaticAllocationScope :
   NativeOpTrait<"AutomaticAllocationScope">;
 // Op supports operand broadcast behavior.
 def ResultsBroadcastableShape :
   NativeOpTrait<"ResultsBroadcastableShape">;
 // X op Y == Y op X
 def Commutative  : NativeOpTrait<"IsCommutative">;
 // op op X == op X (unary) / X op X == X (binary)
-def Idempotent  : NativeOpTrait<"IsIdempotent">;
+// FIXME: Idempotent should depend on SameOperandsAndResultType
+def Idempotent : NativeOpTrait<"IsIdempotent">;
 // op op X == X
-def Involution  : NativeOpTrait<"IsInvolution">;
+// FIXME: Involution should depend on SameOperandsAndResultType
+def Involution : NativeOpTrait<"IsInvolution">;
 // Op behaves like a constant.
 def ConstantLike : NativeOpTrait<"ConstantLike">;
 // Op is isolated from above.
 def IsolatedFromAbove : NativeOpTrait<"IsIsolatedFromAbove">;
 // Op results are float or vectors/tensors thereof.
 def ResultsAreFloatLike : NativeOpTrait<"ResultsAreFloatLike">;
 // Op has the same operand type.
 def SameTypeOperands : NativeOpTrait<"SameTypeOperands">;

 // Op is a terminator.
 def Terminator : NativeOpTrait<"IsTerminator">;
 // Op can be safely normalized in the presence of MemRefs with
 // non-identity maps.
 def MemRefsNormalizable : NativeOpTrait<"MemRefsNormalizable">;
 // Op is elementwise on tensor/vector operands and results.
 def Elementwise : NativeOpTrait<"Elementwise">;
 // Elementwise op can be applied to scalars instead tensor/vector operands.
-def Scalarizable : NativeOpTrait<"Scalarizable">;
+def Scalarizable : NativeOpTrait<"Scalarizable", [Elementwise]>;
 // Elementwise op can be applied to all-vector operands.
-def Vectorizable : NativeOpTrait<"Vectorizable">;
+def Vectorizable : NativeOpTrait<"Vectorizable", [Elementwise]>;
 // Elementwise op can be applied to all-tensor operands.
-def Tensorizable : NativeOpTrait<"Tensorizable">;
+def Tensorizable : NativeOpTrait<"Tensorizable", [Elementwise]>;
 
 // Group together `Elementwise`, `Scalarizable`, `Vectorizable`, and
 // `Tensorizable` for convenience.
 def ElementwiseMappable : TraitList<[
     Elementwise,
     Scalarizable,
     Vectorizable,
     Tensorizable,

mlir/include/mlir/IR/OpDefinition.h

static Operation *buildTerminator(OpBuilder &builder, Location loc) {
       TerminatorOpType::build(builder, state);
       return Operation::create(state);
     }
 
   public:
     /// The type of the operation used as the implicit terminator type.
     using ImplicitTerminatorOpT = TerminatorOpType;
 
-    static LogicalResult verifyTrait(Operation *op) {
+    static LogicalResult verifyRegionTrait(Operation *op) {
       if (failed(Base::verifyTrait(op)))
         return failure();
       for (unsigned i = 0, e = op->getNumRegions(); i < e; ++i) {
         Region &region = op->getRegion(i);
         // Empty regions are fine.
         if (region.empty())
           continue;
         Operation &terminator = region.front().back();

 };
 
 /// This class provides the API for ops that are known to be isolated from
 /// above.
 template <typename ConcreteType>
 class IsIsolatedFromAbove
     : public TraitBase<ConcreteType, IsIsolatedFromAbove> {
 public:
-  static LogicalResult verifyTrait(Operation *op) {
+  static LogicalResult verifyRegionTrait(Operation *op) {
     return impl::verifyIsIsolatedFromAbove(op);
   }
 };
 
 /// A trait of region holding operations that defines a new scope for polyhedral
 /// optimization purposes. Any SSA values of 'index' type that either dominate
 /// such an operation or are used at the top-level of such an operation
 /// automatically become valid symbols for the polyhedral scope defined by that

 /// This class provides a verifier for ops that are expecting their parent
 /// to be one of the given parent ops
 template <typename... ParentOpTypes>
 struct HasParent {
   template <typename ConcreteType>
   class Impl : public TraitBase<ConcreteType, Impl> {
   public:
     static LogicalResult verifyTrait(Operation *op) {
-      if (llvm::isa<ParentOpTypes...>(op->getParentOp()))
+      if (llvm::isa_and_nonnull<ParentOpTypes...>(op->getParentOp()))
         return success();
 
       return op->emitOpError()
              << "expects parent op "
              << (sizeof...(ParentOpTypes) != 1 ? "to be one of '" : "'")
              << llvm::makeArrayRef({ParentOpTypes::getOperationName()...})
              << "'";
     }

mlir/include/mlir/IR/SymbolTable.h

 /// that are directly within the region, i.e not including those within child
 /// regions, that contain a 'SymbolTable::getSymbolAttrName()' StringAttr will
 /// be verified to ensure that the names are uniqued. These operations must also
 /// adhere to the constraints defined by the `Symbol` trait, even if they do not
 /// inherit from it.
 template <typename ConcreteType>
 class SymbolTable : public TraitBase<ConcreteType, SymbolTable> {
 public:
-  static LogicalResult verifyTrait(Operation *op) {
+  static LogicalResult verifyRegionTrait(Operation *op) {
     return ::mlir::detail::verifySymbolTable(op);
   }
 
   /// Look up a symbol with the specified name, returning null if no such
   /// name exists. Symbol names never include the @ on them. Note: This
   /// performs a linear scan of held symbols.
   Operation *lookupSymbol(StringAttr name) {
     return mlir::SymbolTable::lookupSymbolIn(this->getOperation(), name);

mlir/include/mlir/Interfaces/InferTypeOpInterface.td

StaticInterfaceMethod<
       /*defaultImplementation=*/[{
         /// Returns whether two arrays are equal as strongest check for
         /// compatibility by default.
         return lhs == rhs;
       }]
     >,
   ];
 
+  // Inferring result types may need to access the region operations.
+  let verifyWithRegions=1;
   let verify = [{
     return detail::verifyInferredResultTypes($_op);
   }];
 }
 
 def InferShapedTypeOpInterface : OpInterface<"InferShapedTypeOpInterface"> {
   let description = [{
     Interface to infer the components of a ShapedType returned by an operation

mlir/lib/Dialect/LLVMIR/IR/LLVMDialect.cpp

if (auto splatValue = value.dyn_cast<SplatElementsAttr>())
     return isZeroAttribute(splatValue.getSplatValue<Attribute>());
   if (auto elementsValue = value.dyn_cast<ElementsAttr>())
     return llvm::all_of(elementsValue.getValues<Attribute>(), isZeroAttribute);
   if (auto arrayValue = value.dyn_cast<ArrayAttr>())
     return llvm::all_of(arrayValue.getValue(), isZeroAttribute);
   return false;
 }
 
-LogicalResult GlobalOp::verify() {
+LogicalResult GlobalOp::verifyRegions() {
   if (!LLVMPointerType::isValidElementType(getType()))
     return emitOpError(
         "expects type to be a valid element type for an LLVM pointer");
   if ((*this)->getParentOp() && !satisfiesLLVMModule((*this)->getParentOp()))
     return emitOpError("must appear at the module level");
 
   if (auto strAttr = getValueOrNull().dyn_cast_or_null<StringAttr>()) {
     auto type = getType().dyn_cast<LLVMArrayType>();
LogicalResult LLVMFuncOp::verify() {
   }
 
   if (isVarArg())
     return emitOpError("only external functions can be variadic");
 
   unsigned numArguments = getType().getNumParams();
   Block &entryBlock = front();
   for (unsigned i = 0; i < numArguments; ++i) {
     Type argType = entryBlock.getArgument(i).getType();
     if (!isCompatibleType(argType))
       return emitOpError("entry block argument #")
              << i << " is not of LLVM type";
     if (getType().getParamType(i) != argType)
       return emitOpError("the type of entry block argument #")
              << i << " does not match the function signature";
   }
 

mlir/lib/Dialect/OpenMP/IR/OpenMPDialect.cpp

if (auto mo = memory_order())
     p << "memory_order(" << stringifyClauseMemoryOrderKind(*mo) << ") ";
   if (hintAttr())
     printSynchronizationHint(p, *this, hintAttr());
   p << x() << " : " << x().getType();
   p.printRegion(region());
 }
 
 /// Verifier for AtomicUpdateOp
-LogicalResult AtomicUpdateOp::verify() {
+LogicalResult AtomicUpdateOp::verifyRegions() {
   if (auto mo = memory_order()) {
     if (*mo == ClauseMemoryOrderKind::acq_rel ||
         *mo == ClauseMemoryOrderKind::acquire) {
       return emitError(
           "memory-order must not be acq_rel or acquire for atomic updates");
     }
   }
 

mlir/lib/Dialect/Tensor/IR/TensorOps.cpp

if (auto splatDest = dest.dyn_cast<SplatElementsAttr>())
         return dest;
   return {};
 }
 
 //===----------------------------------------------------------------------===//
 // GenerateOp
 //===----------------------------------------------------------------------===//
 
-LogicalResult GenerateOp::verify() {
+LogicalResult GenerateOp::verifyRegions() {
   // Ensure that the tensor type has as many dynamic dimensions as are specified
   // by the operands.
   RankedTensorType resultTy = getType().cast<RankedTensorType>();
   if (getNumOperands() != resultTy.getNumDynamicDims())
     return emitError("must have as many index operands as dynamic extents "
                      "in the result type");
 
   // Ensure that region arguments span the index space.

mlir/lib/IR/Operation.cpp

LogicalResult OpTrait::impl::verifyIsIsolatedFromAbove(Operation *isolatedOp) {
   SmallVector<Region *, 8> pendingRegions;
   for (auto &region : isolatedOp->getRegions()) {
     pendingRegions.push_back(&region);
 
     // Traverse all operations in the region.
     while (!pendingRegions.empty()) {
       for (Operation &op : pendingRegions.pop_back_val()->getOps()) {
         for (Value operand : op.getOperands()) {
-          // operand should be non-null here if the IR is well-formed. But
-          // we don't assert here as this function is called from the verifier
-          // and so could be called on invalid IR.
-          if (!operand)
-            return op.emitOpError("operation's operand is null");
+          // operand should be non-null here. If this is called from the op
+          // verifier, then the region opreations are verified. If it's not from
+          // op verifier, then the caller should ensure all the region
+          // operations are well-formed.
+          assert(operand);
 
           // Check that any value that is used by an operation is defined in the
           // same region as either an operation result.
           auto *operandRegion = operand.getParentRegion();
           if (!region.isAncestor(operandRegion)) {
             return op.emitOpError("using value defined outside the region")
                        .attachNote(isolatedOp->getLoc())
                    << "required by region isolation constraints";

mlir/test/Dialect/LLVMIR/global.mlir

 
 llvm.func @bar() {
   // expected-error @+1 {{the type must be a pointer to the type of the referenced function}}
   llvm.mlir.addressof @foo : !llvm.ptr<i8>
 }
 
 // -----
 
-// expected-error @+2 {{'llvm.mlir.global' op expects regions to end with 'llvm.return', found 'llvm.mlir.constant'}}
-// expected-note @+1 {{in custom textual format, the absence of terminator implies 'llvm.return'}}
+// expected-error @+2 {{block with no terminator, has %0 = llvm.mlir.constant(42 : i64) : i64}}
 llvm.mlir.global internal @g() : i64 {
   %c = llvm.mlir.constant(42 : i64) : i64
 }
 
 // -----
 
 // expected-error @+1 {{'llvm.mlir.global' op initializer region type 'i64' does not match global type 'i32'}}
 llvm.mlir.global internal @g() : i32 {

mlir/test/Dialect/Linalg/invalid.mlir

iterator_types = ["reduction"]}
       outs(%arg1 : tensor<?xf32>) {
     ^bb(%i: f32, %j: f32):
       linalg.yield %i: f32
   } -> tensor<?xf32>
 }
 
 // -----
 
-func @generic(%arg0: memref<?x?xi4>) {
-  // expected-error @+2 {{op expects regions to end with 'linalg.yield', found 'arith.addf'}}
-  // expected-note @+1 {{in custom textual format, the absence of terminator implies 'linalg.yield'}}
+func @generic(%arg0: memref<?x?xf32>) {
+  // expected-error @+6 {{block with no terminator, has %0 = arith.addf %arg1, %arg1 : f32}}
   linalg.generic  {
     indexing_maps = [ affine_map<(i, j) -> (i, j)> ],
     iterator_types = ["parallel", "parallel"]}
-      outs(%arg0 : memref<?x?xi4>) {
-    ^bb(%0: i4) :
-      %1 = arith.addf %0, %0: i4
+      outs(%arg0 : memref<?x?xf32>) {
+    ^bb(%0: f32) :
+      %1 = arith.addf %0, %0: f32
   }
   return
 }
 
 // -----
 
 // This test is currently disabled: subject to verifier ordering issues.
 // Instead, when the ranks are not greater than 2, an assertion will be triggered

mlir/test/Dialect/Tensor/invalid.mlir

func @tensor.generate(%m : index, %n : index)
   } : tensor<?x3x?xf32>
   return %tnsr : tensor<?x3x?xf32>
 }
 
 // -----
 
 func @tensor.generate(%m : index, %n : index)
     -> tensor<?x3x?xf32> {
-  // expected-error @+2 {{op expects regions to end with 'tensor.yield', found 'std.return'}}
-  // expected-note @+1 {{in custom textual format, the absence of terminator implies 'tensor.yield'}}
+  // expected-error @+4 {{'std.return' op expects parent op 'builtin.func'}}
   %tnsr = tensor.generate %m, %n {
     ^bb0(%i : index, %j : index, %k : index):
       %elem = arith.constant 8.0 : f32
       return %elem : f32
   } : tensor<?x3x?xf32>
   return %tnsr : tensor<?x3x?xf32>
 }
 

 }
 
 // -----
 
 func @invalid_splat(%v : vector<8xf32>) {
   // expected-error@+1 {{must be integer/index/float type}}
   %w = tensor.splat %v : tensor<8xvector<8xf32>>
   return
-}
+}
 

mlir/test/IR/invalid.mlir

func @return_type_mismatch() -> i32 {
   %0 = "foo"() : ()->f32
   return %0 : f32  // expected-error {{type of return operand 0 ('f32') doesn't match function result type ('i32') in function @return_type_mismatch}}
 }
 
 // -----
 
 func @return_inside_loop() {
   affine.for %i = 1 to 100 {
-    // expected-error@-1 {{op expects regions to end with 'affine.yield', found 'std.return'}}
-    // expected-note@-2 {{in custom textual format, the absence of terminator implies}}
+    // expected-error@+1 {{op expects parent op 'builtin.func'}}
     return
   }
   return
 }
 
 // -----
 
 // expected-error@+1 {{expected three consecutive dots for an ellipsis}}