Simplify a pattern that may show up when computing the remainder of euclidean division.
Fixes: #64305
Proofs: https://alive2.llvm.org/ce/z/9_KG6c.
Differential D156811
[InstCombine] Fold `select` of `srem` and conditional add antoniofrighetto on Aug 1 2023, 10:14 AM. Authored by
Details Simplify a pattern that may show up when computing the remainder of euclidean division. Fixes: #64305 Proofs: https://alive2.llvm.org/ce/z/9_KG6c.
Diff Detail
Event TimelineComment Actions Didn't manage to generalize the specific pattern out of it, not sure if this can be done here. Comment Actions A note about the proofs. You proved this when the remander is 8, not generically for any power of 2. Proofs with constants should generally look more like: https://alive2.llvm.org/ce/z/9_KG6c
Comment Actions Thanks for reviewing it, and for the note! Updated proofs & changes, and rebased.
Comment Actions Updated & rebased!
Comment Actions @craig.topper, we are still dealing with a SGT as it has not been canonicalized into a SLT, right?
|
Can you remove the NSW from the comment / all the alive2 links. It makes it seem like the nsw is necessary for correctness.