This is an archive of the discontinued LLVM Phabricator instance.

Differential D149414

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

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

Details

Reviewers
StephenFan
nikic
spatel
Commits
rG167ecdaa2cc3: [ValueTracking] Add logic for `isKnownNonZero(sadd.sat X, Y)`
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

Unit TestsFailed

TimeTest
60,410 msx64 debian > Clang.Driver::arm-cortex-cpus-1.c
60,410 msx64 debian > Clang.Driver::arm-cortex-cpus-2.c

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
Herald added a subscriber: llvm-commits. · View Herald Transcript
Harbormaster completed remote builds in B228734: Diff 517798.Apr 27 2023, 11:21 PM
goldstein.w.n added a parent revision: D149413: [ValueTracking] Add logic for `isKnownNonZero(usub.sat X, Y)`.Apr 27 2023, 11:26 PM
goldstein.w.n added a child revision: D149415: [ValueTracking] Add logic for `isKnownNonZero(umax X, Y)`.
StephenFan added a comment.Apr 29 2023, 1:22 AM

LGTM. But wait for @nikic.

goldstein.w.n updated this revision to Diff 518178.Apr 29 2023, 9:14 AM

use new isNonZeroAdd helper and return unconditionally

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

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
2938

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.

Harbormaster completed remote builds in B229019: Diff 518178.Apr 29 2023, 10:47 AM
goldstein.w.n updated this revision to Diff 518209.Apr 29 2023, 11:42 AM

Rebase

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

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.

Harbormaster completed remote builds in B229045: Diff 518209.Apr 29 2023, 1:33 PM
goldstein.w.n edited parent revisions, added: D149412: [ValueTracking] Add logic for `isKnownNonZero(ssub.sat X, Y)`; removed: D149413: [ValueTracking] Add logic for `isKnownNonZero(usub.sat X, Y)`.Apr 29 2023, 3:03 PM
goldstein.w.n updated this revision to Diff 518247.Apr 29 2023, 3:09 PM

Add NSW flag is isNonZeroAdd

goldstein.w.n marked an inline comment as done.Apr 29 2023, 3:11 PM
Harbormaster completed remote builds in B229079: Diff 518247.Apr 29 2023, 4:41 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
Closed by commit rG167ecdaa2cc3: [ValueTracking] Add logic for `isKnownNonZero(sadd.sat X, Y)` (authored by goldstein.w.n). · Explain Why
This revision was automatically updated to reflect the committed changes.
goldstein.w.n added a commit: rG167ecdaa2cc3: [ValueTracking] Add logic for `isKnownNonZero(sadd.sat X, Y)`.

Revision Contents

PathSize
llvm/
lib/
Analysis/
4 lines
test/
Analysis/
ValueTracking/
5 lines

Diff 518247

llvm/lib/Analysis/ValueTracking.cpp

  • This file is larger than 256 KB, so syntax highlighting is disabled by default.
