[mlir] Mark witness related Shape dialect ops as NoSideEffect.

[herhut]

mlir/include/mlir/Dialect/Shape/IR/ShapeOps.td

446

Marking these as NoSideEffect is dangerous. If their witness value goes unused, they will just disappear as the are considered dead at that point. That is likely not what we want.

465

Same here.

[tpopp]

mlir/include/mlir/Dialect/Shape/IR/ShapeOps.td

446

I'm removing these, but just for completeness for anyone reading this want to say that I think these being removed once unused is a good thing because I don't think these should be used as pure assertions and only to prevent incorrect code from being executed, so once the code is known to be correct, this form of assertion should be removed even if it might fire.

The problem with NoSideEffect in my opinion is the fact that they could then be hoisted out of some If-block and then turned into an assertion that would never have executed in the original location.

[herhut]

mlir/include/mlir/Dialect/Shape/IR/ShapeOps.td

446

I think this is another use case for the NoSpeculation trait. Or rather, we should have an AllowsSpeculation trait to attach to operations that can be hoisted across control flow.

mlir/include/mlir/Dialect/Shape/IR/ShapeOps.td

 }
 
 //===----------------------------------------------------------------------===//
 // Shape constraint related ops.
 //===----------------------------------------------------------------------===//
 
 //TODO(tpopp): Move the code below and witnesses to a different file.
 def Shape_AnyOp : Shape_Op<"any",
-    [DeclareOpInterfaceMethods<InferTypeOpInterface>]> {
+    [NoSideEffect, DeclareOpInterfaceMethods<InferTypeOpInterface>]> {
   let summary = "Return any combination of the input shapes.";
   let description = [{
     This operation takes multiple input shapes and returns some combination of
     their dimensions. This can be best seen with examples below.
 
     The result is undefined, but still side-effect free, in cases where the
     inputs have differing ranks or differ in extents of shared dimensions.
 
     Example:
     ```mlir
       %s0 = shape.any([2,?], [?,3]) // [2,3]
       %s1 = shape.any([?,?], [1,2]) // [1,2]
     ```
   }];
 
   let arguments = (ins Variadic<Shape_ShapeType>:$inputs);
   let results = (outs Shape_ShapeType:$result);
 }
 
-def Shape_AssumingAllOp : Shape_Op<"assuming_all", []> {
+def Shape_AssumingAllOp : Shape_Op<"assuming_all", [NoSideEffect]> {
   let summary = "Return a logical AND of all witnesses.";
   let description = [{
     Used to simplify constraints as any single failing precondition is enough
     to prevent execution.
 
     "assuming" operations represent an execution order restriction to the
     compiler, information for dependent code to rely on (by assuming), and
     nothing else. They should not exist after a program is fully lowered and
let description = [{
     region. The operation takes variable number of operands and produces no
     results. The operand number and types must match the return signature of
     the region that contains the operation.
   }];
 
   let arguments = (ins Variadic<AnyType>:$operands);
 }
 
 def Shape_CstrBroadcastableOp : Shape_Op<"cstr_broadcastable", []> {
   let summary = "Determines if 2 shapes can be successfully broadcasted.";
   let description = [{
     Given 2 input shapes, return a witness specifying if they are broadcastable.
     This broadcastable follows the same logic as what shape.broadcast documents.
 
     "cstr" operations represent runtime assertions.
 
     Example:
     ```mlir
       %w0 = shape.cstr_broadcastable([2,2], [3,1,2])  // Success
       %w1 = shape.cstr_broadcastable([2,2], [3,2])    // Failure
     ```
   }];
 
   let arguments = (ins Shape_ShapeType:$lhs, Shape_ShapeType:$rhs);
   let results = (outs Shape_WitnessType:$result);
 }
 
 def Shape_CstrEqOp : Shape_Op<"cstr_eq", []> {
   let summary = "Determines if all input shapes are equal.";
   let description = [{
     Given 1 or more input shapes, determine if all shapes are the exact same.
 
     "cstr" operations represent runtime assertions.
 
     Example:
     ```mlir