<table border="1" cellspacing="0" cellpadding="8">
    <tr>
        <th>Issue</th>
        <td>
            <a href=https://github.com/llvm/llvm-project/issues/150353>150353</a>
        </td>
    </tr>

    <tr>
        <th>Summary</th>
        <td>
            Possible range of values isn't fully tracked after division
        </td>
    </tr>

    <tr>
      <th>Labels</th>
      <td>
            new issue
      </td>
    </tr>

    <tr>
      <th>Assignees</th>
      <td>
      </td>
    </tr>

    <tr>
      <th>Reporter</th>
      <td>
          kornelski
      </td>
    </tr>
</table>

<pre>
    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).
</pre>
<img width="1" height="1" alt="" src="http://email.email.llvm.org/o/eJyslU-P4zYPxj-NciESyJQd2wcfZnZe4x10ii320Lv-0IkaRQokOWn66QvZ050tup0Wuw2cBInph-Tzo02Zkj14ooE1j6x52sg5H0McTiF6culkNyqY-_Dy8vOPoKVn2GZIRCA9SHeT97TNcSaI5GS2waejvYCifCPykG8BjL1aQwb8fFYUExMPjC_Hnq-HZvzhGqwBfSR9YtjNfinIgAv-AFeGPbD2EQAYfwCZEsXMsGPYXYHhCBXnS4j4wMTTEs5Eif7jxXAsYeGS7dn-RgbCnOHjD0UM4Ct6-M16_1Ly7e-ivcq_io4Pzy-f8_AH1j596dSa4qMx7s7wA0hjrD8A23M7vYqK_5UE9ZouUp6jZ-KR7Tmc5YkS2AyXGK4E-VjeNhrQMhHYBIXi98L5pzresehbKP6nCL-P398Ohg83yCG8S1TNGW42H7-KsvoLSptBkQ5nSjD7kw83qRyBPEjrd6vg_ykSwzaBhEjSbW8hOgM6mAJdZvBEJkGa9bGcT8GXOcoBIp3LcKgwe5NW5OWGhVX1mPNluX-XPg82H2e10-HMcPz8sGA4xjllhqNyQTEc-77v961sWqOp71qlpBGNMFWDExda0LRvTV1NyHB0VkUZ7wxHHUr9Y4q6fDqrl1-hQBkTOdJ5FxND8YKI2xcUuBb4DPTrhXQmA88MWwPBu_vSbGnubfDZnl93jvyCuF8sTeCD3_IvTCiBfzYCP0Ah9bworprSGGDN4zlEgqP1ObHmiWH3jlPFna2T_vDm1GV2juFY1bXAluE4WUelO2Onacv3SFwJaTSZVjVUI1eVFm1bm0pKqcW-oqnrOK-bTnOa-oZXlW4m3U9Cd0p-wqrdfkJRBnW3MYMwvejlhoaqbYRA3tbV5ji0imo9tbomrLXUvZTTvq-nlivdqL7SGzsgx4a3WPNKIFa7qqvEvq5lXfU49Z1hNaeztG7n3PW8C_GwsSnNNFQNF43YOKnIpWXFIHq6wXKWIZaNE4dy0VbNh8Rq7mzK6U0m2-xo-CmkZMuYR-kPBGGCq3RzeaKldSVNs3N3yFHqExmQU6a4rJ5kg9_M0Q3vMCm5Xr-2lxh-IV2wLBWmAmZt4Trg7wEAAP__-uwXVg">