[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

8552

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.

8564

There already is getNoopOrSignExtend that does the same thing.

8570

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

8582

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.

8583

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

8586

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

8591

Use getZero(RHS->getType()).

8602

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)?

8610

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

8616

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

8552

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

[mkazantsev]

lib/Analysis/ScalarEvolution.cpp

8552

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

8583

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.

8602

Ok, I got rid of recursive checks.

8616

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

8583

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?

8616

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.

8689

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.

8692

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.

8711

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.

8720

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.

[mkazantsev]

lib/Analysis/ScalarEvolution.cpp

8689

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

8689

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

8689

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

[mkazantsev]

lib/Analysis/ScalarEvolution.cpp

8616

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

8616

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.

8685

This should be called GetOpFromSExt.

8685

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.

8700

Can we avoid the recursion via isImpliedCondOperandsHelper?

8717

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.

8732

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

8732

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

8711

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

8732

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

8700

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).

8717

Shame on me! :D Thanks for pointing out.

[mkazantsev]

lib/Analysis/ScalarEvolution.cpp

8732

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

8700

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

8700

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

8700

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

8550

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

8608

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

8689

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,
+                              unsigned Depth = 0);
+
+  /// 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
public:
   /// return true.
   uint64_t getTypeSizeInBits(Type *Ty) const;
 
   /// Return a type with the same bitwidth as the given type and which
   /// represents how SCEV will treat the given type, for which isSCEVable must
   /// return true. For pointer types, this is the pointer-sized integer type.
   Type *getEffectiveSCEVType(Type *Ty) const;
 
+  // Returns a wider type among {Ty1, Ty2}.
+  Type *getWiderType(Type *Ty1, Type *Ty2) const;
+
   /// Return true if the SCEV is a scAddRecExpr or it contains
   /// scAddRecExpr. The result will be cached in HasRecMap.
   ///
   bool containsAddRecurrence(const SCEV *S);
 
   /// Return the Value set from which the SCEV expr is generated.
   SetVector<ValueOffsetPair> *getSCEVValues(const SCEV *S);
 

lib/Analysis/ScalarEvolution.cpp

static cl::opt<unsigned> AddOpsInlineThreshold(
     cl::desc("Threshold for inlining multiplication operands into a SCEV"),
     cl::init(500));
 
 static cl::opt<unsigned> MaxSCEVCompareDepth(
     "scalar-evolution-max-scev-compare-depth", cl::Hidden,
     cl::desc("Maximum depth of recursive SCEV complexity comparisons"),
     cl::init(32));
 
