llvm / llvm/llvm-project

[MLIR][Index] Miscompilation: index.cmp canonicalization of index.sub can change comparison semantics

Open
#216,042 1 comment 0 reactions 0 assignees View on GitHub
miscompilation mlir
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

Open the contributing 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

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.