[MLIR][Index] Miscompilation: index.cmp canonicalization of index.sub can change comparison semantics
- Dominant language
- LLVM
- Stars
- 40.5k
- Forks
- 18.7k
- PR merge metrics
- PR metrics pending
Description
`CmpOp::canonicalize` in `mlir/lib/Dialect/Index/IR/IndexOps.cpp` rewrites `(x - y) cmp 0` to `x cmp y` while preserving the comparison predicate. This transformation is valid for `eq` and `ne`, but is not valid in general for ordered comparisons because `index.sub` has modular fixed-width semantics. For unsigned predicates, the transformation can change the result when the subtraction wraps due to a borrow. For signed predicates, it can change the result when the subtraction overflows.
## Reproducer
### small.mlir
```mlir
memref.global "private" @gx : memref<1xi64> = dense<0>
func.func @main() {
%m = memref.get_global @gx : memref<1xi64>
%z = arith.constant 0 : index // %z = 0
%v = memref.load %m[%z] : memref<1xi64> // %v = 0
%x = index.casts %v : i64 to index // %x = 0
%two = index.constant 2
%n = index.sub %x, %two // %n = -2 -> 11111111 11111111 ... 11111110
%zero = index.constant 0
%r = index.cmp ule(%n, %zero) // -2 read as unsigned, which is not <= 0, so this is false.
%e = arith.extui %r : i1 to i64 // %e = 0
vector.print %e : i64
return
}
```
### To reproduce:
```bash
$ mlir-opt small.mlir -o lower.mlir \
--canonicalize \
--convert-index-to-llvm --convert-arith-to-llvm --finalize-memref-to-llvm \
--convert-func-to-llvm --convert-vector-to-llvm --reconcile-unrealized-casts
$
$ mlir-runner lower.mlir \
-e main --entry-point-result=void \
--shared-libs=/path/to/mlir/build/lib/libmlir_c_runner_utils.so,/path/to/mlir/build/lib/libmlir_runner_utils.so
```
### Expected output
```
0
```
### Actual output
```
1
```
The same file without `--canonicalize` prints `0`.
Contributor guide
Research direction
Start in mlir/lib/Dialect/Index/IR/IndexOps.cpp at CmpOp::canonicalize, then run the supplied small.mlir pipeline with and without --canonicalize. Check the ordered comparison behavior against the expected output of 0, including the modular subtraction case. Done means canonicalization no longer changes the result for ordered comparisons while the reported eq and ne behavior remains valid.
Written by the indexing model from the issue text.
Assessment
- Tech stack
- cpp
- Domain
- compilers
- Issue type
- Bug
- Difficulty
- 3/5
- Estimated time
- 1-2 days
- Activity status
- Quiet
- Clarity
- Clearly specified
- Newbie friendliness
- 68/100