Skip to content

[mlir][arith] Add ValueBoundsOpInterface external models for the arith integer CeilDiv, RemSI, RemUI, MaxUI, MinUI.#204966

Open
nirhersh wants to merge 6 commits into
llvm:mainfrom
nirhersh:add-more-arith-ops
Open

[mlir][arith] Add ValueBoundsOpInterface external models for the arith integer CeilDiv, RemSI, RemUI, MaxUI, MinUI.#204966
nirhersh wants to merge 6 commits into
llvm:mainfrom
nirhersh:add-more-arith-ops

Conversation

@nirhersh

@nirhersh nirhersh commented Jun 21, 2026

Copy link
Copy Markdown
Contributor

Add ValueBoundsOpInterface external models for the arith integer
CeilDiv, RemSI, RemUI, MaxUI, MinUI.

Since the ValueBoundsConstraintSet infrastructure interprets unsigned integers as signed, unsigned ops needed special handling.
In the unsigned ops we first verify that the integers can be proven as positive, and if yes we add the appropriate constraints to the set.

The only exception for that is the RemUI, since the bound is only dependent on the divider we don't care what's the sign of the lhs.

@llvmorg-github-actions

Copy link
Copy Markdown

@llvm/pr-subscribers-mlir

Author: nirhersh

Changes

Add ValueBoundsOpInterface external models for the arith integer
CielDiv, RemSI, RemUI, MaxUI, MinUI.

Since the ValueBoundsConstraintSet infrastructure interprets unsigned integers as signed, unsigned ops needed special handling.
In the unsigned ops we first verify that the integers can be proven as positive, and if yes we add the appropriate constraints to the set.

The only exception for that is the RemUI, since the bound is only dependent on the divider we don't care what's the sign of the lhs.


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

3 Files Affected:

  • (modified) mlir/lib/Dialect/Arith/IR/ArithDialect.cpp (+2-1)
  • (modified) mlir/lib/Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp (+143)
  • (modified) mlir/test/Dialect/Arith/value-bounds-op-interface-impl.mlir (+295)
diff --git a/mlir/lib/Dialect/Arith/IR/ArithDialect.cpp b/mlir/lib/Dialect/Arith/IR/ArithDialect.cpp
index ec611ca7924be..3799db1cb3cbe 100644
--- a/mlir/lib/Dialect/Arith/IR/ArithDialect.cpp
+++ b/mlir/lib/Dialect/Arith/IR/ArithDialect.cpp
@@ -56,7 +56,8 @@ void arith::ArithDialect::initialize() {
   declarePromisedInterfaces<bufferization::BufferizableOpInterface, ConstantOp,
                             IndexCastOp, SelectOp>();
   declarePromisedInterfaces<ValueBoundsOpInterface, AddIOp, ConstantOp, SubIOp,
-                            MulIOp, SelectOp, FloorDivSIOp, MinSIOp, MaxSIOp>();
+                            MulIOp, SelectOp, FloorDivSIOp, CeilDivSIOp, MinSIOp,
+                            MaxSIOp, MinUIOp, MaxUIOp, RemSIOp, RemUIOp>();
 }
 
 /// Materialize an integer or floating point constant.
diff --git a/mlir/lib/Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp b/mlir/lib/Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp
index 3440c60f169d3..7c53451f35d6a 100644
--- a/mlir/lib/Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp
+++ b/mlir/lib/Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp
@@ -17,6 +17,32 @@ namespace mlir {
 namespace arith {
 namespace {
 
+static bool isProvablyNonNegative(Value value,
+                                  ValueBoundsConstraintSet &cstr) {
+  return cstr.populateAndCompare(
+      /*lhs=*/{value}, ValueBoundsConstraintSet::ComparisonOperator::GE,
+      /*rhs=*/{OpFoldResult(Builder(value.getContext()).getIndexAttr(0))});
+}
+
+static bool isProvablyNonPositive(Value value,
+                                  ValueBoundsConstraintSet &cstr) {
+ return cstr.populateAndCompare(
+      /*lhs=*/{value}, ValueBoundsConstraintSet::ComparisonOperator::LE,
+      /*rhs=*/{OpFoldResult(Builder(value.getContext()).getIndexAttr(0))});
+}
+
+static bool isProvablyPositive(Value value, ValueBoundsConstraintSet &cstr) {
+  return cstr.populateAndCompare(
+      /*lhs=*/{value}, ValueBoundsConstraintSet::ComparisonOperator::GT,
+      /*rhs=*/{OpFoldResult(Builder(value.getContext()).getIndexAttr(0))});
+}
+
+static bool isProvablyNegative(Value value, ValueBoundsConstraintSet &cstr) {
+  return cstr.populateAndCompare(
+      /*lhs=*/{value}, ValueBoundsConstraintSet::ComparisonOperator::LT,
+      /*rhs=*/{OpFoldResult(Builder(value.getContext()).getIndexAttr(0))});
+}
+
 struct AddIOpInterface
     : public ValueBoundsOpInterface::ExternalModel<AddIOpInterface, AddIOp> {
   void populateBoundsForIndexValue(Operation *op, Value value,
@@ -89,6 +115,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 = isProvablyPositive(rhsValue, cstr);
+    bool rhsNegative = 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 (isProvablyNonPositive(lhsValue, cstr)) {
+      cstr.bound(value) <= 0;
+      if (rhsPositive)
+        cstr.bound(value) >= 1 - rhs;
+      if (rhsNegative)
+        cstr.bound(value) >= rhs + 1;
+    }
+    if (isProvablyNonNegative(lhsValue, cstr)) {
+      cstr.bound(value) >= 0;
+      if (rhsPositive)
+        cstr.bound(value) <= rhs - 1;
+      if (rhsNegative)
+        cstr.bound(value) <= -rhs - 1;
+    }
+  }
+};
+
+struct RemUIOpInterface
+    : public ValueBoundsOpInterface::ExternalModel<RemUIOpInterface, RemUIOp> {
+  void populateBoundsForIndexValue(Operation *op, Value value,
+                                   ValueBoundsConstraintSet &cstr) const {
+    auto remUIOp = cast<RemUIOp>(op);
+    assert(value == remUIOp.getResult() && "invalid value");
+
+    Value rhsValue = remUIOp.getRhs();
+    AffineExpr rhs = cstr.getExpr(rhsValue);
+
+    // remui computes an unsigned remainder, so for a provably positive divisor
+    // the result is always in [0, rhs - 1]
+    if (isProvablyPositive(rhsValue, cstr)) {
+      cstr.bound(value) >= 0;
+      cstr.bound(value) <= rhs - 1;
+    }
+  }
+};
+
 struct SelectOpInterface
     : public ValueBoundsOpInterface::ExternalModel<SelectOpInterface,
                                                    SelectOp> {
@@ -190,6 +283,51 @@ 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 = isProvablyNonNegative(minOp.getLhs(), cstr);
+    bool rhsNonNegative = isProvablyNonNegative(minOp.getRhs(), cstr);
+    if (!lhsNonNegative && !rhsNonNegative)
+      return;
+
+    cstr.bound(value) >= 0;
+    if (lhsNonNegative)
+      cstr.bound(value) <= cstr.getExpr(minOp.getLhs());
+    if (rhsNonNegative)
+      cstr.bound(value) <= cstr.getExpr(minOp.getRhs());
+  }
+};
+
+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 (!isProvablyNonNegative(maxOp.getLhs(), cstr) ||
+        !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;
+  }
+};
 } // namespace
 } // namespace arith
 } // namespace mlir
