[ConstraintElimination] Handle equality predicates

[antoniofrighetto]

Summary

Simplification of equality predicates is now supported by transferring equalities into inequalities. This is achieved by separately checking that both isConditionImplied(A >= B) and isConditionImplied(A <= B) hold.

[fhahn]

Thanks for the patch! Some comments inline

llvm/lib/Transforms/Scalar/ConstraintElimination.cpp

1002

The changes here are mostly to avoid having to duplicate the code to create True/false constants, and indepdent of the patch, right? Could you split them of into a separate NFC patch?

1007–1014

It would be nice to print the condition with the negated predicate here (as separate NFC patch)

1036

It would probably be cleaner to move the cod e to check if a constraint is implied to a new member function of ConstraintTy and not expose ::isEq publicly. This should be cleaner overall, especially thinking about adding support for NE as well in the future.

llvm/test/Transforms/ConstraintElimination/eq.ll

382

I think we need some additional tests here, including ones where we have something like a == b && b == c as facts and a + 1 == c +1 and various permutations (also checking that a + 1 == b is not simplified and so on).

It would also be good to have tests where we only know things like a >= b && b >= c and check that we do not simply *a == c` and so on.

[antoniofrighetto]

Added a few more tests, one we check a == b simplified to false, when a + 1 == b is assumed, the other in which no simplification can be done when assuming a >= b && b >= c. Testing the transitivity of equality has been extended to check if a + 1 == c + 1 also holds (via a select, note the orthogonal missed optimization there).

Polished up a bit the code & encapsulate the logic for handling equality constraints into isEqImplied.

[antoniofrighetto]

llvm/lib/Transforms/Scalar/ConstraintElimination.cpp

1002

(Opened a separate patch for it, D152143)

[fhahn]

llvm/lib/Transforms/Scalar/ConstraintElimination.cpp

1002

Great, thanks! Can you rebase this patch on top of D152143?

1034

Thanks for the latest update! I think it should even go further and be something like ConstraintTy::isImpliedBy(CS), so that all logic for querying CSToUse.isConditionImplied is done there.

[antoniofrighetto]

Thanks for the suggestion, rebased & the logic for querying CS.isConditionImplied has been moved into ::isImpliedBy. I’m not completely sure if this may be further ameliorated, considering that computing the negated still needs to be done separately.

[fhahn]

llvm/lib/Transforms/Scalar/ConstraintElimination.cpp

108

Would it be sufficient to have None, ConditionTrue, ConditionFalse and check all in isImpliedBy?

[antoniofrighetto]

We may do that, and eventually ending up with the following:

auto CondImpliedStatus = R.isImpliedBy(CSToUse);

if (CondImpliedStatus == ConditionImpliedTy::ConditionTrue) {
  Changed = ReplaceCmpWithConstant(Cmp, true);
} else if (CondImpliedStatus == ConditionImpliedTy::ConditionFalse) {
  Changed = ReplaceCmpWithConstant(Cmp, false);
}

// Compute the negated separately.
auto Negated = ConstraintSystem::negate(R.Coefficients);
auto IsNegatedImplied =
    !Negated.empty() && CSToUse.isConditionImplied(Negated);

if (IsNegatedImplied) {
  Changed = ReplaceCmpWithConstant(Cmp, false);
}

in checkAndReplaceCondition, as we would still need to compute the negated separately (reproducer-remarks-debug.ll seems to be complaining). Perhaps we slightly lose some of the clarity / self-documenting that comes with distinguishing between EqualityTrue, ConditionTrue (may assist in debugging), though, likewise, that shouldn't be really that much of a problem. Could that work?

[fhahn]

In D152067#4408002, @antoniofrighetto wrote:

in checkAndReplaceCondition, as we would still need to compute the negated separately (reproducer-remarks-debug.ll seems to be complaining). Perhaps we slightly lose some of the clarity / self-documenting that comes with distinguishing between EqualityTrue, ConditionTrue (may assist in debugging), though, likewise, that shouldn't be really that much of a problem. Could that work?

I am not sure why we would need to compute the negation separately? Wouldn't ConditionHoldFalse cover exactly the case where the negated condition holds?

[antoniofrighetto]

Argh, there was a leftover in reproducer-remarks-debug.ll that I hadn't noticed immediately that led to test failure. Should be better now!

[nikic]

llvm/lib/Transforms/Scalar/ConstraintElimination.cpp

129

Might be cleaner to return std::optional<bool>? The use-site then becomes:

if (auto ImpliedCondition = R.isImpliedBy(CSToUse))
  return ReplaceCmpWithConstant(Cmp, *ImpliedCondition);

[fhahn]

llvm/include/llvm/Analysis/ConstraintSystem.h

135

as follow-up, it would be good to use negateOrEqual here as well.

140

Could you add a doc-comment for the function?

148

Could you add a doc-comment for the function?

llvm/lib/Transforms/Scalar/ConstraintElimination.cpp

590

I think it would probably be better to wrap the EQ handling in IsEq and then run the general code afterwards.

llvm/test/Transforms/ConstraintElimination/assumes.ll

636 ↗

(On Diff #530037)

I think those tests would fit better in eq.ll as the assume here is only used to add known facts.

llvm/test/Transforms/ConstraintElimination/eq.ll

413

simpler to either use xor or and instead of the more complicated select.

llvm/test/Transforms/ConstraintElimination/reproducer-remarks-debug.ll

12

What changed here?

[antoniofrighetto]

Thanks for the comments, should be now addressed.

[antoniofrighetto]

llvm/test/Transforms/ConstraintElimination/reproducer-remarks-debug.ll

12

There is a leftover (---) for the current implementation, as even when IsConditionImplied is true, isConditionImplied(Negated) is computed, leading to the following debug output:

---
%a + -1 * null <= 0
%a + -1 * null <= 0
sat

This doesn't occur anymore now, as, for the general case, we do not compute IsNegatedImplied when IsConditionImplied is true.

[fhahn]

LGTM with the additional nits addressed, thanks!

llvm/lib/Transforms/Scalar/ConstraintElimination.cpp

130

nit: Would be good to also document the return value: std;:nullopt if iy couldn't prove the constraint is true or false, otherwise returns whether the constraint was prove true or false.

583

Move this block and the next one after

if (IsConditionImplied && IsNegatedOrEqualImplied)
  return true;

to avoid unnecessary queries.

llvm/include/llvm/Analysis/ConstraintSystem.h

public:
 
   /// Returns true if there may be a solution for the constraints in the system.
   bool mayHaveSolution();
 
   static SmallVector<int64_t, 8> negate(SmallVector<int64_t, 8> R) {
     // The negated constraint R is obtained by multiplying by -1 and adding 1 to
     // the constant.
     R[0] += 1;
+    return negateOrEqual(R);
+  }
+
+  /// Multiplies each coefficient in the given vector by -1. Does not modify the
+  /// original vector.
+  ///
+  /// \param R The vector of coefficients to be negated.
+  static SmallVector<int64_t, 8> negateOrEqual(SmallVector<int64_t, 8> R) {
+    // The negated constraint R is obtained by multiplying by -1.
     for (auto &C : R)
       if (MulOverflow(C, int64_t(-1), C))
         return {};
     return R;
   }
 
+  /// Converts the given vector to form a strict less than inequality. Does not
+  /// modify the original vector.
+  ///
+  /// \param R The vector of coefficients to be converted.
+  static SmallVector<int64_t, 8> toStrictLessThan(SmallVector<int64_t, 8> R) {
+    // The strict less than is obtained by subtracting 1 from the constant.
+    if (SubOverflow(R[0], int64_t(1), R[0])) {
+      return {};
+    }
+    return R;
+  }
+
   bool isConditionImplied(SmallVector<int64_t, 8> R) const;
 
   SmallVector<int64_t> getLastConstraint() const {
     assert(!Constraints.empty() && "Constraint system is empty");
     SmallVector<int64_t> Result(NumVariables, 0);
     for (auto &Entry : Constraints.back())
       Result[Entry.Id] = Entry.Coefficient;
     return Result;

llvm/lib/Transforms/Scalar/ConstraintElimination.cpp

 #include "llvm/Support/Debug.h"
 #include "llvm/Support/DebugCounter.h"
 #include "llvm/Support/KnownBits.h"
 #include "llvm/Support/MathExtras.h"
 #include "llvm/Transforms/Utils/Cloning.h"
 #include "llvm/Transforms/Utils/ValueMapper.h"
 
 #include <cmath>
+#include <optional>
 #include <string>
 
 using namespace llvm;
 using namespace PatternMatch;
 
 #define DEBUG_TYPE "constraint-elimination"
 
 STATISTIC(NumCondsRemoved, "Number of instructions removed");
struct PreconditionTy {
   Value *Op1;
 
   PreconditionTy(CmpInst::Predicate Pred, Value *Op0, Value *Op1)
       : Pred(Pred), Op0(Op0), Op1(Op1) {}
 };
 
 struct ConstraintTy {
   SmallVector<int64_t, 8> Coefficients;
   SmallVector<PreconditionTy, 2> Preconditions;
 
   SmallVector<SmallVector<int64_t, 8>> ExtraInfo;
 
   bool IsSigned = false;
-  bool IsEq = false;
 
   ConstraintTy() = default;
 
-  ConstraintTy(SmallVector<int64_t, 8> Coefficients, bool IsSigned)
-      : Coefficients(Coefficients), IsSigned(IsSigned) {}
+  ConstraintTy(SmallVector<int64_t, 8> Coefficients, bool IsSigned, bool IsEq)
+      : Coefficients(Coefficients), IsSigned(IsSigned), IsEq(IsEq) {}
 
   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; }
+
+  /// 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;
 };
 
 /// 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.
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);
+      IsSigned, IsEq);
   // Collect variables that are known to be positive in all uses in the
   // constraint.
   DenseMap<Value *, bool> KnownNonNegativeVariables;
-  Res.IsEq = IsEq;
   auto &R = Res.Coefficients;
   for (const auto &KV : VariablesA) {
     R[GetOrAddIndex(KV.Variable)] += KV.Coefficient;
     auto I =
         KnownNonNegativeVariables.insert({KV.Variable, KV.IsKnownNonNegative});
     I.first->second &= KV.IsKnownNonNegative;
   }
 
ConstraintTy ConstraintInfo::getConstraintForSolving(CmpInst::Predicate Pred,
   // with the signed <-> unsigned transfer logic.
   if (CmpInst::isSigned(Pred) &&
       isKnownNonNegative(Op0, DL, /*Depth=*/MaxAnalysisRecursionDepth - 1) &&
       isKnownNonNegative(Op1, DL, /*Depth=*/MaxAnalysisRecursionDepth - 1))
     Pred = CmpInst::getUnsignedPredicate(Pred);
 
   SmallVector<Value *> NewVariables;
   ConstraintTy R = getConstraint(Pred, Op0, Op1, NewVariables);
-  if (R.IsEq || !NewVariables.empty())
+  if (!NewVariables.empty())
     return {};
   return R;
 }
 
 bool ConstraintTy::isValid(const ConstraintInfo &Info) const {
   return Coefficients.size() > 0 &&
          all_of(Preconditions, [&Info](const PreconditionTy &C) {
            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) {
+    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.
+    if (IsConditionImplied && IsNegatedOrEqualImplied)
+      return true;
+
+    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.
+    if (IsNegatedImplied || IsStrictLessThanImplied)
+      return false;
+
+    return std::nullopt;
+  }
+
+  if (IsConditionImplied)
+    return true;
+
+  auto Negated = ConstraintSystem::negate(Coefficients);
+  auto IsNegatedImplied = !Negated.empty() && CS.isConditionImplied(Negated);
+  if (IsNegatedImplied)
+    return false;
+
+  // Neither the condition nor its negated holds, did not prove anything.
+  return std::nullopt;
+}
+
 bool ConstraintInfo::doesHold(CmpInst::Predicate Pred, Value *A,
                               Value *B) const {
   auto R = getConstraintForSolving(Pred, A, B);
   return R.Preconditions.empty() && !R.empty() &&
          getCS(R.IsSigned).isConditionImplied(R.Coefficients);
 }
 
 void ConstraintInfo::transferToOtherSystem(
static bool checkAndReplaceCondition(
   // about the constraint.
   for (auto &Row : R.ExtraInfo)
     CSToUse.addVariableRow(Row);
   auto InfoRestorer = make_scope_exit([&]() {
     for (unsigned I = 0; I < R.ExtraInfo.size(); ++I)
       CSToUse.popLastConstraint();
   });
 
   auto ReplaceCmpWithConstant = [&](CmpInst *Cmp, bool IsTrue) {
     if (!DebugCounter::shouldExecute(EliminatedCounter))
       return false;
 
     LLVM_DEBUG({
       if (IsTrue) {
         dbgs() << "Condition " << *Cmp;
       } else {
         auto InversePred = Cmp->getInversePredicate();
         dbgs() << "Condition " << CmpInst::getPredicateName(InversePred) << " "
                << *A << ", " << *B;
       }
       dbgs() << " implied by dominating constraints\n";
       CSToUse.dump();
     });
 
     generateReproducer(Cmp, ReproducerModule, ReproducerCondStack, Info, DT);
     Constant *ConstantC = ConstantInt::getBool(
         CmpInst::makeCmpResultType(Cmp->getType()), IsTrue);
     Cmp->replaceUsesWithIf(ConstantC, [](Use &U) {
       // Conditions in an assume trivially simplify to true. Skip uses
       // in assume calls to not destroy the available information.
       auto *II = dyn_cast<IntrinsicInst>(U.getUser());
       return !II || II->getIntrinsicID() != Intrinsic::assume;
     });
     NumCondsRemoved++;
     return true;
   };
 
-  bool Changed = false;
-  bool IsConditionImplied = CSToUse.isConditionImplied(R.Coefficients);
-
-  if (IsConditionImplied) {
-    Changed = ReplaceCmpWithConstant(Cmp, true);
-    if (!Changed)
-      return false;
-  }
+  if (auto ImpliedCondition = R.isImpliedBy(CSToUse))
+    return ReplaceCmpWithConstant(Cmp, *ImpliedCondition);
 
-  // Compute them separately.
-  auto Negated = ConstraintSystem::negate(R.Coefficients);
-  auto IsNegatedImplied =
-      !Negated.empty() && CSToUse.isConditionImplied(Negated);
-
-  if (IsNegatedImplied) {
-    Changed = ReplaceCmpWithConstant(Cmp, false);
-    if (!Changed)
-      return false;
-  }
 
-  return Changed;
-}
-
 static void
 removeEntryFromStack(const StackEntry &E, ConstraintInfo &Info,
                      Module *ReproducerModule,
                      SmallVectorImpl<ReproducerEntry> &ReproducerCondStack,
                      SmallVectorImpl<StackEntry> &DFSInStack) {
   Info.popLastConstraint(E.IsSigned);
   // Remove variables in the system that went out of scope.
   auto &Mapping = Info.getValue2Index(E.IsSigned);
LLVM_DEBUG({
       dbgs() << "  constraint: ";
       dumpConstraint(R.Coefficients, getValue2Index(R.IsSigned));
       dbgs() << "\n";
     });
 
     DFSInStack.emplace_back(NumIn, NumOut, R.IsSigned,
                             std::move(ValuesToRelease));
 
-    if (R.IsEq) {
+    if (R.isEq()) {
       // Also add the inverted constraint for equality constraints.
       for (auto &Coeff : R.Coefficients)
         Coeff *= -1;
       CSToUse.addVariableRowFill(R.Coefficients);
 
       DFSInStack.emplace_back(NumIn, NumOut, R.IsSigned,
                               SmallVector<Value *, 2>());
     }

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

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

llvm/test/Transforms/ConstraintElimination/eq.ll

 ; NOTE: Assertions have been autogenerated by utils/update_test_checks.py
 ; RUN: opt -passes=constraint-elimination -S %s | FileCheck %s
 
+declare void @llvm.assume(i1)
+
 define i1 @test_eq_1(i8 %a, i8 %b) {
 ; CHECK-LABEL: @test_eq_1(
 ; CHECK-NEXT:  entry:
 ; CHECK-NEXT:    [[CMP:%.*]] = icmp eq i8 [[A:%.*]], [[B:%.*]]
 ; CHECK-NEXT:    br i1 [[CMP]], label [[THEN:%.*]], label [[ELSE:%.*]]
 ; CHECK:       then:
 ; CHECK-NEXT:    [[T_1:%.*]] = icmp uge i8 [[A]], [[B]]
 ; CHECK-NEXT:    [[T_2:%.*]] = icmp ule i8 [[A]], [[B]]
 ; CHECK-NEXT:    [[RES_1:%.*]] = xor i1 true, true
 ; CHECK-NEXT:    [[T_3:%.*]] = icmp eq i8 [[A]], [[B]]
-; CHECK-NEXT:    [[RES_2:%.*]] = xor i1 [[RES_1]], [[T_3]]
+; CHECK-NEXT:    [[RES_2:%.*]] = xor i1 [[RES_1]], true
 ; CHECK-NEXT:    [[T_4:%.*]] = icmp eq i8 [[B]], [[A]]
-; CHECK-NEXT:    [[RES_3:%.*]] = xor i1 [[RES_2]], [[T_4]]
+; CHECK-NEXT:    [[RES_3:%.*]] = xor i1 [[RES_2]], true
 ; CHECK-NEXT:    [[F_1:%.*]] = icmp ugt i8 [[B]], [[A]]
 ; CHECK-NEXT:    [[RES_4:%.*]] = xor i1 [[RES_3]], false
 ; CHECK-NEXT:    [[F_2:%.*]] = icmp ult i8 [[B]], [[A]]
 ; CHECK-NEXT:    [[RES_5:%.*]] = xor i1 [[RES_4]], false
 ; CHECK-NEXT:    [[C_1:%.*]] = icmp ult i8 [[B]], 99
 ; CHECK-NEXT:    [[RES_6:%.*]] = xor i1 [[RES_5]], [[C_1]]
 ; CHECK-NEXT:    ret i1 [[RES_6]]
 ; CHECK:       else:
else:
   %c.3 = icmp ult i8 %a, 99
   %xor.11 = xor i1 %xor.10, %c.3
 
   %c.4 = icmp ugt i8 %a, 98
   %xor.12 = xor i1 %xor.11, %c.4
 
   ret i1 %xor.12
 }
+
+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 eq i64 [[A]], [[B]]
+; CHECK-NEXT:    ret i1 false
+;
+  %1 = add nuw i64 %b, 1
+  %2 = icmp ult i64 %1, %a
+  tail call void @llvm.assume(i1 %2)
+  %3 = icmp eq i64 %a, %b
+  ret i1 %3
+}
+
+define i1 @assume_a_plus_1_eq_b(i64 %a, i64 %b)  {
+; CHECK-LABEL: @assume_a_plus_1_eq_b(
+; CHECK-NEXT:    [[TMP1:%.*]] = add nuw i64 [[A:%.*]], 1
+; CHECK-NEXT:    [[TMP2:%.*]] = icmp eq i64 [[TMP1]], [[B:%.*]]
+; CHECK-NEXT:    tail call void @llvm.assume(i1 [[TMP2]])
+; CHECK-NEXT:    [[TMP3:%.*]] = icmp eq i64 [[A]], [[B]]
+; CHECK-NEXT:    ret i1 false
+;
+  %1 = add nuw i64 %a, 1
+  %2 = icmp eq i64 %1, %b
+  tail call void @llvm.assume(i1 %2)
+  %3 = icmp eq i64 %a, %b
+  ret i1 %3
+}
+
+define i1 @assume_a_ge_b_and_b_ge_c(i64 %a, i64 %b, i64 %c)  {
+; CHECK-LABEL: @assume_a_ge_b_and_b_ge_c(
+; CHECK-NEXT:    [[TMP1:%.*]] = icmp uge 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 eq i64 [[A]], [[C]]
+; CHECK-NEXT:    ret i1 [[TMP3]]
+;
+  %1 = icmp uge 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 eq i64 %a, %c
+  ret i1 %3
+}
+
+define i1 @test_transitivity_of_equality_and_plus_1(i64 %a, i64 %b, i64 %c) {
+; CHECK-LABEL: @test_transitivity_of_equality_and_plus_1(
+; CHECK-NEXT:  entry:
+; CHECK-NEXT:    [[PRE_1:%.*]] = icmp eq i64 [[A:%.*]], [[B:%.*]]
+; CHECK-NEXT:    br i1 [[PRE_1]], label [[AB_EQUAL:%.*]], label [[NOT_EQ:%.*]]
+; CHECK:       ab_equal:
+; CHECK-NEXT:    [[BC_EQ:%.*]] = icmp eq i64 [[B]], [[C:%.*]]
+; CHECK-NEXT:    br i1 [[BC_EQ]], label [[BC_EQUAL:%.*]], label [[NOT_EQ]]
+; CHECK:       bc_equal:
+; CHECK-NEXT:    [[AC_EQ:%.*]] = icmp eq i64 [[A]], [[C]]
+; CHECK-NEXT:    [[A_PLUS_1:%.*]] = add nuw i64 [[A]], 1
+; CHECK-NEXT:    [[C_PLUS_1:%.*]] = add nuw i64 [[C]], 1
+; CHECK-NEXT:    [[AC_PLUS_1_EQ:%.*]] = icmp eq i64 [[A_PLUS_1]], [[C_PLUS_1]]
+; CHECK-NEXT:    [[RESULT:%.*]] = and i1 true, true
+; CHECK-NEXT:    ret i1 [[RESULT]]
+; CHECK:       not_eq:
+; CHECK-NEXT:    ret i1 false
+;
+entry:
+  %pre.1 = icmp eq i64 %a, %b
+  br i1 %pre.1, label %ab_equal, label %not_eq
+
+ab_equal:
+  %bc_eq = icmp eq i64 %b, %c
+  br i1 %bc_eq, label %bc_equal, label %not_eq
+
+bc_equal:
+  %ac_eq = icmp eq i64 %a, %c
+  %a_plus_1 = add nuw i64 %a, 1
+  %c_plus_1 = add nuw i64 %c, 1
+  %ac_plus_1_eq = icmp eq i64 %a_plus_1, %c_plus_1
+  %result = and i1 %ac_eq, %ac_plus_1_eq
+  ret i1 %result
+
+not_eq:
+  ret i1 false
+}

llvm/test/Transforms/ConstraintElimination/reproducer-remarks-debug.ll

 ; RUN: opt -passes=constraint-elimination -constraint-elimination-dump-reproducers -pass-remarks=constraint-elimination -debug %s 2>&1 | FileCheck %s
 
 ; REQUIRES: asserts
 
 target datalayout = "e-m:o-p270:32:32-p271:32:32-p272:64:64-i64:64-f80:128-n8:16:32:64-S128"
 
 ; CHECK:      Condition   %c.2 = icmp eq ptr %a, null implied by dominating constraints
 ; CHECK-NEXT: %a + -1 * null <= 0
 ; CHECK-NEXT: Creating reproducer for   %c.2 = icmp eq ptr %a, null
 ; CHECK-NEXT:   found external input ptr %a
 ; CHECK-NEXT:   Materializing assumption   %c.1 = icmp eq ptr %a, null
-; CHECK-NEXT: ---
 
 define i1 @test_ptr_null_constant(ptr %a) {
 ; CHECK-LABEL: define i1 @"{{.+}}test_ptr_null_constantrepro"(ptr %a) {
 ; CHECK-NEXT: entry:
 ; CHECK-NEXT:   %0 = icmp eq ptr %a, null
 ; CHECK-NEXT:   call void @llvm.assume(i1 %0)
 ; CHECK-NEXT:   %c.2 = icmp eq ptr %a, null
 ; CHECK-NEXT:   ret i1 %c.2