[ScalarEvolution] Re-enable Predicate implication from operations

The patch rL298481 was reverted due to crash on clang-with-lto-ubuntu build.
The reason of the crash was type mismatch between either a or b and RHS in the following situation:

  LHS = sext(a +nsw b) > RHS.

This is quite rare, but still possible situation. Normally we need to cast all {a, b, RHS} to their widest type.
But we try to avoid creation of new SCEV that are not constants to avoid initiating recursive analysis that
can take a lot of time and/or cache a bad value for iterations number. To deal with this, in this patch we
reject this case and will not try to analyze it if the type of sum doesn't match with the type of RHS. In this
situation we don't need to create any non-constant SCEVs.

This patch also adds an assertion to the method IsProvedViaContext so that we could fail on it and not
go further into range analysis etc (because in some situations these analyzes succeed even when the passed
arguments have wrong types, what should not normally happen).

The patch also contains a fix for a problem with too narrow scope of the analysis caused by wrong
usage of predicates in recursive invocations.

The regression test on the said failure: test/Analysis/ScalarEvolution/implied-via-addition.ll

Reviewers: reames, apilipenko, anna, sanjoy

Reviewed By: sanjoy

Subscribers: mzolotukhin, mehdi_amini, llvm-commits

Differential Revision: https://reviews.llvm.org/D31238

llvm-svn: 299205

include/llvm/Analysis/ScalarEvolution.h

@@ -976,6 +976,20 @@ private:
                              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.
@@ -1123,6 +1137,9 @@ public:
   /// 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.
   ///

lib/Analysis/ScalarEvolution.cpp

@@ -137,6 +137,11 @@ static cl::opt<unsigned> MaxSCEVCompareDepth(
     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(2));
+
 static cl::opt<unsigned> MaxValueCompareDepth(
     "scalar-evolution-max-value-compare-depth", cl::Hidden,
     cl::desc("Maximum depth of recursive value complexity comparisons"),
@@ -3418,6 +3423,10 @@ Type *ScalarEvolution::getEffectiveSCEVType(Type *Ty) const {
   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();
 }
@@ -8559,19 +8568,161 @@ static bool IsKnownPredicateViaMinOrMax(ScalarEvolution &SE,
   llvm_unreachable("covered switch fell through?!");
 }
 
+bool ScalarEvolution::isImpliedViaOperations(ICmpInst::Predicate Pred,
+                                             const SCEV *LHS, const SCEV *RHS,
+                                             const SCEV *FoundLHS,
+                                             const SCEV *FoundRHS,
+                                             unsigned Depth) {
+  assert(getTypeSizeInBits(LHS->getType()) ==
+             getTypeSizeInBits(RHS->getType()) &&
+         "LHS and RHS have different sizes?");
+  assert(getTypeSizeInBits(FoundLHS->getType()) ==
+             getTypeSizeInBits(FoundRHS->getType()) &&
+         "FoundLHS and FoundRHS have different sizes?");
+  // 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();
+    // TODO: If S is a SCEVConstant then you can cheaply "strip" the sext off
+    // the constant in some cases.
+    return S;
+  };
+
+  // Acquire values from extensions.
+  auto *OrigFoundLHS = FoundLHS;
+  LHS = GetOpFromSExt(LHS);
+  FoundLHS = GetOpFromSExt(FoundLHS);
+
+  // Is the SGT predicate can be proved trivially or using the found context.
+  auto IsSGTViaContext = [&](const SCEV *S1, const SCEV *S2) {
+    return isKnownViaSimpleReasoning(ICmpInst::ICMP_SGT, S1, S2) ||
+           isImpliedViaOperations(ICmpInst::ICMP_SGT, S1, S2, OrigFoundLHS,
+                                  FoundRHS, Depth + 1);
+  };
+
+  if (auto *LHSAddExpr = dyn_cast<SCEVAddExpr>(LHS)) {
+    // We want to avoid creation of any new non-constant SCEV. Since we are
+    // going to compare the operands to RHS, we should be certain that we don't
+    // need any size extensions for this. So let's decline all cases when the
+    // sizes of types of LHS and RHS do not match.
+    // TODO: Maybe try to get RHS from sext to catch more cases?
+    if (getTypeSizeInBits(LHS->getType()) != getTypeSizeInBits(RHS->getType()))
+      return false;
+
+    // Should not overflow.
+    if (!LHSAddExpr->hasNoSignedWrap())
+      return false;
+
+    auto *LL = LHSAddExpr->getOperand(0);
+    auto *LR = LHSAddExpr->getOperand(1);
+    auto *MinusOne = getNegativeSCEV(getOne(RHS->getType()));
+
+    // Checks that S1 >= 0 && S2 > RHS, trivially or using the found context.
+    auto IsSumGreaterThanRHS = [&](const SCEV *S1, const SCEV *S2) {
+      return IsSGTViaContext(S1, MinusOne) && IsSGTViaContext(S2, RHS);
+    };
+    // 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. 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);
+      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;
+
+      auto *DTy = Denominator->getType();
+      auto *FRHSTy = FoundRHS->getType();
+      if (DTy->isPointerTy() != FRHSTy->isPointerTy())
+        // One of types is a pointer and another one is not. We cannot extend
+        // them properly to a wider type, so let us just reject this case.
+        // TODO: Usage of getEffectiveSCEVType for DTy, FRHSTy etc should help
+        // to avoid this check.
+        return false;
+
+      // Given that:
+      // FoundLHS > FoundRHS, LHS = FoundLHS / Denominator, Denominator > 0.
+      auto *WTy = getWiderType(DTy, FRHSTy);
+      auto *DenominatorExt = getNoopOrSignExtend(Denominator, WTy);
+      auto *FoundRHSExt = getNoopOrSignExtend(FoundRHS, WTy);
+
+      // Try to prove the following rule:
+      // (FoundRHS > Denominator - 2) && (RHS <= 0) => (LHS > RHS).
+      // For example, given that FoundLHS > 2. It means that FoundLHS is at
+      // least 3. If we divide it by Denominator < 4, we will have at least 1.
+      auto *DenomMinusTwo = getMinusSCEV(DenominatorExt, getConstant(WTy, 2));
+      if (isKnownNonPositive(RHS) &&
+          IsSGTViaContext(FoundRHSExt, DenomMinusTwo))
+        return true;
+
+      // Try to prove the following rule:
+      // (FoundRHS > -1 - Denominator) && (RHS < 0) => (LHS > RHS).
+      // For example, given that FoundLHS > -3. Then FoundLHS is at least -2.
+      // If we divide it by Denominator > 2, 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 *MinusOne = getNegativeSCEV(getOne(WTy));
+      auto *NegDenomMinusOne = getMinusSCEV(MinusOne, DenominatorExt);
+      if (isKnownNegative(RHS) &&
+          IsSGTViaContext(FoundRHSExt, NegDenomMinusOne))
+        return true;
+    }
+  }
+
+  return false;
+}
+
+bool
+ScalarEvolution::isKnownViaSimpleReasoning(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);
+}
+
 bool
 ScalarEvolution::isImpliedCondOperandsHelper(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);
