[MLIR][Standard] Add `assert` operation to the standard dialect

[herhut]

Can you post on discourse that you are looking to add this to std?

mlir/include/mlir/Dialect/StandardOps/IR/Ops.td

452

I would make printing the message a requirement. Instead, how about

Optionally, a runtime might use the provided message to print an error.

[frgossen]

Update doc

[frgossen]

For discussion, see https://llvm.discourse.group/t/standard-add-std-assert-operation/1353

[herhut]

Looks good to me. Maybe wait for reactions on discourse.

[stellaraccident]

Thanks for posting on discourse.

Makes sense to me. We can lower this to our vm.cond_fail pseudo-op (https://github.com/google/iree/blob/bf894c869e281985f392775c0cc0bb199201b477/iree/compiler/Dialect/VM/IR/VMOps.td#L1875), which forget lowers to a cond_br with a vm.fail terminator in the target block.

[bondhugula]

mlir/include/mlir/Dialect/StandardOps/IR/Ops.td

451

I think the semantics would need to be spelt out. Is execution guaranteed to abort on failure? The next line only talks about the error message printing being optional.

[bondhugula]

mlir/test/Dialect/Standard/ops.mlir

22

This is inconsistent with the doc description which says the error message is optional.

[frgossen]

Update doc

[frgossen]

mlir/test/Dialect/Standard/ops.mlir

22

The error message is required. What the runtime does with it is up to the user though.

[bondhugula]

mlir/include/mlir/Dialect/StandardOps/IR/Ops.td

451

Nit: Boolean -> boolean

453

Nit: You can use the whole line - here and above.

[rriddle]

mlir/include/mlir/Dialect/StandardOps/IR/Ops.td

467

nit: You don't need to specify this if it is empty.

[herhut]

Thanks

[silvas]

mlir/include/mlir/Dialect/StandardOps/IR/Ops.td

457

There is no "assert" function. (it's a macro; see my post on discourse). I think we should just remove this line from the description.

[frgossen]

Update documentation

mlir/include/mlir/Dialect/StandardOps/IR/Ops.td

453

I always found line breaks after sentences more semantic, they lead to more readable diffs, and prevent line fragmentation when the text is changed.
Should I change this anyways?

[jpienaar]

mlir/include/mlir/Dialect/StandardOps/IR/Ops.td

453

Yes please. Keeping consistency with the rest of the file and project comment style is important.

We have been following "regular" writing practices wrt lines vs sentences vs paragraph as one is optimising for the reader and not for changes/diffing (where tools do a good job with highlighting already and changing isn't the common case). Inconsistencies/deviations make readers wonder about the significance and impairs reading. Of course if there is a discussion where we adopt a new documentation convention, then this may change.

[frgossen]

mlir/include/mlir/Dialect/StandardOps/IR/Ops.td

453

Will keep this in mind and corrected the documentation in a separate CL.
See https://reviews.llvm.org/D83769

mlir/include/mlir/Dialect/StandardOps/IR/Ops.td

let description = [{
     The `alloca` operation allocates memory on the stack, to be automatically
     released when control transfers back from the region of its closest
     surrounding operation with an
     [`AutomaticAllocationScope`](../Traits.md#automaticallocationscope) trait.
     The amount of memory allocated is specified by its memref and additional
     operands. For example:
 
     ```mlir
-    %0 = alloca() : memref<8x64xf32>
+    %0 = alloca() : memref<8x64xf32>
     ```
 
     The optional list of dimension operands are bound to the dynamic dimensions
     specified in its memref type. In the example below, the SSA value '%d' is
     bound to the second dimension of the memref (which is dynamic).
 
     ```mlir
-    %0 = alloca(%d) : memref<8x?xf32>
+    %0 = alloca(%d) : memref<8x?xf32>
     ```
 
     The optional list of symbol operands are bound to the symbols of the
     memref's affine map. In the example below, the SSA value '%s' is bound to
     the symbol 's0' in the affine map specified in the allocs memref type.
 
     ```mlir
-    %0 = alloca()[%s] : memref<8x64xf32,
+    %0 = alloca()[%s] : memref<8x64xf32,
                                affine_map<(d0, d1)[s0] -> ((d0 + s0), d1)>>
     ```
 
     This operation returns a single SSA value of memref type, which can be used
     by subsequent load and store operations. An optional alignment attribute, if
     specified, guarantees alignment at least to that boundary. If not specified,
     an alignment on any convenient boundary compatible with the type will be
     chosen.
let description = [{
     // Tensor element-wise bitwise integer and.
     %x = and %y, %z : tensor<4x?xi8>
     ```
   }];
   let hasFolder = 1;
 }
 
 //===----------------------------------------------------------------------===//
+// AssertOp
+//===----------------------------------------------------------------------===//
+
+def AssertOp : Std_Op<"assert"> {
+  let summary = "Assert operation with message attribute";
+  let description = [{
+    Assert operation with single boolean operand and an error message attribute.
+    If the argument is `true` this operation has no effect.
+    Otherwise, the program execution will abort.
+    The provided error message may be used by a runtime to propagate the error
+    to the user.
+
+    Example:
+
+    ```mlir
+    assert %b, "Expected ... to be true"
+    ```
+  }];
+
+  let arguments = (ins I1:$arg, StrAttr:$msg);
+
+  let assemblyFormat = "$arg `,` $msg attr-dict";
+
+  // AssertOp is fully verified by its traits.
+  let verifier = ?;
+}
+
+//===----------------------------------------------------------------------===//
 // AssumeAlignmentOp
 //===----------------------------------------------------------------------===//
 
 def AssumeAlignmentOp : Std_Op<"assume_alignment"> {
   let summary =
       "assertion that gives alignment information to the input memref";
   let description = [{
     The `assume_alignment` operation takes a memref and an integer of alignment

mlir/test/Dialect/Standard/ops.mlir

 }
 
 // CHECK-LABEL: test_index_cast_tensor_reverse
 func @test_index_cast_tensor_reverse(%arg0 : tensor<i64>) -> tensor<index> {
   %0 = index_cast %arg0 : tensor<i64> to tensor<index>
   return %0 : tensor<index>
 }
 
+func @assert(%arg : i1) {
+  assert %arg, "Some message in case this assertion fails."
+  return
+}