[InstSimplify] Fold simple known implications to true

This was split off of http://reviews.llvm.org/D13040 to make it easier to test the correctness of the implication logic. For the moment, this only handles a single easy case which shows up when eliminating and combining range checks. In the (near) future, I plan to extend this for other cases which show up in range checks, but I wanted to make those changes incrementally once the framework was in place.

At the moment, the implication logic will be used by three places. One in InstSimplify (this review) and two in SimplifyCFG (http://reviews.llvm.org/D13040 & http://reviews.llvm.org/D13070). Can anyone think of other locations this style of reasoning would make sense?

Differential Revision: http://reviews.llvm.org/D13074

git-svn-id: https://llvm.org/svn/llvm-project/llvm/trunk@248719 91177308-0d34-0410-b5e6-96231b3b80d8

diff --git a/lib/Analysis/InstructionSimplify.cpp b/lib/Analysis/InstructionSimplify.cpp
index 2086337df8b02ff03bfe434281bf3dd07dc9622c..c8a13c79f576292e77fc3addf7e557048cc84f5b 100644 (file)
--- a/lib/Analysis/InstructionSimplify.cpp
+++ b/lib/Analysis/InstructionSimplify.cpp
@@ -2128,6 +2128,47 @@ static Constant *computePointerICmp(const DataLayout &DL,
   return nullptr;
 }
 
+/// Return true if B is known to be implied by A.  A & B must be i1 (boolean)
+/// values. Note that the truth table for implication is the same as <=u on i1
+/// values (but not <=s!).  The truth table for both is:
+///    | T | F (B)
+///  T | T | F
+///  F | T | T
+/// (A)
+static bool implies(Value *A, Value *B) {
+  // TODO: Consider extending this to vector of i1?
+  assert(A->getType()->isIntegerTy(1) && B->getType()->isIntegerTy(1));
+  
+  // A ==> A by definition
+  if (A == B) return true;
+
+  ICmpInst::Predicate APred, BPred;
+  Value *I;
+  Value *L;
+  ConstantInt *CI;
+  // i +_{nsw} C_{>0} <s L ==> i <s L
+  if (match(A, m_ICmp(APred,
+                      m_NSWAdd(m_Value(I), m_ConstantInt(CI)),
+                      m_Value(L))) &&
+      APred == ICmpInst::ICMP_SLT &&
+      !CI->isNegative() &&
+      match(B, m_ICmp(BPred, m_Specific(I), m_Specific(L))) &&
+      BPred == ICmpInst::ICMP_SLT)
+    return true;
+
+  // i +_{nuw} C_{>0} <u L ==> i <u L
+  if (match(A, m_ICmp(APred,
+                      m_NUWAdd(m_Value(I), m_ConstantInt(CI)),
+                      m_Value(L))) &&
+      APred == ICmpInst::ICMP_ULT &&
+      !CI->isNegative() &&
+      match(B, m_ICmp(BPred, m_Specific(I), m_Specific(L))) &&
+      BPred == ICmpInst::ICMP_ULT)
+    return true;
+
+  return false;
+}
+
 static ConstantRange GetConstantRangeFromMetadata(MDNode *Ranges, uint32_t BitWidth) {
   const unsigned NumRanges = Ranges->getNumOperands() / 2;
   assert(NumRanges >= 1);
@@ -2199,6 +2240,8 @@ static Value *SimplifyICmpInst(unsigned Predicate, Value *LHS, Value *RHS,
       // X >=u 1 -> X
       if (match(RHS, m_One()))
         return LHS;
+      if (implies(RHS, LHS))
+        return getTrue(ITy);
       break;
     case ICmpInst::ICMP_SLT:
       // X <s 0 -> X
@@ -2210,6 +2253,10 @@ static Value *SimplifyICmpInst(unsigned Predicate, Value *LHS, Value *RHS,
       if (match(RHS, m_One()))
         return LHS;
       break;
+    case ICmpInst::ICMP_ULE:
+      if (implies(LHS, RHS))
+        return getTrue(ITy);
+      break;
     }
   }
 

diff --git a/test/Transforms/InstSimplify/implies.ll b/test/Transforms/InstSimplify/implies.ll
new file mode 100644 (file)
index 0000000..19e6193
--- /dev/null
+++ b/test/Transforms/InstSimplify/implies.ll
@@ -0,0 +1,77 @@
+; RUN: opt -S %s -instsimplify | FileCheck %s
+
+; A ==> A -> true
+define i1 @test(i32 %length.i, i32 %i) {
+; CHECK-LABEL: @test
+; CHECK: ret i1 true
+  %var29 = icmp slt i32 %i, %length.i
+  %res = icmp uge i1 %var29, %var29
+  ret i1 %res
+}
+
+; i +_{nsw} C_{>0} <s L ==> i <s L -> true
+define i1 @test2(i32 %length.i, i32 %i) {
+; CHECK-LABEL: @test2
+; CHECK: ret i1 true
+  %iplus1 = add nsw i32 %i, 1
+  %var29 = icmp slt i32 %i, %length.i
+  %var30 = icmp slt i32 %iplus1, %length.i
+  %res = icmp ule i1 %var30, %var29
+  ret i1 %res
+}
+
+; i + C_{>0} <s L ==> i <s L -> unknown without the nsw
+define i1 @test2_neg(i32 %length.i, i32 %i) {
+; CHECK-LABEL: @test2_neg
+; CHECK:   ret i1 %res
+  %iplus1 = add i32 %i, 1
+  %var29 = icmp slt i32 %i, %length.i
+  %var30 = icmp slt i32 %iplus1, %length.i
+  %res = icmp ule i1 %var30, %var29
+  ret i1 %res
+}
+
+; sle is not implication
+define i1 @test2_neg2(i32 %length.i, i32 %i) {
+; CHECK-LABEL: @test2_neg2
+; CHECK:   ret i1 %res
+  %iplus1 = add i32 %i, 1
+  %var29 = icmp slt i32 %i, %length.i
+  %var30 = icmp slt i32 %iplus1, %length.i
+  %res = icmp sle i1 %var30, %var29
+  ret i1 %res
+}
+
+; The binary operator has to be an add
+define i1 @test2_neg3(i32 %length.i, i32 %i) {
+; CHECK-LABEL: @test2_neg3
+; CHECK:   ret i1 %res
+  %iplus1 = sub nsw i32 %i, 1
+  %var29 = icmp slt i32 %i, %length.i
+  %var30 = icmp slt i32 %iplus1, %length.i
+  %res = icmp ule i1 %var30, %var29
+  ret i1 %res
+}
+
+; i +_{nsw} C_{>0} <s L ==> i <s L -> true
+; With an inverted conditional (ule B A rather than canonical ugt A B
+define i1 @test3(i32 %length.i, i32 %i) {
+; CHECK-LABEL: @test3
+; CHECK: ret i1 true
+  %iplus1 = add nsw i32 %i, 1
+  %var29 = icmp slt i32 %i, %length.i
+  %var30 = icmp slt i32 %iplus1, %length.i
+  %res = icmp uge i1 %var29, %var30
+  ret i1 %res
+}
+
+; i +_{nuw} C_{>0} <u L ==> i <u L
+define i1 @test4(i32 %length.i, i32 %i) {
+; CHECK-LABEL: @test4
+; CHECK: ret i1 true
+  %iplus1 = add nuw i32 %i, 1
+  %var29 = icmp ult i32 %i, %length.i
+  %var30 = icmp ult i32 %iplus1, %length.i
+  %res = icmp ule i1 %var30, %var29
+  ret i1 %res
+}