[mlir][IntRangeInference] Handle ceildivsi(INT_MIN, x > 1) as expected #116284
Conversation
Fixes llvm#115293 While the definition of ceildivsi is integer division, rounding up, most implementations will use `-(-a / b)` for dividing `a ceildiv b` with `a` negative and `b` positive. Mathematically, and for most integers, these two definitions are equivalent. However, with `a == INT_MIN`, the initial negation is a noop, which means that, while divinding and rounding up would give a negative result, `-((- INT_MIN) / b)` is `-(INT_MIN / b)`, which is positive. This commit adds a special case to ceilDivSI inference to handle this case and bring it in line with the operational instead of the mathematical semantics of ceiling division.
|
@llvm/pr-subscribers-mlir-arith @llvm/pr-subscribers-mlir Author: Krzysztof Drewniak (krzysz00) ChangesFixes #115293 While the definition of ceildivsi is integer division, rounding up, most implementations will use Mathematically, and for most integers, these two definitions are equivalent. However, with This commit adds a special case to ceilDivSI inference to handle this case and bring it in line with the operational instead of the mathematical semantics of ceiling division. Full diff: https://github.com/llvm/llvm-project/pull/116284.diff 2 Files Affected:
diff --git a/mlir/lib/Interfaces/Utils/InferIntRangeCommon.cpp b/mlir/lib/Interfaces/Utils/InferIntRangeCommon.cpp
index c5610ba5d3c0bc..0b085b10b2b337 100644
--- a/mlir/lib/Interfaces/Utils/InferIntRangeCommon.cpp
+++ b/mlir/lib/Interfaces/Utils/InferIntRangeCommon.cpp
@@ -375,6 +375,15 @@ mlir::intrange::inferCeilDivS(ArrayRef<ConstantIntRanges> argRanges) {
result.sadd_ov(APInt(result.getBitWidth(), 1), overflowed);
return overflowed ? std::optional<APInt>() : corrected;
}
+ // Special case where the usual implementation of ceilDiv causes
+ // INT_MIN / [positive number] to be positive. This doesn't match the
+ // definition of signed ceiling division mathematically, but it prevents
+ // inconsistent constant-folding results. This arises because (-int_min) is
+ // still negative, so -(-int_min / b) is -(int_min / b), which is
+ // positive See #115293.
+ if (lhs.isMinSignedValue() && rhs.sgt(1)) {
+ return -result;
+ }
return result;
};
return inferDivSRange(lhs, rhs, ceilDivSIFix);
diff --git a/mlir/test/Dialect/Arith/int-range-interface.mlir b/mlir/test/Dialect/Arith/int-range-interface.mlir
index 6d66da2fc1eb35..235d61f2f042ac 100644
--- a/mlir/test/Dialect/Arith/int-range-interface.mlir
+++ b/mlir/test/Dialect/Arith/int-range-interface.mlir
@@ -249,6 +249,19 @@ func.func @ceil_divsi(%arg0 : index) -> i1 {
func.return %10 : i1
}
+// CHECK-LABEL: func @ceil_divsi_intmin_bug_115293
+// CHECK: %[[ret:.*]] = arith.constant true
+// CHECK: return %[[ret]]
+func.func @ceil_divsi_intmin_bug_115293() -> i1 {
+ %cIntMin_i64 = arith.constant -9223372036854775808 : i64
+ %cDenom_i64 = arith.constant 1189465982 : i64
+ %cRes_i64 = arith.constant 7754212542 : i64
+
+ %0 = arith.ceildivsi %cIntMin_i64, %cDenom_i64 : i64
+ %1 = arith.cmpi eq, %0, %cRes_i64 : i64
+ func.return %1 : i1
+}
+
// CHECK-LABEL: func @floor_divsi
// CHECK: %[[true:.*]] = arith.constant true
// CHECK: return %[[true]]
|
| func.func @ceil_divsi_intmin_bug_115293() -> i1 { | ||
| %cIntMin_i64 = arith.constant -9223372036854775808 : i64 | ||
| %cDenom_i64 = arith.constant 1189465982 : i64 | ||
| %cRes_i64 = arith.constant 7754212542 : i64 |
There was a problem hiding this comment.
General comment: this check doesn't look very reliable, as this folding can be result from both int-range-optimizations and just usual folding. We probably should use with_bounds everywhere.
There was a problem hiding this comment.
Point, I can change it (though I do know this one doesn't constant-fold)
There was a problem hiding this comment.
Wait, intMin_i64 is not used?
There was a problem hiding this comment.
... hold on, wait what? How'd my local run pass? Checking again.
Fixes #115293
While the definition of ceildivsi is integer division, rounding up, most implementations will use
-(-a / b)for dividinga ceildiv bwithanegative andbpositive.Mathematically, and for most integers, these two definitions are equivalent. However, with
a == INT_MIN, the initial negation is a noop, which means that, while divinding and rounding up would give a negative result,-((- INT_MIN) / b)is-(INT_MIN / b), which is positive.This commit adds a special case to ceilDivSI inference to handle this case and bring it in line with the operational instead of the mathematical semantics of ceiling division.