This is an archive of the discontinued LLVM Phabricator instance.

[ConstraintElim] Try to use first cmp to prove second cmp for ANDs.
ClosedPublic

Authored by fhahn on May 31 2023, 6:24 AM.

Details

Summary

This patch extends the existing logic to handle cases where we have
branch conditions of the form (AND icmp, icmp) where the first icmp
implies the second. This can improve results in some cases, e.g. if
SimplifyCFG folded conditions from multiple branches to an AND.

The implementation handles this by adding a new type of check
(AndImpliedCheck), which are queued before conditional facts for the same
block.

When encountering AndImpliedChecks during solving, the first condition
is optimistically added to the constraint system, then we check if the
second icmp can be simplified, and finally the newly added entries are
removed.

The reason for doing things this way is to avoid clashes with signed
<-> unsigned condition transfer, which require us to re-order facts to
increase effectiveness.

Diff Detail

Event Timeline

fhahn created this revision.May 31 2023, 6:24 AM
Herald added a project: Restricted Project. · View Herald TranscriptMay 31 2023, 6:24 AM
fhahn requested review of this revision.May 31 2023, 6:24 AM
Herald added a project: Restricted Project. · View Herald TranscriptMay 31 2023, 6:24 AM

LG! Perhaps worth to add something along these lines?

define i1 @test_icmp_proved_by_previous_icmp(i64 %x, i64 %y, i64 %z) {
  %assumption = icmp sgt i64 %y, %z
  call void @llvm.assume(i1 %assumption)  ; assume y > z
  %1 = icmp sgt i64 %x, %y                ; check if x > y
  %2 = icmp sgt i64 %x, %z                ; check if x > z
  %cond = and i1 %1, %2
  br i1 %cond, label %t1, label %f1

t1:
  ret i1 true

f1:
  ret i1 false
}

As x > z is implied, the second icmp should always be true.

For some reason I didn't see gep-arithmetic-signed-predicates.ll :( Scratch that, signed comparisons seem to be already tested.

antoniofrighetto accepted this revision.Jun 18 2023, 7:04 AM
This revision is now accepted and ready to land.Jun 18 2023, 7:04 AM
nikic added a comment.Jun 18 2023, 7:47 AM

Are you planning to implement the de Morgan conjugate for or as well? I don't like having asymmetric handling for and/or.

llvm/lib/Transforms/Scalar/ConstraintElimination.cpp
802

Given that this is a check, why is this only handled for branch operands and only if we can add a successor? Shouldn't this be handled the same as icmps in the loop above?

1127

Okay, so I guess this is the bit that makes use of the branch -- but I don't really get what this has to do with the and.

We're already going to add both and operands as facts for the branch. The only situation where I would expect this to make a difference if an icmp gets defined outside the branch and used inside the branch, and also just happens to be part of a dominating and.

But this "defined in a different block" situation is a generic problem for constraint elimination, it seems odd to handle it for this specific special case.

antoniofrighetto added a comment.EditedJun 18 2023, 8:00 AM

@nikic, just to say that in D152684 I'm digging into a way to support the disjunction in NE case for the general instance through De-Morgan laws (turning (A>B) || (A<B) into !(!(A>B) && !(A<B))), although I'm not completely sure how the final negation may be performed, once adding the two into the system. Any comments there would be appreciated.

fhahn updated this revision to Diff 534057.Jun 23 2023, 1:09 PM

Rebased on top of D153660 which helps to simplify the implementation.

fhahn marked an inline comment as done.Jun 23 2023, 1:12 PM
fhahn added inline comments.
llvm/lib/Transforms/Scalar/ConstraintElimination.cpp
802

The original intention here was to simplify both the second operand of the AND and then also propagate the fact to true successors.

I shared D153660 which tracks uses of conditions to simplify, which automatically takes care of that part and allows to greatly simplify this patch.

1127

But this "defined in a different block" situation is a generic problem for constraint elimination, it seems odd to handle it for this specific special case.

Agreed, a cleaner way to handle this should be tracking the uses of conditions for simplifications as done in D153660 . That simplifies the code in this patch quite a bit.

fhahn updated this revision to Diff 534490.Jun 26 2023, 3:56 AM
fhahn marked an inline comment as done.

Rebase on latest version of D153660

nikic accepted this revision.Jun 27 2023, 7:10 AM

LGTM

llvm/lib/Transforms/Scalar/ConstraintElimination.cpp
1007

Commit this refactoring separately?

1127

Use ConstantInt::getBool()?

fhahn updated this revision to Diff 535336.Jun 28 2023, 5:06 AM

Rebase on 4b47711ae2ed16014a1b34fb5b4270f5572fd72e which introduced checkCondition, use getBool, thanks!

fhahn marked 2 inline comments as done.Jun 28 2023, 5:07 AM
fhahn added inline comments.
llvm/lib/Transforms/Scalar/ConstraintElimination.cpp
1007
1127

Updated, thanks!

This revision was landed with ongoing or failed builds.Jun 28 2023, 5:21 AM
This revision was automatically updated to reflect the committed changes.
fhahn marked 2 inline comments as done.