Possible range of values isn't fully tracked after division

[kornelski]

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.

[nikic]

Optimizing (v / 200) <= (v / 2) would be pretty simple, but your actual motivating case looks very hard.