This is an archive of the discontinued LLVM Phabricator instance.

[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 Timeline

goldstein.w.n created this revision.Apr 25 2023, 2:30 PM
Herald added a project: Restricted Project. · View Herald TranscriptApr 25 2023, 2:30 PM
Herald added a subscriber: hiraditya. · View Herald Transcript
goldstein.w.n requested review of this revision.Apr 25 2023, 2:30 PM
Herald added a project: Restricted Project. · View Herald TranscriptApr 25 2023, 2:30 PM
nikic requested changes to this revision.Apr 26 2023, 12:15 AM

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

llvm/lib/Analysis/ValueTracking.cpp
2778–2782

I found the swapped operand order confusing.

This revision now requires changes to proceed.Apr 26 2023, 12:15 AM

Remove extreneous isknownonzero on X. Cleanup logic. Flip YUleX - >XUgeY

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 edited the summary of this revision. (Show Details)
goldstein.w.n marked an inline comment as done.

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

Bright. Updated title and summary with your alive2 link.

Fix type in comment

nikic accepted this revision.Apr 27 2023, 12:12 AM

LGTM

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
This revision was automatically updated to reflect the committed changes.