-  };
-
   switch (Pred) {
   default: llvm_unreachable("Unexpected ICmpInst::Predicate value!");
   case ICmpInst::ICMP_EQ:
@@ -8581,30 +8732,34 @@ ScalarEvolution::isImpliedCondOperandsHelper(ICmpInst::Predicate Pred,
     break;
   case ICmpInst::ICMP_SLT:
   case ICmpInst::ICMP_SLE:
-    if (IsKnownPredicateFull(ICmpInst::ICMP_SLE, LHS, FoundLHS) &&
+    if (isKnownViaSimpleReasoning(ICmpInst::ICMP_SLE, LHS, FoundLHS) &&
-        IsKnownPredicateFull(ICmpInst::ICMP_SGE, RHS, FoundRHS))
+        isKnownViaSimpleReasoning(ICmpInst::ICMP_SGE, RHS, FoundRHS))
       return true;
     break;
   case ICmpInst::ICMP_SGT:
   case ICmpInst::ICMP_SGE:
-    if (IsKnownPredicateFull(ICmpInst::ICMP_SGE, LHS, FoundLHS) &&
+    if (isKnownViaSimpleReasoning(ICmpInst::ICMP_SGE, LHS, FoundLHS) &&
-        IsKnownPredicateFull(ICmpInst::ICMP_SLE, RHS, FoundRHS))
+        isKnownViaSimpleReasoning(ICmpInst::ICMP_SLE, RHS, FoundRHS))
       return true;
     break;
   case ICmpInst::ICMP_ULT:
   case ICmpInst::ICMP_ULE:
-    if (IsKnownPredicateFull(ICmpInst::ICMP_ULE, LHS, FoundLHS) &&
+    if (isKnownViaSimpleReasoning(ICmpInst::ICMP_ULE, LHS, FoundLHS) &&
-        IsKnownPredicateFull(ICmpInst::ICMP_UGE, RHS, FoundRHS))
+        isKnownViaSimpleReasoning(ICmpInst::ICMP_UGE, RHS, FoundRHS))
       return true;
     break;
   case ICmpInst::ICMP_UGT:
   case ICmpInst::ICMP_UGE:
-    if (IsKnownPredicateFull(ICmpInst::ICMP_UGE, LHS, FoundLHS) &&
+    if (isKnownViaSimpleReasoning(ICmpInst::ICMP_UGE, LHS, FoundLHS) &&
-        IsKnownPredicateFull(ICmpInst::ICMP_ULE, RHS, FoundRHS))
+        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;
 }
 

test/Analysis/ScalarEvolution/implied-via-addition.ll

@@ -0,0 +1,50 @@
+; RUN: opt -indvars -S < %s | FileCheck %s
+
+declare void @use(i1)
+
+declare void @llvm.experimental.guard(i1, ...)
+
+define void @test_01(i8 %t) {
+; CHECK-LABEL: test_01
+ entry:
+  %st = sext i8 %t to i16
+  %cmp1 = icmp slt i16 %st, 42
+  call void(i1, ...) @llvm.experimental.guard(i1 %cmp1) [ "deopt"() ]
+  br label %loop
+
+ loop:
+; CHECK-LABEL: loop
+  %idx = phi i8 [ %t, %entry ], [ %idx.inc, %loop ]
+  %idx.inc = add i8 %idx, 1
+  %c = icmp slt i8 %idx, 42
+; CHECK: call void @use(i1 true)
+  call void @use(i1 %c)
+  %be = icmp slt i8 %idx.inc, 42
+  br i1 %be, label %loop, label %exit
+
+ exit:
+  ret void
+}
+
+define void @test_02(i8 %t) {
+; CHECK-LABEL: test_02
+ entry:
+  %t.ptr = inttoptr i8 %t to i8*
+  %p.42 = inttoptr i8 42 to i8*
+  %cmp1 = icmp slt i8* %t.ptr, %p.42
+  call void(i1, ...) @llvm.experimental.guard(i1 %cmp1) [ "deopt"() ]
+  br label %loop
+
+ loop:
+; CHECK-LABEL: loop
+  %idx = phi i8* [ %t.ptr, %entry ], [ %snext, %loop ]
+  %snext = getelementptr inbounds i8, i8* %idx, i64 1
+  %c = icmp slt i8* %idx, %p.42
+; CHECK: call void @use(i1 true)
+  call void @use(i1 %c)
+  %be = icmp slt i8* %snext, %p.42
+  br i1 %be, label %loop, label %exit
+
+ exit:
+  ret void
+}

test/Analysis/ScalarEvolution/implied-via-division.ll

@@ -0,0 +1,331 @@
+; RUN: opt < %s -analyze -scalar-evolution | FileCheck %s
+
+declare void @llvm.experimental.guard(i1, ...)
+
+define void @test_1(i32 %n) nounwind {
+; Prove that (n > 1) ===> (n / 2 > 0).
+; CHECK:         Determining loop execution counts for: @test_1
+; 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 @test_1neg(i32 %n) nounwind {
+; Prove that (n > 0) =\=> (n / 2 > 0).
+; CHECK:         Determining loop execution counts for: @test_1neg
+; 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 @test_2(i32 %n) nounwind {
+; Prove that (n >= 2) ===> (n / 2 > 0).
+; CHECK:         Determining loop execution counts for: @test_2
+; 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 @test_2neg(i32 %n) nounwind {
+; Prove that (n >= 1) =\=> (n / 2 > 0).
+; CHECK:         Determining loop execution counts for: @test_2neg
+; 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 @test_3(i32 %n) nounwind {
+; Prove that (n > -2) ===> (n / 2 >= 0).
+; CHECK:         Determining loop execution counts for: @test_3
+; 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 @test_3neg(i32 %n) nounwind {
+; Prove that (n > -3) =\=> (n / 2 >= 0).
+; CHECK:         Determining loop execution counts for: @test_3neg
+; 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 @test_4(i32 %n) nounwind {
+; Prove that (n >= -1) ===> (n / 2 >= 0).
+; CHECK:         Determining loop execution counts for: @test_4
+; 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 @test_4neg(i32 %n) nounwind {
+; Prove that (n >= -2) =\=> (n / 2 >= 0).
+; CHECK:         Determining loop execution counts for: @test_4neg
+; 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 @test_ext_01(i32 %n) nounwind {
+; Prove that (n > 1) ===> (n / 2 > 0).
+; CHECK:         Determining loop execution counts for: @test_ext_01
+; 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 @test_ext_01neg(i32 %n) nounwind {
+; Prove that (n > 0) =\=> (n / 2 > 0).
+; CHECK:         Determining loop execution counts for: @test_ext_01neg
+; 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 @test_ext_02(i32 %n) nounwind {
+; Prove that (n >= 2) ===> (n / 2 > 0).
+; CHECK:         Determining loop execution counts for: @test_ext_02
+; 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 @test_ext_02neg(i32 %n) nounwind {
+; Prove that (n >= 1) =\=> (n / 2 > 0).
+; CHECK:         Determining loop execution counts for: @test_ext_02neg
+; 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 @test_ext_03(i32 %n) nounwind {
+; Prove that (n > -2) ===> (n / 2 >= 0).
+; CHECK:         Determining loop execution counts for: @test_ext_03
+; 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 @test_ext_03neg(i32 %n) nounwind {
+; Prove that (n > -3) =\=> (n / 2 >= 0).
+; CHECK:         Determining loop execution counts for: @test_ext_03neg
+; 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 @test_ext_04(i32 %n) nounwind {
+; Prove that (n >= -1) ===> (n / 2 >= 0).
+; CHECK:         Determining loop execution counts for: @test_ext_04
+; 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 @test_ext_04neg(i32 %n) nounwind {
+; Prove that (n >= -2) =\=> (n / 2 >= 0).
+; CHECK:         Determining loop execution counts for: @test_ext_04neg
+; 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
+}