[ValueTracking] Infer relationship for the select with ICmp #66668

vfdff · 2023-09-18T16:20:03Z

x -nsw y < C is false when x > y and C <= 0
Alive2 proof for sgt, sge, ugt, uge : https://alive2.llvm.org/ce/z/tupvfi

Fixes #54735

llvmbot · 2023-09-18T16:21:44Z

@llvm/pr-subscribers-llvm-transforms

@llvm/pr-subscribers-llvm-analysis

Changes

x-y+1 is positive when x > y, so abs (x-y+1) --> x-y+1

Fixes #54735

Full diff: https://github.com/llvm/llvm-project/pull/66668.diff

2 Files Affected:

(modified) llvm/lib/Analysis/InstructionSimplify.cpp (+25)
(added) llvm/test/Transforms/InstSimplify/select-icmp.ll (+33)

diff --git a/llvm/lib/Analysis/InstructionSimplify.cpp b/llvm/lib/Analysis/InstructionSimplify.cpp
index 5fe0d53c313d40e..ecb261716cb71fb 100644
--- a/llvm/lib/Analysis/InstructionSimplify.cpp
+++ b/llvm/lib/Analysis/InstructionSimplify.cpp
@@ -4547,6 +4547,20 @@ static Value *simplifySelectWithICmpEq(Value *CmpLHS, Value *CmpRHS,
   return nullptr;
 }
 
+/// Return nullptr if the comparison relationship of X and Y can't be inferred.
+static Value *simplifySelectWithICmpKnownRelation(ICmpInst::Predicate Pred,
+                                                  Value *CmpLHS, Value *CmpRHS,
+                                                  Value *TrueVal,
+                                                  Value *FalseVal,
+                                                  const SimplifyQuery &Q) {
+  if (std::optional<bool> Flag =
+          isImpliedByDomCondition(Pred, CmpLHS, CmpRHS, Q.CxtI, Q.DL)) {
+    if (Flag)
+      return *Flag ? TrueVal : FalseVal;
+  }
+  return nullptr;
+}
+
 /// Try to simplify a select instruction when its condition operand is an
 /// integer comparison.
 static Value *simplifySelectWithICmpCond(Value *CondVal, Value *TrueVal,
@@ -4669,6 +4683,17 @@ static Value *simplifySelectWithICmpCond(Value *CondVal, Value *TrueVal,
     }
   }
 
+  if (Pred == ICmpInst::ICMP_SLT) {
+    Value *X;
+    Value *Y;
+    const APInt *C;
+    // x-y+1 is positive when x >= y or non-positive when x < y
+    if (match(CmpLHS, m_NSWSub(m_Value(X), m_Value(Y))) &&
+        match(CmpRHS, m_AllOnes()))
+      return simplifySelectWithICmpKnownRelation(ICmpInst::ICMP_SLT, X, Y,
+                                                 TrueVal, FalseVal, Q);
+  }
+
   return nullptr;
 }
 
