[ScalarEvolution] Predicate implication from operations

[mkazantsev]

Summary

This patch allows SCEV predicate analysis to prove implication of some expression predicates
from context predicates related to arguments of those expressions.

It introduces three new rules:

For addition:

1. (A >X && B >= 0) || (B >= 0 && A > X) ===> (A + B) > X.

For division:

1. (A > X) && (0 < B <= X + 1) ===> (A / B > 0).
2. (A > X) && (-B <= X < 0) ===> (A / B >= 0).

Using these rules, SCEV is able to prove facts like "if X > 1 then X / 2 > 0".
They can also be combined with the same context, to prove more complex expressions like
"if X > 1 then X/2 + 1 > 1".

[sanjoy]

Hi Maxim,

First of all, great work!

Can you try to split this change up into the addition transform (which, as I said inline, probably makes sense to put in ScalarEvolution::isKnownPredicateViaNoOverflow) and the division transform? If one depends one the other, then we can just put denote the dependencies on phabricator, and check them in in the right order.

Other than that I have a few comments inline and here:

This rule seems a bit restrictive:

(A > X) && (B > X) && (A >= 0 || B >= 0) ===> (A + B) > X.

Why not:

(A >= 0 && B > X) ==> ((A +nsw B) > X?

(and the symmetric variant with A and B swapped)?

I've not checked if the code matches the commit message, but in

(A > X) && (-B <= X < 0) ===> (A / B > 0), what if X is -10, A is -5 and B is 10? Won't A / B be 0 then?

lib/Analysis/ScalarEvolution.cpp

8501

The usual way to do this is

if (Pred == ICmpInst::ICMP_SLT) {
  Pred = ICmpInst::ICMP_SGT;
  std::swap(LHS, RHS);
  std::swap(FoundLHS, FoundRHS);
}

Actually, you should not need to do this. ScalarEvolution::isImpliedCond should be handling this case for you.

8513

There already is getNoopOrSignExtend that does the same thing.

8519

Use getTypeSizeInBits(S1->getType()) instead, that will do the right thing for pointer types.

8531

Don't call it Operation, that name says nothing about where the value came from and what it represents. For a small scope I would not mind Operation, but this scope is more than a few lines long. I'd go with something more mnemonic, like AddExprLHS or LHSAddExpr.

8532

Did you consider putting this logic in ScalarEvolution::isKnownPredicateViaNoOverflow?

8535

Similarly, good names for these would be LL ("LHS of LHS"), and RL ("RHS of LHS").

8540

Use getZero(RHS->getType()).

8551

This is probably too expensive to put in here (at the very least, this is risky from a compile time perspective). How far can we get just by looking at the ranges for each of the inputs (i.e. via calling getRange and doing some manipulations on the returned ranges)?

8559

Same comment w.r.t. naming -- let's call it something more specific than Operation.

8565

Let's avoid creating SCEV expressions here (via getSCEV or getAddExpr). One problem is that it may be a compile time hit. They can also cause use to compute overly conservative trip counts, since this call to isImpliedViaOperations may have itself been done during a trip count computation, and invoking getSCEV may try to (recursively) compute the trip count of the same loop again which would cache a conservative SCEVCouldNotCompute (to avoid recursing infinitely).

[mkazantsev]

Hi Sanjoy!

Thank you for review and detailed comment, I will try to address them all soon as I can!

Why not:
(A >= 0 && B > X) ==> ((A +nsw B) > X?

Good catch!

(A > X) && (-B <= X < 0) ===> (A / B > 0), what if X is -10, A is -5 and B is 10? Won't A / B be 0 then?

Thanks for pointing out, actuall the commit message is wrong. It should be "A / B >= 0". Line 8590 checks that RHS should be negative.

[mkazantsev]

lib/Analysis/ScalarEvolution.cpp

8501

I will check this. If you are right, checking "less" cases in switch of ScalarEvolution::isImpliedCondOperandsHelper seems redundant.

[mkazantsev]

lib/Analysis/ScalarEvolution.cpp

8501

This is not true, we sometimes have "less" conditions at this point.

8532

Actually isKnownPredicateViaNoOverflow already does a particular case of it, which is "X + C > X if C > 0". The point here is that I need the context of FoundLHS and FounrRHS for further proofs. For example, I want to prove thing like "1 + n / 2 > 1 if n > 1". The rule which is used in isKnownPredicateViaNoOverflow does not work here, because n/2 does not match with 0 or 1. It also is unable to prove that n/2 > 0, because for this we need the proof via operation that uses context.

For the same reason I don't want to split this into two patches, because the only real benefit of the rule for addition is that it can recursively invoke the rule for division with the same context, and vice versa. Without the division rule, this addition work simply duplicates the logic of "isKnownPredicateViaNoOverflow".

I have removed "isKnownPredicate" invocation from here to avoid potential recursion, replacing it with more light-weight check. But we cannot move it out of here due to this context restriction.

8551

Ok, I got rid of recursive checks.

8565

I have removed the call of "isKnownPredicate" that might request recursive recalculation of the same trip count; now we use more light-weight check that used to be "IsKnownPredicateFull" lambda. So now this problem should have gone.

As for the compile time issue, what is the alternative to using SCEV for Num/Denum/FoundRHS+ 1?

[sanjoy]

Hi Max,

I have some more comments. This time I was not able to be as thorough as I wanted to be (got busy with other things during the day, and now it is bed time :) ), but hopefully whatever comments I have will let you make some progress.

lib/Analysis/ScalarEvolution.cpp

8527

Can we get what we want here without sign extension? As I've said below, sign extension can be expensive.

In fact, it would be surprising if we see LHS is not the same as OrigLHS since that would mean a sext (%a + %b)<nsw> did not get transformed to (sext %a + sext %b)<nsw> as per the rule in ScalarEvolution::getSignExtendExpr. That situation is possible, but should be rare.

8530

Add a one liner above this stating what this function is checking for. If you can give it a better name then that would be even better.

8532

I may have missed it, but I did not see (in the current version of the patch) where the division case calls into the addition case.

The addition case calling into the division case is fine, but I want to avoid "arbitrary recursion" by recursively calling into isImpliedCondOperandsHelper. Can you structure the code in a way that that doesn't happen? Maybe extract out the division case into a separate function that you directly call from here?

8549

This seems general enough to me that we should put this on ScalarEvolution itself, as Type *ScalarEvolution::getWiderType(Type *, Type *). It also makes isImpliedViaOperations less cluttered.

8558

Sign extending has the same problem as calling getSCEV (as you can probably tell from looking at ScalarEvolution::getSignExtendExpr, it can do a lot of work in the worst case). It isn't terrible because SCEV will cache the result in most cases once it has computed it, but we should try very hard to not call it so deep in the stack.

8565

One possibility would be to put the actual core of the logic in llvm::isImpliedCondition (which is in ValueTracking), and then try to call into that helper from there.

That is, say the antecedent is (sext i16 %t to i32) s< i32 44 and the consequent is %s != 400. We could then ask ValueTracking llvm::isImpliedCondition(i16 %t s< i16 44, %s != 400) [0] and return whatever ValueTracking told us.

We will probably need to generalize the interface of ValueTracking's llvm::isImpliedCondition a bit though, but that should be fine.

[0] Using the fact that (sext(A) s< sext(B)) == A s< B.

[mkazantsev]

lib/Analysis/ScalarEvolution.cpp

8527

Why is it rare? We can calculate sdiv i32 %a, %b and than use it in multiple ways, one of them being comparison to an i64 constant. In this case we will see exactly this.

[sanjoy]

lib/Analysis/ScalarEvolution.cpp

8527

Maybe we're misinterpreting each other, but I was specifically talking about this SCEVAddExpr case. That is, I'd be surprised if all of the following are simultaneously true:

• LHS is a SCEVAddExpr marked as NSW
• FoundLHS was a SCEVSignExtendExpr with LHS as its operand

because if they were, I'd have expected the sign extend to have been have been commuted to inside the add expression.

[mkazantsev]

lib/Analysis/ScalarEvolution.cpp

8527

Sorry, I misinterpreted it. Yes, this can be removed, I think.

[mkazantsev]

lib/Analysis/ScalarEvolution.cpp

8565

I noticed that Num never needs a new SCEV creation in good case, because all we want is to prove that it's SCEV is actually FoundLHS. thus, it and some type conversions have gone.

Now we only have SCEV creation left for Denum-related stuff (such as constructing -Denum and Denum + 1). Here I believe that we cannot get rid of it, because for using implied conditions interfaces we will have to construct those sum and neg in terms of values if not in terms of SCEVs.

To avoid reculsive recalculations in this last case, let's just reduce the scope of the optimization to Denum being a constant. In this case creating Denum+1, -Denum or type extensions will only require constants creation, and there is a very high chance that these contant SCEVs already exist.

[mkazantsev]

Addressed Sanjoy's comments. Made some generalization. Division rule now works for constant denumerator only to avoid recursive invocation of the analysis for the same loop.

[mkazantsev]

Minor type mismatch bug fix.

[sanjoy]

One more round of comments.

lib/Analysis/ScalarEvolution.cpp

8508

This should be called GetOpFromSExt.

8523

Can we avoid the recursion via isImpliedCondOperandsHelper?

8523

Why not just

return IsProvedViaContext(ICmpInst::ICMP_SGE, S1, getZero(RHS->getType()))) && IsProvedViaContext(Pred, S2, RHS);

