[ConstraintElimination] Handle solving-only non-equality predicates

[antoniofrighetto]

Summary

Simplification of non-equality predicates for solving constraints system is now supported by checking the validity of related inequalities and equalities.

[fhahn]

llvm/lib/Transforms/Scalar/ConstraintElimination.cpp

536

I think this is not correct, as this effectively means we will be adding Op0 <= Op1 to the constraint system as fact for Op0 != Op1 at the moment. To start with, it would be good to only support NE predicates for solving, not when adding facts.

A test case that shows the issue is below. Would be good to have similar variants with UGE/UGT/ULT and signed variants.

define i1 @assume(i64 %a, i64 %b, i64 %c) {
  %1 = icmp ne i64 %a, %b
  tail call void @llvm.assume(i1 %1)
  %r = icmp ule i64 %a, %b
  ret i1 %r
}

llvm/test/Transforms/ConstraintElimination/ne.ll

298

please add the additional test coverage separately. It would also be good to use names for the various values (instead of numbers) so they are easier to modify/play with.

[antoniofrighetto]

Reviewing this, as, indeed, I have been meaning to add this for solving only, not as fact for now, which would need further handling. I believe that simplifying NE to ULE for solving only, as it is being done for EQ, should be OK though. For facts, we should add something close to (Op0 < Op1) ∨ (Op1 > Op0), but I need to think further on how to model this. Perhaps, for now we could return from addFact when if (!R.isValid(*this) || R.IsNe()).

[fhahn]

llvm/lib/Transforms/Scalar/ConstraintElimination.cpp

671–673

might be good to expand the comment here, explaining how this handles == and !=. Same below.

llvm/test/Transforms/ConstraintElimination/assumes.ll

626 ↗

