[InstSimplify] Fold simple known implications to true

[reames]

Summary

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 two 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?

[sanjoy]

lib/Analysis/InstructionSimplify.cpp

2140

Same comment here as in D13040: "Why not use matchers from PatternMatch.h here? I think that will make the logic a lot more obvious."

2216

You could also match >=s here.

[reames]

Match via pattern matchers not raw inspection; in the process fix a bug - I was accepting any binary operator, not just add.

Handle one more case while I'm at it.

[reames]

lib/Analysis/InstructionSimplify.cpp

2216

Pretty sure I can't use signed compares. I believe "1" is interpreted as "-1" in a signed compare. This generates a different truth table.

[hfinkel]

lib/Analysis/InstructionSimplify.cpp

2216

FWIW, yes, i1 signed values are interpreted as 0 and -1.

[sanjoy]

lib/Analysis/InstructionSimplify.cpp

2216

I was taking about matching LHS >=s RHS as LHS implies RHS. I
think the truth table is

LHS | RHS | LHS >=s RHS   | LHS implies RHS
 0  |  0  |  1 (0 >= 0)   |  1
 0  |  1  |  1 (0 >= -1)  |  1
 1  |  0  |  0 (-1 >= 0)  |  0
 1  |  1  |  1 (-1 >= -1) |  1

[reames]

lib/Analysis/InstructionSimplify.cpp

2216

Hm, interesting. You appear to be right. Assume I've added this, anything else?

[sanjoy]

This looks good to me (both with or without the sle change, as you see fit), but given that I haven't worked on instsimplify, I'd wait for @hfinkel to take a final look.

I don't know if instcombine transforms Not(A) | B to A ULE B. If it does not, adding that seems like a logical thing to do (in a later change) -- I think that's a more idiomatic way to represent implication.

[reames]

Ping. Hal? David?

[hfinkel]

LGTM too.

lib/Analysis/InstructionSimplify.cpp

if ((IsNAC(LHSUObjs) && IsAllocDisjoint(RHSUObjs)) ||
         return ConstantInt::get(GetCompareTy(LHS),
                                 !CmpInst::isTrueWhenEqual(Pred));
   }
 
   // Otherwise, fail.
   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;
+}
+
 /// SimplifyICmpInst - Given operands for an ICmpInst, see if we can
 /// fold the result.  If not, this returns null.
 static Value *SimplifyICmpInst(unsigned Predicate, Value *LHS, Value *RHS,
                                const Query &Q, unsigned MaxRecurse) {
   CmpInst::Predicate Pred = (CmpInst::Predicate)Predicate;
   assert(CmpInst::isIntPredicate(Pred) && "Not an integer compare!");
 
   if (Constant *CLHS = dyn_cast<Constant>(LHS)) {
case ICmpInst::ICMP_NE:
       if (match(RHS, m_Zero()))
         return LHS;
       break;
     case ICmpInst::ICMP_UGT:
       // X >u 0 -> X
       if (match(RHS, m_Zero()))
         return LHS;
       break;
     case ICmpInst::ICMP_UGE:
       // 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
       if (match(RHS, m_Zero()))
         return LHS;
       break;
     case ICmpInst::ICMP_SLE:
       // X <=s -1 -> X
       if (match(RHS, m_One()))
         return LHS;
       break;
+    case ICmpInst::ICMP_ULE:
+      if (implies(LHS, RHS))
+        return getTrue(ITy);
+      break;
     }
   }
 
   // If we are comparing with zero then try hard since this is a common case.
   if (match(RHS, m_Zero())) {
     bool LHSKnownNonNegative, LHSKnownNegative;
     switch (Pred) {
     default: llvm_unreachable("Unknown ICmp predicate!");

test/Transforms/InstSimplify/implies.ll

+; 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
+}