[llvm] r298481 - [ScalarEvolution] Predicate implication from operations
Max Kazantsev via llvm-commits
llvm-commits at lists.llvm.org
Tue Mar 21 21:48:47 PDT 2017
Author: mkazantsev
Date: Tue Mar 21 23:48:46 2017
New Revision: 298481
URL: http://llvm.org/viewvc/llvm-project?rev=298481&view=rev
Log:
[ScalarEvolution] Predicate implication from operations
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:
(A >X && B >= 0) || (B >= 0 && A > X) ===> (A + B) > X.
For division:
(A > X) && (0 < B <= X + 1) ===> (A / B > 0).
(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".
Diffirential Revision: https://reviews.llvm.org/D30887
Reviewed by: sanjoy
Added:
llvm/trunk/test/Analysis/ScalarEvolution/scev-division.ll
Modified:
llvm/trunk/include/llvm/Analysis/ScalarEvolution.h
llvm/trunk/lib/Analysis/ScalarEvolution.cpp
Modified: llvm/trunk/include/llvm/Analysis/ScalarEvolution.h
URL: http://llvm.org/viewvc/llvm-project/llvm/trunk/include/llvm/Analysis/ScalarEvolution.h?rev=298481&r1=298480&r2=298481&view=diff
==============================================================================
--- llvm/trunk/include/llvm/Analysis/ScalarEvolution.h (original)
+++ llvm/trunk/include/llvm/Analysis/ScalarEvolution.h Tue Mar 21 23:48:46 2017
@@ -978,6 +978,20 @@ private:
/// 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,
@@ -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.
///
Modified: llvm/trunk/lib/Analysis/ScalarEvolution.cpp
URL: http://llvm.org/viewvc/llvm-project/llvm/trunk/lib/Analysis/ScalarEvolution.cpp?rev=298481&r1=298480&r2=298481&view=diff
==============================================================================
--- llvm/trunk/lib/Analysis/ScalarEvolution.cpp (original)
+++ llvm/trunk/lib/Analysis/ScalarEvolution.cpp Tue Mar 21 23:48:46 2017
@@ -137,6 +137,11 @@ static cl::opt<unsigned> MaxSCEVCompareD
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"),
@@ -3418,6 +3423,10 @@ Type *ScalarEvolution::getEffectiveSCEVT
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();
}
@@ -8532,19 +8541,137 @@ static bool IsKnownPredicateViaMinOrMax(
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) {
+ // 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) {
+ 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:
@@ -8554,30 +8681,34 @@ ScalarEvolution::isImpliedCondOperandsHe
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;
}
Added: llvm/trunk/test/Analysis/ScalarEvolution/scev-division.ll
URL: http://llvm.org/viewvc/llvm-project/llvm/trunk/test/Analysis/ScalarEvolution/scev-division.ll?rev=298481&view=auto
==============================================================================
--- llvm/trunk/test/Analysis/ScalarEvolution/scev-division.ll (added)
+++ llvm/trunk/test/Analysis/ScalarEvolution/scev-division.ll Tue Mar 21 23:48:46 2017
@@ -0,0 +1,334 @@
+; 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
+}
+
More information about the llvm-commits
mailing list