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

    <tr>
        <th>Summary</th>
        <td>
            Missed optimization: fail to infer `c - b != a` under dominating condition `a + b == c`
        </td>
    </tr>

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

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

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

<pre>
    Alive2 proof: https://alive2.llvm.org/ce/z/xWrpYo (generalized)

### Motivating example 

```llvm
define void @src(i32 %a, i32 %b) {
entry:
 %add1 = add i32 %b, %a
  %cmp = icmp eq i32 %add1, 32
  br i1 %cmp, label %return, label %dead

dead: 
  %sub36 = sub i32 32, %b
  %cmp1 = icmp eq i32 %sub36, %a
  br i1 %cmp1, label %then, label %else

then: 
  call void @dummy()
  br label %return

else: 
  call void @dummy1()
  br label %return

return:                                           
  ret void
}
```

can be transformed to

```llvm

define void @tgt(i32 %a, i32 %b) {
entry:
  %add1 = add i32 %b, %a
  %cmp = icmp eq i32 %add1, 32
  br i1 %cmp, label %return, label %else

else:                                     
  call void @dummy1()
  br label %return

return: 
  ret void
}
```
This leads to unoptimized dead code in real-world program.
Canonicalizing `c - b != a` to `a + b == c` would resolve this simple example easily. But for sure, InstCombine cannot handle the real-world multi-use case. Or fixing it in ConstraintElimination could be another alternative.

### Real-world motivation

This snippet of IR is derived from [qemu/tcg/tcg-op.c@tcg_gen_sextract_i32](https://github.com/qemu/qemu/blob/02e16ab9f4f19c4bdd17c51952d70e2ded74c6bf/tcg/tcg-op.c#L1036) (after O3 pipeline).
The example above is a reduced version. If you're interested in the original suboptimal IR and optimal IR, see also:https://godbolt.org/z/8aKo5M9GK

**Let me know if you can confirm that it's an optimization opportunity, thanks.**
</pre>
<img width="1px" height="1px" alt="" src="http://email.email.llvm.org/o/eJzEVs2O2zYQfhr6MrAgkZItHXzw2nURJEGAoEDbU0CRI5kNRSok5V3n6QtSdmJvF2m3KFBDsETN3zczH4fi3qveIG5I9UCq_YJP4Wjd5rfd8bxorTxvtlqdkMLorO0I28IxhNETtiX0QOiBJ2mm9WnIrOsJPQgk9PCV0MPTr2783QKhdY8GHdfqK0pCG5LvSb69_FM2X_DeBnXiQZke8IkPo0a4U1zl8xUjza8kdsognKySQMrcO0ForRgFQitO6A4uzy2hDZD1w2yFJrhzhJ9WSVfKAgjbA5fyxmY3-5nV4rMYxqSm4gN-uapG86jN6FW3daCKi0WUaN6ijmuHYXLm7pVELm_zTGu2hZu4fmrZKkX2U5uiMnqB197DK17Cl8yfp3MLsbgDFI54jxC1x1uESeEGoeBaf2uCnIbhTGj9rc0p1PMC3HhL3n_orXiNu8sbtoV__rt6dhhS5Iu_9f4Z827jCG6gRQiOG99ZN6CEYP-Gry-yNvThX7D2f6ftc1Jc2_iaev9nrX5dA385Kg8aufQQLEzGjkENcTRB3HsgrERQBhxyvXy0Tss4-nrHh2y233FjjRJxnMVhRVa5gCW0QGiRukFWeXRMVjkHQh-ihO2jRETJo520BIfe6hNCiFi8StPuOvWQe6XPGTxMATrrwE8OY-3fGB92dmgjewQ3xgY4ciN19IK3cIdJB7WcfFTzmMEHB516ilhViJntrPHBcWXCT1oNyvCgrAGRgLUI3NhwRAdcB3RReMLs5ZH98SbmZXrbuxalUnujxhED2A7efATlQaJTJ5TQOTsAqR6-4DARegiin_-XdsxE3Bqi_9Sj-eTxKTguwifFKKn2hNb3R1CvwnFqM2EHQg8XZ5dbq21L6CGnWKx423RlVzSibKUs1qIqmorKdY5UolyXYtV2f0VB2bsij-OziecY7wI6-MBgVCNqZZDQJrum-r2DvLUnjJlycCgngRJO6LyyJoM3HZztROjaRZYFdOgDytiW2EXrVK8M13HSJ15yHYvGjYTvy0gGjwhce0vY9lkxrGytDpezOB7DNX9rq_fNz2_vmxivdxhgQPhs7COoBCwyC4Q1nXIDhCMPoAKhaw_cwGWjzHSx42hdmIwK54gnHLn57LPZ7UJumGxYwxe4KdYFrfNyVVeL46ao8mpV52vKkdayWTW8qLu6pZKxVuQNX6gNzWmZl0WRs7wsq4wztmKC5VVViKJcU1LmOHClv31wLJT3E27qmpXVIk0Ln75kKDX4CElIaKTNwm2izbKdek_KXCsf_HcvQQWNm_fKe5R3icb50nGl45ZWpkP38oafjEQH0s7byfSxhlKlSr08CBaT05sf8DgdG_NtOTr7B4pA6CHl42NTY75_BgAA__8Lp9dH">