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

    <tr>
        <th>Summary</th>
        <td>
            Failure to infer `udiv exact`/`sdiv exact` from `assume`
        </td>
    </tr>

    <tr>
      <th>Labels</th>
      <td>
            missed-optimization
      </td>
    </tr>

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

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

<pre>
    There is no easy way to generate `udiv exact` or `sdiv exact` LLVM IR from c. These functions use `assume`, but the `exact` flag is not inferred from the assume:

https://godbolt.org/z/vWxPW1qr6
```c
u32 udiv_exact(u32 x, u32 y) {
    assume(x % y == 0);
    return x / y;
}

i32 sdiv_exact(i32 x, i32 y) {
    assume(x % y == 0);
    return x / y;
}
```

Alive proof:
https://alive2.llvm.org/ce/z/VGa4WM
```llvm
define dso_local noundef i32 @src1(i32 noundef %0, i32 noundef %1) local_unnamed_addr #0 {
 %3 = udiv i32 %0, %1
  %4 = mul i32 %3, %1
  %5 = sub i32 %0, %4
 %6 = icmp eq i32 %5, 0
  tail call void @llvm.assume(i1 %6)
  ret i32 %3
}

define dso_local noundef i32 @tgt1(i32 noundef %0, i32 noundef %1) local_unnamed_addr #0 {
  %3 = udiv exact i32 %0, %1
  ret i32 %3
}

define dso_local noundef i32 @src2(i32 noundef %0, i32 noundef %1) local_unnamed_addr #0 {
  %3 = sdiv i32 %0, %1
  %4 = mul i32 %3, %1
  %5 = sub i32 %0, %4
  %6 = icmp eq i32 %5, 0
  tail call void @llvm.assume(i1 %6)
  ret i32 %3
}

define dso_local noundef i32 @tgt2(i32 noundef %0, i32 noundef %1) local_unnamed_addr #0 {
  %3 = sdiv exact i32 %0, %1
  ret i32 %3
}
```
</pre>
<img width="1px" height="1px" alt="" src="http://email.email.llvm.org/o/eJzMVV2L4zYU_TXyy2WCfP2R-MEPuw0upbtQyrLzOMj2daJWtrL6SCf764tkO5NNpxTaTimEJL4-Ojr36KIjrJWHiahmxXtW7BPh3VGb-seRxK9ySlrdX-pPRzIE0sKkgYS9wG_iAk7DgSYywhGwkvtenoGeRedYyUGbULPf1D58-PwRfvgZBqNH6Dbw6UiWYPBT56SeLHgbiYS1fiRWcobfQesduGOsX3kGJQ6zGAdyGsgY6mfSgFyWZ-8Y3zO-fB-dO9lQw4Zhc9B9q5XbaHNg2Hxl2Jwfn396TL-YcllU8vnTzc8-Qwj9Pc0acBcKz0Ff-HNhWAHbvp-xALBqwN0zMCzgAizbs2wPnGHFshugIefNBAHWwOX6im33t-plhmBvt5fr9vKNt199uFXzTskzwcloPVxd_tZfERC4Ueo8Lh53tBj9-XuRP368Yw_AudTTICeC3uonpTuhYNJ-6mmIjbKcW9OlS__rG4YFX624qaXBlcjx5KdJjNQ_ib43wDDjN24xLLJgTzzeeZeFL3IsTjEs8ogavVpB2SugIoKsb--Z8pftyoiR3XgC-rLiioDjK5MTUkEnlIKzln3oO1p5PVaZRqJwmssKQ-5F12sj9FfGuoP7d429czZO7p_6-4_lW9PhG8m3_8lg_K8n402t_fuTsV4fSV9nfZVVIqE63WKZbrM8xeRYFyUfBs6HjIusJdq1w65HKvO8y4tym2aJrJFjzqsUkWdlgZtql3Zix3O-S6ttiwPLOY1CqutdlkhrPdUp3-V5lSjRkrIxORFHaS31D_rk5Ci_ipBpDDFEqqnD8ofWH2w4MWmdfSF00imqGyGVNxRCNUbaHxI13Kz3gRoz7zYxE29UfZd10h19u-n0yLCJF-3883Ay-hcKadLElizDZunqXOPvAQAA__9cVz8-">