[SCEV] Prove implication of predicates to their sign-flipped counterparts

[mkazantsev]

Summary

This patch teaches SCEV two implication rules:

x <u y && y >=s 0 --> x <s y,
x <s y && y <s 0 --> x <u y.

And all equivalents with signs/parts swapped.

[nikic]

llvm/lib/Analysis/ScalarEvolution.cpp

10725

This looks correct to me, but also rather ad-hoc -- it handles one out of multiple symmetrical patterns. For example, if we just swap both predicates (Pred == SGT and non-negative LHS) this will not trigger anymore. Or did that already get canonicalized away (in which case we should test it)?

[reames]

llvm/lib/Analysis/ScalarEvolution.cpp

10725

In line with the point Nikita makes, there's also an interesting case we should handle when RHS is known negative. In that case, ult A, B && A < 0 is enough to prove slt A, B. What's interesting to me is that we've already paid the cost of determining if A is known negative, so this becomes just a canonicalization.

All of this is building on the equivalence:
SLT A, B == (ULT A, B && signof(A) == signof(B)) || (A < 0 && B > 0)

(Note that ULT A, B + B > 0 => A > 0.)

Thinking about all this, it feels unfortunate that we're dropping to implication instead of rewriting based on equivalence. At the same time though, I don't really see an obvious code structure to use the equivalence fact though, so maybe there's nothing we can do on that front.

[mkazantsev]

llvm/lib/Analysis/ScalarEvolution.cpp

10725

As for canonicalization, we try to canonicalize so that LHS matched FoundLHS or RHS matched FoundRHS, and we also try to move constant to right hand side. So in practice, I think in some cases it will be canonicalized so that constant (which is surely a known (non) negative) will be in RHS, but it's not guaranteed for all cases. I'll add more tests to see how it reacts on different equivalent code patterns, and if it's not general enough, I'll try to make the logic smarter.

[mkazantsev]

Generalized as widely as I could, now this covers all varieties of these.

[mkazantsev]

Ping

[nikic]

LGTM

llvm/lib/Analysis/ScalarEvolution.cpp

10729

Is this malicious compliance? ^^

[mkazantsev]

llvm/lib/Analysis/ScalarEvolution.cpp

10729

It's full-scaled paranoia! :)

llvm/lib/Analysis/ScalarEvolution.cpp

if (!FoundLHS->getType()->isPointerTy() &&
         !FoundRHS->getType()->isPointerTy() &&
         isImpliedCondOperands(Pred, LHS, RHS, getNotSCEV(FoundLHS),
                               getNotSCEV(FoundRHS), CtxI))
       return true;
 
     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))))
+  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 &&
       (isa<SCEVConstant>(FoundLHS) || isa<SCEVConstant>(FoundRHS))) {
 
     const SCEVConstant *C = nullptr;
     const SCEV *V = nullptr;
 
     if (isa<SCEVConstant>(FoundLHS)) {
       C = cast<SCEVConstant>(FoundLHS);
       V = FoundRHS;
     } else {

llvm/test/Transforms/IndVarSimplify/outer_phi.ll

 
 side.exit:
   ret i32 0
 
 exit:
   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:
 ; CHECK-NEXT:    [[B:%.*]] = load i32, i32* [[BP:%.*]], align 4, !range [[RNG0]]
 ; CHECK-NEXT:    br label [[OUTER:%.*]]
 ; CHECK:       outer:
 ; CHECK-NEXT:    [[OUTER_IV:%.*]] = phi i32 [ 0, [[ENTRY:%.*]] ], [ [[IV_NEXT_LCSSA:%.*]], [[OUTER_BACKEDGE:%.*]] ]
 ; CHECK-NEXT:    br label [[INNER:%.*]]
 ; CHECK:       inner:
 ; CHECK-NEXT:    [[IV:%.*]] = phi i32 [ [[OUTER_IV]], [[OUTER]] ], [ [[IV_NEXT:%.*]], [[INNER_BACKEDGE:%.*]] ]
 ; 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()
 ; CHECK-NEXT:    br i1 [[INNER_LOOP_COND]], label [[INNER]], label [[OUTER_BACKEDGE]]
 ; CHECK:       outer.backedge:
 ; CHECK-NEXT:    [[IV_NEXT_LCSSA]] = phi i32 [ [[IV_NEXT]], [[INNER_BACKEDGE]] ]
 ; CHECK-NEXT:    [[OUTER_LOOP_COND:%.*]] = call i1 @cond()
 ; CHECK-NEXT:    br i1 [[OUTER_LOOP_COND]], label [[OUTER]], label [[EXIT:%.*]]