[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
Mon Jun 22 01:22:06 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 2aa96fe9641259bf201b1d38fe05b7a1ff3fa4b1 Mon Sep 17 00:00:00 2001
From: Nir Herscovici <nir.herscovici at mobileye.com>
Date: Mon, 22 Jun 2026 11:21:50 +0300
Subject: [PATCH 7/7] nits
---
.../Arith/IR/ValueBoundsOpInterfaceImpl.cpp | 16 ++++++++++------
1 file changed, 10 insertions(+), 6 deletions(-)
diff --git a/mlir/lib/Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp b/mlir/lib/Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp
index 725d5a60e95fd..f2bba03ea0a50 100644
--- a/mlir/lib/Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp
+++ b/mlir/lib/Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp
@@ -172,7 +172,7 @@ struct RemUIOpInterface
AffineExpr rhs = cstr.getExpr(rhsValue);
// remui computes an unsigned remainder, so for a provably positive divisor
- // the result is always in [0, rhs - 1]
+ // the result is always in [0, rhs - 1].
if (isProvablyPositive(rhsValue, cstr)) {
cstr.bound(value) >= 0;
cstr.bound(value) <= rhs - 1;
@@ -293,17 +293,21 @@ struct MinUIOpInterface
// 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)
+ // [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());
+ if (lhsNonNegative) {
+ AffineExpr lhs = cstr.getExpr(minOp.getLhs());
+ cstr.bound(value) <= lhs;
+ }
+ if (rhsNonNegative) {
+ AffineExpr rhs = cstr.getExpr(minOp.getRhs());
+ cstr.bound(value) <= rhs;
+ }
}
};
More information about the Mlir-commits
mailing list