(On Diff #530510)

better move those to ne.ll and also add variants with ule/uge. Would be good to add the tests separately.

[antoniofrighetto]

I think for now it should be fine to handle ICMP_NE in solving, support for facts to be added at a later time.

[fhahn]

LGTM, thanks!

llvm/test/Transforms/ConstraintElimination/ne.ll

408

Might be good to add a TODO for signed support.

llvm/lib/Transforms/Scalar/ConstraintElimination.cpp

struct ConstraintTy {
   SmallVector<PreconditionTy, 2> Preconditions;
 
   SmallVector<SmallVector<int64_t, 8>> ExtraInfo;
 
   bool IsSigned = false;
 
   ConstraintTy() = default;
 
-  ConstraintTy(SmallVector<int64_t, 8> Coefficients, bool IsSigned, bool IsEq)
-      : Coefficients(Coefficients), IsSigned(IsSigned), IsEq(IsEq) {}
+  ConstraintTy(SmallVector<int64_t, 8> Coefficients, bool IsSigned, bool IsEq,
+               bool IsNe)
+      : Coefficients(Coefficients), IsSigned(IsSigned), IsEq(IsEq), IsNe(IsNe) {
+  }
 
   unsigned size() const { return Coefficients.size(); }
 
   unsigned empty() const { return Coefficients.empty(); }
 
   /// Returns true if all preconditions for this list of constraints are
   /// satisfied given \p CS and the corresponding \p Value2Index mapping.
   bool isValid(const ConstraintInfo &Info) const;
 
   bool isEq() const { return IsEq; }
 
+  bool isNe() const { return IsNe; }
+
   /// Check if the current constraint is implied by the given ConstraintSystem.
   ///
   /// \return true or false if the constraint is proven to be respectively true,
   /// or false. When the constraint cannot be proven to be either true or false,
   /// std::nullopt is returned.
   std::optional<bool> isImpliedBy(const ConstraintSystem &CS) const;
 
 private:
   bool IsEq = false;
+  bool IsNe = false;
 };
 
 /// Wrapper encapsulating separate constraint systems and corresponding value
 /// mappings for both unsigned and signed information. Facts are added to and
 /// conditions are checked against the corresponding system depending on the
 /// signed-ness of their predicates. While the information is kept separate
 /// based on signed-ness, certain conditions can be transferred between the two
 /// systems.
static Decomposition decompose(Value *V,
   return {V, IsKnownNonNegative};
 }
 
 ConstraintTy
 ConstraintInfo::getConstraint(CmpInst::Predicate Pred, Value *Op0, Value *Op1,
                               SmallVectorImpl<Value *> &NewVariables) const {
   assert(NewVariables.empty() && "NewVariables must be empty when passed in");
   bool IsEq = false;
+  bool IsNe = false;
+
   // Try to convert Pred to one of ULE/SLT/SLE/SLT.
   switch (Pred) {
   case CmpInst::ICMP_UGT:
   case CmpInst::ICMP_UGE:
   case CmpInst::ICMP_SGT:
   case CmpInst::ICMP_SGE: {
     Pred = CmpInst::getSwappedPredicate(Pred);
     std::swap(Op0, Op1);
     break;
   }
   case CmpInst::ICMP_EQ:
     if (match(Op1, m_Zero())) {
       Pred = CmpInst::ICMP_ULE;
     } else {
       IsEq = true;
       Pred = CmpInst::ICMP_ULE;
     }
     break;
   case CmpInst::ICMP_NE:
-    if (!match(Op1, m_Zero()))
-      return {};
+    if (match(Op1, m_Zero())) {
       Pred = CmpInst::getSwappedPredicate(CmpInst::ICMP_UGT);
       std::swap(Op0, Op1);
+    } else {
+      IsNe = true;
+      Pred = CmpInst::ICMP_ULE;
+    }
     break;
   default:
     break;
   }
 
   if (Pred != CmpInst::ICMP_ULE && Pred != CmpInst::ICMP_ULT &&
       Pred != CmpInst::ICMP_SLE && Pred != CmpInst::ICMP_SLT)
     return {};
ConstraintInfo::getConstraint(CmpInst::Predicate Pred, Value *Op0, Value *Op1,
   // Make sure all variables have entries in Value2Index or NewVariables.
   for (const auto &KV : concat<DecompEntry>(VariablesA, VariablesB))
     GetOrAddIndex(KV.Variable);
 
   // Build result constraint, by first adding all coefficients from A and then
   // subtracting all coefficients from B.
   ConstraintTy Res(
       SmallVector<int64_t, 8>(Value2Index.size() + NewVariables.size() + 1, 0),
-      IsSigned, IsEq);
+      IsSigned, IsEq, IsNe);
   // Collect variables that are known to be positive in all uses in the
   // constraint.
   DenseMap<Value *, bool> KnownNonNegativeVariables;
   auto &R = Res.Coefficients;
   for (const auto &KV : VariablesA) {
     R[GetOrAddIndex(KV.Variable)] += KV.Coefficient;
     auto I =
         KnownNonNegativeVariables.insert({KV.Variable, KV.IsKnownNonNegative});
return Coefficients.size() > 0 &&
            return Info.doesHold(C.Pred, C.Op0, C.Op1);
          });
 }
 
 std::optional<bool>
 ConstraintTy::isImpliedBy(const ConstraintSystem &CS) const {
   bool IsConditionImplied = CS.isConditionImplied(Coefficients);
 
-  if (IsEq) {
+  if (IsEq || IsNe) {
     auto NegatedOrEqual = ConstraintSystem::negateOrEqual(Coefficients);
     bool IsNegatedOrEqualImplied =
         !NegatedOrEqual.empty() && CS.isConditionImplied(NegatedOrEqual);
 
-    // In order to check that `%a == %b` is true, we want to check that `%a >=
-    // %b` and `%a <= %b` must hold.
+    // In order to check that `%a == %b` is true (equality), both conditions `%a
+    // >= %b` and `%a <= %b` must hold true. When checking for equality (`IsEq`
+    // is true), we return true if they both hold, false in the other cases.
     if (IsConditionImplied && IsNegatedOrEqualImplied)
-      return true;
+      return IsEq;
 
     auto Negated = ConstraintSystem::negate(Coefficients);
     bool IsNegatedImplied = !Negated.empty() && CS.isConditionImplied(Negated);
 
     auto StrictLessThan = ConstraintSystem::toStrictLessThan(Coefficients);
     bool IsStrictLessThanImplied =
         !StrictLessThan.empty() && CS.isConditionImplied(StrictLessThan);
 
-    // In order to check that `%a == %b` is false, we want to check whether
-    // either `%a > %b` or `%a < %b` holds.
+    // In order to check that `%a != %b` is true (non-equality), either
+    // condition `%a > %b` or `%a < %b` must hold true. When checking for
+    // non-equality (`IsNe` is true), we return true if one of the two holds,
+    // false in the other cases.
     if (IsNegatedImplied || IsStrictLessThanImplied)
-      return false;
+      return IsNe;
 
     return std::nullopt;
   }
 
   if (IsConditionImplied)
     return true;
 
   auto Negated = ConstraintSystem::negate(Coefficients);

 
 void ConstraintInfo::addFact(CmpInst::Predicate Pred, Value *A, Value *B,
                              unsigned NumIn, unsigned NumOut,
                              SmallVectorImpl<StackEntry> &DFSInStack) {
   // If the constraint has a pre-condition, skip the constraint if it does not
   // hold.
   SmallVector<Value *> NewVariables;
   auto R = getConstraint(Pred, A, B, NewVariables);
-  if (!R.isValid(*this))
+
+  // TODO: Support non-equality for facts as well.
+  if (!R.isValid(*this) || R.isNe())
     return;
 
   LLVM_DEBUG(dbgs() << "Adding '" << Pred << " ";
              A->printAsOperand(dbgs(), false); dbgs() << ", ";
              B->printAsOperand(dbgs(), false); dbgs() << "'\n");
   bool Added = false;
   auto &CSToUse = getCS(R.IsSigned);
   if (R.Coefficients.empty())

llvm/test/Transforms/ConstraintElimination/constants-unsigned-predicates.ll

entry:
   ret i1 %res.2
 }
 
 define i1 @test_ne() {
 ; CHECK-LABEL: @test_ne(
 ; CHECK-NEXT:  entry:
 ; CHECK-NEXT:    [[T_0:%.*]] = icmp ne i8 10, 11
 ; CHECK-NEXT:    [[F_0:%.*]] = icmp ne i8 10, 10
-; CHECK-NEXT:    [[RES_1:%.*]] = xor i1 [[T_0]], [[F_0]]
+; CHECK-NEXT:    [[RES_1:%.*]] = xor i1 true, false
 ; CHECK-NEXT:    [[T_1:%.*]] = icmp ne i8 10, 9
-; CHECK-NEXT:    [[RES_2:%.*]] = xor i1 [[RES_1]], [[T_1]]
+; CHECK-NEXT:    [[RES_2:%.*]] = xor i1 [[RES_1]], true
 ; CHECK-NEXT:    ret i1 [[RES_2]]
 ;
 entry:
   %t.0 = icmp ne i8 10, 11
   %f.0 = icmp ne i8 10, 10
   %res.1 = xor i1 %t.0, %f.0
   %t.1 = icmp ne i8 10, 9
   %res.2 = xor i1 %res.1, %t.1
   ret i1 %res.2
 }

llvm/test/Transforms/ConstraintElimination/ne.ll

 ; NOTE: Assertions have been autogenerated by utils/update_test_checks.py UTC_ARGS: --check-attributes
 ; RUN: opt -passes=constraint-elimination -S %s | FileCheck %s
 
+declare void @llvm.assume(i1)
+
 define i1 @test_eq_ne_0(i8 %a, i8 %b) {
 ; CHECK-LABEL: @test_eq_ne_0(
 ; CHECK-NEXT:  entry:
 ; CHECK-NEXT:    [[CMP:%.*]] = icmp eq i8 [[A:%.*]], 0
 ; CHECK-NEXT:    br i1 [[CMP]], label [[THEN:%.*]], label [[ELSE:%.*]]
 ; CHECK:       then:
 ; CHECK-NEXT:    [[F_1:%.*]] = icmp ne i8 [[A]], 0
 ; CHECK-NEXT:    [[C_1:%.*]] = icmp ne i8 [[A]], 1
 ; CHECK-NEXT:    [[C_2:%.*]] = icmp ne i8 [[A]], [[B:%.*]]
-; CHECK-NEXT:    [[RES_1:%.*]] = xor i1 false, [[C_1]]
+; CHECK-NEXT:    [[RES_1:%.*]] = xor i1 false, true
 ; CHECK-NEXT:    [[RES_2:%.*]] = xor i1 [[RES_1]], [[C_2]]
 ; CHECK-NEXT:    ret i1 [[RES_2]]
 ; CHECK:       else:
 ; CHECK-NEXT:    [[T_1:%.*]] = icmp ne i8 [[A]], 0
 ; CHECK-NEXT:    [[C_3:%.*]] = icmp ne i8 [[A]], 1
 ; CHECK-NEXT:    [[C_4:%.*]] = icmp ne i8 [[A]], [[B]]
 ; CHECK-NEXT:    [[RES_3:%.*]] = xor i1 true, [[C_3]]
 ; CHECK-NEXT:    [[RES_4:%.*]] = xor i1 [[RES_3]], [[C_4]]

 ; CHECK-NEXT:    [[C_5:%.*]] = icmp ugt i8 [[A]], 1
 ; CHECK-NEXT:    [[RES_7:%.*]] = xor i1 [[RES_6]], [[C_5]]
 ; CHECK-NEXT:    [[C_6:%.*]] = icmp sgt i8 [[A]], 0
 ; CHECK-NEXT:    [[RES_8:%.*]] = xor i1 [[RES_7]], [[C_6]]
 ; CHECK-NEXT:    ret i1 [[RES_8]]
 ; CHECK:       else:
 ; CHECK-NEXT:    [[F_1:%.*]] = icmp ne i8 [[A]], 0
 ; CHECK-NEXT:    [[C_7:%.*]] = icmp ne i8 [[A]], 1
-; CHECK-NEXT:    [[RES_9:%.*]] = xor i1 false, [[C_7]]
+; CHECK-NEXT:    [[RES_9:%.*]] = xor i1 false, true
 ; CHECK-NEXT:    [[C_8:%.*]] = icmp ne i8 [[A]], [[B]]
 ; CHECK-NEXT:    [[RES_10:%.*]] = xor i1 [[RES_9]], [[C_8]]
 ; CHECK-NEXT:    [[C_9:%.*]] = icmp eq i8 [[A]], [[B]]
 ; CHECK-NEXT:    [[RES_11:%.*]] = xor i1 [[RES_10]], [[C_9]]
 ; CHECK-NEXT:    [[C_10:%.*]] = icmp eq i8 [[A]], 0
 ; CHECK-NEXT:    [[RES_12:%.*]] = xor i1 [[RES_11]], true
 ; CHECK-NEXT:    [[F_2:%.*]] = icmp ugt i8 [[A]], 0
 ; CHECK-NEXT:    [[RES_13:%.*]] = xor i1 [[RES_12]], false

 ; CHECK-LABEL: @test_eq_ne_1(
 ; CHECK-NEXT:  entry:
 ; CHECK-NEXT:    [[CMP:%.*]] = icmp eq i8 [[A:%.*]], 1
 ; CHECK-NEXT:    br i1 [[CMP]], label [[THEN:%.*]], label [[ELSE:%.*]]
 ; CHECK:       then:
 ; CHECK-NEXT:    [[F_1:%.*]] = icmp ne i8 [[A]], 0
 ; CHECK-NEXT:    [[C_1:%.*]] = icmp ne i8 [[A]], 1
 ; CHECK-NEXT:    [[C_2:%.*]] = icmp ne i8 [[A]], [[B:%.*]]
-; CHECK-NEXT:    [[RES_1:%.*]] = xor i1 true, [[C_1]]
+; CHECK-NEXT:    [[RES_1:%.*]] = xor i1 true, false
 ; CHECK-NEXT:    [[RES_2:%.*]] = xor i1 [[RES_1]], [[C_2]]
 ; CHECK-NEXT:    ret i1 [[RES_2]]
 ; CHECK:       else:
 ; CHECK-NEXT:    [[T_1:%.*]] = icmp ne i8 [[A]], 0
 ; CHECK-NEXT:    [[C_3:%.*]] = icmp ne i8 [[A]], 1
 ; CHECK-NEXT:    [[C_4:%.*]] = icmp ne i8 [[A]], [[B]]
 ; CHECK-NEXT:    [[RES_3:%.*]] = xor i1 [[T_1]], [[C_3]]
 ; CHECK-NEXT:    [[RES_4:%.*]] = xor i1 [[RES_3]], [[C_4]]

 ; CHECK-NEXT:    [[C_7:%.*]] = icmp ugt i8 [[A]], 1
 ; CHECK-NEXT:    [[RES_7:%.*]] = xor i1 [[RES_6]], [[C_5]]
 ; CHECK-NEXT:    [[C_8:%.*]] = icmp sgt i8 [[A]], 0
 ; CHECK-NEXT:    [[RES_8:%.*]] = xor i1 [[RES_7]], [[C_6]]
 ; CHECK-NEXT:    ret i1 [[RES_8]]
 ; CHECK:       else:
 ; CHECK-NEXT:    [[T_2:%.*]] = icmp ne i8 [[A]], 0
 ; CHECK-NEXT:    [[C_9:%.*]] = icmp ne i8 [[A]], 1
-; CHECK-NEXT:    [[RES_9:%.*]] = xor i1 true, [[C_9]]
+; CHECK-NEXT:    [[RES_9:%.*]] = xor i1 true, false
 ; CHECK-NEXT:    [[C_10:%.*]] = icmp ne i8 [[A]], [[B]]
 ; CHECK-NEXT:    [[RES_10:%.*]] = xor i1 [[RES_9]], [[C_10]]
 ; CHECK-NEXT:    [[C_11:%.*]] = icmp eq i8 [[A]], [[B]]
 ; CHECK-NEXT:    [[RES_11:%.*]] = xor i1 [[RES_10]], [[C_11]]
 ; CHECK-NEXT:    [[F_1:%.*]] = icmp eq i8 [[A]], 0
 ; CHECK-NEXT:    [[RES_12:%.*]] = xor i1 [[RES_11]], false
 ; CHECK-NEXT:    [[T_3:%.*]] = icmp ugt i8 [[A]], 0
 ; CHECK-NEXT:    [[RES_13:%.*]] = xor i1 [[RES_12]], true
else:
   %f.2 = icmp ugt i8 %a, 1
   %res.15 = xor i1 %res.14, %f.2
 
   %c.12 = icmp sgt i8 %a, 0
   %res.16 = xor i1 %res.15, %c.12
 
   ret i1 %res.16
 }
+
+define i1 @assume_b_plus_1_ult_a(i64 %a, i64 %b) {
+; CHECK-LABEL: @assume_b_plus_1_ult_a(
+; CHECK-NEXT:    [[TMP1:%.*]] = add nuw i64 [[B:%.*]], 1
+; CHECK-NEXT:    [[TMP2:%.*]] = icmp ult i64 [[TMP1]], [[A:%.*]]
+; CHECK-NEXT:    tail call void @llvm.assume(i1 [[TMP2]])
+; CHECK-NEXT:    [[TMP3:%.*]] = icmp ne i64 [[A]], [[B]]
+; CHECK-NEXT:    ret i1 true
+;
+  %1 = add nuw i64 %b, 1
+  %2 = icmp ult i64 %1, %a
+  tail call void @llvm.assume(i1 %2)
+  %3 = icmp ne i64 %a, %b
+  ret i1 %3
+}
+
+define i1 @assume_a_gt_b_and_b_ge_c(i64 %a, i64 %b, i64 %c) {
+; CHECK-LABEL: @assume_a_gt_b_and_b_ge_c(
+; CHECK-NEXT:    [[TMP1:%.*]] = icmp ugt i64 [[A:%.*]], [[B:%.*]]
+; CHECK-NEXT:    tail call void @llvm.assume(i1 [[TMP1]])
+; CHECK-NEXT:    [[TMP2:%.*]] = icmp uge i64 [[B]], [[C:%.*]]
+; CHECK-NEXT:    tail call void @llvm.assume(i1 [[TMP2]])
+; CHECK-NEXT:    [[TMP3:%.*]] = icmp ne i64 [[A]], [[C]]
+; CHECK-NEXT:    ret i1 true
+;
+  %1 = icmp ugt i64 %a, %b
+  tail call void @llvm.assume(i1 %1)
+  %2 = icmp uge i64 %b, %c
+  tail call void @llvm.assume(i1 %2)
+  %3 = icmp ne i64 %a, %c
+  ret i1 %3
+}
+
+define i1 @assume_a_ne_b_and_b_ne_c(i64 %a, i64 %b, i64 %c) {
+; CHECK-LABEL: @assume_a_ne_b_and_b_ne_c(
+; CHECK-NEXT:    [[TMP1:%.*]] = icmp ne i64 [[A:%.*]], [[B:%.*]]
+; CHECK-NEXT:    tail call void @llvm.assume(i1 [[TMP1]])
+; CHECK-NEXT:    [[TMP2:%.*]] = icmp ne i64 [[B]], [[C:%.*]]
+; CHECK-NEXT:    tail call void @llvm.assume(i1 [[TMP2]])
+; CHECK-NEXT:    [[TMP3:%.*]] = icmp ne i64 [[A]], [[C]]
+; CHECK-NEXT:    ret i1 [[TMP3]]
+;
+  %1 = icmp ne i64 %a, %b
+  tail call void @llvm.assume(i1 %1)
+  %2 = icmp ne i64 %b, %c
+  tail call void @llvm.assume(i1 %2)
+  %3 = icmp ne i64 %a, %c
+  ret i1 %3
+}
+
+define i1 @assume_1a(i64 %a, i64 %b) {
+; CHECK-LABEL: @assume_1a(
+; CHECK-NEXT:    [[NE:%.*]] = icmp ne i64 [[A:%.*]], [[B:%.*]]
+; CHECK-NEXT:    tail call void @llvm.assume(i1 [[NE]])
+; CHECK-NEXT:    [[RET:%.*]] = icmp ugt i64 [[A]], [[B]]
+; CHECK-NEXT:    ret i1 [[RET]]
+;
+  %ne = icmp ne i64 %a, %b
+  tail call void @llvm.assume(i1 %ne)
+  %ret = icmp ugt i64 %a, %b
+  ret i1 %ret
+}
+
+define i1 @assume_1b(i64 %a, i64 %b) {
+; CHECK-LABEL: @assume_1b(
+; CHECK-NEXT:    [[NE:%.*]] = icmp ne i64 [[A:%.*]], [[B:%.*]]
+; CHECK-NEXT:    tail call void @llvm.assume(i1 [[NE]])
+; CHECK-NEXT:    [[RET:%.*]] = icmp uge i64 [[A]], [[B]]
+; CHECK-NEXT:    ret i1 [[RET]]
+;
+  %ne = icmp ne i64 %a, %b
+  tail call void @llvm.assume(i1 %ne)
+  %ret = icmp uge i64 %a, %b
+  ret i1 %ret
+}
+
+define i1 @assume_2a(i64 %a, i64 %b) {
+; CHECK-LABEL: @assume_2a(
+; CHECK-NEXT:    [[NE:%.*]] = icmp ne i64 [[A:%.*]], [[B:%.*]]
+; CHECK-NEXT:    tail call void @llvm.assume(i1 [[NE]])
+; CHECK-NEXT:    [[RET:%.*]] = icmp ult i64 [[A]], [[B]]
+; CHECK-NEXT:    ret i1 [[RET]]
+;
+  %ne = icmp ne i64 %a, %b
+  tail call void @llvm.assume(i1 %ne)
+  %ret = icmp ult i64 %a, %b
+  ret i1 %ret
+}
+
+define i1 @assume_2b(i64 %a, i64 %b) {
+; CHECK-LABEL: @assume_2b(
+; CHECK-NEXT:    [[NE:%.*]] = icmp ne i64 [[A:%.*]], [[B:%.*]]
+; CHECK-NEXT:    tail call void @llvm.assume(i1 [[NE]])
+; CHECK-NEXT:    [[RET:%.*]] = icmp ule i64 [[A]], [[B]]
+; CHECK-NEXT:    ret i1 [[RET]]
+;
+  %ne = icmp ne i64 %a, %b
+  tail call void @llvm.assume(i1 %ne)
+  %ret = icmp ule i64 %a, %b
+  ret i1 %ret
+}
+
+; TODO: extend to support signed comparisons
+define i1 @assume_3a(i64 %a, i64 %b) {
+; CHECK-LABEL: @assume_3a(
+; CHECK-NEXT:    [[NE:%.*]] = icmp ne i64 [[A:%.*]], [[B:%.*]]
+; CHECK-NEXT:    tail call void @llvm.assume(i1 [[NE]])
+; CHECK-NEXT:    [[RET:%.*]] = icmp sgt i64 [[A]], [[B]]
+; CHECK-NEXT:    ret i1 [[RET]]
+;
+  %ne = icmp ne i64 %a, %b
+  tail call void @llvm.assume(i1 %ne)
+  %ret = icmp sgt i64 %a, %b
+  ret i1 %ret
+}
+
+define i1 @assume_3b(i64 %a, i64 %b) {
+; CHECK-LABEL: @assume_3b(
+; CHECK-NEXT:    [[NE:%.*]] = icmp ne i64 [[A:%.*]], [[B:%.*]]
+; CHECK-NEXT:    tail call void @llvm.assume(i1 [[NE]])
+; CHECK-NEXT:    [[RET:%.*]] = icmp sge i64 [[A]], [[B]]
+; CHECK-NEXT:    ret i1 [[RET]]
+;
+  %ne = icmp ne i64 %a, %b
+  tail call void @llvm.assume(i1 %ne)
+  %ret = icmp sge i64 %a, %b
+  ret i1 %ret
+}
+
+define i1 @assume_4a(i64 %a, i64 %b) {
+; CHECK-LABEL: @assume_4a(
+; CHECK-NEXT:    [[NE:%.*]] = icmp ne i64 [[A:%.*]], [[B:%.*]]
+; CHECK-NEXT:    tail call void @llvm.assume(i1 [[NE]])
+; CHECK-NEXT:    [[RET:%.*]] = icmp slt i64 [[A]], [[B]]
+; CHECK-NEXT:    ret i1 [[RET]]
+;
+  %ne = icmp ne i64 %a, %b
+  tail call void @llvm.assume(i1 %ne)
+  %ret = icmp slt i64 %a, %b
+  ret i1 %ret
+}
+
+define i1 @assume_4b(i64 %a, i64 %b) {
+; CHECK-LABEL: @assume_4b(
+; CHECK-NEXT:    [[NE:%.*]] = icmp ne i64 [[A:%.*]], [[B:%.*]]
+; CHECK-NEXT:    tail call void @llvm.assume(i1 [[NE]])
+; CHECK-NEXT:    [[RET:%.*]] = icmp sle i64 [[A]], [[B]]
+; CHECK-NEXT:    ret i1 [[RET]]
+;
+  %ne = icmp ne i64 %a, %b
+  tail call void @llvm.assume(i1 %ne)
+  %ret = icmp sle i64 %a, %b
+  ret i1 %ret
+}