?

Please also avoid using Pred in the second call to IsProvedViaContext, but use a literal ICmpInst::ICMP_SGT instead.

8555

This is minor, and I'll understand if you don't want to change it, but let's call Num Numerator. Num is too ambiguous -- it can also mean Number for instance.

Paradoxically, I think N and D is less ambiguous than Num and Denum. :)

I'd also call Denum Denom if you must use an abbreviation, since the full spelling is Denominator.

8565

Your point is solid.

What do you think about creating a helper called (say) isSCEVSameAsValue(const SCEV *, const Value *) that checks cheaply (i.e. without creating new SCEV expressions) if a SCEV * and Value * compute the same thing at runtime? It would have to be best effort, but that's fine for now.

You can use this getExistingSCEV trick in that helper, and also use ExprValueMap to do the inverse.

8570

Any reason why you need to check Denum <= FoundRHS + 1 instead of Denum < FoundRHS? Since FoundRHS < FoundLHS, FoundRHS + 1 can't sign overflow, so the above two should be equivalent with Denum < FoundRHS being (slightly) faster since we're not adding.

Can you also add one or two lines of comment as an informal proof on why this is correct?

Same for the second rule.

[mkazantsev]

lib/Analysis/ScalarEvolution.cpp

8570

Imagine Denum = 3, FoundRHS = 2. Denum <= FoundRHS + 1 is true, but Denum < FoundRHS is false. These two are not equivalent.