@@ -202,8 +340,13 @@ void mlir::arith::registerValueBoundsOpInterfaceExternalModels(
     arith::SubIOp::attachInterface<arith::SubIOpInterface>(*ctx);
     arith::MulIOp::attachInterface<arith::MulIOpInterface>(*ctx);
     arith::FloorDivSIOp::attachInterface<arith::FloorDivSIOpInterface>(*ctx);
+    arith::CeilDivSIOp::attachInterface<arith::CeilDivSIOpInterface>(*ctx);
+    arith::RemSIOp::attachInterface<arith::RemSIOpInterface>(*ctx);
+    arith::RemUIOp::attachInterface<arith::RemUIOpInterface>(*ctx);
     arith::SelectOp::attachInterface<arith::SelectOpInterface>(*ctx);
     arith::MinSIOp::attachInterface<arith::MinSIOpInterface>(*ctx);
     arith::MaxSIOp::attachInterface<arith::MaxSIOpInterface>(*ctx);
+    arith::MinUIOp::attachInterface<arith::MinUIOpInterface>(*ctx);
+    arith::MaxUIOp::attachInterface<arith::MaxUIOpInterface>(*ctx);
   });
 }
diff --git a/mlir/test/Dialect/Arith/value-bounds-op-interface-impl.mlir b/mlir/test/Dialect/Arith/value-bounds-op-interface-impl.mlir
index 3f55037f46f09..ba5a5f9d5acf7 100644
--- a/mlir/test/Dialect/Arith/value-bounds-op-interface-impl.mlir
+++ b/mlir/test/Dialect/Arith/value-bounds-op-interface-impl.mlir
@@ -112,6 +112,157 @@ func.func @arith_floordivsi_non_pure(%a: index, %b: index) -> index {
 
 // -----
 
+// CHECK: #[[$map:.*]] = affine_map<()[s0] -> ((s0 + 4) floordiv 5)>
+// CHECK-LABEL: func @arith_ceildivsi(
+//  CHECK-SAME:     %[[a:.*]]: index
+//       CHECK:   %[[apply:.*]] = affine.apply #[[$map]]()[%[[a]]]
+//       CHECK:   return %[[apply]]
+func.func @arith_ceildivsi(%a: index) -> index {
+  %0 = arith.constant 5 : index
+  %1 = arith.ceildivsi %a, %0 : index
+  %2 = "test.reify_bound"(%1) : (index) -> (index)
+  return %2 : index
+}
+
+// -----
+
+func.func @arith_ceildivsi_non_pure(%a: index, %b: index) -> index {
+  %0 = arith.ceildivsi %a, %b : index
+  // Semi-affine expressions (such as "symbol * symbol") are not supported.
+  // expected-error @below{{could not reify bound}}
+  %1 = "test.reify_bound"(%0) : (index) -> (index)
+  return %1 : index
+}
+
+// -----
+
+// CHECK-LABEL: func @arith_remsi_positive_positive()
+//       CHECK:   %[[c0:.*]] = arith.constant 0 : index
+//       CHECK:   %[[c5:.*]] = arith.constant 5 : index
+//       CHECK:   return %[[c0]], %[[c5]]
+func.func @arith_remsi_positive_positive() -> (index, index) {
+  %c7 = arith.constant 7 : index
+  %c5 = arith.constant 5 : index
+  %0 = arith.remsi %c7, %c5 : index
+  %1 = "test.reify_bound"(%0) {type = "LB"} : (index) -> (index)
+  %2 = "test.reify_bound"(%0) {type = "UB"} : (index) -> (index)
+  return %1, %2 : index, index
+}
+
+// -----
+
+// CHECK-LABEL: func @arith_remsi_negative_positive()
+//       CHECK:   %[[cm4:.*]] = arith.constant -4 : index
+//       CHECK:   %[[c1:.*]] = arith.constant 1 : index
+//       CHECK:   return %[[cm4]], %[[c1]]
+func.func @arith_remsi_negative_positive() -> (index, index) {
+  %cm7 = arith.constant -7 : index
+  %c5 = arith.constant 5 : index
+  %0 = arith.remsi %cm7, %c5 : index
+  %1 = "test.reify_bound"(%0) {type = "LB"} : (index) -> (index)
+  %2 = "test.reify_bound"(%0) {type = "UB"} : (index) -> (index)
+  return %1, %2 : index, index
+}
+
+// -----
+
+// CHECK-LABEL: func @arith_remsi_positive_negative()
+//       CHECK:   %[[c0:.*]] = arith.constant 0 : index
+//       CHECK:   %[[c5:.*]] = arith.constant 5 : index
+//       CHECK:   return %[[c0]], %[[c5]]
+func.func @arith_remsi_positive_negative() -> (index, index) {
+  %c7 = arith.constant 7 : index
+  %cm5 = arith.constant -5 : index
+  %0 = arith.remsi %c7, %cm5 : index
+  %1 = "test.reify_bound"(%0) {type = "LB"} : (index) -> (index)
+  %2 = "test.reify_bound"(%0) {type = "UB"} : (index) -> (index)
+  return %1, %2 : index, index
+}
+
+// -----
+
+// CHECK-LABEL: func @arith_remsi_negative_negative()
+//       CHECK:   %[[cm4:.*]] = arith.constant -4 : index
+//       CHECK:   %[[c1:.*]] = arith.constant 1 : index
+//       CHECK:   return %[[cm4]], %[[c1]]
+func.func @arith_remsi_negative_negative() -> (index, index) {
+  %cm7 = arith.constant -7 : index
+  %cm5 = arith.constant -5 : index
+  %0 = arith.remsi %cm7, %cm5 : index
+  %1 = "test.reify_bound"(%0) {type = "LB"} : (index) -> (index)
+  %2 = "test.reify_bound"(%0) {type = "UB"} : (index) -> (index)
+  return %1, %2 : index, index
+}
+
+// -----
+
+// CHECK-LABEL: func @arith_remsi_positive_lhs_symbolic_positive_rhs(
+//  CHECK-SAME:     %[[a:.*]]: index
+//       CHECK:   %[[lb:.*]] = arith.constant 0 : index
+//       CHECK:   return %[[lb]]
+func.func @arith_remsi_positive_lhs_symbolic_positive_rhs(%a: index) -> index {
+  %c1 = arith.constant 1 : index
+  %c7 = arith.constant 7 : index
+  %rhs = arith.maxsi %a, %c1 : index
+  %0 = arith.remsi %c7, %rhs : index
+  %1 = "test.reify_bound"(%0) {type = "LB", constant} : (index) -> (index)
+  return %1 : index
+}
+
+// -----
+
+// CHECK-LABEL: func @arith_remsi_negative_lhs_symbolic_positive_rhs(
+//  CHECK-SAME:     %[[a:.*]]: index
+//       CHECK:   %[[ub:.*]] = arith.constant 1 : index
+//       CHECK:   return %[[ub]]
+func.func @arith_remsi_negative_lhs_symbolic_positive_rhs(%a: index) -> index {
+  %c1 = arith.constant 1 : index
+  %cm7 = arith.constant -7 : index
+  %rhs = arith.maxsi %a, %c1 : index
+  %0 = arith.remsi %cm7, %rhs : index
+  %1 = "test.reify_bound"(%0) {type = "UB", constant} : (index) -> (index)
+  return %1 : index
+}
+
+// -----
+
+// CHECK-LABEL: func @arith_remui_constant()
+//       CHECK:   %[[c0:.*]] = arith.constant 0 : index
+//       CHECK:   %[[c5:.*]] = arith.constant 5 : index
+//       CHECK:   return %[[c0]], %[[c5]]
+func.func @arith_remui_constant() -> (index, index) {
+  %c7 = arith.constant 7 : index
+  %c5 = arith.constant 5 : index
+  %0 = arith.remui %c7, %c5 : index
+  %1 = "test.reify_bound"(%0) {type = "LB"} : (index) -> (index)
+  %2 = "test.reify_bound"(%0) {type = "UB"} : (index) -> (index)
+  return %1, %2 : index, index
+}
+
+// -----
+
+// CHECK-LABEL: func @arith_remui_symbolic_dividend(
+//  CHECK-SAME:     %[[a:.*]]: index
+//       CHECK:   %[[ub:.*]] = arith.constant 5 : index
+//       CHECK:   return %[[ub]]
+func.func @arith_remui_symbolic_dividend(%a: index) -> index {
+  %c5 = arith.constant 5 : index
+  %0 = arith.remui %a, %c5 : index
+  %1 = "test.reify_bound"(%0) {type = "UB", constant} : (index) -> (index)
+  return %1 : index
+}
+
+// -----
+
+func.func @arith_remui_unknown_divisor(%a: index, %b: index) -> index {
+  %0 = arith.remui %a, %b : index
+  // expected-error @below{{could not reify bound}}
+  %1 = "test.reify_bound"(%0) {type = "UB", constant} : (index) -> (index)
+  return %1 : index
+}
+
+// -----
+
 // CHECK-LABEL: func @arith_const()
 //       CHECK:   %[[c5:.*]] = arith.constant 5 : index
 //       CHECK:   %[[c5:.*]] = arith.constant 5 : index
@@ -217,3 +368,147 @@ func.func @arith_maxsi_ub(%a: index) -> index {
   %1 = "test.reify_bound"(%0) {type = "UB"} : (index) -> (index)
   return %1 : index
 }
+
+// -----
+
+// CHECK-LABEL: func @arith_minui(
+//       CHECK:   %[[ub:.*]] = arith.constant 5 : index
+//       CHECK:   return %[[ub]]
+func.func @arith_minui() -> index {
+  %c4 = arith.constant 4 : index
+  %c10 = arith.constant 10 : index
+  %0 = arith.minui %c10, %c4 : index
+  %1 = "test.reify_bound"(%0) {type = "UB"} : (index) -> (index)
+  return %1 : index
+}
+
+// -----
+
+// CHECK-LABEL: func @arith_minui_unknown_sign(
+//  CHECK-SAME:     %[[a:.*]]: index
+//       CHECK:   %[[ub:.*]] = arith.constant 5 : index
+//       CHECK:   return %[[ub]]
+func.func @arith_minui_unknown_sign(%a: index) -> index {
+  %c4 = arith.constant 4 : index
+  %0 = arith.minui %a, %c4 : index
+  %1 = "test.reify_bound"(%0) {type = "UB"} : (index) -> (index)
+  return %1 : index
+}
+
+// -----
+
+// CHECK-LABEL: func @arith_maxui(
+//       CHECK:   %[[lb:.*]] = arith.constant 10 : index
+//       CHECK:   return %[[lb]]
+func.func @arith_maxui() -> index {
+  %c4 = arith.constant 4 : index
+  %c10 = arith.constant 10 : index
+  %0 = arith.maxui %c10, %c4 : index
+  %1 = "test.reify_bound"(%0) {type = "LB"} : (index) -> (index)
+  return %1 : index
+}
+
+// -----
+
+func.func @arith_maxui_unknown_sign(%a: index) -> index {
+  %c4 = arith.constant 4 : index
+  %0 = arith.maxui %a, %c4 : index
+  // expected-error @below{{could not reify bound}}
+  %1 = "test.reify_bound"(%0) {type = "LB"} : (index) -> (index)
+  return %1 : index
+}
+
+// -----
+
+// CHECK-LABEL: func @arith_minui_wraparound(
+//       CHECK:   %[[ub:.*]] = arith.constant 11 : index
+//       CHECK:   return %[[ub]]
+func.func @arith_minui_wraparound() -> index {
+  %c255 = arith.constant 0xFF : i8
+  %c10 = arith.constant 10 : i8
+  %0 = arith.minui %c255, %c10 : i8
+  %1 = "test.reify_bound"(%0) {type = "UB", allow_integer_type} : (i8) -> (index)
+  return %1 : index
+}
+
+// -----
+
+func.func @arith_maxui_wraparound() -> index {
+  %c255 = arith.constant 0xFF : i8
+  %c10 = arith.constant 10 : i8
+  %0 = arith.maxui %c255, %c10 : i8
+  // expected-error @below{{could not reify bound}}
+  %1 = "test.reify_bound"(%0) {type = "LB", allow_integer_type} : (i8) -> (index)
+  return %1 : index
+}
+
+// -----
+
+// CHECK-LABEL: func @arith_maxui_addi(
+//       CHECK:   %[[lb:.*]] = arith.constant 14 : index
+//       CHECK:   return %[[lb]]
+func.func @arith_maxui_addi() -> index {
+  %c4 = arith.constant 4 : index
+  %c10 = arith.constant 10 : index
+  %sum = arith.addi %c4, %c10 : index
+  %0 = arith.maxui %sum, %c4 : index
+  %1 = "test.reify_bound"(%0) {type = "LB", constant} : (index) -> (index)
+  return %1 : index
+}
+
+// -----
+
+// CHECK-LABEL: func @arith_minui_nonneg_symbolic(
+//  CHECK-SAME:     %[[a:.*]]: index
+//       CHECK:   %[[ub:.*]] = arith.constant 5 : index
+//       CHECK:   return %[[ub]]
+func.func @arith_minui_nonneg_symbolic(%a: index) -> index {
+  %c0 = arith.constant 0 : index
+  %c4 = arith.constant 4 : index
+  %nn = arith.maxsi %a, %c0 : index
+  %0 = arith.minui %nn, %c4 : index
+  %1 = "test.reify_bound"(%0) {type = "UB", constant} : (index) -> (index)
+  return %1 : index
+}
+
+// -----
+
+// CHECK-LABEL: func @arith_minui_negative_symbolic(
+//  CHECK-SAME:     %[[a:.*]]: index
+//       CHECK:   %[[ub:.*]] = arith.constant 5 : index
+//       CHECK:   return %[[ub]]
+func.func @arith_minui_negative_symbolic(%a: index) -> index {
+  %cm1 = arith.constant -1 : index
+  %c4 = arith.constant 4 : index
+  %neg = arith.minsi %a, %cm1 : index
+  %0 = arith.minui %neg, %c4 : index
+  %1 = "test.reify_bound"(%0) {type = "UB", constant} : (index) -> (index)
+  return %1 : index
+}
+
+// -----
+
+// CHECK-LABEL: func @arith_maxui_nonneg_symbolic(
+//  CHECK-SAME:     %[[a:.*]]: index
+//       CHECK:   %[[lb:.*]] = arith.constant 4 : index
+//       CHECK:   return %[[lb]]
+func.func @arith_maxui_nonneg_symbolic(%a: index) -> index {
+  %c0 = arith.constant 0 : index
+  %c4 = arith.constant 4 : index
+  %nn = arith.maxsi %a, %c0 : index
+  %0 = arith.maxui %nn, %c4 : index
+  %1 = "test.reify_bound"(%0) {type = "LB", constant} : (index) -> (index)
+  return %1 : index
+}
+
+// -----
+
+func.func @arith_maxui_negative_symbolic(%a: index) -> index {
+  %cm1 = arith.constant -1 : index
+  %c4 = arith.constant 4 : index
+  %neg = arith.minsi %a, %cm1 : index
+  %0 = arith.maxui %neg, %c4 : index
+  // expected-error @below{{could not reify bound}}
+  %1 = "test.reify_bound"(%0) {type = "LB", constant} : (index) -> (index)
+  return %1 : index
+}

@llvmorg-github-actions

Copy link
Copy Markdown

@llvm/pr-subscribers-mlir-arith

Author: nirhersh

Changes

Add ValueBoundsOpInterface external models for the arith integer
CielDiv, RemSI, RemUI, MaxUI, MinUI.

Since the ValueBoundsConstraintSet infrastructure interprets unsigned integers as signed, unsigned ops needed special handling.
In the unsigned ops we first verify that the integers can be proven as positive, and if yes we add the appropriate constraints to the set.

The only exception for that is the RemUI, since the bound is only dependent on the divider we don't care what's the sign of the lhs.


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

3 Files Affected:

  • (modified) mlir/lib/Dialect/Arith/IR/ArithDialect.cpp (+2-1)
  • (modified) mlir/lib/Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp (+143)
  • (modified) mlir/test/Dialect/Arith/value-bounds-op-interface-impl.mlir (+295)
diff --git a/mlir/lib/Dialect/Arith/IR/ArithDialect.cpp b/mlir/lib/Dialect/Arith/IR/ArithDialect.cpp
index ec611ca7924be..3799db1cb3cbe 100644
--- a/mlir/lib/Dialect/Arith/IR/ArithDialect.cpp
+++ b/mlir/lib/Dialect/Arith/IR/ArithDialect.cpp
@@ -56,7 +56,8 @@ void arith::ArithDialect::initialize() {
   declarePromisedInterfaces<bufferization::BufferizableOpInterface, ConstantOp,
                             IndexCastOp, SelectOp>();
   declarePromisedInterfaces<ValueBoundsOpInterface, AddIOp, ConstantOp, SubIOp,
-                            MulIOp, SelectOp, FloorDivSIOp, MinSIOp, MaxSIOp>();
+                            MulIOp, SelectOp, FloorDivSIOp, CeilDivSIOp, MinSIOp,
+                            MaxSIOp, MinUIOp, MaxUIOp, RemSIOp, RemUIOp>();
 }
 
 /// Materialize an integer or floating point constant.
diff --git a/mlir/lib/Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp b/mlir/lib/Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp
index 3440c60f169d3..7c53451f35d6a 100644
--- a/mlir/lib/Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp
+++ b/mlir/lib/Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp
@@ -17,6 +17,32 @@ namespace mlir {
 namespace arith {
 namespace {
 
+static bool isProvablyNonNegative(Value value,
+                                  ValueBoundsConstraintSet &cstr) {
+  return cstr.populateAndCompare(
+      /*lhs=*/{value}, ValueBoundsConstraintSet::ComparisonOperator::GE,
+      /*rhs=*/{OpFoldResult(Builder(value.getContext()).getIndexAttr(0))});
+}
+
+static bool isProvablyNonPositive(Value value,
+                                  ValueBoundsConstraintSet &cstr) {
+ return cstr.populateAndCompare(
+      /*lhs=*/{value}, ValueBoundsConstraintSet::ComparisonOperator::LE,
+      /*rhs=*/{OpFoldResult(Builder(value.getContext()).getIndexAttr(0))});
+}
+
+static bool isProvablyPositive(Value value, ValueBoundsConstraintSet &cstr) {
+  return cstr.populateAndCompare(
+      /*lhs=*/{value}, ValueBoundsConstraintSet::ComparisonOperator::GT,
+      /*rhs=*/{OpFoldResult(Builder(value.getContext()).getIndexAttr(0))});
+}
+
+static bool isProvablyNegative(Value value, ValueBoundsConstraintSet &cstr) {
+  return cstr.populateAndCompare(
+      /*lhs=*/{value}, ValueBoundsConstraintSet::ComparisonOperator::LT,
+      /*rhs=*/{OpFoldResult(Builder(value.getContext()).getIndexAttr(0))});
+}
+
 struct AddIOpInterface
     : public ValueBoundsOpInterface::ExternalModel<AddIOpInterface, AddIOp> {
   void populateBoundsForIndexValue(Operation *op, Value value,
@@ -89,6 +115,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 = isProvablyPositive(rhsValue, cstr);
+    bool rhsNegative = 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 (isProvablyNonPositive(lhsValue, cstr)) {
+      cstr.bound(value) <= 0;
+      if (rhsPositive)
+        cstr.bound(value) >= 1 - rhs;
+      if (rhsNegative)
+        cstr.bound(value) >= rhs + 1;
+    }
+    if (isProvablyNonNegative(lhsValue, cstr)) {
+      cstr.bound(value) >= 0;
+      if (rhsPositive)
+        cstr.bound(value) <= rhs - 1;
+      if (rhsNegative)
+        cstr.bound(value) <= -rhs - 1;
+    }
+  }
+};
+
+struct RemUIOpInterface
+    : public ValueBoundsOpInterface::ExternalModel<RemUIOpInterface, RemUIOp> {
+  void populateBoundsForIndexValue(Operation *op, Value value,
+                                   ValueBoundsConstraintSet &cstr) const {
+    auto remUIOp = cast<RemUIOp>(op);
+    assert(value == remUIOp.getResult() && "invalid value");
+
+    Value rhsValue = remUIOp.getRhs();
+    AffineExpr rhs = cstr.getExpr(rhsValue);
+
+    // remui computes an unsigned remainder, so for a provably positive divisor
+    // the result is always in [0, rhs - 1]
+    if (isProvablyPositive(rhsValue, cstr)) {
+      cstr.bound(value) >= 0;
+      cstr.bound(value) <= rhs - 1;
+    }
+  }
+};
+
 struct SelectOpInterface
     : public ValueBoundsOpInterface::ExternalModel<SelectOpInterface,
                                                    SelectOp> {
@@ -190,6 +283,51 @@ 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 = isProvablyNonNegative(minOp.getLhs(), cstr);
+    bool rhsNonNegative = isProvablyNonNegative(minOp.getRhs(), cstr);
+    if (!lhsNonNegative && !rhsNonNegative)
+      return;
+
+    cstr.bound(value) >= 0;
+    if (lhsNonNegative)
+      cstr.bound(value) <= cstr.getExpr(minOp.getLhs());
+    if (rhsNonNegative)
+      cstr.bound(value) <= cstr.getExpr(minOp.getRhs());
+  }
+};
+
+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 (!isProvablyNonNegative(maxOp.getLhs(), cstr) ||
+        !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;
+  }
+};
 } // namespace
 } // namespace arith
 } // namespace mlir
