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

[Matthias Springer]

================
@@ -89,6 +90,73 @@ struct FloorDivSIOpInterface
   }
 };
 
+struct CeilDivSIOpInterface
+    : public ValueBoundsOpInterface::ExternalModel<CeilDivSIOpInterface,
+                                                   CeilDivSIOp> {
+  void populateBoundsForIndexValue(Operation *op, Value value,
+                                   ValueBoundsConstraintSet &cstr) const {
+    auto divSIOp = cast<CeilDivSIOp>(op);
+    assert(value == divSIOp.getResult() && "invalid value");
+
+    AffineExpr lhs = cstr.getExpr(divSIOp.getLhs());
+    AffineExpr rhs = cstr.getExpr(divSIOp.getRhs());
+    cstr.bound(value) == lhs.ceilDiv(rhs);
+  }
+};
+
+struct RemSIOpInterface
+    : public ValueBoundsOpInterface::ExternalModel<RemSIOpInterface, RemSIOp> {
+  void populateBoundsForIndexValue(Operation *op, Value value,
+                                   ValueBoundsConstraintSet &cstr) const {
+    auto remSIOp = cast<RemSIOp>(op);
+    assert(value == remSIOp.getResult() && "invalid value");
+
+    Value lhsValue = remSIOp.getLhs();
+    Value rhsValue = remSIOp.getRhs();
+    AffineExpr rhs = cstr.getExpr(rhsValue);
+    bool rhsPositive = ValueBoundsConstraintSet::isProvablyPositive(rhsValue, cstr);
+    bool rhsNegative = ValueBoundsConstraintSet::isProvablyNegative(rhsValue, cstr);
+
+    // The result of remsi has the same sign as the dividend (lhs). The sign
+    // of lhs does not need to be a compile-time constant: it is sufficient if
+    // the constraint set can prove it. For lhs == 0 both branches may fire,
+    // which is consistent since the result is then 0.
+    if (ValueBoundsConstraintSet::isProvablyNonPositive(lhsValue, cstr)) {
----------------
matthias-springer wrote:

I think these cases are correct, but a concrete example as a comment would help.

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