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

llvmlistbot at llvm.org llvmlistbot at llvm.org
Sun Jun 21 04:00:09 PDT 2026


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

>From cb284cc931dbe48d359e3c565dcf97943c140426 Mon Sep 17 00:00:00 2001
From: Nir Herscovici <nir.herscovici at mobileye.com>
Date: Wed, 17 Jun 2026 18:42:50 +0300
Subject: [PATCH 1/7] [mlir][arith] Implement ValueBoundsOpInterface For
 Unsigned ops, CielDiv and Rem

---
 .../Arith/IR/ValueBoundsOpInterfaceImpl.cpp   | 145 +++++++-
 .../Arith/value-bounds-op-interface-impl.mlir | 312 ++++++++++++++++++
 2 files changed, 456 insertions(+), 1 deletion(-)

diff --git a/mlir/lib/Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp b/mlir/lib/Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp
index 3440c60f169d3..c150c47df4207 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> {
@@ -183,7 +276,52 @@ struct MaxSIOpInterface
                                    ValueBoundsConstraintSet &cstr) const {
     auto maxOp = cast<arith::MaxSIOp>(op);
     assert(value == maxOp.getResult() && "invalid value");
-    
+
+    AffineExpr lhs = cstr.getExpr(maxOp.getLhs());
+    AffineExpr rhs = cstr.getExpr(maxOp.getRhs());
+    cstr.bound(value) >= lhs;
+    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;
@@ -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..2c65f18e708f3 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,158 @@ 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
+}
+
+// -----
+
+// not sure this is correct
+// 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 +369,163 @@ 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
+}
+
+// -----
+
+// `minui` with a symbolic operand whose non-negativity is established through
+// the constraint set (`%nn = maxsi(%a, 0)` proves `%nn >= 0`). The guard then
+// passes and the (exclusive) upper bound reifies to `5`, exactly like `minsi`.
+
+// 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
+}
+
+// -----
+
+// `minui` with a symbolic operand that is provably *negative*
+// (`%neg = minsi(%a, -1)` proves `%neg <= -1`). That operand contributes no
+// bound, but the other operand `4` is non-negative and still bounds the
+// unsigned min, so the (exclusive) upper bound reifies to `5`.
+
+// 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
+}
+
+// -----
+
+// `maxui` with a symbolic operand whose non-negativity is established through
+// the constraint set. The guard passes and the lower bound reifies to `4`,
+// exactly like `maxsi`.
+
+// 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
+}
+
+// -----
+
+// `maxui` with a symbolic operand that is provably *negative*. As above, the
+// guard suppresses all bounds and reification fails.
+
+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
+}

>From 3e9e2774367fd92659c469c8bda68c97820b38e1 Mon Sep 17 00:00:00 2001
From: Nir Herscovici <nir.herscovici at mobileye.com>
Date: Wed, 17 Jun 2026 18:46:34 +0300
Subject: [PATCH 2/7] remove comment