@@ -202,8 +340,13 @@ void mlir::arith::registerValueBoundsOpInterfaceExternalModels(
     arith::SubIOp::attachInterface<arith::SubIOpInterface>(*ctx);
     arith::MulIOp::attachInterface<arith::MulIOpInterface>(*ctx);
     arith::FloorDivSIOp::attachInterface<arith::FloorDivSIOpInterface>(*ctx);
+    arith::CeilDivSIOp::attachInterface<arith::CeilDivSIOpInterface>(*ctx);
+    arith::RemSIOp::attachInterface<arith::RemSIOpInterface>(*ctx);
+    arith::RemUIOp::attachInterface<arith::RemUIOpInterface>(*ctx);
     arith::SelectOp::attachInterface<arith::SelectOpInterface>(*ctx);
     arith::MinSIOp::attachInterface<arith::MinSIOpInterface>(*ctx);
     arith::MaxSIOp::attachInterface<arith::MaxSIOpInterface>(*ctx);
+    arith::MinUIOp::attachInterface<arith::MinUIOpInterface>(*ctx);
+    arith::MaxUIOp::attachInterface<arith::MaxUIOpInterface>(*ctx);
   });
 }
diff --git a/mlir/test/Dialect/Arith/value-bounds-op-interface-impl.mlir b/mlir/test/Dialect/Arith/value-bounds-op-interface-impl.mlir
index 3f55037f46f09..ba5a5f9d5acf7 100644
--- a/mlir/test/Dialect/Arith/value-bounds-op-interface-impl.mlir
+++ b/mlir/test/Dialect/Arith/value-bounds-op-interface-impl.mlir
@@ -112,6 +112,157 @@ func.func @arith_floordivsi_non_pure(%a: index, %b: index) -> index {
 
 // -----
 
+// CHECK: #[[$map:.*]] = affine_map<()[s0] -> ((s0 + 4) floordiv 5)>
+// CHECK-LABEL: func @arith_ceildivsi(
+//  CHECK-SAME:     %[[a:.*]]: index
+//       CHECK:   %[[apply:.*]] = affine.apply #[[$map]]()[%[[a]]]
+//       CHECK:   return %[[apply]]
+func.func @arith_ceildivsi(%a: index) -> index {
+  %0 = arith.constant 5 : index
+  %1 = arith.ceildivsi %a, %0 : index
+  %2 = "test.reify_bound"(%1) : (index) -> (index)
+  return %2 : index
+}
+
+// -----
+
+func.func @arith_ceildivsi_non_pure(%a: index, %b: index) -> index {
+  %0 = arith.ceildivsi %a, %b : index
+  // Semi-affine expressions (such as "symbol * symbol") are not supported.
+  // expected-error @below{{could not reify bound}}
+  %1 = "test.reify_bound"(%0) : (index) -> (index)
+  return %1 : index
+}
+
+// -----
+
+// CHECK-LABEL: func @arith_remsi_positive_positive()
+//       CHECK:   %[[c0:.*]] = arith.constant 0 : index
+//       CHECK:   %[[c5:.*]] = arith.constant 5 : index
+//       CHECK:   return %[[c0]], %[[c5]]
+func.func @arith_remsi_positive_positive() -> (index, index) {
+  %c7 = arith.constant 7 : index
+  %c5 = arith.constant 5 : index
+  %0 = arith.remsi %c7, %c5 : index
+  %1 = "test.reify_bound"(%0) {type = "LB"} : (index) -> (index)
+  %2 = "test.reify_bound"(%0) {type = "UB"} : (index) -> (index)
+  return %1, %2 : index, index
+}
+
+// -----
+
+// CHECK-LABEL: func @arith_remsi_negative_positive()
+//       CHECK:   %[[cm4:.*]] = arith.constant -4 : index
+//       CHECK:   %[[c1:.*]] = arith.constant 1 : index
+//       CHECK:   return %[[cm4]], %[[c1]]
+func.func @arith_remsi_negative_positive() -> (index, index) {
+  %cm7 = arith.constant -7 : index
+  %c5 = arith.constant 5 : index
+  %0 = arith.remsi %cm7, %c5 : index
+  %1 = "test.reify_bound"(%0) {type = "LB"} : (index) -> (index)
+  %2 = "test.reify_bound"(%0) {type = "UB"} : (index) -> (index)
+  return %1, %2 : index, index
+}
+
+// -----
+
+// CHECK-LABEL: func @arith_remsi_positive_negative()
+//       CHECK:   %[[c0:.*]] = arith.constant 0 : index
+//       CHECK:   %[[c5:.*]] = arith.constant 5 : index
+//       CHECK:   return %[[c0]], %[[c5]]
+func.func @arith_remsi_positive_negative() -> (index, index) {
+  %c7 = arith.constant 7 : index
+  %cm5 = arith.constant -5 : index
+  %0 = arith.remsi %c7, %cm5 : index
+  %1 = "test.reify_bound"(%0) {type = "LB"} : (index) -> (index)
+  %2 = "test.reify_bound"(%0) {type = "UB"} : (index) -> (index)
+  return %1, %2 : index, index
+}
+
+// -----
+
+// CHECK-LABEL: func @arith_remsi_negative_negative()
+//       CHECK:   %[[cm4:.*]] = arith.constant -4 : index
+//       CHECK:   %[[c1:.*]] = arith.constant 1 : index
+//       CHECK:   return %[[cm4]], %[[c1]]
+func.func @arith_remsi_negative_negative() -> (index, index) {
+  %cm7 = arith.constant -7 : index
+  %cm5 = arith.constant -5 : index
+  %0 = arith.remsi %cm7, %cm5 : index
+  %1 = "test.reify_bound"(%0) {type = "LB"} : (index) -> (index)
+  %2 = "test.reify_bound"(%0) {type = "UB"} : (index) -> (index)
+  return %1, %2 : index, index
+}
+
+// -----
+
+// CHECK-LABEL: func @arith_remsi_positive_lhs_symbolic_positive_rhs(
+//  CHECK-SAME:     %[[a:.*]]: index
+//       CHECK:   %[[lb:.*]] = arith.constant 0 : index
+//       CHECK:   return %[[lb]]
+func.func @arith_remsi_positive_lhs_symbolic_positive_rhs(%a: index) -> index {
+  %c1 = arith.constant 1 : index
+  %c7 = arith.constant 7 : index
+  %rhs = arith.maxsi %a, %c1 : index
+  %0 = arith.remsi %c7, %rhs : index
+  %1 = "test.reify_bound"(%0) {type = "LB", constant} : (index) -> (index)
+  return %1 : index
+}
+
+// -----
+
+// CHECK-LABEL: func @arith_remsi_negative_lhs_symbolic_positive_rhs(
+//  CHECK-SAME:     %[[a:.*]]: index
+//       CHECK:   %[[ub:.*]] = arith.constant 1 : index
+//       CHECK:   return %[[ub]]
+func.func @arith_remsi_negative_lhs_symbolic_positive_rhs(%a: index) -> index {
+  %c1 = arith.constant 1 : index
+  %cm7 = arith.constant -7 : index
+  %rhs = arith.maxsi %a, %c1 : index
+  %0 = arith.remsi %cm7, %rhs : index
+  %1 = "test.reify_bound"(%0) {type = "UB", constant} : (index) -> (index)
+  return %1 : index
+}
+
+// -----
+
+// CHECK-LABEL: func @arith_remui_constant()
+//       CHECK:   %[[c0:.*]] = arith.constant 0 : index
+//       CHECK:   %[[c5:.*]] = arith.constant 5 : index
+//       CHECK:   return %[[c0]], %[[c5]]
+func.func @arith_remui_constant() -> (index, index) {
+  %c7 = arith.constant 7 : index
+  %c5 = arith.constant 5 : index
+  %0 = arith.remui %c7, %c5 : index
+  %1 = "test.reify_bound"(%0) {type = "LB"} : (index) -> (index)
+  %2 = "test.reify_bound"(%0) {type = "UB"} : (index) -> (index)
+  return %1, %2 : index, index
+}
+
+// -----
+
+// CHECK-LABEL: func @arith_remui_symbolic_dividend(
+//  CHECK-SAME:     %[[a:.*]]: index
+//       CHECK:   %[[ub:.*]] = arith.constant 5 : index
+//       CHECK:   return %[[ub]]
+func.func @arith_remui_symbolic_dividend(%a: index) -> index {
+  %c5 = arith.constant 5 : index
+  %0 = arith.remui %a, %c5 : index
+  %1 = "test.reify_bound"(%0) {type = "UB", constant} : (index) -> (index)
+  return %1 : index
+}
+
+// -----
+
+func.func @arith_remui_unknown_divisor(%a: index, %b: index) -> index {
+  %0 = arith.remui %a, %b : index
+  // expected-error @below{{could not reify bound}}
+  %1 = "test.reify_bound"(%0) {type = "UB", constant} : (index) -> (index)
+  return %1 : index
+}
+
+// -----
+
 // CHECK-LABEL: func @arith_const()
 //       CHECK:   %[[c5:.*]] = arith.constant 5 : index
 //       CHECK:   %[[c5:.*]] = arith.constant 5 : index
@@ -217,3 +368,147 @@ func.func @arith_maxsi_ub(%a: index) -> index {
   %1 = "test.reify_bound"(%0) {type = "UB"} : (index) -> (index)
   return %1 : index
 }
+
+// -----
+
+// CHECK-LABEL: func @arith_minui(
+//       CHECK:   %[[ub:.*]] = arith.constant 5 : index
+//       CHECK:   return %[[ub]]
+func.func @arith_minui() -> index {
+  %c4 = arith.constant 4 : index
+  %c10 = arith.constant 10 : index
+  %0 = arith.minui %c10, %c4 : index
+  %1 = "test.reify_bound"(%0) {type = "UB"} : (index) -> (index)
+  return %1 : index
+}
+
+// -----
+
+// CHECK-LABEL: func @arith_minui_unknown_sign(
+//  CHECK-SAME:     %[[a:.*]]: index
+//       CHECK:   %[[ub:.*]] = arith.constant 5 : index
+//       CHECK:   return %[[ub]]
+func.func @arith_minui_unknown_sign(%a: index) -> index {
+  %c4 = arith.constant 4 : index
+  %0 = arith.minui %a, %c4 : index
+  %1 = "test.reify_bound"(%0) {type = "UB"} : (index) -> (index)
+  return %1 : index
+}
+
+// -----
+
+// CHECK-LABEL: func @arith_maxui(
+//       CHECK:   %[[lb:.*]] = arith.constant 10 : index
+//       CHECK:   return %[[lb]]
+func.func @arith_maxui() -> index {
+  %c4 = arith.constant 4 : index
+  %c10 = arith.constant 10 : index
+  %0 = arith.maxui %c10, %c4 : index
+  %1 = "test.reify_bound"(%0) {type = "LB"} : (index) -> (index)
+  return %1 : index
+}
+
+// -----
+
+func.func @arith_maxui_unknown_sign(%a: index) -> index {
+  %c4 = arith.constant 4 : index
+  %0 = arith.maxui %a, %c4 : index
+  // expected-error @below{{could not reify bound}}
+  %1 = "test.reify_bound"(%0) {type = "LB"} : (index) -> (index)
+  return %1 : index
+}
+
+// -----
+
+// CHECK-LABEL: func @arith_minui_wraparound(
+//       CHECK:   %[[ub:.*]] = arith.constant 11 : index
+//       CHECK:   return %[[ub]]
+func.func @arith_minui_wraparound() -> index {
+  %c255 = arith.constant 0xFF : i8
+  %c10 = arith.constant 10 : i8
+  %0 = arith.minui %c255, %c10 : i8
+  %1 = "test.reify_bound"(%0) {type = "UB", allow_integer_type} : (i8) -> (index)
+  return %1 : index
+}
+
+// -----
+
+func.func @arith_maxui_wraparound() -> index {
+  %c255 = arith.constant 0xFF : i8
+  %c10 = arith.constant 10 : i8
+  %0 = arith.maxui %c255, %c10 : i8
+  // expected-error @below{{could not reify bound}}
+  %1 = "test.reify_bound"(%0) {type = "LB", allow_integer_type} : (i8) -> (index)
+  return %1 : index
+}
+
+// -----
+
+// CHECK-LABEL: func @arith_maxui_addi(
+//       CHECK:   %[[lb:.*]] = arith.constant 14 : index
+//       CHECK:   return %[[lb]]
+func.func @arith_maxui_addi() -> index {
+  %c4 = arith.constant 4 : index
+  %c10 = arith.constant 10 : index
+  %sum = arith.addi %c4, %c10 : index
+  %0 = arith.maxui %sum, %c4 : index
+  %1 = "test.reify_bound"(%0) {type = "LB", constant} : (index) -> (index)
+  return %1 : index
+}
+
+// -----
+
+// CHECK-LABEL: func @arith_minui_nonneg_symbolic(
+//  CHECK-SAME:     %[[a:.*]]: index
+//       CHECK:   %[[ub:.*]] = arith.constant 5 : index
+//       CHECK:   return %[[ub]]
+func.func @arith_minui_nonneg_symbolic(%a: index) -> index {
+  %c0 = arith.constant 0 : index
+  %c4 = arith.constant 4 : index
+  %nn = arith.maxsi %a, %c0 : index
+  %0 = arith.minui %nn, %c4 : index
+  %1 = "test.reify_bound"(%0) {type = "UB", constant} : (index) -> (index)
+  return %1 : index
+}
+
+// -----
+
+// CHECK-LABEL: func @arith_minui_negative_symbolic(
+//  CHECK-SAME:     %[[a:.*]]: index
+//       CHECK:   %[[ub:.*]] = arith.constant 5 : index
+//       CHECK:   return %[[ub]]
+func.func @arith_minui_negative_symbolic(%a: index) -> index {
+  %cm1 = arith.constant -1 : index
+  %c4 = arith.constant 4 : index
+  %neg = arith.minsi %a, %cm1 : index
+  %0 = arith.minui %neg, %c4 : index
+  %1 = "test.reify_bound"(%0) {type = "UB", constant} : (index) -> (index)
+  return %1 : index
+}
+
+// -----
+
+// CHECK-LABEL: func @arith_maxui_nonneg_symbolic(
+//  CHECK-SAME:     %[[a:.*]]: index
+//       CHECK:   %[[lb:.*]] = arith.constant 4 : index
+//       CHECK:   return %[[lb]]
+func.func @arith_maxui_nonneg_symbolic(%a: index) -> index {
+  %c0 = arith.constant 0 : index
+  %c4 = arith.constant 4 : index
+  %nn = arith.maxsi %a, %c0 : index
+  %0 = arith.maxui %nn, %c4 : index
+  %1 = "test.reify_bound"(%0) {type = "LB", constant} : (index) -> (index)
+  return %1 : index
+}
+
+// -----
+
+func.func @arith_maxui_negative_symbolic(%a: index) -> index {
+  %cm1 = arith.constant -1 : index
+  %c4 = arith.constant 4 : index
+  %neg = arith.minsi %a, %cm1 : index
+  %0 = arith.maxui %neg, %c4 : index
+  // expected-error @below{{could not reify bound}}
+  %1 = "test.reify_bound"(%0) {type = "LB", constant} : (index) -> (index)
+  return %1 : index
+}

@github-actions

github-actions Bot commented Jun 21, 2026

Copy link
Copy Markdown

✅ With the latest revision this PR passed the C/C++ code formatter.

@nirhersh

nirhersh commented Jun 21, 2026

Copy link
Copy Markdown
Contributor Author

@amirBish @ofri-frishman @AviadCo can you please also take a look? thanks :)

