| Issue |
150353
|
| Summary |
Possible range of values isn't fully tracked after division
|
| Labels |
new issue
|
| Assignees |
|
| Reporter |
kornelski
|
LLVM can't see an always-true relationship between two divided numbers:
```c
void check(unsigned long v) {
assert((v / 100) <= v); // optimized out OK
assert((v / 200) <= v); // optimized out OK
assert((v / 200) <= (v / 2)); // FAIL
}
```
Oddly, adding `if (v >= 400) return;` makes it prove the third case is true:
```c
void check(unsigned long v) {
if (v >= 400) return;
assert((v / 100) <= v); // optimized out
assert((v / 200) <= v); // optimized out
assert((v / 200) <= (v / 2)); // optimized out now too
}
```
but with `if (v >= 401) return;` it becomes unknowable again.
Here's a real-world code that needs such reasoning to remove bounds checks:
https://github.com/kornelski/rust/blob/999967a57dce987bbad353d152f03c3ef67d41f2/library/core/src/slice/sort/select.rs#L222-L232
I expected I'd only need to prove the `v.len()` is non-0 to remove the bounds checks, but I needed to add [more hints](https://github.com/rust-lang/rust/pull/144327/files#diff-062e0b3adced7b5e420b1c3774d1aaac361ef8800458c0ef95011c5fc9f3c8baR217-R239).
![]()
_______________________________________________
llvm-bugs mailing list
llvm-bugs@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-bugs
