ConstraintAnalysis: Add AND fusing of { x <= C && x < C } => x < C

src/ir/constraint.cpp

@@ -34,43 +34,45 @@ Result provesConstantPair(Abstract::Op aOp,
                           Abstract::Op bOp,
                           const Literal& bConstant,
                           bool recursing = false) {
+  using namespace Abstract;
+
   // a == A =?=> a op B. Simply apply A to the operation against B.
-  if (aOp == Abstract::Eq) {
+  if (aOp == Eq) {
     switch (bOp) {
-      case Abstract::Eq:
+      case Eq:
         return TrueFalse(aConstant == bConstant);
-      case Abstract::Ne:
+      case Ne:
         return TrueFalse(aConstant != bConstant);
-      case Abstract::LtS:
+      case LtS:
         return TrueFalse(aConstant.ltS(bConstant));
-      case Abstract::LeS:
+      case LeS:
         return TrueFalse(aConstant.leS(bConstant));
-      case Abstract::GtS:
+      case GtS:
         return TrueFalse(aConstant.gtS(bConstant));
-      case Abstract::GeS:
+      case GeS:
         return TrueFalse(aConstant.geS(bConstant));
-      case Abstract::LtU:
+      case LtU:
         return TrueFalse(aConstant.ltU(bConstant));
-      case Abstract::LeU:
+      case LeU:
         return TrueFalse(aConstant.leU(bConstant));
-      case Abstract::GtU:
+      case GtU:
         return TrueFalse(aConstant.gtU(bConstant));
-      case Abstract::GeU:
+      case GeU:
         return TrueFalse(aConstant.geU(bConstant));
       default: {
       }
     }
   }
 
   // a != A =?=> a == B. False if A = B, else unknown.
-  if (aOp == Abstract::Ne && bOp == Abstract::Eq) {
+  if (aOp == Ne && bOp == Eq) {
     if (aConstant == bConstant) {
       return False;
     }
   }
 
   // a != A =?=> a != B. True if A = B, else unknown.
-  if (aOp == Abstract::Ne && bOp == Abstract::Ne) {
+  if (aOp == Ne && bOp == Ne) {
     if (aConstant == bConstant) {
       return True;
     }
@@ -160,6 +162,55 @@ Result AndedConstraintSet::proves(const AndedConstraintSet& other) const {
   return hasUnknown ? Unknown : True;
 }
 
+namespace {
+
+// Do an AND on a pair of constraints, looking for a way to fuse them together
+// into a single constraint that represents them both, while assuming the
+// constraints have an equal term. If we fail, return nullopt.
+std::optional<Constraint> fusedApproximateAndTermEqualPair(
+  const Abstract::Op aOp, const Abstract::Op bOp, const Term& term) {
+  using namespace Abstract;
+
+  // x < C && x <= C  ===  x < C
+  if (aOp == LtS && bOp == LeS) {
+    return Constraint{LtS, term};
+  }
+  if (aOp == LtU && bOp == LeU) {
+    return Constraint{LtU, term};
+  }
+
+  // TODO: all the rest
+
+  return {};
+}
+
+// Do an AND on a pair of constraints, looking for a way to fuse them together
+// into a single constraint that represents them both. If we fail, return
+// nullopt.
+std::optional<Constraint> fusedApproximateAndPair(const Constraint& a,
+                                                  const Constraint& b,
+                                                  bool recursing = false) {
+  // If a proves b is true, all we need is a (e.g. { x == 5 && x > 0 } => x == 5
+  if (provesPair(a, b) == True) {
+    return a;
+  }
+
+  if (a.term == b.term) {
+    if (auto result = fusedApproximateAndTermEqualPair(a.op, b.op, a.term)) {
+      return result;
+    }
+  }
+
+  if (!recursing) {
+    // The flipped form may be recognized.
+    return fusedApproximateAndPair(b, a, true);
+  }
+
+  return {};
+}
+
+} // anonymous namespace
+
 void AndedConstraintSet::approximateAnd(const Constraint& c) {
   if (provesEverything()) {
     // Nothing to add.
@@ -172,24 +223,20 @@ void AndedConstraintSet::approximateAnd(const Constraint& c) {
     return;
   } else if (result == False) {
     // We are now a contradiction.
-    isContradiction = true;
+    setProvesEverything();
     return;
   }
 
-  // If c proves something already present to be true, it can just replace it.
   for (auto& existing : *this) {
-    auto result = provesPair(c, existing);
-    if (result == True) {
-      existing = c;
+    // Some ANDed constraints fuse together into a new constraint.
+    if (auto fused = fusedApproximateAndPair(existing, c)) {
+      existing = *fused;
 
       // Sort to ensure we are in the right place.
       std::sort(begin(), end());
 
       return;
     }
-
-    // There cannot be a contradiction here, because we checked for that above.
-    assert(result != False);
   }
 
   if (size() < MaxConstraints) {

test/gtest/constraint.cpp

@@ -254,25 +254,26 @@ static void checkOr(const AndedConstraintSet& a,
 
 TEST(ConstraintTest, TestOrInequality) {
   // x == 5 || x >= 0  =>  x >= 0
-  AndedConstraintSet eq5{Constraint{Eq, {Literal(int32_t(5))}}};
-  AndedConstraintSet ge0{Constraint{GeU, {Literal(int32_t(0))}}};
+  AndedConstraintSet eq5{{Eq, {Literal(int32_t(5))}}};
+  AndedConstraintSet ge0{{GeU, {Literal(int32_t(0))}}};
   checkOr(eq5, ge0, ge0);
 
   // x == 5 || x > 5  =>  x >= 5
-  AndedConstraintSet gts5{Constraint{GtS, {Literal(int32_t(5))}}};
-  AndedConstraintSet ges5{Constraint{GeS, {Literal(int32_t(5))}}};
+  AndedConstraintSet gts5{{GtS, {Literal(int32_t(5))}}};
+  AndedConstraintSet ges5{{GeS, {Literal(int32_t(5))}}};
   checkOr(eq5, gts5, ges5);
 
   // x == 5 || x >= 5  =>  x >= 5
   checkOr(eq5, ges5, ges5);
 }
 
 TEST(ConstraintTest, TestOrLoop) {
-  // Check common loop patterns:
+  // Check common loop patterns at the loop top (merging an initial value with
+  // an incremented and bounded one):
   // { x == A } || { x > A && x <= B }   ==>   { x >= A && x <= B }
 
   // { x == 5 } || { x > 5 && x <= 42 }   ==>   { x >= 5 && x <= 42 }
-  AndedConstraintSet left{Constraint{Eq, {Literal(int32_t(5))}}};
+  AndedConstraintSet left{{Eq, {Literal(int32_t(5))}}};
   AndedConstraintSet right(
     {{GtS, {Literal(int32_t(5))}}, {LeS, {Literal(int32_t(42))}}});
   AndedConstraintSet result(
@@ -283,20 +284,20 @@ TEST(ConstraintTest, TestOrLoop) {
 
   // Change 5 on the left to 7:
   // { x == 7 } || { x > 5 && x <= 42 }   ==>   { x > 5 && x <= 42}
-  AndedConstraintSet left7{Constraint{Eq, {Literal(int32_t(7))}}};
+  AndedConstraintSet left7{{Eq, {Literal(int32_t(7))}}};
   checkOr(left7, right, right);
 
   // Change 5 on the left to 99:
   // { x == 99 } || { x > 5 && x <= 42 }   ==>   { x > 5 }
   // TODO: we could emit a range (5, 99]
-  AndedConstraintSet left99{Constraint{Eq, {Literal(int32_t(99))}}};
-  AndedConstraintSet rightOnly5{Constraint{GtS, {Literal(int32_t(5))}}};
+  AndedConstraintSet left99{{Eq, {Literal(int32_t(99))}}};
+  AndedConstraintSet rightOnly5{{GtS, {Literal(int32_t(5))}}};
   checkOr(left99, right, rightOnly5);
 
   // Change 5 on the left to 4:
   // { x == 4 } || { x > 5 && x <= 42 }   ==>   { x <= 42 }
   // TODO: we could emit a range [4, 42]
-  AndedConstraintSet left4{Constraint{Eq, {Literal(int32_t(4))}}};
+  AndedConstraintSet left4{{Eq, {Literal(int32_t(4))}}};
   AndedConstraintSet rightOnly42({{LeS, {Literal(int32_t(42))}}});
   checkOr(left4, right, rightOnly42);
 
@@ -311,7 +312,7 @@ TEST(ConstraintTest, TestOrLoop) {
   // Change the Eq on the left to Ne. We fail to find anything for the OR.
   // { x != 5 } || { x > 5 && x <= 42 }   ==>   {}
   // TODO: we could emit x != 5
-  AndedConstraintSet leftNe{Constraint{Ne, {Literal(int32_t(5))}}};
+  AndedConstraintSet leftNe{{Ne, {Literal(int32_t(5))}}};
   auto empty = AndedConstraintSet::makeProvesNothing();
   checkOr(leftNe, right, empty);
 
@@ -340,3 +341,73 @@ TEST(ConstraintTest, TestOrLoop) {
                                   {Ne, {Literal(int32_t(21))}}});
   checkOr(left, rightAdded, resultAdded);
 }
+
+static void checkAnd(const AndedConstraintSet& a,
+                     const AndedConstraintSet& b,
+                     const AndedConstraintSet& result) {
+  auto anded = a;
+  for (auto& bc : b) {
+    anded.approximateAnd(bc);
+  }
+  EXPECT_EQ(anded, result);
+
+  anded = b;
+  for (auto& ac : a) {
+    anded.approximateAnd(ac);
+  }
+  EXPECT_EQ(anded, result);
+}
+
+TEST(ConstraintTest, TestAndInequality) {
+  // x == 5 && x >= 0  =>  x == 5
+  AndedConstraintSet eq5{{Eq, {Literal(int32_t(5))}}};
+  AndedConstraintSet ge0{{GeS, {Literal(int32_t(0))}}};
+  checkAnd(eq5, ge0, eq5);
+
+  // x == 5 && x >= 5  =>  x == 5
+  AndedConstraintSet ge5{{GeS, {Literal(int32_t(5))}}};
+  checkAnd(eq5, ge5, eq5);
+
+  // x == 5 && x >= 6  =>  contradiction
+  AndedConstraintSet ge6{{GeS, {Literal(int32_t(6))}}};
+  AndedConstraintSet contradiction;
+  checkAnd(eq5, ge6, contradiction);
+}
+
+TEST(ConstraintTest, TestAndLoop) {
+  // Check common loop patterns after incrementing and bounds-checking:
+  // x <= A && x < A  =>  x < A
+
+  // x <= 5 && x < 5  =>  x < 5
+  AndedConstraintSet le5{{LeS, {Literal(int32_t(5))}}};
+  AndedConstraintSet lt5{{LtS, {Literal(int32_t(5))}}};
+  checkAnd(le5, lt5, lt5);
+
+  // Ditto, but unsigned.
+  AndedConstraintSet le5U{{LeU, {Literal(int32_t(5))}}};
+  AndedConstraintSet lt5U{{LtU, {Literal(int32_t(5))}}};
+  checkAnd(le5U, lt5U, lt5U);
+
+  // Mixing signed and unsigned does not optimize (so we just end up ANDing both
+  // inputs).
+  checkAnd(le5, lt5U, AndedConstraintSet{le5[0], lt5U[0]});
+
+  // Different constants do not optimize, but could TODO
+  AndedConstraintSet lt6{{LtS, {Literal(int32_t(6))}}};
+  checkAnd(le5, lt6, AndedConstraintSet{le5[0], lt6[0]});
+
+  // A non-constant.
+  // x <= y && x < y  =>  x < y
+  AndedConstraintSet ley{{LeS, {Index(1)}}};
+  AndedConstraintSet lty{{LtS, {Index(1)}}};
+  checkAnd(ley, lty, lty);
+
+  // A non-constant with extra info.
+  // { x <= y && x != 42 } && x < y  =>  x < y && x != 42
+  Constraint ne42{Ne, {Literal(int32_t(42))}};
+  checkAnd({ley[0], ne42}, lty, {lty[0], ne42});
+
+  // Extra info on the other side, same result.
+  // x <= y && { x < y && x != 42 }  =>  x < y && x != 42
+  checkAnd(ley, {lty[0], ne42}, {lty[0], ne42});
+}