For example given that FoundRHS = 2. The given fact FoundLHS > 2 means that FoundLHS is at least 3. Then we can prove that FoundLHS / (2 + 1) is at least one. If we used you rule, we could only prove that FoundLHS / 1 > 0, which is a weaker statement.

I will add a comment on that proof.

[sanjoy]

lib/Analysis/ScalarEvolution.cpp

8549

It might be better to do auto *Denum = cast<SCEVConstant>(getSCEV(LR)).

8570

Yes, you're right -- they're not equivalent. I think I confused it with Denum + 1 <= FoundRHS.

On the other hand, can we write the condition as (Denum - 1) <= FoundRHS? Again, we know that Denum - 1 won't sign overflow, and computing (Denum - 1) may be faster than computing FoundRHS + 1 because Denum is a constant.

[mkazantsev]

Addressed Sanjoy's new comments.

lib/Analysis/ScalarEvolution.cpp

8523

That's the point of the optimization! Sometimes we cannot simply prove that (a + b > c), but can do it via the context passed from division. And vice versa, if we have something like ( a / ( a / b + c)), we can prove the inner division using the context from outer division.

We are now not creating non-constant SCEVs, so all recursion will stay between the isImpliedCondOperandsHelper and isImpliedViaOperations, and we will always go down the syntax tree and never go into the infinite recursion. Actually its depth is not really big (not bigger than the depth of expressions).

8555

Shame on me! :D Thanks for pointing out.

[mkazantsev]

lib/Analysis/ScalarEvolution.cpp

8570

Indeed, this makes sense. Will do.

[sanjoy]

This looks good to me.

I have two concerns that I've mentioned inline. Feel free to fix them however you see fit.

lib/Analysis/ScalarEvolution.cpp

8523

Do you rely only recursing into isImpliedViaOperations or into the whole of isImpliedCondOperandsHelper? If the former, I'd be much more comfortable if you:

• Changed IsProvedViaContext to directly call into isImpliedViaOperations
• Passed along a Depth parameter and cap it at a fairly low threshold (let's say 3?) to protect us from the truly pathological cases

We should implement the second point even if we need to recurse into isImpliedCondOperandsHelper, but if recursing into isImpliedViaOperations directly gives us what we want for cheap, we should just do that.

I'm not just worried about infinite recursion -- isImpliedCondOperandsHelper is called often enough that even a somewhat deep recursion here will slow things down.

test/Analysis/ScalarEvolution/scev-division.ll

9

Are you intentionally matching for Predicated backedge-taken count? I'd have expected you to match for just Loop %xxx: backedge-taken count is yyy etc.

[mkazantsev]

lib/Analysis/ScalarEvolution.cpp

8523

The logic here is following: the chain isImpliedViaOperations -> IsProvedViaContext -> isImpliedViaOperations goes down the expression tree to its operands. This process cannot be infinite since it always goes only UP by CFG and never comes down through Phis. Its depth doesn't exceed the depth of expression tree.

This recursive chain does not prove anything by itself. The terminal facts it uses are proved in isImpliedCondOperandsHelper (via range analysis etc). So we cannot throw it away, since it is the essential part for proving the lowest-level facts.

I can add a depth here to avoid analyzing too big expression trees, though.

[mkazantsev]

lib/Analysis/ScalarEvolution.cpp

8523

UPD: I took a carefull look into it and now think that you are right. Seems that it is sufficient to have proofs without implication for terminal impressions which is done in isKnownViaSimpleReasoning. Context-biased analysis in helper seems redundant.

[mkazantsev]

Added threshold, slightly changed tests.

[sanjoy]

Did a quick rescan, LGTM again!

(You have commit access now, right?)

lib/Analysis/ScalarEvolution.cpp

8499

I'd write this as "We want to avoid hurting compile time ..."

8557

Indent is off?

[mkazantsev]

Thanks for review, Sanjoy! Yes, I have the rights. Let me try to merge it myself. :)

[mkazantsev]

Closed by the commit https://reviews.llvm.org/rL298481 [ScalarEvolution] Predicate implication from operations

[mkazantsev]

lib/Analysis/ScalarEvolution.cpp

8527

In fact, it would be surprising if we see LHS is not the same as OrigLHS since that would mean a sext (%a + %b)<nsw> did not get transformed to (sext %a + sext %b)<nsw> as per the rule in ScalarEvolution::getSignExtendExpr. That situation is possible, but should be rare.

It is possible indeed, and it lead to a crash on CLang built. I should prohibit it.

include/llvm/Analysis/ScalarEvolution.h

private:
   /// whenever the condition described by Pred, FoundLHS, and FoundRHS is
   /// true.
   bool isImpliedCondOperands(ICmpInst::Predicate Pred, const SCEV *LHS,
                              const SCEV *RHS, const SCEV *FoundLHS,
                              const SCEV *FoundRHS);
 
   /// Test whether the condition described by Pred, LHS, and RHS is true
   /// whenever the condition described by Pred, FoundLHS, and FoundRHS is
