[Mlir-commits] [mlir] [mlir][arith] Add ValueBoundsOpInterface external models for the arith integer CeilDiv, RemSI, RemUI, MaxUI, MinUI. (PR #204966)

[Max Graey]

================
@@ -190,6 +268,58 @@ struct MaxSIOpInterface
     cstr.bound(value) >= rhs;
   }
 };
+
+struct MinUIOpInterface
+    : public ValueBoundsOpInterface::ExternalModel<MinUIOpInterface,
+                                                   arith::MinUIOp> {
+  void populateBoundsForIndexValue(Operation *op, Value value,
+                                   ValueBoundsConstraintSet &cstr) const {
+    auto minOp = cast<arith::MinUIOp>(op);
+    assert(value == minOp.getResult() && "invalid value");
+
+    // ValueBoundsConstraintSet models values as signed integers (e.g. an i8
+    // 0xff is treated as -1, not 255). For an unsigned minimum it is enough
+    // that a single operand is provably non-negative: minui(x, y) is in
+    // [0, y] whenever y >= 0 (and symmetrically for x).
+    bool lhsNonNegative =
+        ValueBoundsConstraintSet::isProvablyNonNegative(minOp.getLhs(), cstr);
+    bool rhsNonNegative =
+        ValueBoundsConstraintSet::isProvablyNonNegative(minOp.getRhs(), cstr);
+    if (!lhsNonNegative && !rhsNonNegative)
+      return;
+
+    cstr.bound(value) >= 0;
+    if (lhsNonNegative) {
+      AffineExpr lhs = cstr.getExpr(minOp.getLhs());
+      cstr.bound(value) <= lhs;
+    }
+    if (rhsNonNegative) {
+      AffineExpr rhs = cstr.getExpr(minOp.getRhs());
+      cstr.bound(value) <= rhs;
+    }
+  }
+};
+
+struct MaxUIOpInterface
+    : public ValueBoundsOpInterface::ExternalModel<MaxUIOpInterface,
+                                                   arith::MaxUIOp> {
+  void populateBoundsForIndexValue(Operation *op, Value value,
+                                   ValueBoundsConstraintSet &cstr) const {
+    auto maxOp = cast<arith::MaxUIOp>(op);
+    assert(value == maxOp.getResult() && "invalid value");
+
+    // See MinUIOpInterface comment
+    if (!ValueBoundsConstraintSet::isProvablyNonNegative(maxOp.getLhs(),
+                                                         cstr) ||
+        !ValueBoundsConstraintSet::isProvablyNonNegative(maxOp.getRhs(), cstr))
+      return;
+
+    AffineExpr lhs = cstr.getExpr(maxOp.getLhs());
+    AffineExpr rhs = cstr.getExpr(maxOp.getRhs());
+    cstr.bound(value) >= lhs;
+    cstr.bound(value) >= rhs;
+  }
----------------
MaxGraey wrote:

This is correct but too conservative. We can split checks to several scenarios which depend on sign and zero rhs/lhs relations:

| Signed facts | Value bounds |
|-- | --|
lhs >= 0 && rhs >= 0 | cstr.bound(value) >= lhs, cstr.bound(value) >= rhs
lhs < 0 && rhs < 0| cstr.bound(value) >= lhs, cstr.bound(value) >= rhs
lhs < 0 && rhs >= 0  | cstr.bound(value) == lhs
lhs >= 0 && rhs < 0 | cstr.bound(value) == rhs

</body></html>

https://github.com/llvm/llvm-project/pull/204966