[Mlir-commits] [mlir] [mlir][arith] Fold ceildivsi with MININT operands (PR #214637)
llvmlistbot at llvm.org
llvmlistbot at llvm.org
Thu Aug 6 22:24:49 PDT 2026
llvmorg-github-actions[bot] wrote:
<!--LLVM PR SUMMARY COMMENT-->
@llvm/pr-subscribers-mlir-arith
Author: 曾鈜寬 Tseng Hung Kuan (Tim096)
<details>
<summary>Changes</summary>
`CeilDivSIOp::fold` computes the ceiling by negating operands so that the
division runs on two non-negative values. Negating `MININT` overflows, so the
folder gives up on any `MININT` operand, even when the result is perfectly
representable:
```mlir
// i8, MININT = -128. ceil(-128 / 7) = -18, which fits, but does not fold.
%0 = arith.constant 7 : i8
%min = arith.constant -128 : i8
%1 = arith.ceildivsi %min, %0 : i8
```
The existing TODO on the folder mentions only a `MININT` dividend, but a
`MININT` divisor is affected the same way, since that operand gets negated too.
Over all 65280 `i8` operand pairs, 507 do not fold today: 253 with a `MININT`
dividend and **254 with a `MININT` divisor**. The divisor half has not been
recorded anywhere so far.
Note this is a missed fold, not a miscompile. The current code is correct, just
conservative; it bails rather than producing a wrong constant.
## Change
Compute the ceiling without negating anything. `sdiv` truncates towards zero,
which already rounds up whenever the exact quotient is negative, so the only
correction needed is `+1` when the operands share a sign and the division is
inexact:
```c++
APInt quotient = a.sdiv_ov(b, overflowDiv);
if (overflowDiv) // MININT / -1
bail;
if (a.srem(b).isZero() || a.isNegative() != b.isNegative())
return quotient;
return quotient.sadd_ov(one, overflowOrDiv0);
```
This is the same shape `ExpandOps.cpp` already uses to expand the op, so the
folder and the expansion now agree by construction rather than by coincidence.
After the change the folder bails on exactly two things: division by zero, as
before, and `MININT / -1`, whose result `-MININT` is not representable. Every
other operand pair folds.
`signedCeilNonnegInputs` has no callers left and is removed. The four
quadrant-specific branches and their four overflow flags collapse into one
path, for a net reduction of about 50 lines.
## Correctness
**Alive2** — the new algorithm against the expansion `arith-expand` already
uses, both lowered from MLIR via `--convert-to-llvm | mlir-translate
--mlir-to-llvmir`: https://alive2.llvm.org/ce/z/Chnon4 ✓ *Transformation seems
to be correct!*
The two differ only in how inexactness is tested, `srem != 0` versus
`a != (a sdiv b) * b`; the rest is identical. Alive2 treats division by zero and
`MININT / -1` as poison, so the cases the folder bails on are covered.
**Exhaustive check against an oracle** — every operand pair, compared against
exact ceiling division computed independently of any LLVM code:
| Width | Pairs | Result |
|---|---|---|
| `i4` | 240 | all agree; 1 unfolded (`-8 / -1`) |
| `i8` | 65280 | all agree; 1 unfolded (`-128 / -1`) |
Before and after, over the same `i8` sweep:
| | Unfolded | Folded to a wrong value |
|---|---|---|
| Before | 507 | 0 |
| After | **1** | 0 |
This pair of checks is deliberate: Alive2 proves the algorithm symbolically but
against upstream's own expansion, while the oracle sweep compares against
mathematical ceiling division, so a mistake shared by both implementations would
still be caught.
## Tests
The first commit pre-commits the missing `MININT` divisor cases, plus
`MININT / -1`, with check lines showing current behaviour. The second commit
contains the functional change and the resulting check-line diffs.
This **updates an existing test**: `@<!-- -->simple_arith.ceildivsi_overflow` asserted
that `MININT` dividends do not fold, and they now fold to `-18`, `-4681` and
`-306783378`. It is renamed to `@<!-- -->simple_arith.ceildivsi_minint_dividend` since
it no longer describes a bail-out, and the TODO it carried, "The folder should
be able to fold the following by avoiding intermediate operations that
overflow", is resolved and removed.
`ninja check-mlir` passes.
## Prior art
PR #<!-- -->90855 attempted the mixed-sign part of this in 2024 but stalled on a request
for exactly this kind of analysis; it has been inactive since and its base has
drifted considerably. cc @<!-- -->bviyer in case there is interest.
---
Full diff: https://github.com/llvm/llvm-project/pull/214637.diff
2 Files Affected:
- (modified) mlir/lib/Dialect/Arith/IR/ArithOps.cpp (+21-53)
- (modified) mlir/test/Transforms/constant-fold.mlir (+60-21)
``````````diff
diff --git a/mlir/lib/Dialect/Arith/IR/ArithOps.cpp b/mlir/lib/Dialect/Arith/IR/ArithOps.cpp
index ff6a5d4a0c29a..412c378cce531 100644
--- a/mlir/lib/Dialect/Arith/IR/ArithOps.cpp
+++ b/mlir/lib/Dialect/Arith/IR/ArithOps.cpp
@@ -912,18 +912,6 @@ Speculation::Speculatability arith::DivSIOp::getSpeculatability() {
return getDivSISpeculatability(getRhs());
}
-//===----------------------------------------------------------------------===//
-// Ceil and floor division folding helpers
-//===----------------------------------------------------------------------===//
-
-static APInt signedCeilNonnegInputs(const APInt &a, const APInt &b,
- bool &overflow) {
- // Returns (a-1)/b + 1
- APInt one(a.getBitWidth(), 1, true); // Signed value 1.
- APInt val = a.ssub_ov(one, overflow).sdiv_ov(b, overflow);
- return val.sadd_ov(one, overflow);
-}
-
//===----------------------------------------------------------------------===//
// CeilDivUIOp
//===----------------------------------------------------------------------===//
@@ -988,56 +976,36 @@ OpFoldResult arith::CeilDivSIOp::fold(FoldAdaptor adaptor) {
return getIntegerAttrOfType(getType(), 1);
// Don't fold if it would overflow or if it requires a division by zero.
- // TODO: This hook won't fold operations where a = MININT, because
- // negating MININT overflows. This can be improved.
bool overflowOrDiv0 = false;
auto result = constFoldBinaryOp<IntegerAttr>(
- adaptor.getOperands(), [&](APInt a, const APInt &b) {
+ adaptor.getOperands(), [&](const APInt &a, const APInt &b) {
if (overflowOrDiv0 || !b) {
overflowOrDiv0 = true;
return a;
}
- if (!a)
- return a;
- // After this point we know that neither a or b are zero.
- unsigned bits = a.getBitWidth();
- APInt zero = APInt::getZero(bits);
- bool aGtZero = a.sgt(zero);
- bool bGtZero = b.sgt(zero);
- if (aGtZero && bGtZero) {
- // Both positive, return ceil(a, b).
- return signedCeilNonnegInputs(a, b, overflowOrDiv0);
- }
-
- // No folding happens if any of the intermediate arithmetic operations
- // overflows.
- bool overflowNegA = false;
- bool overflowNegB = false;
+ // Compute the ceiling without negating either operand, so that MININT
+ // operands still fold whenever the result is representable.
+ //
+ // sdiv truncates towards zero, so it already rounds up whenever the
+ // exact quotient is negative. When the exact quotient is positive, i.e.
+ // when the operands have the same sign, an inexact division has to be
+ // corrected by one. This mirrors the expansion in ExpandOps.cpp.
bool overflowDiv = false;
- bool overflowNegRes = false;
- if (!aGtZero && !bGtZero) {
- // Both negative, return ceil(-a, -b).
- APInt posA = zero.ssub_ov(a, overflowNegA);
- APInt posB = zero.ssub_ov(b, overflowNegB);
- APInt res = signedCeilNonnegInputs(posA, posB, overflowDiv);
- overflowOrDiv0 = (overflowNegA || overflowNegB || overflowDiv);
- return res;
- }
- if (!aGtZero && bGtZero) {
- // A is negative, b is positive, return - ( -a / b).
- APInt posA = zero.ssub_ov(a, overflowNegA);
- APInt div = posA.sdiv_ov(b, overflowDiv);
- APInt res = zero.ssub_ov(div, overflowNegRes);
- overflowOrDiv0 = (overflowNegA || overflowDiv || overflowNegRes);
- return res;
+ APInt quotient = a.sdiv_ov(b, overflowDiv);
+ if (overflowDiv) {
+ // MININT / -1. The exact result is -MININT, which is not
+ // representable.
+ overflowOrDiv0 = true;
+ return a;
}
- // A is positive, b is negative, return - (a / -b).
- APInt posB = zero.ssub_ov(b, overflowNegB);
- APInt div = a.sdiv_ov(posB, overflowDiv);
- APInt res = zero.ssub_ov(div, overflowNegRes);
+ if (a.srem(b).isZero() || a.isNegative() != b.isNegative())
+ return quotient;
- overflowOrDiv0 = (overflowNegB || overflowDiv || overflowNegRes);
- return res;
+ // The correction cannot overflow: it only applies when the exact
+ // quotient is positive and the division is inexact, which bounds the
+ // quotient well below the maximum. Check anyway, at no cost.
+ APInt one(a.getBitWidth(), 1, /*isSigned=*/true);
+ return quotient.sadd_ov(one, overflowOrDiv0);
});
return overflowOrDiv0 ? Attribute() : result;
diff --git a/mlir/test/Transforms/constant-fold.mlir b/mlir/test/Transforms/constant-fold.mlir
index 0b393bf0556b9..f3ca18c56baab 100644
--- a/mlir/test/Transforms/constant-fold.mlir
+++ b/mlir/test/Transforms/constant-fold.mlir
@@ -478,35 +478,26 @@ func.func @simple_arith.ceildivsi() -> (i32, i32, i32, i32, i32) {
// -----
-// CHECK-LABEL: func @simple_arith.ceildivsi_overflow
-func.func @simple_arith.ceildivsi_overflow() -> (i8, i16, i32) {
- // The negative values below are MININTs for the corresponding bit-width. The
- // folder will try to negate them (so that the division operates on two
- // positive numbers), but that would cause overflow (negating MININT
- // overflows). Hence folding should not happen and the original ceildivsi is
- // preserved.
-
- // TODO: The folder should be able to fold the following by avoiding
- // intermediate operations that overflow.
-
- // CHECK-DAG: %[[C_1:.*]] = arith.constant 7 : i8
- // CHECK-DAG: %[[MIN_I8:.*]] = arith.constant -128 : i8
- // CHECK-DAG: %[[C_2:.*]] = arith.constant 7 : i16
- // CHECK-DAG: %[[MIN_I16:.*]] = arith.constant -32768 : i16
- // CHECK-DAG: %[[C_3:.*]] = arith.constant 7 : i32
- // CHECK-DAG: %[[MIN_I32:.*]] = arith.constant -2147483648 : i32
-
- // CHECK-NEXT: %[[CEILDIV_1:.*]] = arith.ceildivsi %[[MIN_I8]], %[[C_1]] : i8
+// The dividends below are MININTs for the corresponding bit-width. Every
+// result is representable, so all of them fold.
+
+// CHECK-LABEL: func @simple_arith.ceildivsi_minint_dividend
+// CHECK-DAG: %[[CEILDIV_1:.*]] = arith.constant -18 : i8
+// CHECK-DAG: %[[CEILDIV_2:.*]] = arith.constant -4681 : i16
+// CHECK-DAG: %[[CEILDIV_3:.*]] = arith.constant -306783378 : i32
+// CHECK: return %[[CEILDIV_1]], %[[CEILDIV_2]], %[[CEILDIV_3]]
+func.func @simple_arith.ceildivsi_minint_dividend() -> (i8, i16, i32) {
+ // ceil(-128 / 7) = -18
%0 = arith.constant 7 : i8
%min_int_i8 = arith.constant -128 : i8
%2 = arith.ceildivsi %min_int_i8, %0 : i8
- // CHECK-NEXT: %[[CEILDIV_2:.*]] = arith.ceildivsi %[[MIN_I16]], %[[C_2]] : i16
+ // ceil(-32768 / 7) = -4681
%3 = arith.constant 7 : i16
%min_int_i16 = arith.constant -32768 : i16
%5 = arith.ceildivsi %min_int_i16, %3 : i16
- // CHECK-NEXT: %[[CEILDIV_2:.*]] = arith.ceildivsi %[[MIN_I32]], %[[C_3]] : i32
+ // ceil(-2147483648 / 7) = -306783378
%6 = arith.constant 7 : i32
%min_int_i32 = arith.constant -2147483648 : i32
%8 = arith.ceildivsi %min_int_i32, %6 : i32
@@ -516,6 +507,54 @@ func.func @simple_arith.ceildivsi_overflow() -> (i8, i16, i32) {
// -----
+// The divisor, rather than the dividend, is MININT here.
+
+// CHECK-LABEL: func @simple_arith.ceildivsi_minint_divisor
+// CHECK-DAG: %[[C_0:.*]] = arith.constant 0 : i8
+// CHECK-DAG: %[[C_1:.*]] = arith.constant 1 : i8
+// CHECK: return %[[C_0]], %[[C_1]], %[[C_1]]
+func.func @simple_arith.ceildivsi_minint_divisor() -> (i8, i8, i8) {
+ %min_int_i8 = arith.constant -128 : i8
+ %0 = arith.constant 7 : i8
+ %1 = arith.constant -9 : i8
+
+ // ceil(7 / -128) = 0
+ %2 = arith.ceildivsi %0, %min_int_i8 : i8
+ // ceil(-9 / -128) = 1
+ %3 = arith.ceildivsi %1, %min_int_i8 : i8
+ // ceil(-128 / -128) = 1, already folded by the ceildivsi(x, x) -> 1 pattern.
+ %4 = arith.ceildivsi %min_int_i8, %min_int_i8 : i8
+
+ return %2, %3, %4 : i8, i8, i8
+}
+
+// -----
+
+// ceil(MININT / -1) is -MININT, which is not representable. Unlike the cases
+// above, these must never fold.
+
+// CHECK-LABEL: func @simple_arith.ceildivsi_minint_div_minus_one
+// CHECK: arith.ceildivsi
+// CHECK-NEXT: arith.ceildivsi
+// CHECK-NEXT: arith.ceildivsi
+func.func @simple_arith.ceildivsi_minint_div_minus_one() -> (i8, i16, i32) {
+ %min_int_i8 = arith.constant -128 : i8
+ %0 = arith.constant -1 : i8
+ %1 = arith.ceildivsi %min_int_i8, %0 : i8
+
+ %min_int_i16 = arith.constant -32768 : i16
+ %2 = arith.constant -1 : i16
+ %3 = arith.ceildivsi %min_int_i16, %2 : i16
+
+ %min_int_i32 = arith.constant -2147483648 : i32
+ %4 = arith.constant -1 : i32
+ %5 = arith.ceildivsi %min_int_i32, %4 : i32
+
+ return %1, %3, %5 : i8, i16, i32
+}
+
+// -----
+
// CHECK-LABEL: func @simple_arith.ceildivui
func.func @simple_arith.ceildivui() -> (i32, i32, i32, i32, i32) {
// CHECK-DAG: [[C0:%.+]] = arith.constant 0
``````````
</details>
https://github.com/llvm/llvm-project/pull/214637
More information about the Mlir-commits
mailing list