This is an archive of the discontinued LLVM Phabricator instance.

[ValueTracking] Add logic for `isKnownNonZero(sadd.sat X, Y)`
ClosedPublic

Authored by goldstein.w.n on Apr 27 2023, 11:20 PM.

Details

Summary

The logic here is the same for add so reuse the existing helper
isNonZeroAdd

Alive2 Link:

https://alive2.llvm.org/ce/z/mhKvC5

Diff Detail

Event Timeline

goldstein.w.n created this revision.Apr 27 2023, 11:20 PM
Herald added a project: Restricted Project. · View Herald TranscriptApr 27 2023, 11:20 PM
Herald added a subscriber: hiraditya. · View Herald Transcript
goldstein.w.n requested review of this revision.Apr 27 2023, 11:20 PM
Herald added a project: Restricted Project. · View Herald TranscriptApr 27 2023, 11:20 PM

LGTM. But wait for @nikic.

use new isNonZeroAdd helper and return unconditionally

nikic added inline comments.Apr 29 2023, 10:21 AM
llvm/lib/Analysis/ValueTracking.cpp
2921

I think you can set NSW=true here, based on the following reasoning: If the addition were to overflow, then the result would be either SignedMin or SignedMax, neither of which is zero. As such, we can ignore overflow cases.

goldstein.w.n added inline comments.Apr 29 2023, 10:46 AM
llvm/lib/Analysis/ValueTracking.cpp
2921

I don't think we have NSW I tried:
https://alive2.llvm.org/ce/z/ZBJP5e to see if sadd.sat was a superset and think we might run into some edge cases.
https://alive2.llvm.org/ce/z/9Hz7sn OTOH verifies.

nikic added inline comments.Apr 29 2023, 12:20 PM
llvm/lib/Analysis/ValueTracking.cpp
2921

Here's a variant of your proof that works: https://alive2.llvm.org/ce/z/qFwKbT You need to use logical or in this case.

Alternatively, this one also works: https://alive2.llvm.org/ce/z/6px6Ss

We have to exclude undef due to use count increases, but that's just an artifact of the proof.

Add NSW flag is isNonZeroAdd

goldstein.w.n marked an inline comment as done.Apr 29 2023, 3:11 PM
nikic accepted this revision.Apr 30 2023, 12:52 AM

LGTM

This revision is now accepted and ready to land.Apr 30 2023, 12:52 AM
This revision was landed with ongoing or failed builds.Apr 30 2023, 8:07 AM
This revision was automatically updated to reflect the committed changes.