LLVM can't see an always-true relationship between two divided numbers:
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:
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.
LLVM can't see an always-true relationship between two divided numbers:
Oddly, adding
if (v >= 400) return;makes it prove the third case is true: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.