+  /// true. Here LHS is an operation that includes FoundLHS as one of its
+  /// arguments.
+  bool isImpliedViaOperations(ICmpInst::Predicate Pred,
+                              const SCEV *LHS, const SCEV *RHS,
+                              const SCEV *FoundLHS,
+                              const SCEV *FoundRHS);
+
+  /// Test whether the condition described by Pred, LHS, and RHS is true.
+  /// Use only simple non-recursive types of checks, such as range analysis etc.
+  bool isKnownViaSimpleReasoning(ICmpInst::Predicate Pred,
+                                 const SCEV *LHS, const SCEV *RHS);
+
+  /// Test whether the condition described by Pred, LHS, and RHS is true
+  /// whenever the condition described by Pred, FoundLHS, and FoundRHS is
   /// true.
   bool isImpliedCondOperandsHelper(ICmpInst::Predicate Pred, const SCEV *LHS,
                                    const SCEV *RHS, const SCEV *FoundLHS,
                                    const SCEV *FoundRHS);
 
   /// Test whether the condition described by Pred, LHS, and RHS is true
   /// whenever the condition described by Pred, FoundLHS, and FoundRHS is
   /// true.  Utility function used by isImpliedCondOperands.  Tries to get

lib/Analysis/ScalarEvolution.cpp

return
       IsMinConsistingOf<SCEVUMaxExpr>(SE, LHS, RHS) ||
       // A <= max(A, ...)
       IsMaxConsistingOf<SCEVUMaxExpr>(RHS, LHS);
   }
 
   llvm_unreachable("covered switch fell through?!");
 }
 
-bool
-ScalarEvolution::isImpliedCondOperandsHelper(ICmpInst::Predicate Pred,
+bool ScalarEvolution::isImpliedViaOperations(ICmpInst::Predicate Pred,
                                              const SCEV *LHS, const SCEV *RHS,
                                              const SCEV *FoundLHS,
                                              const SCEV *FoundRHS) {
-  auto IsKnownPredicateFull =
-      [this](ICmpInst::Predicate Pred, const SCEV *LHS, const SCEV *RHS) {
-    return isKnownPredicateViaConstantRanges(Pred, LHS, RHS) ||
-           IsKnownPredicateViaMinOrMax(*this, Pred, LHS, RHS) ||
-           IsKnownPredicateViaAddRecStart(*this, Pred, LHS, RHS) ||
-           isKnownPredicateViaNoOverflow(Pred, LHS, RHS);
-  };
+  // We only want to work with ICMP_SGT comparison so far.
+  // TODO: Extend to ICMP_UGT?
+  if (Pred == ICmpInst::ICMP_SLT) {
+    Pred = ICmpInst::ICMP_SGT;
+    std::swap(LHS, RHS);
+    std::swap(FoundLHS, FoundRHS);
+  }
+  if (Pred != ICmpInst::ICMP_SGT)
+    return false;
+
+  auto GetOpFromExt = [&](const SCEV *S) {
+    if (auto *Ext = dyn_cast<SCEVSignExtendExpr>(S))
+      return Ext->getOperand();
+    return S;
+  };
+
+  // Acquire values from extensions.
+  auto *OrigLHS = LHS;
+  auto *OrigFoundLHS = FoundLHS;
+  LHS = GetOpFromExt(LHS);
+  FoundLHS = GetOpFromExt(FoundLHS);
+
+  if (auto *LHSAddExpr = dyn_cast<SCEVAddExpr>(LHS)) {
+    // Should not overflow.
+    if (!LHSAddExpr->hasNoSignedWrap())
+      return false;
+    auto *LL = LHSAddExpr->getOperand(0);
+    auto *LR = LHSAddExpr->getOperand(1);
+    auto *Zero = getZero(RHS->getType());
+    auto *LLExt = getNoopOrSignExtend(LL, OrigLHS->getType());
+    auto *LRExt = getNoopOrSignExtend(LR, OrigLHS->getType());
+
+    auto AdditionRule = [&](const SCEV *S1, const SCEV *S2) {
+      if (isKnownNonNegative(S1) ||
+          isImpliedCondOperandsHelper(ICmpInst::ICMP_SGE, S1, Zero,
+                                      OrigFoundLHS, FoundRHS))
+        if (isKnownViaSimpleReasoning(Pred, S2, RHS) ||
+            isImpliedCondOperandsHelper(Pred, S2, RHS, OrigFoundLHS, FoundRHS))
+          return true;
+      return false;
+    };
+    // Try to prove the following rule:
+    // (LHS = LL + LR) && (LL >= 0) && (LR > RHS) => (LHS > RHS).
+    // (LHS = LL + LR) && (LR >= 0) && (LL > RHS) => (LHS > RHS).
+    if (AdditionRule(LLExt, LRExt) || AdditionRule(LRExt, LLExt))
+      return true;
+  } else if (auto *LHSUnknownExpr = dyn_cast<SCEVUnknown>(LHS)) {
+    Value *LL, *LR;
+    // FIXME: Once we have SDiv implemented, we can get rid of this matching.
+    using namespace llvm::PatternMatch;
+    if (match(LHSUnknownExpr->getValue(), m_SDiv(m_Value(LL), m_Value(LR)))) {
+      auto MaxType = [&](const SCEV *S1, const SCEV *S2) {
+        auto Size1 = getTypeSizeInBits(S1->getType());
+        auto Size2 = getTypeSizeInBits(S2->getType());
+        return  Size1 > Size2 ? S1->getType() : S2->getType();
+      };
+      // Rules for division.
+      auto *Num = getSCEV(LL);
+      auto *Denum = getSCEV(LR);
+      auto *Ty1 = MaxType(Num, FoundLHS);
+      auto *NumExt = getNoopOrSignExtend(Num, Ty1);
+      auto *FoundLHSExt = getNoopOrSignExtend(FoundLHS, Ty1);
+
+      if (!HasSameValue(NumExt, FoundLHSExt) || !isKnownPositive(Denum))
+        return false;
+
+      // Given that FoundLHS > FoundRHS, LHS = FoundLHS / Denum, Denum > 0.
+      auto *Ty2 = MaxType(Denum, FoundRHS);
+      auto *DenumExt = getNoopOrSignExtend(Denum, Ty2);
+      auto *FoundRHSExt = getNoopOrSignExtend(FoundRHS, Ty2);
+
+      // Try to prove the following rule:
+      // (Denum <= FoundRHS + 1) && (RHS <= 0) => (LHS > RHS).
+      auto *One = getOne(Ty2);
+      auto *Next = getAddExpr(FoundRHSExt, One);
+      if (isKnownNonPositive(RHS) &&
+          isKnownViaSimpleReasoning(ICmpInst::ICMP_SLE, DenumExt, Next))
+        return true;
+
+      // Try to prove the following rule:
+      // (-Denum <= FoundRHS) && (RHS < 0) => (LHS > RHS).
+      auto *NegDenum = getNegativeSCEV(DenumExt);
+      if (isKnownNegative(RHS) &&
+          isKnownViaSimpleReasoning(ICmpInst::ICMP_SLE, NegDenum, FoundRHSExt))
+        return true;
+    }
+  }
+
+  return false;
+}
+
+bool
+ScalarEvolution::isKnownViaSimpleReasoning(ICmpInst::Predicate Pred,
+                                           const SCEV *LHS, const SCEV *RHS) {
+}
 
+bool
+ScalarEvolution::isImpliedCondOperandsHelper(ICmpInst::Predicate Pred,
+                                             const SCEV *LHS, const SCEV *RHS,
+                                             const SCEV *FoundLHS,
+                                             const SCEV *FoundRHS) {
   switch (Pred) {
   default: llvm_unreachable("Unexpected ICmpInst::Predicate value!");
   case ICmpInst::ICMP_EQ:
   case ICmpInst::ICMP_NE:
     if (HasSameValue(LHS, FoundLHS) && HasSameValue(RHS, FoundRHS))
       return true;
     break;
   case ICmpInst::ICMP_SLT:
   case ICmpInst::ICMP_SLE:
-    if (IsKnownPredicateFull(ICmpInst::ICMP_SLE, LHS, FoundLHS) &&
-        IsKnownPredicateFull(ICmpInst::ICMP_SGE, RHS, FoundRHS))
+    if (isKnownViaSimpleReasoning(ICmpInst::ICMP_SLE, LHS, FoundLHS) &&
+        isKnownViaSimpleReasoning(ICmpInst::ICMP_SGE, RHS, FoundRHS))
       return true;
     break;
   case ICmpInst::ICMP_SGT:
   case ICmpInst::ICMP_SGE:
-    if (IsKnownPredicateFull(ICmpInst::ICMP_SGE, LHS, FoundLHS) &&
-        IsKnownPredicateFull(ICmpInst::ICMP_SLE, RHS, FoundRHS))
+    if (isKnownViaSimpleReasoning(ICmpInst::ICMP_SGE, LHS, FoundLHS) &&
+        isKnownViaSimpleReasoning(ICmpInst::ICMP_SLE, RHS, FoundRHS))
       return true;
     break;
   case ICmpInst::ICMP_ULT:
   case ICmpInst::ICMP_ULE:
-    if (IsKnownPredicateFull(ICmpInst::ICMP_ULE, LHS, FoundLHS) &&
-        IsKnownPredicateFull(ICmpInst::ICMP_UGE, RHS, FoundRHS))
+    if (isKnownViaSimpleReasoning(ICmpInst::ICMP_ULE, LHS, FoundLHS) &&
+        isKnownViaSimpleReasoning(ICmpInst::ICMP_UGE, RHS, FoundRHS))
       return true;
     break;
   case ICmpInst::ICMP_UGT:
   case ICmpInst::ICMP_UGE:
-    if (IsKnownPredicateFull(ICmpInst::ICMP_UGE, LHS, FoundLHS) &&
-        IsKnownPredicateFull(ICmpInst::ICMP_ULE, RHS, FoundRHS))
+    if (isKnownViaSimpleReasoning(ICmpInst::ICMP_UGE, LHS, FoundLHS) &&
+        isKnownViaSimpleReasoning(ICmpInst::ICMP_ULE, RHS, FoundRHS))
       return true;
     break;
   }
 
+  // Maybe it can be proved via operations?
+  if (isImpliedViaOperations(Pred, LHS, RHS, FoundLHS, FoundRHS))
+    return true;
+
   return false;
 }
 
 bool ScalarEvolution::isImpliedCondOperandsViaRanges(ICmpInst::Predicate Pred,
                                                      const SCEV *LHS,
                                                      const SCEV *RHS,
                                                      const SCEV *FoundLHS,
                                                      const SCEV *FoundRHS) {

test/Analysis/ScalarEvolution/scev-division.ll

+; RUN: opt < %s -analyze -scalar-evolution | FileCheck %s
+
+declare void @llvm.experimental.guard(i1, ...)
+
+define void @test01(i32 %a, i32 %n) nounwind {
+; Prove that (n > 1) ===> (n / 2 > 0).
+; CHECK:         Determining loop execution counts for: @test01
+; CHECK:         Loop %header: Predicated backedge-taken count is (-1 + %n.div.2)<nsw>
+entry:
+  %cmp1 = icmp sgt i32 %n, 1
+  %n.div.2 = sdiv i32 %n, 2
+  call void(i1, ...) @llvm.experimental.guard(i1 %cmp1) [ "deopt"() ]
+  br label %header
+
+header:
+  %indvar = phi i32 [ %indvar.next, %header ], [ 0, %entry ]
+  %indvar.next = add i32 %indvar, 1
+  %exitcond = icmp sgt i32 %n.div.2, %indvar.next
+  br i1 %exitcond, label %header, label %exit
+
+exit:
+  ret void
+}
+
+define void @test01neg(i32 %a, i32 %n) nounwind {
+; Prove that (n > 0) =\=> (n / 2 > 0).
+; CHECK:         Determining loop execution counts for: @test01neg
+; CHECK:         Loop %header: Predicated backedge-taken count is (-1 + (1 smax %n.div.2))<nsw>
+entry:
+  %cmp1 = icmp sgt i32 %n, 0
+  %n.div.2 = sdiv i32 %n, 2
+  call void(i1, ...) @llvm.experimental.guard(i1 %cmp1) [ "deopt"() ]
+  br label %header
+
+header:
+  %indvar = phi i32 [ %indvar.next, %header ], [ 0, %entry ]
+  %indvar.next = add i32 %indvar, 1
+  %exitcond = icmp sgt i32 %n.div.2, %indvar.next
+  br i1 %exitcond, label %header, label %exit
+
+exit:
+  ret void
+}
+
+define void @test02(i32 %a, i32 %n) nounwind {
+; Prove that (n >= 2) ===> (n / 2 > 0).
+; CHECK:         Determining loop execution counts for: @test02
+; CHECK:         Loop %header: Predicated backedge-taken count is (-1 + %n.div.2)<nsw>
+entry:
+  %cmp1 = icmp sge i32 %n, 2
+  %n.div.2 = sdiv i32 %n, 2
+  call void(i1, ...) @llvm.experimental.guard(i1 %cmp1) [ "deopt"() ]
+  br label %header
+
+header:
+  %indvar = phi i32 [ %indvar.next, %header ], [ 0, %entry ]
+  %indvar.next = add i32 %indvar, 1
+  %exitcond = icmp sgt i32 %n.div.2, %indvar.next
+  br i1 %exitcond, label %header, label %exit
+
+exit:
+  ret void
+}
+
+define void @test02neg(i32 %a, i32 %n) nounwind {
+; Prove that (n >= 1) =\=> (n / 2 > 0).
+; CHECK:         Determining loop execution counts for: @test02neg
+; CHECK:         Loop %header: Predicated backedge-taken count is (-1 + (1 smax %n.div.2))<nsw>
+entry:
+  %cmp1 = icmp sge i32 %n, 1
+  %n.div.2 = sdiv i32 %n, 2
+  call void(i1, ...) @llvm.experimental.guard(i1 %cmp1) [ "deopt"() ]
+  br label %header
+
+header:
+  %indvar = phi i32 [ %indvar.next, %header ], [ 0, %entry ]
+  %indvar.next = add i32 %indvar, 1
+  %exitcond = icmp sgt i32 %n.div.2, %indvar.next
+  br i1 %exitcond, label %header, label %exit
+
+exit:
+  ret void
+}
+
+define void @test03(i32 %a, i32 %n) nounwind {
+; Prove that (n > -2) ===> (n / 2 >= 0).
+; TODO: We should be able to prove that (n > -2) ===> (n / 2 >= 0).
+; CHECK:         Determining loop execution counts for: @test03
+; CHECK:         Loop %header: Predicated backedge-taken count is (1 + %n.div.2)<nsw>
+entry:
+  %cmp1 = icmp sgt i32 %n, -2
+  %n.div.2 = sdiv i32 %n, 2
+  call void(i1, ...) @llvm.experimental.guard(i1 %cmp1) [ "deopt"() ]
+  br label %header
+
+header:
+  %indvar = phi i32 [ %indvar.next, %header ], [ 0, %entry ]
+  %indvar.next = add i32 %indvar, 1
+  %exitcond = icmp sge i32 %n.div.2, %indvar
+  br i1 %exitcond, label %header, label %exit
+
+exit:
+  ret void
+}
+
+define void @test03neg(i32 %a, i32 %n) nounwind {
+; Prove that (n > -3) =\=> (n / 2 >= 0).
+; CHECK:         Determining loop execution counts for: @test03neg
+; CHECK:         Loop %header: Predicated backedge-taken count is (0 smax (1 + %n.div.2)<nsw>)
+entry:
+  %cmp1 = icmp sgt i32 %n, -3
+  %n.div.2 = sdiv i32 %n, 2
+  call void(i1, ...) @llvm.experimental.guard(i1 %cmp1) [ "deopt"() ]
+  br label %header
+
+header:
+  %indvar = phi i32 [ %indvar.next, %header ], [ 0, %entry ]
+  %indvar.next = add i32 %indvar, 1
+  %exitcond = icmp sge i32 %n.div.2, %indvar
+  br i1 %exitcond, label %header, label %exit
+
+exit:
+  ret void
+}
+
+define void @test04(i32 %a, i32 %n) nounwind {
+; Prove that (n >= -1) ===> (n / 2 >= 0).
+; CHECK:         Determining loop execution counts for: @test04
+; CHECK:         Loop %header: Predicated backedge-taken count is (1 + %n.div.2)<nsw>
+entry:
+  %cmp1 = icmp sge i32 %n, -1
+  %n.div.2 = sdiv i32 %n, 2
+  call void(i1, ...) @llvm.experimental.guard(i1 %cmp1) [ "deopt"() ]
+  br label %header
+
+header:
+  %indvar = phi i32 [ %indvar.next, %header ], [ 0, %entry ]
+  %indvar.next = add i32 %indvar, 1
+  %exitcond = icmp sge i32 %n.div.2, %indvar
+  br i1 %exitcond, label %header, label %exit
+
+exit:
+  ret void
+}
+
+define void @test04neg(i32 %a, i32 %n) nounwind {
+; Prove that (n >= -2) =\=> (n / 2 >= 0).
+; CHECK:         Determining loop execution counts for: @test04neg
+; CHECK:         Loop %header: Predicated backedge-taken count is (0 smax (1 + %n.div.2)<nsw>)
+entry:
+  %cmp1 = icmp sge i32 %n, -2
+  %n.div.2 = sdiv i32 %n, 2
+  call void(i1, ...) @llvm.experimental.guard(i1 %cmp1) [ "deopt"() ]
+  br label %header
+
+header:
+  %indvar = phi i32 [ %indvar.next, %header ], [ 0, %entry ]
+  %indvar.next = add i32 %indvar, 1
+  %exitcond = icmp sge i32 %n.div.2, %indvar
+  br i1 %exitcond, label %header, label %exit
+
+exit:
+  ret void
+}
+
+define void @testext01(i32 %a, i32 %n) nounwind {
+; Prove that (n > 1) ===> (n / 2 > 0).
+; CHECK:         Determining loop execution counts for: @testext01
+; CHECK:         Loop %header: Predicated backedge-taken count is (-1 + (sext i32 %n.div.2 to i64))<nsw>
+entry:
+  %cmp1 = icmp sgt i32 %n, 1
+  %n.div.2 = sdiv i32 %n, 2
+  %n.div.2.ext = sext i32 %n.div.2 to i64
+  call void(i1, ...) @llvm.experimental.guard(i1 %cmp1) [ "deopt"() ]
+  br label %header
+
+header:
+  %indvar = phi i64 [ %indvar.next, %header ], [ 0, %entry ]
+  %indvar.next = add i64 %indvar, 1
+  %exitcond = icmp sgt i64 %n.div.2.ext, %indvar.next
+  br i1 %exitcond, label %header, label %exit
+
+exit:
+  ret void
+}
+
+define void @testext01neg(i32 %a, i32 %n) nounwind {
+; Prove that (n > 0) =\=> (n / 2 > 0).
+; CHECK:         Determining loop execution counts for: @testext01neg
+; CHECK:         Loop %header: Predicated backedge-taken count is (-1 + (1 smax (sext i32 %n.div.2 to i64)))<nsw>
+entry:
+  %cmp1 = icmp sgt i32 %n, 0
+  %n.div.2 = sdiv i32 %n, 2
+  %n.div.2.ext = sext i32 %n.div.2 to i64
+  call void(i1, ...) @llvm.experimental.guard(i1 %cmp1) [ "deopt"() ]
+  br label %header
+
+header:
+  %indvar = phi i64 [ %indvar.next, %header ], [ 0, %entry ]
+  %indvar.next = add i64 %indvar, 1
+  %exitcond = icmp sgt i64 %n.div.2.ext, %indvar.next
+  br i1 %exitcond, label %header, label %exit
+
+exit:
+  ret void
+}
+
+define void @testext02(i32 %a, i32 %n) nounwind {
+; Prove that (n >= 2) ===> (n / 2 > 0).
+; CHECK:         Determining loop execution counts for: @testext02
+; CHECK:         Loop %header: Predicated backedge-taken count is (-1 + (sext i32 %n.div.2 to i64))<nsw>
+entry:
+  %cmp1 = icmp sge i32 %n, 2
+  %n.div.2 = sdiv i32 %n, 2
+  %n.div.2.ext = sext i32 %n.div.2 to i64
+  call void(i1, ...) @llvm.experimental.guard(i1 %cmp1) [ "deopt"() ]
+  br label %header
+
+header:
+  %indvar = phi i64 [ %indvar.next, %header ], [ 0, %entry ]
+  %indvar.next = add i64 %indvar, 1
+  %exitcond = icmp sgt i64 %n.div.2.ext, %indvar.next
+  br i1 %exitcond, label %header, label %exit
+
+exit:
+  ret void
+}
+
+define void @testext02neg(i32 %a, i32 %n) nounwind {
+; Prove that (n >= 1) =\=> (n / 2 > 0).
+; CHECK:         Determining loop execution counts for: @testext02neg
+; CHECK:         Loop %header: Predicated backedge-taken count is (-1 + (1 smax (sext i32 %n.div.2 to i64)))<nsw>
+entry:
+  %cmp1 = icmp sge i32 %n, 1
+  %n.div.2 = sdiv i32 %n, 2
+  %n.div.2.ext = sext i32 %n.div.2 to i64
+  call void(i1, ...) @llvm.experimental.guard(i1 %cmp1) [ "deopt"() ]
+  br label %header
+
+header:
+  %indvar = phi i64 [ %indvar.next, %header ], [ 0, %entry ]
+  %indvar.next = add i64 %indvar, 1
+  %exitcond = icmp sgt i64 %n.div.2.ext, %indvar.next
+  br i1 %exitcond, label %header, label %exit
+
+exit:
+  ret void
+}
+
+define void @testext03(i32 %a, i32 %n) nounwind {
+; Prove that (n > -2) ===> (n / 2 >= 0).
+; TODO: We should be able to prove that (n > -2) ===> (n / 2 >= 0).
+; CHECK:         Determining loop execution counts for: @testext03
+; CHECK:         Loop %header: Predicated backedge-taken count is (1 + (sext i32 %n.div.2 to i64))<nsw>
+entry:
+  %cmp1 = icmp sgt i32 %n, -2
+  %n.div.2 = sdiv i32 %n, 2
+  %n.div.2.ext = sext i32 %n.div.2 to i64
+  call void(i1, ...) @llvm.experimental.guard(i1 %cmp1) [ "deopt"() ]
+  br label %header
+
+header:
+  %indvar = phi i64 [ %indvar.next, %header ], [ 0, %entry ]
+  %indvar.next = add i64 %indvar, 1
+  %exitcond = icmp sge i64 %n.div.2.ext, %indvar
+  br i1 %exitcond, label %header, label %exit
+
+exit:
+  ret void
+}
+
+define void @testext03neg(i32 %a, i32 %n) nounwind {
+; Prove that (n > -3) =\=> (n / 2 >= 0).
+; CHECK:         Determining loop execution counts for: @testext03neg
+; CHECK:         Loop %header: Predicated backedge-taken count is (0 smax (1 + (sext i32 %n.div.2 to i64))<nsw>)
+entry:
+  %cmp1 = icmp sgt i32 %n, -3
+  %n.div.2 = sdiv i32 %n, 2
+  %n.div.2.ext = sext i32 %n.div.2 to i64
+  call void(i1, ...) @llvm.experimental.guard(i1 %cmp1) [ "deopt"() ]
+  br label %header
+
+header:
+  %indvar = phi i64 [ %indvar.next, %header ], [ 0, %entry ]
+  %indvar.next = add i64 %indvar, 1
+  %exitcond = icmp sge i64 %n.div.2.ext, %indvar
+  br i1 %exitcond, label %header, label %exit
+
+exit:
+  ret void
+}
+
+define void @testext04(i32 %a, i32 %n) nounwind {
+; Prove that (n >= -1) ===> (n / 2 >= 0).
+; CHECK:         Determining loop execution counts for: @testext04
+; CHECK:         Loop %header: Predicated backedge-taken count is (1 + (sext i32 %n.div.2 to i64))<nsw>
+entry:
+  %cmp1 = icmp sge i32 %n, -1
+  %n.div.2 = sdiv i32 %n, 2
+  %n.div.2.ext = sext i32 %n.div.2 to i64
+  call void(i1, ...) @llvm.experimental.guard(i1 %cmp1) [ "deopt"() ]
+  br label %header
+
+header:
+  %indvar = phi i64 [ %indvar.next, %header ], [ 0, %entry ]
+  %indvar.next = add i64 %indvar, 1
+  %exitcond = icmp sge i64 %n.div.2.ext, %indvar
+  br i1 %exitcond, label %header, label %exit
+
+exit:
+  ret void
+}
+
+define void @testext04neg(i32 %a, i32 %n) nounwind {
+; Prove that (n >= -2) =\=> (n / 2 >= 0).
+; CHECK:         Determining loop execution counts for: @testext04neg
+; CHECK:         Loop %header: Predicated backedge-taken count is (0 smax (1 + (sext i32 %n.div.2 to i64))<nsw>)
+entry:
+  %cmp1 = icmp sge i32 %n, -2
+  %n.div.2 = sdiv i32 %n, 2
+  %n.div.2.ext = sext i32 %n.div.2 to i64
+  call void(i1, ...) @llvm.experimental.guard(i1 %cmp1) [ "deopt"() ]
+  br label %header
+
+header:
+  %indvar = phi i64 [ %indvar.next, %header ], [ 0, %entry ]
+  %indvar.next = add i64 %indvar, 1
+  %exitcond = icmp sge i64 %n.div.2.ext, %indvar
+  br i1 %exitcond, label %header, label %exit
+
+exit:
+  ret void
+}
+