[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
Sat Jun 27 03:49: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 01/11] [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 02/11] 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 03/11] 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 04/11] 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 05/11] 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 06/11] 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 07/11] 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;
+ }
}
};
>From d6f52e8ccbc5fb3f415e7221238edb6beec95a26 Mon Sep 17 00:00:00 2001
From: Nir Herscovici <nir.herscovici at mobileye.com>
Date: Wed, 24 Jun 2026 09:50:24 +0300
Subject: [PATCH 08/11] move helpers to ValueBoundsOpInterface
---
.../mlir/Interfaces/ValueBoundsOpInterface.h | 16 ++++++++
.../Arith/IR/ValueBoundsOpInterfaceImpl.cpp | 41 ++++---------------
.../lib/Interfaces/ValueBoundsOpInterface.cpp | 24 +++++++++++
3 files changed, 49 insertions(+), 32 deletions(-)
diff --git a/mlir/include/mlir/Interfaces/ValueBoundsOpInterface.h b/mlir/include/mlir/Interfaces/ValueBoundsOpInterface.h
index 434f786c161d8..2bffb2b93e4b2 100644
--- a/mlir/include/mlir/Interfaces/ValueBoundsOpInterface.h
+++ b/mlir/include/mlir/Interfaces/ValueBoundsOpInterface.h
@@ -313,6 +313,22 @@ class ValueBoundsConstraintSet
static FailureOr<bool>
areEquivalentSlices(MLIRContext *ctx, const HyperrectangularSlice &slice1,
const HyperrectangularSlice &slice2);
+
+ /// Return "true" if the given value is provably non-negative. If it's provably positive,
+ /// or nothing can be proven, return "false".
+ static bool isProvablyNonNegative(Value value, ValueBoundsConstraintSet &cstr);
+
+ /// Return "true" if the given value is provably non-positive. If it's provably negative,
+ /// or nothing can be proven, return "false".
+ static bool isProvablyNonPositive(Value value, ValueBoundsConstraintSet &cstr);
+
+ /// Return "true" if the given value is provably positive. If it's provably non-negative,
+ /// or nothing can be proven, return "false".
+ static bool isProvablyPositive(Value value, ValueBoundsConstraintSet &cstr);
+
+ /// Return "true" if the given value is provably negative. If it's provably non-positive,
+ /// or nothing can be proven, return "false".
+ static bool isProvablyNegative(Value value, ValueBoundsConstraintSet &cstr);
/// Add a bound for the given index-typed value or shaped value. This function
/// returns a builder that adds the bound.
diff --git a/mlir/lib/Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp b/mlir/lib/Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp
index f2bba03ea0a50..0e42eccd92115 100644
--- a/mlir/lib/Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp
+++ b/mlir/lib/Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp
@@ -17,29 +17,6 @@ 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> {
@@ -137,21 +114,21 @@ struct RemSIOpInterface
Value lhsValue = remSIOp.getLhs();
Value rhsValue = remSIOp.getRhs();
AffineExpr rhs = cstr.getExpr(rhsValue);
- bool rhsPositive = isProvablyPositive(rhsValue, cstr);
- bool rhsNegative = isProvablyNegative(rhsValue, cstr);
+ bool rhsPositive = ValueBoundsConstraintSet::isProvablyPositive(rhsValue, cstr);
+ bool rhsNegative = ValueBoundsConstraintSet::isProvablyNegative(rhsValue, cstr);
// The result of remsi has the same sign as the dividend (lhs). The sign
// of lhs does not need to be a compile-time constant: it is sufficient if
// the constraint set can prove it. For lhs == 0 both branches may fire,
// which is consistent since the result is then 0.
- if (isProvablyNonPositive(lhsValue, cstr)) {
+ if (ValueBoundsConstraintSet::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)) {
+ if (ValueBoundsConstraintSet::isProvablyNonNegative(lhsValue, cstr)) {
cstr.bound(value) >= 0;
if (rhsPositive)
cstr.bound(value) <= rhs - 1;
@@ -173,7 +150,7 @@ struct RemUIOpInterface
// remui computes an unsigned remainder, so for a provably positive divisor
// the result is always in [0, rhs - 1].
- if (isProvablyPositive(rhsValue, cstr)) {
+ if (ValueBoundsConstraintSet::isProvablyPositive(rhsValue, cstr)) {
cstr.bound(value) >= 0;
cstr.bound(value) <= rhs - 1;
}
@@ -294,8 +271,8 @@ struct MinUIOpInterface
// 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);
+ bool lhsNonNegative = ValueBoundsConstraintSet::isProvablyNonNegative(minOp.getLhs(), cstr);
+ bool rhsNonNegative = ValueBoundsConstraintSet::isProvablyNonNegative(minOp.getRhs(), cstr);
if (!lhsNonNegative && !rhsNonNegative)
return;
@@ -320,8 +297,8 @@ struct MaxUIOpInterface
assert(value == maxOp.getResult() && "invalid value");
// See MinUIOpInterface comment
- if (!isProvablyNonNegative(maxOp.getLhs(), cstr) ||
- !isProvablyNonNegative(maxOp.getRhs(), cstr))
+ if (!ValueBoundsConstraintSet::isProvablyNonNegative(maxOp.getLhs(), cstr) ||
+ !ValueBoundsConstraintSet::isProvablyNonNegative(maxOp.getRhs(), cstr))
return;
AffineExpr lhs = cstr.getExpr(maxOp.getLhs());
diff --git a/mlir/lib/Interfaces/ValueBoundsOpInterface.cpp b/mlir/lib/Interfaces/ValueBoundsOpInterface.cpp
index b2b33b7441c37..d40b4193bc997 100644
--- a/mlir/lib/Interfaces/ValueBoundsOpInterface.cpp
+++ b/mlir/lib/Interfaces/ValueBoundsOpInterface.cpp
@@ -29,6 +29,30 @@ namespace mlir {
#include "mlir/Interfaces/ValueBoundsOpInterface.cpp.inc"
} // namespace mlir
+bool ValueBoundsConstraintSet::isProvablyNonNegative(Value value, ValueBoundsConstraintSet &cstr) {
+ return cstr.populateAndCompare(
+ /*lhs=*/{value}, ValueBoundsConstraintSet::ComparisonOperator::GE,
+ /*rhs=*/{OpFoldResult(Builder(value.getContext()).getIndexAttr(0))});
+}
+
+bool ValueBoundsConstraintSet::isProvablyNonPositive(Value value, ValueBoundsConstraintSet &cstr) {
+ return cstr.populateAndCompare(
+ /*lhs=*/{value}, ValueBoundsConstraintSet::ComparisonOperator::LE,
+ /*rhs=*/{OpFoldResult(Builder(value.getContext()).getIndexAttr(0))});
+}
+
+bool ValueBoundsConstraintSet::isProvablyPositive(Value value, ValueBoundsConstraintSet &cstr) {
+ return cstr.populateAndCompare(
+ /*lhs=*/{value}, ValueBoundsConstraintSet::ComparisonOperator::GT,
+ /*rhs=*/{OpFoldResult(Builder(value.getContext()).getIndexAttr(0))});
+}
+
+bool ValueBoundsConstraintSet::isProvablyNegative(Value value, ValueBoundsConstraintSet &cstr) {
+ return cstr.populateAndCompare(
+ /*lhs=*/{value}, ValueBoundsConstraintSet::ComparisonOperator::LT,
+ /*rhs=*/{OpFoldResult(Builder(value.getContext()).getIndexAttr(0))});
+}
+
static Operation *getOwnerOfValue(Value value) {
if (auto bbArg = dyn_cast<BlockArgument>(value))
return bbArg.getOwner()->getParentOp();
>From 6ecd7deaa8f04f9f59e50b3f42e0fce3be879a51 Mon Sep 17 00:00:00 2001
From: Nir Herscovici <nir.herscovici at mobileye.com>
Date: Wed, 24 Jun 2026 16:39:39 +0300
Subject: [PATCH 09/11] add a concrete example for remsi
---
.../Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp | 13 ++++++++++---
1 file changed, 10 insertions(+), 3 deletions(-)
diff --git a/mlir/lib/Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp b/mlir/lib/Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp
index 0e42eccd92115..10d974f9b79ce 100644
--- a/mlir/lib/Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp
+++ b/mlir/lib/Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp
@@ -117,10 +117,17 @@ struct RemSIOpInterface
bool rhsPositive = ValueBoundsConstraintSet::isProvablyPositive(rhsValue, cstr);
bool rhsNegative = ValueBoundsConstraintSet::isProvablyNegative(rhsValue, cstr);
- // The result of remsi has the same sign as the dividend (lhs). The sign
- // of lhs does not need to be a compile-time constant: it is sufficient if
+ // The result of remsi has the same sign as the dividend (lhs) and also fulfills |result| < |rhs|.
+ // 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.
+ // which is consistent since the result is then 0. f.e:
+ // lhs rhs result bounds
+ // ---- ---- ------ --------------------------------------------------
+ // 7 3 1 0 <= val && val <= rhs-1 = 2 -> [0, 2]
+ // 7 -3 1 0 <= val && val <= -rhs-1 = 2 -> [0, 2]
+ // -7 3 -1 val <= 0 && val >= 1-rhs = -2 -> [-2, 0]
+ // -7 -3 -1 val <= 0 && val >= rhs+1 = -2 -> [-2, 0]
+ // 0 3 0 both lhs branches fire (0<=val and val<=0) -> val == 0
if (ValueBoundsConstraintSet::isProvablyNonPositive(lhsValue, cstr)) {
cstr.bound(value) <= 0;
if (rhsPositive)
>From 52d1e34783f2498adfb333d20abb6a3deb0b3544 Mon Sep 17 00:00:00 2001
From: Nir Herscovici <nir.herscovici at mobileye.com>
Date: Wed, 24 Jun 2026 16:40:18 +0300
Subject: [PATCH 10/11] clang format
---
.../mlir/Interfaces/ValueBoundsOpInterface.h | 26 ++++++++--------
.../Arith/IR/ValueBoundsOpInterfaceImpl.cpp | 30 +++++++++++--------
.../lib/Interfaces/ValueBoundsOpInterface.cpp | 12 +++++---
3 files changed, 40 insertions(+), 28 deletions(-)
diff --git a/mlir/include/mlir/Interfaces/ValueBoundsOpInterface.h b/mlir/include/mlir/Interfaces/ValueBoundsOpInterface.h
index 2bffb2b93e4b2..f6dfa5855d011 100644
--- a/mlir/include/mlir/Interfaces/ValueBoundsOpInterface.h
+++ b/mlir/include/mlir/Interfaces/ValueBoundsOpInterface.h
@@ -313,21 +313,23 @@ class ValueBoundsConstraintSet
static FailureOr<bool>
areEquivalentSlices(MLIRContext *ctx, const HyperrectangularSlice &slice1,
const HyperrectangularSlice &slice2);
-
- /// Return "true" if the given value is provably non-negative. If it's provably positive,
- /// or nothing can be proven, return "false".
- static bool isProvablyNonNegative(Value value, ValueBoundsConstraintSet &cstr);
- /// Return "true" if the given value is provably non-positive. If it's provably negative,
- /// or nothing can be proven, return "false".
- static bool isProvablyNonPositive(Value value, ValueBoundsConstraintSet &cstr);
+ /// Return "true" if the given value is provably non-negative. If it's
+ /// provably positive, or nothing can be proven, return "false".
+ static bool isProvablyNonNegative(Value value,
+ ValueBoundsConstraintSet &cstr);
- /// Return "true" if the given value is provably positive. If it's provably non-negative,
- /// or nothing can be proven, return "false".
+ /// Return "true" if the given value is provably non-positive. If it's
+ /// provably negative, or nothing can be proven, return "false".
+ static bool isProvablyNonPositive(Value value,
+ ValueBoundsConstraintSet &cstr);
+
+ /// Return "true" if the given value is provably positive. If it's provably
+ /// non-negative, or nothing can be proven, return "false".
static bool isProvablyPositive(Value value, ValueBoundsConstraintSet &cstr);
-
- /// Return "true" if the given value is provably negative. If it's provably non-positive,
- /// or nothing can be proven, return "false".
+
+ /// Return "true" if the given value is provably negative. If it's provably
+ /// non-positive, or nothing can be proven, return "false".
static bool isProvablyNegative(Value value, ValueBoundsConstraintSet &cstr);
/// Add a bound for the given index-typed value or shaped value. This function
diff --git a/mlir/lib/Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp b/mlir/lib/Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp
index 10d974f9b79ce..b14978ec7b230 100644
--- a/mlir/lib/Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp
+++ b/mlir/lib/Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp
@@ -17,7 +17,6 @@ namespace mlir {
namespace arith {
namespace {
-
struct AddIOpInterface
: public ValueBoundsOpInterface::ExternalModel<AddIOpInterface, AddIOp> {
void populateBoundsForIndexValue(Operation *op, Value value,
@@ -114,20 +113,24 @@ struct RemSIOpInterface
Value lhsValue = remSIOp.getLhs();
Value rhsValue = remSIOp.getRhs();
AffineExpr rhs = cstr.getExpr(rhsValue);
- bool rhsPositive = ValueBoundsConstraintSet::isProvablyPositive(rhsValue, cstr);
- bool rhsNegative = ValueBoundsConstraintSet::isProvablyNegative(rhsValue, cstr);
-
- // The result of remsi has the same sign as the dividend (lhs) and also fulfills |result| < |rhs|.
- // 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. f.e:
+ bool rhsPositive =
+ ValueBoundsConstraintSet::isProvablyPositive(rhsValue, cstr);
+ bool rhsNegative =
+ ValueBoundsConstraintSet::isProvablyNegative(rhsValue, cstr);
+
+ // The result of remsi has the same sign as the dividend (lhs) and also
+ // fulfills |result| < |rhs|. 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. f.e:
// lhs rhs result bounds
// ---- ---- ------ --------------------------------------------------
// 7 3 1 0 <= val && val <= rhs-1 = 2 -> [0, 2]
// 7 -3 1 0 <= val && val <= -rhs-1 = 2 -> [0, 2]
// -7 3 -1 val <= 0 && val >= 1-rhs = -2 -> [-2, 0]
// -7 -3 -1 val <= 0 && val >= rhs+1 = -2 -> [-2, 0]
- // 0 3 0 both lhs branches fire (0<=val and val<=0) -> val == 0
+ // 0 3 0 both lhs branches fire (0<=val and val<=0) -> val
+ // == 0
if (ValueBoundsConstraintSet::isProvablyNonPositive(lhsValue, cstr)) {
cstr.bound(value) <= 0;
if (rhsPositive)
@@ -278,8 +281,10 @@ struct MinUIOpInterface
// 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 = ValueBoundsConstraintSet::isProvablyNonNegative(minOp.getLhs(), cstr);
- bool rhsNonNegative = ValueBoundsConstraintSet::isProvablyNonNegative(minOp.getRhs(), cstr);
+ bool lhsNonNegative =
+ ValueBoundsConstraintSet::isProvablyNonNegative(minOp.getLhs(), cstr);
+ bool rhsNonNegative =
+ ValueBoundsConstraintSet::isProvablyNonNegative(minOp.getRhs(), cstr);
if (!lhsNonNegative && !rhsNonNegative)
return;
@@ -304,7 +309,8 @@ struct MaxUIOpInterface
assert(value == maxOp.getResult() && "invalid value");
// See MinUIOpInterface comment
- if (!ValueBoundsConstraintSet::isProvablyNonNegative(maxOp.getLhs(), cstr) ||
+ if (!ValueBoundsConstraintSet::isProvablyNonNegative(maxOp.getLhs(),
+ cstr) ||
!ValueBoundsConstraintSet::isProvablyNonNegative(maxOp.getRhs(), cstr))
return;
diff --git a/mlir/lib/Interfaces/ValueBoundsOpInterface.cpp b/mlir/lib/Interfaces/ValueBoundsOpInterface.cpp
index d40b4193bc997..02780048f7556 100644
--- a/mlir/lib/Interfaces/ValueBoundsOpInterface.cpp
+++ b/mlir/lib/Interfaces/ValueBoundsOpInterface.cpp
@@ -29,25 +29,29 @@ namespace mlir {
#include "mlir/Interfaces/ValueBoundsOpInterface.cpp.inc"
} // namespace mlir
-bool ValueBoundsConstraintSet::isProvablyNonNegative(Value value, ValueBoundsConstraintSet &cstr) {
+bool ValueBoundsConstraintSet::isProvablyNonNegative(
+ Value value, ValueBoundsConstraintSet &cstr) {
return cstr.populateAndCompare(
/*lhs=*/{value}, ValueBoundsConstraintSet::ComparisonOperator::GE,
/*rhs=*/{OpFoldResult(Builder(value.getContext()).getIndexAttr(0))});
}
-bool ValueBoundsConstraintSet::isProvablyNonPositive(Value value, ValueBoundsConstraintSet &cstr) {
+bool ValueBoundsConstraintSet::isProvablyNonPositive(
+ Value value, ValueBoundsConstraintSet &cstr) {
return cstr.populateAndCompare(
/*lhs=*/{value}, ValueBoundsConstraintSet::ComparisonOperator::LE,
/*rhs=*/{OpFoldResult(Builder(value.getContext()).getIndexAttr(0))});
}
-bool ValueBoundsConstraintSet::isProvablyPositive(Value value, ValueBoundsConstraintSet &cstr) {
+bool ValueBoundsConstraintSet::isProvablyPositive(
+ Value value, ValueBoundsConstraintSet &cstr) {
return cstr.populateAndCompare(
/*lhs=*/{value}, ValueBoundsConstraintSet::ComparisonOperator::GT,
/*rhs=*/{OpFoldResult(Builder(value.getContext()).getIndexAttr(0))});
}
-bool ValueBoundsConstraintSet::isProvablyNegative(Value value, ValueBoundsConstraintSet &cstr) {
+bool ValueBoundsConstraintSet::isProvablyNegative(
+ Value value, ValueBoundsConstraintSet &cstr) {
return cstr.populateAndCompare(
/*lhs=*/{value}, ValueBoundsConstraintSet::ComparisonOperator::LT,
/*rhs=*/{OpFoldResult(Builder(value.getContext()).getIndexAttr(0))});
>From 32c7eacded75d2818f8a9080487194a02096ce24 Mon Sep 17 00:00:00 2001
From: Nir Herscovici <nir.herscovici at mobileye.com>
Date: Sat, 27 Jun 2026 13:48:49 +0300
Subject: [PATCH 11/11] require both sides non negative in minui
---
.../Arith/IR/ValueBoundsOpInterfaceImpl.cpp | 27 +++++++++----------
.../Arith/value-bounds-op-interface-impl.mlir | 22 ++-------------
2 files changed, 14 insertions(+), 35 deletions(-)
diff --git a/mlir/lib/Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp b/mlir/lib/Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp
index b14978ec7b230..dd8d573fac331 100644
--- a/mlir/lib/Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp
+++ b/mlir/lib/Dialect/Arith/IR/ValueBoundsOpInterfaceImpl.cpp
@@ -278,25 +278,20 @@ struct MinUIOpInterface
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).
+ // 0xff is treated as -1, not 255).So, we can only derive bounds for minui
+ // if both operands are provably non-negative.
bool lhsNonNegative =
ValueBoundsConstraintSet::isProvablyNonNegative(minOp.getLhs(), cstr);
bool rhsNonNegative =
ValueBoundsConstraintSet::isProvablyNonNegative(minOp.getRhs(), cstr);
- if (!lhsNonNegative && !rhsNonNegative)
+ if (!lhsNonNegative || !rhsNonNegative)
return;
cstr.bound(value) >= 0;
- if (lhsNonNegative) {
- AffineExpr lhs = cstr.getExpr(minOp.getLhs());
- cstr.bound(value) <= lhs;
- }
- if (rhsNonNegative) {
- AffineExpr rhs = cstr.getExpr(minOp.getRhs());
- cstr.bound(value) <= rhs;
- }
+ AffineExpr lhs = cstr.getExpr(minOp.getLhs());
+ AffineExpr rhs = cstr.getExpr(minOp.getRhs());
+ cstr.bound(value) <= lhs;
+ cstr.bound(value) <= rhs;
}
};
@@ -309,9 +304,11 @@ struct MaxUIOpInterface
assert(value == maxOp.getResult() && "invalid value");
// See MinUIOpInterface comment
- if (!ValueBoundsConstraintSet::isProvablyNonNegative(maxOp.getLhs(),
- cstr) ||
- !ValueBoundsConstraintSet::isProvablyNonNegative(maxOp.getRhs(), cstr))
+ bool lhsNonNegative =
+ ValueBoundsConstraintSet::isProvablyNonNegative(maxOp.getLhs(), cstr);
+ bool rhsNonNegative =
+ ValueBoundsConstraintSet::isProvablyNonNegative(maxOp.getRhs(), cstr);
+ if (!lhsNonNegative || !rhsNonNegative)
return;
AffineExpr lhs = cstr.getExpr(maxOp.getLhs());
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 ba5a5f9d5acf7..eb67998c52990 100644
--- a/mlir/test/Dialect/Arith/value-bounds-op-interface-impl.mlir
+++ b/mlir/test/Dialect/Arith/value-bounds-op-interface-impl.mlir
@@ -384,19 +384,6 @@ func.func @arith_minui() -> 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]]
@@ -420,13 +407,11 @@ func.func @arith_maxui_unknown_sign(%a: index) -> 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
+ // expected-error @below{{could not reify bound}}
%1 = "test.reify_bound"(%0) {type = "UB", allow_integer_type} : (i8) -> (index)
return %1 : index
}
@@ -473,15 +458,12 @@ func.func @arith_minui_nonneg_symbolic(%a: index) -> 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
+ // expected-error @below{{could not reify bound}}
%1 = "test.reify_bound"(%0) {type = "UB", constant} : (index) -> (index)
return %1 : index
}
More information about the Mlir-commits
mailing list