+static cl::opt<unsigned> MaxSCEVOperationsImplicationDepth(
+    "scalar-evolution-max-scev-operations-implication-depth", cl::Hidden,
+    cl::desc("Maximum depth of recursive SCEV operations implication analysis"),
+    cl::init(4));
+
 static cl::opt<unsigned> MaxValueCompareDepth(
     "scalar-evolution-max-value-compare-depth", cl::Hidden,
     cl::desc("Maximum depth of recursive value complexity comparisons"),
     cl::init(2));
 
 static cl::opt<unsigned>
     MaxAddExprDepth("scalar-evolution-max-addexpr-depth", cl::Hidden,
                     cl::desc("Maximum depth of recursive AddExpr"),
Type *ScalarEvolution::getEffectiveSCEVType(Type *Ty) const {
   if (Ty->isIntegerTy())
     return Ty;
 
   // The only other support type is pointer.
   assert(Ty->isPointerTy() && "Unexpected non-pointer non-integer type!");
   return getDataLayout().getIntPtrType(Ty);
 }
 
+Type *ScalarEvolution::getWiderType(Type *T1, Type *T2) const {
+  return  getTypeSizeInBits(T1) >= getTypeSizeInBits(T2) ? T1 : T2;
+}
+
 const SCEV *ScalarEvolution::getCouldNotCompute() {
   return CouldNotCompute.get();
 }
 
 bool ScalarEvolution::checkValidity(const SCEV *S) const {
   bool ContainsNulls = SCEVExprContains(S, [](const SCEV *S) {
     auto *SU = dyn_cast<SCEVUnknown>(S);
     return SU && SU->getValue() == nullptr;
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);
-  };
+                                             const SCEV *FoundRHS,
+                                             unsigned Depth) {
+  // We want to avoid hurting the compile time with analysis of too big trees.
+  if (Depth > MaxSCEVOperationsImplicationDepth)
+    return false;
+  // 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 GetOpFromSExt = [&](const SCEV *S) {
+    if (auto *Ext = dyn_cast<SCEVSignExtendExpr>(S))
+      return Ext->getOperand();
+    return S;
+  };
+
+  // Acquire values from extensions.
+  auto *OrigFoundLHS = FoundLHS;
+  LHS = GetOpFromSExt(LHS);
+  FoundLHS = GetOpFromSExt(FoundLHS);
+
+  // Is a predicate can be proved trivially or using the found context.
+  auto IsProvedViaContext = [&](ICmpInst::Predicate Pred,
+                                const SCEV *S1, const SCEV *S2) {
+    return isKnownViaSimpleReasoning(Pred, S1, S2) ||
+           isImpliedViaOperations(Pred, S1, S2, OrigFoundLHS, FoundRHS,
+                                  Depth + 1);
+  };
+
+  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);
+
+    // Checks that S1 >= 0 && S2 > RHS, trivially or using the found context.
+    auto IsSumGreaterThanRHS = [&](const SCEV *S1, const SCEV *S2) {
+      return IsProvedViaContext(ICmpInst::ICMP_SGT, S2, RHS) &&
+             IsProvedViaContext(Pred, S1, getZero(RHS->getType()));
+    };
+    // 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 (IsSumGreaterThanRHS(LL, LR) || IsSumGreaterThanRHS(LR, LL))
+      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)))) {
+      // Rules for division.
+      // We are going to perform some comparisons with Denominator and its
+      // derivative expressions. In general case, creating a SCEV for it may
+      // lead to a complex analysis of the entire graph, and in particular it
+      // can request trip count recalculation for the same loop. This would
+      // cache as SCEVCouldNotCompute to avoid the infinite recursion. This is a
+      // sad thing. To avoid this, we only want to create SCEVs that are
+      // constants in this section. So we bail if Denominator is not a constant.
+      if (!isa<ConstantInt>(LR))
+        return false;
+
+      auto *Denominator = cast<SCEVConstant>(getSCEV(LR));
+
+      // We want to make sure that LHS = FoundLHS / Denominator. If it is so,
+      // then a SCEV for the numerator already exists and matches with FoundLHS.
+      auto *Numerator = getExistingSCEV(LL);
+
+      // Make sure that it exists and has the same type.
+      if (!Numerator || Numerator->getType() != FoundLHS->getType())
+        return false;
+
+      // Make sure that the numerator matches with FoundLHs and the denominator
+      // is positive.
+      if (!HasSameValue(Numerator, FoundLHS) || !isKnownPositive(Denominator))
+        return false;
+
+      // Given that:
+      // FoundLHS > FoundRHS, LHS = FoundLHS / Denominator, Denominator > 0.
+      auto *Ty2 = getWiderType(Denominator->getType(), FoundRHS->getType());
+      auto *DenominatorExt = getNoopOrSignExtend(Denominator, Ty2);
+      auto *FoundRHSExt = getNoopOrSignExtend(FoundRHS, Ty2);
+
+      // Try to prove the following rule:
+      // (Denominator - 1 <= FoundRHS) && (RHS <= 0) => (LHS > RHS).
+      // For example, given that FoundLHS > 2. It means that FoundLHS is at
+      // least 3. If we divide it by Denominator <= 3, we will have at least 1.
+      auto *DenomMinusOne = getMinusSCEV(DenominatorExt, getOne(Ty2));
+      if (isKnownNonPositive(RHS) &&
+          IsProvedViaContext(ICmpInst::ICMP_SLE, DenomMinusOne, FoundRHSExt))
+        return true;
+
+      // Try to prove the following rule:
+      // (-Denominator <= FoundRHS) && (RHS < 0) => (LHS > RHS).
+      // For example, given that FoundLHS > -3. Then FoundLHS is at least -2.
+      // If we divide it by Denominator >= 3, then:
+      // 1. If FoundLHS is negative, then the result is 0.
+      // 2. If FoundLHS is non-negative, then the result is non-negative.
+      // Anyways, the result is non-negative.
+      auto *NegDenominator = getNegativeSCEV(DenominatorExt);
+      if (isKnownNegative(RHS) &&
+          IsProvedViaContext(ICmpInst::ICMP_SLE, NegDenominator, 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) {
   if (!isa<SCEVConstant>(RHS) || !isa<SCEVConstant>(FoundRHS))
     // The restriction on `FoundRHS` be lifted easily -- it exists only to
     // reduce the compile time impact of this optimization.
     return false;
 
   Optional<APInt> Addend = computeConstantDifference(LHS, FoundLHS);
   if (!Addend)
     return false;
 
   APInt ConstFoundRHS = cast<SCEVConstant>(FoundRHS)->getAPInt();
 
   // `FoundLHSRange` is the range we know `FoundLHS` to be in by virtue of the
   // antecedent "`FoundLHS` `Pred` `FoundRHS`".
   ConstantRange FoundLHSRange =
       ConstantRange::makeAllowedICmpRegion(Pred, ConstFoundRHS);
 
   // Since `LHS` is `FoundLHS` + `Addend`, we can compute a range for `LHS`:
   ConstantRange LHSRange = FoundLHSRange.add(ConstantRange(*Addend));
 
   // We can also compute the range of values for `LHS` that satisfy the

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: 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: 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: 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: 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: 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: 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: 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: 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: 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: 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: 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: 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: 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: 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: 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: 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
+}
+