diff --git a/llvm/test/Transforms/InstSimplify/select-icmp.ll b/llvm/test/Transforms/InstSimplify/select-icmp.ll
new file mode 100755
index 000000000000000..1271941565d9dc3
--- /dev/null
+++ b/llvm/test/Transforms/InstSimplify/select-icmp.ll
@@ -0,0 +1,33 @@
+; NOTE: Assertions have been autogenerated by utils/update_test_checks.py
+; RUN: opt < %s -passes=instsimplify -S | FileCheck %s
+
+; https://alive2.llvm.org/ce/z/zKX64J
+define i32 @pr54735(i32 noundef %x, i32 noundef %y) {
+; CHECK-LABEL: @pr54735(
+; CHECK-NEXT:  entry:
+; CHECK-NEXT:    [[CMP:%.*]] = icmp sgt i32 [[X:%.*]], [[Y:%.*]]
+; CHECK-NEXT:    br i1 [[CMP]], label [[COND_TRUE:%.*]], label [[COND_END:%.*]]
+; CHECK:       cond.true:
+; CHECK-NEXT:    [[SUB:%.*]] = sub nsw i32 [[X]], [[Y]]
+; CHECK-NEXT:    [[ADD:%.*]] = add nsw i32 [[SUB]], 1
+; CHECK-NEXT:    br label [[COND_END]]
+; CHECK:       cond.end:
+; CHECK-NEXT:    [[COND:%.*]] = phi i32 [ [[ADD]], [[COND_TRUE]] ], [ 0, [[ENTRY:%.*]] ]
+; CHECK-NEXT:    ret i32 [[COND]]
+;
+entry:
+  %cmp = icmp sgt i32 %x, %y
+  br i1 %cmp, label %cond.true, label %cond.end
+
+cond.true:                                        ; preds = %entry
+  %sub = sub nsw i32 %x, %y
+  %add = add nsw i32 %sub, 1
+  %neg = xor i32 %sub, -1                         ; sub nsw i32 0, %add
+  %abscond = icmp slt i32 %sub, -1
+  %abs = select i1 %abscond, i32 %neg, i32 %add
+  br label %cond.end
+
+cond.end:                                         ; preds = %entry, %cond.true
+  %cond = phi i32 [ %abs, %cond.true ], [ 0, %entry ]
+  ret i32 %cond
+}

llvm/test/Transforms/InstSimplify/select-icmp.ll

llvm/lib/Analysis/InstructionSimplify.cpp

nikic

I believe this needs to be handled in isImpliedCondition. There is already existing code that will simplify implications from dominating conditions.

Though really, this seems like something that ConstraintElimination should handle, not InstSimplify.

nikic

Please add an alive2 proof to the patch description. This should also needs additional tests (preferably more minimal than the example you added), e.g. that this does not fold without nsw, wrong constant, etc.

llvm/lib/Analysis/ValueTracking.cpp

vfdff · 2023-09-21T14:24:28Z

Please add an alive2 proof to the patch description. This should also needs additional tests (preferably more minimal than the example you added), e.g. that this does not fold without nsw, wrong constant, etc.

Thanks, Added alive2 proof link and 2 extra negative test cases.

vfdff · 2023-09-28T01:18:39Z

ping ?

llvm/lib/Analysis/ValueTracking.cpp

github-actions · 2023-10-17T04:30:16Z

✅ With the latest revision this PR passed the C/C++ code formatter.

llvm/lib/Analysis/ValueTracking.cpp

vfdff · 2023-11-04T08:25:34Z

revert the change for x -nsw y <= -1 <==> x < y because sle -1 will get canonicalized to slt 0, so should consider other way to address that.

llvm/lib/Analysis/ValueTracking.cpp

llvm/test/Transforms/InstSimplify/select-icmp.ll

vfdff · 2023-11-22T08:18:33Z

ping ?

llvm/lib/Analysis/ValueTracking.cpp

goldsteinn · 2023-11-22T17:01:10Z

llvm/lib/Analysis/ValueTracking.cpp

@@ -8294,6 +8294,17 @@ static std::optional<bool> isImpliedCondICmps(const ICmpInst *LHS,
  if (areMatchingOperands(L0, L1, R0, R1, AreSwappedOps))
    return isImpliedCondMatchingOperands(LPred, RPred, AreSwappedOps);

+  if (LPred == ICmpInst::ICMP_SGT) {


Should also handle the less-than variant no?

hi @goldsteinn
I reverted the change for less-than because the commit #66668 (review), so I think it may be addressed with some other method.
If you don't object, I think it is fine to keep this PR to fix the issue in the comment link.

vfdff · 2023-12-05T10:09:08Z

rebase to fix the conflict to commit 460faa0

vfdff · 2023-12-08T03:17:59Z

ping ?

PR Link: llvm/llvm-project#66668

dtcxzyw

The implementation LGTM. But it would be good to support more predicates (slt/ult).

Please wait for additional approval from other reviewers.

llvm/lib/Analysis/ValueTracking.cpp

vfdff · 2023-12-30T02:54:54Z

The implementation LGTM. But it would be good to support more predicates (slt/ult).

Please wait for additional approval from other reviewers.
Thanks for your notification, I'll follow to address slt/ult after this PR is accepted.

vfdff · 2023-12-30T02:57:02Z

hi @nikic, would you help to give some suggestion on this PR ?

vfdff · 2024-02-04T03:18:45Z

ping ?

vfdff · 2024-03-09T07:16:08Z

If there's no objection, I'll take a try for this commit in the next week?

PR Link: llvm/llvm-project#66668

dtcxzyw · 2024-03-09T07:59:42Z

Ping @nikic @goldsteinn

llvm/lib/Analysis/ValueTracking.cpp

goldsteinn · 2024-03-09T16:21:02Z

llvm/lib/Analysis/ValueTracking.cpp

+    if (match(R1, m_NonPositive()) &&
+        areMatchingOperands(L0, L1, X, Y, AreSwappedOps) &&
+        isImpliedCondMatchingOperands(LPred, RPred, AreSwappedOps) == false)
+      return false;


you could handle SLT/SLE/ULT/ULE as true here no?

hi @dtcxzyw, @goldsteinn
I add the addressing for SLT/SLE/ULT/ULE now, thanks

goldsteinn · 2024-06-01T17:47:01Z

llvm/lib/Analysis/ValueTracking.cpp

+    if (match(R1, m_NonNegative()) && (L0 == X && L1 == Y) &&
+        isImpliedCondMatchingOperands(LPred, RPred) == true)
+      return true;
+  }


Both here and above, instead of m_Value(X)/m_Value(Y), how about m_Specific(L0)/m_Specific(L1)?

Apply your comment, thanks

goldsteinn · 2024-06-01T17:49:29Z

llvm/lib/Analysis/ValueTracking.cpp

+  if (((LPred == ICmpInst::ICMP_SGT || LPred == ICmpInst::ICMP_SGE) &&
+       match(R0, m_NSWSub(m_Value(X), m_Value(Y)))) ||
+      ((LPred == ICmpInst::ICMP_UGT || LPred == ICmpInst::ICMP_UGE) &&
+       match(R0, m_NUWSub(m_Value(X), m_Value(Y))))) {


Here and below, don't think you need nuw for the sub. Its implied by LPred.

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

Actually I misspoke, but I don't think your proofs are correct. The nuw on the sub nuw i8 0, %add forces %add to be 0. Likewise the sub nuw i8 %sub, %c essentially forces the condition you want, not the dominating predicates.

Thanks @goldsteinn , If this only valid for 0 with nuw, so the transformation of unsigned should be deleted (only keep it for signed types) ? or do you have other suggestion ？

Yeah, unsigned doesn't make sense here. The is really saying "X - Y must be positive if X >= Y and no overflow". That only really makes sense in the context of signed comparison.

Thanks for the confirmation, and delete the parts of unsigned.

goldsteinn · 2024-06-05T19:25:27Z

llvm/test/Transforms/InstSimplify/select-icmp.ll

+  ret i8 %abs
+
+cond.end:                                         ; preds = %entry, %cond.true
+  ret i8 0


You can drop the unsigned tests.

Apply your comments, thanks @goldsteinn

x-y+1 is positive when x > y, so abs (x-y+1) --> x-y+1 Fixes llvm#54735

x -nsw y < -C is false when x > y and C >= 0 Alive2 proof for sgt, sge : https://alive2.llvm.org/ce/z/tupvfi Note: It only really makes sense in the context of signed comparison for "X - Y must be positive if X >= Y and no overflow". Fixes llvm#54735

goldsteinn · 2024-06-06T05:51:08Z

llvm/lib/Analysis/ValueTracking.cpp

+    if (match(R1, m_NonPositive()) &&
+        isImpliedCondMatchingOperands(LPred, RPred) == false)
+      return false;
+  }


Is this right for sge if C == 0? Your proofs checkout but afaict its b.c your proof is using X != -X to handle the false case which has problems with this case...

Does the link https://alive2.llvm.org/ce/z/N4uvTh proof it is valid for sge with C == 0 ?

I made a mistake think this is okay.

goldsteinn · 2024-06-06T16:31:43Z

LGTM. Please wait for an additional approval

vfdff · 2024-06-07T03:44:42Z

LGTM. Please wait for an additional approval
Thank very much for your reviewing

llvmbot added llvm:analysis llvm:transforms labels Sep 18, 2023

goldsteinn reviewed Sep 18, 2023

View reviewed changes

llvm/test/Transforms/InstSimplify/select-icmp.ll Show resolved Hide resolved

llvm/lib/Analysis/InstructionSimplify.cpp Outdated Show resolved Hide resolved

nikic requested changes Sep 18, 2023

View reviewed changes

vfdff force-pushed the PR54735 branch from fe146fc to 343af0a Compare September 19, 2023 08:21

nikic reviewed Sep 19, 2023

View reviewed changes

llvm/lib/Analysis/ValueTracking.cpp Outdated Show resolved Hide resolved

vfdff force-pushed the PR54735 branch from 343af0a to 5551b33 Compare September 21, 2023 14:20

vfdff requested review from nikic and goldsteinn October 7, 2023 16:53

vfdff requested a review from dtcxzyw October 15, 2023 09:04

dtcxzyw requested changes Oct 15, 2023

View reviewed changes

llvm/lib/Analysis/ValueTracking.cpp Outdated Show resolved Hide resolved

vfdff force-pushed the PR54735 branch from 5551b33 to ca94b99 Compare October 17, 2023 04:19

nikic reviewed Oct 17, 2023

View reviewed changes

llvm/lib/Analysis/ValueTracking.cpp Outdated Show resolved Hide resolved

vfdff force-pushed the PR54735 branch from ca94b99 to 2af469e Compare October 20, 2023 01:07

vfdff requested a review from nikic October 20, 2023 06:53

vfdff force-pushed the PR54735 branch from 2af469e to 781dc7f Compare November 4, 2023 08:24

vfdff requested a review from dtcxzyw November 7, 2023 03:19

dtcxzyw reviewed Nov 11, 2023

View reviewed changes

llvm/lib/Analysis/ValueTracking.cpp Outdated Show resolved Hide resolved

dtcxzyw reviewed Nov 11, 2023

View reviewed changes

llvm/test/Transforms/InstSimplify/select-icmp.ll Outdated Show resolved Hide resolved

vfdff force-pushed the PR54735 branch from 781dc7f to 1ffe54e Compare November 13, 2023 14:26

vfdff requested review from dtcxzyw and preames November 13, 2023 14:27

goldsteinn reviewed Nov 22, 2023

View reviewed changes

llvm/lib/Analysis/ValueTracking.cpp Outdated Show resolved Hide resolved

goldsteinn reviewed Nov 22, 2023

View reviewed changes

dtcxzyw added a commit to dtcxzyw/llvm-opt-benchmark that referenced this pull request Dec 29, 2023

pre-commit: test PR66668

1b5f42b

PR Link: llvm/llvm-project#66668

dtcxzyw mentioned this pull request Dec 29, 2023

pre-commit: test PR66668 dtcxzyw/llvm-opt-benchmark#67

Closed

dtcxzyw approved these changes Dec 29, 2023

View reviewed changes

llvm/lib/Analysis/ValueTracking.cpp Outdated Show resolved Hide resolved

vfdff force-pushed the PR54735 branch from 358cc40 to f442760 Compare December 30, 2023 02:50

dtcxzyw added a commit to dtcxzyw/llvm-opt-benchmark that referenced this pull request Mar 9, 2024

pre-commit: test PR66668

2e169e9

PR Link: llvm/llvm-project#66668

dtcxzyw mentioned this pull request Mar 9, 2024

pre-commit: test PR66668 dtcxzyw/llvm-opt-benchmark#345

Closed

goldsteinn reviewed Mar 9, 2024

View reviewed changes

llvm/lib/Analysis/ValueTracking.cpp Show resolved Hide resolved

goldsteinn reviewed Mar 9, 2024

View reviewed changes

vfdff force-pushed the PR54735 branch 2 times, most recently from 5aa207b to 8a732dc Compare June 1, 2024 09:42

dtcxzyw requested a review from goldsteinn June 1, 2024 14:17

goldsteinn reviewed Jun 1, 2024

View reviewed changes

preames removed their request for review June 4, 2024 15:49

vfdff force-pushed the PR54735 branch from 8a732dc to 0dacae0 Compare June 5, 2024 02:25

goldsteinn reviewed Jun 5, 2024

View reviewed changes

vfdff added 3 commits June 6, 2024 09:24

[tests] precommit tests for ValueTracking

80aa88f

x-y+1 is positive when x > y, so abs (x-y+1) --> x-y+1 Fixes llvm#54735

[ValueTracking] Infer relationship for the select with SLT

aff2a17

vfdff force-pushed the PR54735 branch from 0dacae0 to aff2a17 Compare June 6, 2024 01:25

goldsteinn reviewed Jun 6, 2024

View reviewed changes

[ValueTracking] Infer relationship for the select with ICmp #66668

Are you sure you want to change the base?

[ValueTracking] Infer relationship for the select with ICmp #66668

Conversation

vfdff commented Sep 18, 2023 • edited

llvmbot commented Sep 18, 2023 • edited

nikic left a comment

Choose a reason for hiding this comment

nikic left a comment

Choose a reason for hiding this comment

vfdff commented Sep 21, 2023

vfdff commented Sep 28, 2023

github-actions bot commented Oct 17, 2023 • edited

vfdff commented Nov 4, 2023

vfdff commented Nov 22, 2023

Choose a reason for hiding this comment

Choose a reason for hiding this comment

vfdff commented Dec 5, 2023

vfdff commented Dec 8, 2023

dtcxzyw left a comment

Choose a reason for hiding this comment

vfdff commented Dec 30, 2023

vfdff commented Dec 30, 2023

vfdff commented Feb 4, 2024

vfdff commented Mar 9, 2024

dtcxzyw commented Mar 9, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

goldsteinn commented Jun 6, 2024

vfdff commented Jun 7, 2024

vfdff commented Sep 18, 2023 •

edited

llvmbot commented Sep 18, 2023 •

edited

github-actions bot commented Oct 17, 2023 •

edited