@MaxGraey

Copy link
Copy Markdown
Contributor

nit for title & description: CielDiv -> CeilDiv

Comment on lines +22 to +23
/*lhs=*/{value}, ValueBoundsConstraintSet::ComparisonOperator::GE,
/*rhs=*/{OpFoldResult(Builder(value.getContext()).getIndexAttr(0))});

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
/*lhs=*/{value}, ValueBoundsConstraintSet::ComparisonOperator::GE,
/*rhs=*/{OpFoldResult(Builder(value.getContext()).getIndexAttr(0))});
/*lhs=*/{value},
ValueBoundsConstraintSet::ComparisonOperator::GE,
/*rhs=*/{OpFoldResult(Builder(value.getContext()).getIndexAttr(0))});

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

And same for the rest

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

the clang format doesnt allow this

@nirhersh nirhersh changed the title [mlir][arith] Add ValueBoundsOpInterface external models for the arith integer CielDiv, RemSI, RemUI, MaxUI, MinUI. [mlir][arith] Add ValueBoundsOpInterface external models for the arith integer CeilDiv, RemSI, RemUI, MaxUI, MinUI. Jun 21, 2026
@nirhersh nirhersh force-pushed the add-more-arith-ops branch from ab07ec1 to b91e5b0 Compare June 21, 2026 11:04
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants