[Mlir-commits] [mlir] [mlir][arith] Add ValueBoundsOpInterface external models for the arith integer CielDiv, RemSI, RemUI, MaxUI, MinUI. (PR #204966)
llvmlistbot at llvm.org
llvmlistbot at llvm.org
Sun Jun 21 01:26:24 PDT 2026
https://github.com/nirhersh created https://github.com/llvm/llvm-project/pull/204966
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.
>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/5] [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/5] 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/5] 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/5] 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/5] 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.
More information about the Mlir-commits
mailing list