[llvm] [InstCombine] Simplify fractions when there is no overflow (PR #92949)

via llvm-commits llvm-commits at lists.llvm.org
Thu Jun 27 06:41:43 PDT 2024


goldsteinn wrote:

Two further notes about your proofs:
1) This is general (regarding all your proofs across PRs). **Please label your proofs**. Either label the individual links, have a reasonably descriptive function name, or comment them (or all 3!). The way you do it now, where each proof is just a mystery link (and historically has been to completely incorrect/unrelated proofs) adds to reviewer burden. 
2) Make sure your proofs match your implementation, not your goal. I.e in this case you implement the `sdiv` case with `abs`. Your proofs should do that same.

But anyways, here are I *think* correct proofs: https://alive2.llvm.org/ce/z/1failT
The only missing check I see is that `NewC2 != -1` in the `sdiv` case. I think the `C2 != -1` is also gratuitous.
Please check over the proofs, if they make sense, please update your implementation to match their constraints. If you see issues, please update them and post back the corrected proofs (and maybe a correct impl).

https://github.com/llvm/llvm-project/pull/92949


More information about the llvm-commits mailing list