Show First 20 Lines • Show All 2,926 Lines • ▼ Show 20 Lines if (auto *II = dyn_cast<IntrinsicInst>(I)) {
case Intrinsic::bswap: case Intrinsic::bswap:
case Intrinsic::ctpop: case Intrinsic::ctpop:
if (isKnownNonZero(II->getArgOperand(0), DemandedElts, Depth, Q)) if (isKnownNonZero(II->getArgOperand(0), DemandedElts, Depth, Q))
return true; return true;
break; break;
case Intrinsic::ssub_sat: case Intrinsic::ssub_sat:
return isNonZeroSub(DemandedElts, Depth, Q, BitWidth, return isNonZeroSub(DemandedElts, Depth, Q, BitWidth,
II->getArgOperand(0), II->getArgOperand(1)); II->getArgOperand(0), II->getArgOperand(1));
case Intrinsic::sadd_sat:
return isNonZeroAdd(DemandedElts, Depth, Q, BitWidth,
II->getArgOperand(0), II->getArgOperand(1),
/*NSW*/ true);
nikicUnsubmitted
Not Done
ReplyInline Actions

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.

nikic: I think you can set NSW=true here, based on the following reasoning: If the addition were to…
goldstein.w.nAuthorUnsubmitted
Done
ReplyInline Actions

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.

goldstein.w.n: I don't think we have `NSW` I tried: https://alive2.llvm.org/ce/z/ZBJP5e to see if `sadd.sat`…
nikicUnsubmitted
Done
ReplyInline Actions

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.

nikic: Here's a variant of your proof that works: https://alive2.llvm.org/ce/z/qFwKbT You need to use…
case Intrinsic::uadd_sat: case Intrinsic::uadd_sat:
if (isKnownNonZero(II->getArgOperand(0), DemandedElts, Depth, Q) || if (isKnownNonZero(II->getArgOperand(0), DemandedElts, Depth, Q) ||
isKnownNonZero(II->getArgOperand(1), DemandedElts, Depth, Q)) isKnownNonZero(II->getArgOperand(1), DemandedElts, Depth, Q))
return true; return true;
break; break;
case Intrinsic::cttz: case Intrinsic::cttz:
return computeKnownBits(II->getArgOperand(0), DemandedElts, Depth, Q) return computeKnownBits(II->getArgOperand(0), DemandedElts, Depth, Q)
.Zero[0]; .Zero[0];
▲ Show 20 Lines • Show All 5,759 Lines • Show Last 20 Lines

llvm/test/Analysis/ValueTracking/known-non-zero.ll

Show First 20 Lines • Show All 918 Lines • ▼ Show 20 Lines
} }
define i1 @sadd_sat_nonzero(i8 %xx, i8 %yy, i8 %ind) { define i1 @sadd_sat_nonzero(i8 %xx, i8 %yy, i8 %ind) {
; CHECK-LABEL: @sadd_sat_nonzero( ; CHECK-LABEL: @sadd_sat_nonzero(
; CHECK-NEXT: [[X_STRICT_POS:%.*]] = icmp sgt i8 [[XX:%.*]], 0 ; CHECK-NEXT: [[X_STRICT_POS:%.*]] = icmp sgt i8 [[XX:%.*]], 0
; CHECK-NEXT: [[Y_POS:%.*]] = icmp sge i8 [[YY:%.*]], 0 ; CHECK-NEXT: [[Y_POS:%.*]] = icmp sge i8 [[YY:%.*]], 0
; CHECK-NEXT: call void @llvm.assume(i1 [[X_STRICT_POS]]) ; CHECK-NEXT: call void @llvm.assume(i1 [[X_STRICT_POS]])
; CHECK-NEXT: call void @llvm.assume(i1 [[Y_POS]]) ; CHECK-NEXT: call void @llvm.assume(i1 [[Y_POS]])
; CHECK-NEXT: [[X:%.*]] = call i8 @llvm.sadd.sat.i8(i8 [[XX]], i8 [[YY]]) ; CHECK-NEXT: ret i1 false
; CHECK-NEXT: [[Z:%.*]] = or i8 [[X]], [[IND:%.*]]
; CHECK-NEXT: [[R:%.*]] = icmp eq i8 [[Z]], 0
; CHECK-NEXT: ret i1 [[R]]
; ;
%x_strict_pos = icmp sgt i8 %xx, 0 %x_strict_pos = icmp sgt i8 %xx, 0
%y_pos = icmp sge i8 %yy, 0 %y_pos = icmp sge i8 %yy, 0
call void @llvm.assume(i1 %x_strict_pos) call void @llvm.assume(i1 %x_strict_pos)
call void @llvm.assume(i1 %y_pos) call void @llvm.assume(i1 %y_pos)
%x = call i8 @llvm.sadd.sat.i8(i8 %xx, i8 %yy) %x = call i8 @llvm.sadd.sat.i8(i8 %xx, i8 %yy)
%z = or i8 %x, %ind %z = or i8 %x, %ind
%r = icmp eq i8 %z, 0 %r = icmp eq i8 %z, 0
▲ Show 20 Lines • Show All 181 Lines • Show Last 20 Lines