Alive2 Link:
https://alive2.llvm.org/ce/z/2DKh46
Paths
| Differential D149203
[ValueTracking] Add logic for `udiv x,y != 0` if `y u<= x` ClosedPublic Authored by goldstein.w.n on Apr 25 2023, 2:30 PM.
Details Summary Alive2 Link: https://alive2.llvm.org/ce/z/2DKh46
Diff Detail
Event Timelinegoldstein.w.n added a child revision: D149204: [ValueTracking] Add logic for `add nuw x,y != 0` -> `x != 0 || y != 0`.Apr 25 2023, 2:31 PM goldstein.w.n added a parent revision: D149202: [ValueTracking] Add logic for `(sub x, y) != 0` if we know `KnownX != KnownY`. Comment Actions I don't think you need the isKnownNonZero() check? If X >= Y and X == 0 then Y == 0, which is UB. https://alive2.llvm.org/ce/z/hw8Gs9 Or maybe even simpler: https://alive2.llvm.org/ce/z/QhiNtE
This revision now requires changes to proceed.Apr 26 2023, 12:15 AM goldstein.w.n retitled this revision from [ValueTracking] Add logic for `udiv x,y != 0` iff `y u<= x` -> `x != 0` to [ValueTracking] Add logic for `udiv x,y != 0` if `y u<= x`.Apr 26 2023, 3:08 PM goldstein.w.n marked an inline comment as done. Comment Actions
Bright. Updated title and summary with your alive2 link. This revision is now accepted and ready to land.Apr 27 2023, 12:12 AM This revision was landed with ongoing or failed builds.Apr 27 2023, 11:48 AM Closed by commit rGd8e9dd33b2a5: [ValueTracking] Add logic for `udiv x,y != 0` if `y u<= x` (authored by goldstein.w.n). · Explain Why This revision was automatically updated to reflect the committed changes.
Revision Contents
Diff 517663 llvm/lib/Analysis/ValueTracking.cpp
llvm/test/Analysis/ValueTracking/known-non-zero.ll
|
I found the swapped operand order confusing.