---
 mlir/test/Dialect/Arith/value-bounds-op-interface-impl.mlir | 1 -
 1 file changed, 1 deletion(-)

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 2c65f18e708f3..d47179e16b56e 100644
--- a/mlir/test/Dialect/Arith/value-bounds-op-interface-impl.mlir
+++ b/mlir/test/Dialect/Arith/value-bounds-op-interface-impl.mlir
@@ -211,7 +211,6 @@ func.func @arith_remsi_positive_lhs_symbolic_positive_rhs(%a: index) -> index {
 
 // -----
 
-// not sure this is correct
 // CHECK-LABEL: func @arith_remsi_negative_lhs_symbolic_positive_rhs(
 //  CHECK-SAME:     %[[a:.*]]: index
 //       CHECK:   %[[ub:.*]] = arith.constant 1 : index

>From bb33b2e7c50a475db10f3e999f36117f9fd9eb5f Mon Sep 17 00:00:00 2001
From: Nir Herscovici <nir.herscovici at mobileye.com>
Date: Wed, 17 Jun 2026 20:04:47 +0300
Subject: [PATCH 3/7] nit

---
 mlir/lib/Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/mlir/lib/Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp b/mlir/lib/Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp
index c150c47df4207..7c53451f35d6a 100644
--- a/mlir/lib/Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp
+++ b/mlir/lib/Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp
@@ -276,7 +276,7 @@ struct MaxSIOpInterface
                                    ValueBoundsConstraintSet &cstr) const {
     auto maxOp = cast<arith::MaxSIOp>(op);
     assert(value == maxOp.getResult() && "invalid value");
-
+    
     AffineExpr lhs = cstr.getExpr(maxOp.getLhs());
     AffineExpr rhs = cstr.getExpr(maxOp.getRhs());
     cstr.bound(value) >= lhs;

>From 64f0c3bee934d86f6bd4de144c65b4a438af3c1c Mon Sep 17 00:00:00 2001
From: Nir Herscovici <nir.herscovici at mobileye.com>
Date: Wed, 17 Jun 2026 20:07:47 +0300
Subject: [PATCH 4/7] remove test comments

---
 .../Arith/value-bounds-op-interface-impl.mlir    | 16 ----------------
 1 file changed, 16 deletions(-)

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 d47179e16b56e..ba5a5f9d5acf7 100644
--- a/mlir/test/Dialect/Arith/value-bounds-op-interface-impl.mlir
+++ b/mlir/test/Dialect/Arith/value-bounds-op-interface-impl.mlir
@@ -458,10 +458,6 @@ func.func @arith_maxui_addi() -> index {
 
 // -----
 
-// `minui` with a symbolic operand whose non-negativity is established through
-// the constraint set (`%nn = maxsi(%a, 0)` proves `%nn >= 0`). The guard then
-// passes and the (exclusive) upper bound reifies to `5`, exactly like `minsi`.
-
 // CHECK-LABEL: func @arith_minui_nonneg_symbolic(
 //  CHECK-SAME:     %[[a:.*]]: index
 //       CHECK:   %[[ub:.*]] = arith.constant 5 : index
@@ -477,11 +473,6 @@ func.func @arith_minui_nonneg_symbolic(%a: index) -> index {
 
 // -----
 
-// `minui` with a symbolic operand that is provably *negative*
-// (`%neg = minsi(%a, -1)` proves `%neg <= -1`). That operand contributes no
-// bound, but the other operand `4` is non-negative and still bounds the
-// unsigned min, so the (exclusive) upper bound reifies to `5`.
-
 // CHECK-LABEL: func @arith_minui_negative_symbolic(
 //  CHECK-SAME:     %[[a:.*]]: index
 //       CHECK:   %[[ub:.*]] = arith.constant 5 : index
@@ -497,10 +488,6 @@ func.func @arith_minui_negative_symbolic(%a: index) -> index {
 
 // -----
 
-// `maxui` with a symbolic operand whose non-negativity is established through
-// the constraint set. The guard passes and the lower bound reifies to `4`,
-// exactly like `maxsi`.
-
 // CHECK-LABEL: func @arith_maxui_nonneg_symbolic(
 //  CHECK-SAME:     %[[a:.*]]: index
 //       CHECK:   %[[lb:.*]] = arith.constant 4 : index
@@ -516,9 +503,6 @@ func.func @arith_maxui_nonneg_symbolic(%a: index) -> index {
 
 // -----
 
-// `maxui` with a symbolic operand that is provably *negative*. As above, the
-// guard suppresses all bounds and reification fails.
-
 func.func @arith_maxui_negative_symbolic(%a: index) -> index {
   %cm1 = arith.constant -1 : index
   %c4 = arith.constant 4 : index

>From 08f26d1a8c9d741d4d48c12abcaecd45c2f1c6ca Mon Sep 17 00:00:00 2001
From: Nir Herscovici <nir.herscovici at mobileye.com>
Date: Sun, 21 Jun 2026 10:30:34 +0300
Subject: [PATCH 5/7] add promises

---
 mlir/lib/Dialect/Arith/IR/ArithDialect.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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.

>From b91e5b079b530dad675769f51e43c8d2f14fb504 Mon Sep 17 00:00:00 2001
From: Nir Herscovici <nir.herscovici at mobileye.com>
Date: Sun, 21 Jun 2026 11:44:04 +0300
Subject: [PATCH 6/7] clang format fix

---
 mlir/lib/Dialect/Arith/IR/ArithDialect.cpp               | 5 +++--
 mlir/lib/Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp | 8 +++-----
 2 files changed, 6 insertions(+), 7 deletions(-)

diff --git a/mlir/lib/Dialect/Arith/IR/ArithDialect.cpp b/mlir/lib/Dialect/Arith/IR/ArithDialect.cpp
index 3799db1cb3cbe..5f645af274b8b 100644
--- a/mlir/lib/Dialect/Arith/IR/ArithDialect.cpp
+++ b/mlir/lib/Dialect/Arith/IR/ArithDialect.cpp
@@ -56,8 +56,9 @@ void arith::ArithDialect::initialize() {
   declarePromisedInterfaces<bufferization::BufferizableOpInterface, ConstantOp,
                             IndexCastOp, SelectOp>();
   declarePromisedInterfaces<ValueBoundsOpInterface, AddIOp, ConstantOp, SubIOp,
-                            MulIOp, SelectOp, FloorDivSIOp, CeilDivSIOp, MinSIOp,
-                            MaxSIOp, MinUIOp, MaxUIOp, RemSIOp, RemUIOp>();
+                            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 7c53451f35d6a..725d5a60e95fd 100644
--- a/mlir/lib/Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp
+++ b/mlir/lib/Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp
@@ -17,16 +17,14 @@ namespace mlir {
 namespace arith {
 namespace {
 
-static bool isProvablyNonNegative(Value value,
-                                  ValueBoundsConstraintSet &cstr) {
+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(
+static bool isProvablyNonPositive(Value value, ValueBoundsConstraintSet &cstr) {
+  return cstr.populateAndCompare(
       /*lhs=*/{value}, ValueBoundsConstraintSet::ComparisonOperator::LE,
       /*rhs=*/{OpFoldResult(Builder(value.getContext()).getIndexAttr(0))});
 }

>From ab07ec1f23584a28406b1b95b9671c1a1f8884c8 Mon Sep 17 00:00:00 2001
From: Nir Herscovici <nir.herscovici at mobileye.com>
Date: Sun, 21 Jun 2026 13:57:46 +0300
Subject: [PATCH 7/7] nit

---
 .../Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp  | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/mlir/lib/Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp b/mlir/lib/Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp
index 725d5a60e95fd..87407f729d713 100644
--- a/mlir/lib/Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp
+++ b/mlir/lib/Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp
@@ -19,25 +19,29 @@ namespace {
 
 static bool isProvablyNonNegative(Value value, ValueBoundsConstraintSet &cstr) {
   return cstr.populateAndCompare(
-      /*lhs=*/{value}, ValueBoundsConstraintSet::ComparisonOperator::GE,
+      /*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,
+      /*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,
+      /*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,
+      /*lhs=*/{value},
+      ValueBoundsConstraintSet::ComparisonOperator::LT,
       /*rhs=*/{OpFoldResult(Builder(value.getContext()).getIndexAttr(0))});
 }
 



More information about the Mlir-commits mailing list