[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

llvm-svn: 298481

1 files changed, 334 insertions, 0 deletions

diff --git a/llvm/test/Analysis/ScalarEvolution/scev-division.ll b/llvm/test/Analysis/ScalarEvolution/scev-division.ll
new file mode 100644
index 00000000000..230ffa3bbd6
--- /dev/null
+++ b/llvm/test/Analysis/ScalarEvolution/scev-division.ll
@@ -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
+}
+