[PATCH] D110517: [SCEV] Prove implication X <u Y, Y >=s 0 --> X <s Y

[Max Kazantsev via Phabricator via llvm-commits]

mkazantsev created this revision.
mkazantsev added reviewers: reames, nikic, lebedev.ri, fhahn, efriedma.
Herald added a subscriber: hiraditya.
mkazantsev requested review of this revision.
Herald added a project: LLVM.
Herald added a subscriber: llvm-commits.

If we need to prove that `LHS <s RHS`, and we can also prove that
`RHS` is non negative, then it's enough to prove `LHS <u RHS` and
this will imply the fact we need.


https://reviews.llvm.org/D110517

Files:
  llvm/lib/Analysis/ScalarEvolution.cpp
  llvm/test/Transforms/IndVarSimplify/outer_phi.ll


Index: llvm/test/Transforms/IndVarSimplify/outer_phi.ll
===================================================================
--- llvm/test/Transforms/IndVarSimplify/outer_phi.ll
+++ llvm/test/Transforms/IndVarSimplify/outer_phi.ll
@@ -461,9 +461,7 @@
   ret i32 1
 }
 
-
 ; Same as test_01a, but non-negativity of %b is known without context.
-; FIXME: We can remove 2nd check in loop.
 define i32 @test_05a(i32 %a, i32* %bp) {
 ; CHECK-LABEL: @test_05a(
 ; CHECK-NEXT:  entry:
@@ -477,8 +475,7 @@
 ; CHECK-NEXT:    [[SIGNED_COND:%.*]] = icmp ult i32 [[IV]], [[B]]
 ; CHECK-NEXT:    br i1 [[SIGNED_COND]], label [[INNER_1:%.*]], label [[SIDE_EXIT:%.*]]
 ; CHECK:       inner.1:
-; CHECK-NEXT:    [[UNSIGNED_COND:%.*]] = icmp slt i32 [[IV]], [[B]]
-; CHECK-NEXT:    br i1 [[UNSIGNED_COND]], label [[INNER_BACKEDGE]], label [[SIDE_EXIT]]
+; CHECK-NEXT:    br i1 true, label [[INNER_BACKEDGE]], label [[SIDE_EXIT]]
 ; CHECK:       inner.backedge:
 ; CHECK-NEXT:    [[IV_NEXT]] = add nuw nsw i32 [[IV]], 1
 ; CHECK-NEXT:    [[INNER_LOOP_COND:%.*]] = call i1 @cond()
Index: llvm/lib/Analysis/ScalarEvolution.cpp
===================================================================
--- llvm/lib/Analysis/ScalarEvolution.cpp
+++ llvm/lib/Analysis/ScalarEvolution.cpp
@@ -10702,18 +10702,27 @@
     return false;
   }
 
-  // Unsigned comparison is the same as signed comparison when both the operands
-  // are non-negative or negative.
   auto IsSignFlippedPredicate = [](CmpInst::Predicate P1,
                                    CmpInst::Predicate P2) {
     assert(P1 != P2 && "Handled earlier!");
     return CmpInst::isRelational(P2) &&
            P1 == CmpInst::getFlippedSignednessPredicate(P2);
   };
-  if (IsSignFlippedPredicate(Pred, FoundPred) &&
-      ((isKnownNonNegative(FoundLHS) && isKnownNonNegative(FoundRHS)) ||
-       (isKnownNegative(FoundLHS) && isKnownNegative(FoundRHS))))
-    return isImpliedCondOperands(Pred, LHS, RHS, FoundLHS, FoundRHS, CtxI);
+  if (IsSignFlippedPredicate(Pred, FoundPred)) {
+    // Unsigned comparison is the same as signed comparison when both the
+    // operands are non-negative or negative.
+    if ((isKnownNonNegative(FoundLHS) && isKnownNonNegative(FoundRHS)) ||
+        (isKnownNegative(FoundLHS) && isKnownNegative(FoundRHS)))
+      return isImpliedCondOperands(Pred, LHS, RHS, FoundLHS, FoundRHS, CtxI);
+    // TODO: A symmetrical fact should be provable for replacing an unsigned
+    // predicate with signed.
+    if (Pred == ICmpInst::ICMP_SLT || Pred == ICmpInst::ICMP_SLE)
+      if (isKnownNonNegative(RHS))
+        // We need to prove that LHS <s RHS. Knowing that RHS is non-negative,
+        // if we can prove that LHS <u RHS, this will automatically imply the
+        // fact we need.
+        return isImpliedCondOperands(FoundPred, LHS, RHS, FoundLHS, FoundRHS);
+  }
 
   // Check if we can make progress by sharpening ranges.
   if (FoundPred == ICmpInst::ICMP_NE &&


-------------- next part --------------
A non-text attachment was scrubbed...
Name: D110517.375145.patch
Type: text/x-patch
Size: 2946 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/llvm-commits/attachments/20210927/f5ca7886/attachment.bin>