[llvm] r249168 - [SCEV] Try to prove predicates by splitting them
Sanjoy Das via llvm-commits
llvm-commits at lists.llvm.org
Fri Oct 2 11:50:30 PDT 2015
Author: sanjoy
Date: Fri Oct 2 13:50:30 2015
New Revision: 249168
URL: http://llvm.org/viewvc/llvm-project?rev=249168&view=rev
Log:
[SCEV] Try to prove predicates by splitting them
Summary:
This change teaches SCEV that to prove `A u< B` it is sufficient to
prove each of these facts individually:
- B >= 0
- A s< B
- A >= 0
In practice, SCEV sometimes finds it easier to prove these facts
individually than to prove `A u< B` as one atomic step.
Reviewers: reames, atrick, nlewycky, hfinkel
Subscribers: sanjoy, llvm-commits
Differential Revision: http://reviews.llvm.org/D13042
Modified:
llvm/trunk/include/llvm/Analysis/ScalarEvolution.h
llvm/trunk/lib/Analysis/ScalarEvolution.cpp
llvm/trunk/test/Transforms/IndVarSimplify/eliminate-comparison.ll
Modified: llvm/trunk/include/llvm/Analysis/ScalarEvolution.h
URL: http://llvm.org/viewvc/llvm-project/llvm/trunk/include/llvm/Analysis/ScalarEvolution.h?rev=249168&r1=249167&r2=249168&view=diff
==============================================================================
--- llvm/trunk/include/llvm/Analysis/ScalarEvolution.h (original)
+++ llvm/trunk/include/llvm/Analysis/ScalarEvolution.h Fri Oct 2 13:50:30 2015
@@ -253,6 +253,10 @@ namespace llvm {
/// conditions dominating the backedge of a loop.
bool WalkingBEDominatingConds;
+ /// Set to true by isKnownPredicateViaSplitting when we're trying to prove a
+ /// predicate by splitting it into a set of independent predicates.
+ bool ProvingSplitPredicate;
+
/// Information about the number of loop iterations for which a loop exit's
/// branch condition evaluates to the not-taken path. This is a temporary
/// pair of exact and max expressions that are eventually summarized in
@@ -559,6 +563,11 @@ namespace llvm {
bool isKnownPredicateWithRanges(ICmpInst::Predicate Pred,
const SCEV *LHS, const SCEV *RHS);
+ /// Try to split Pred LHS RHS into logical conjunctions (and's) and try to
+ /// prove them individually.
+ bool isKnownPredicateViaSplitting(ICmpInst::Predicate Pred, const SCEV *LHS,
+ const SCEV *RHS);
+
/// Drop memoized information computed for S.
void forgetMemoizedResults(const SCEV *S);
Modified: llvm/trunk/lib/Analysis/ScalarEvolution.cpp
URL: http://llvm.org/viewvc/llvm-project/llvm/trunk/lib/Analysis/ScalarEvolution.cpp?rev=249168&r1=249167&r2=249168&view=diff
==============================================================================
--- llvm/trunk/lib/Analysis/ScalarEvolution.cpp (original)
+++ llvm/trunk/lib/Analysis/ScalarEvolution.cpp Fri Oct 2 13:50:30 2015
@@ -6764,6 +6764,9 @@ bool ScalarEvolution::isKnownPredicate(I
if (LeftGuarded && RightGuarded)
return true;
+ if (isKnownPredicateViaSplitting(Pred, LHS, RHS))
+ return true;
+
// Otherwise see what can be done with known constant ranges.
return isKnownPredicateWithRanges(Pred, LHS, RHS);
}
@@ -6969,6 +6972,31 @@ ScalarEvolution::isKnownPredicateWithRan
return false;
}
+bool ScalarEvolution::isKnownPredicateViaSplitting(ICmpInst::Predicate Pred,
+ const SCEV *LHS,
+ const SCEV *RHS) {
+ if (ProvingSplitPredicate)
+ return false;
+
+ // Allowing arbitrary number of activations of isKnownPredicateViaSplitting on
+ // the stack can result in exponential time complexity.
+ SaveAndRestore<bool> Restore(ProvingSplitPredicate, true);
+
+ // If L >= 0 then I `ult` L <=> I >= 0 && I `slt` L
+ //
+ // To prove L >= 0 we use isKnownNonNegative whereas to prove I >= 0 we use
+ // isKnownPredicate. isKnownPredicate is more powerful, but also more
+ // expensive; and using isKnownNonNegative(RHS) is sufficient for most of the
+ // interesting cases seen in practice. We can consider "upgrading" L >= 0 to
+ // use isKnownPredicate later if needed.
+ if (Pred == ICmpInst::ICMP_ULT && isKnownNonNegative(RHS) &&
+ isKnownPredicate(CmpInst::ICMP_SGE, LHS, getZero(LHS->getType())) &&
+ isKnownPredicate(CmpInst::ICMP_SLT, LHS, RHS))
+ return true;
+
+ return false;
+}
+
/// isLoopBackedgeGuardedByCond - Test whether the backedge of the loop is
/// protected by a conditional between LHS and RHS. This is used to
/// to eliminate casts.
@@ -8529,14 +8557,15 @@ ScalarEvolution::ScalarEvolution(Functio
LoopInfo &LI)
: F(F), TLI(TLI), AC(AC), DT(DT), LI(LI),
CouldNotCompute(new SCEVCouldNotCompute()),
- WalkingBEDominatingConds(false), ValuesAtScopes(64), LoopDispositions(64),
- BlockDispositions(64), FirstUnknown(nullptr) {}
+ WalkingBEDominatingConds(false), ProvingSplitPredicate(false),
+ ValuesAtScopes(64), LoopDispositions(64), BlockDispositions(64),
+ FirstUnknown(nullptr) {}
ScalarEvolution::ScalarEvolution(ScalarEvolution &&Arg)
: F(Arg.F), TLI(Arg.TLI), AC(Arg.AC), DT(Arg.DT), LI(Arg.LI),
CouldNotCompute(std::move(Arg.CouldNotCompute)),
ValueExprMap(std::move(Arg.ValueExprMap)),
- WalkingBEDominatingConds(false),
+ WalkingBEDominatingConds(false), ProvingSplitPredicate(false),
BackedgeTakenCounts(std::move(Arg.BackedgeTakenCounts)),
ConstantEvolutionLoopExitValue(
std::move(Arg.ConstantEvolutionLoopExitValue)),
@@ -8573,6 +8602,7 @@ ScalarEvolution::~ScalarEvolution() {
assert(PendingLoopPredicates.empty() && "isImpliedCond garbage");
assert(!WalkingBEDominatingConds && "isLoopBackedgeGuardedByCond garbage!");
+ assert(!ProvingSplitPredicate && "ProvingSplitPredicate garbage!");
}
bool ScalarEvolution::hasLoopInvariantBackedgeTakenCount(const Loop *L) {
Modified: llvm/trunk/test/Transforms/IndVarSimplify/eliminate-comparison.ll
URL: http://llvm.org/viewvc/llvm-project/llvm/trunk/test/Transforms/IndVarSimplify/eliminate-comparison.ll?rev=249168&r1=249167&r2=249168&view=diff
==============================================================================
--- llvm/trunk/test/Transforms/IndVarSimplify/eliminate-comparison.ll (original)
+++ llvm/trunk/test/Transforms/IndVarSimplify/eliminate-comparison.ll Fri Oct 2 13:50:30 2015
@@ -394,4 +394,87 @@ bb3:
ret i1 true
}
+define void @func_19(i32* %length.ptr) {
+; CHECK-LABEL: @func_19(
+ entry:
+ %length = load i32, i32* %length.ptr, !range !0
+ %length.is.nonzero = icmp ne i32 %length, 0
+ br i1 %length.is.nonzero, label %loop, label %leave
+
+ loop:
+; CHECK: loop:
+ %iv = phi i32 [ 0, %entry ], [ %iv.inc, %be ]
+ %iv.inc = add i32 %iv, 1
+ %range.check = icmp ult i32 %iv, %length
+ br i1 %range.check, label %be, label %leave
+; CHECK: br i1 true, label %be, label %leave.loopexit
+; CHECK: be:
+
+ be:
+ call void @side_effect()
+ %be.cond = icmp slt i32 %iv.inc, %length
+ br i1 %be.cond, label %loop, label %leave
+
+ leave:
+ ret void
+}
+
+define void @func_20(i32* %length.ptr) {
+; Like @func_19, but %length is no longer provably positive, so
+; %range.check cannot be proved to be always true.
+
+; CHECK-LABEL: @func_20(
+ entry:
+ %length = load i32, i32* %length.ptr
+ %length.is.nonzero = icmp ne i32 %length, 0
+ br i1 %length.is.nonzero, label %loop, label %leave
+
+ loop:
+; CHECK: loop:
+ %iv = phi i32 [ 0, %entry ], [ %iv.inc, %be ]
+ %iv.inc = add i32 %iv, 1
+ %range.check = icmp ult i32 %iv, %length
+ br i1 %range.check, label %be, label %leave
+; CHECK: br i1 %range.check, label %be, label %leave.loopexit
+; CHECK: be:
+
+ be:
+ call void @side_effect()
+ %be.cond = icmp slt i32 %iv.inc, %length
+ br i1 %be.cond, label %loop, label %leave
+
+ leave:
+ ret void
+}
+
+define void @func_21(i32* %length.ptr, i32 %init) {
+; Like @func_19, but it is no longer possible to prove %iv's start
+; value is positive without doing some control flow analysis.
+
+; CHECK-LABEL: @func_21(
+ entry:
+ %length = load i32, i32* %length.ptr, !range !0
+ %length.is.nonzero = icmp ne i32 %length, 0
+ %init.is.positive = icmp sgt i32 %init, 0
+ %entry.cond = and i1 %length.is.nonzero, %init.is.positive
+ br i1 %length.is.nonzero, label %loop, label %leave
+
+ loop:
+; CHECK: loop:
+ %iv = phi i32 [ 0, %entry ], [ %iv.inc, %be ]
+ %iv.inc = add i32 %iv, 1
+ %range.check = icmp ult i32 %iv, %length
+ br i1 %range.check, label %be, label %leave
+; CHECK: br i1 true, label %be, label %leave.loopexit
+; CHECK: be:
+
+ be:
+ call void @side_effect()
+ %be.cond = icmp slt i32 %iv.inc, %length
+ br i1 %be.cond, label %loop, label %leave
+
+ leave:
+ ret void
+}
+
!0 = !{i32 0, i32 2147483647}
More information about the llvm-commits
mailing list