From 4727133524a00789b4d45e53aa51aa30fdae8e5c Mon Sep 17 00:00:00 2001
From: Florian Hahn <flo@fhahn.com>
Date: Tue, 15 Sep 2020 13:50:11 +0100
Subject: [PATCH] [ConstraintSolver] Add isConditionImplied helper.

This patch adds a isConditionImplied function that
takes a constraint and returns true if the constraint
is implied by the current constraints in the system.

Reviewed By: spatel

Differential Revision: https://reviews.llvm.org/D84545
---
 include/llvm/Analysis/ConstraintSystem.h    | 11 ++++
 lib/Analysis/ConstraintSystem.cpp           | 10 +++
 unittests/Analysis/ConstraintSystemTest.cpp | 73 ++++++++++++++++++++-
 3 files changed, 93 insertions(+), 1 deletion(-)

diff --git a/include/llvm/Analysis/ConstraintSystem.h b/include/llvm/Analysis/ConstraintSystem.h
index 7de787c1fc3..01f09f3daaa 100644
--- a/include/llvm/Analysis/ConstraintSystem.h
+++ b/include/llvm/Analysis/ConstraintSystem.h
@@ -51,6 +51,17 @@ 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;
+    for (auto &C : R)
+      C *= -1;
+    return R;
+  }
+
+  bool isConditionImplied(SmallVector<int64_t, 8> R);
 };
 } // namespace llvm
 
diff --git a/lib/Analysis/ConstraintSystem.cpp b/lib/Analysis/ConstraintSystem.cpp
index 21115fc946e..818cfe0a171 100644
--- a/lib/Analysis/ConstraintSystem.cpp
+++ b/lib/Analysis/ConstraintSystem.cpp
@@ -140,3 +140,13 @@ bool ConstraintSystem::mayHaveSolution() {
   LLVM_DEBUG(dbgs() << (HasSolution ? "sat" : "unsat") << "\n");
   return HasSolution;
 }
+
+bool ConstraintSystem::isConditionImplied(SmallVector<int64_t, 8> R) {
+  // If there is no solution with the negation of R added to the system, the
+  // condition must hold based on the existing constraints.
+  R = ConstraintSystem::negate(R);
+
+  auto NewSystem = *this;
+  NewSystem.addVariableRow(R);
+  return !NewSystem.mayHaveSolution();
+}
diff --git a/unittests/Analysis/ConstraintSystemTest.cpp b/unittests/Analysis/ConstraintSystemTest.cpp
index 2301da7ec29..337a1116341 100644
--- a/unittests/Analysis/ConstraintSystemTest.cpp
+++ b/unittests/Analysis/ConstraintSystemTest.cpp
@@ -13,7 +13,7 @@ using namespace llvm;
 
 namespace {
 
-TEST(ConstraintSloverTest, TestSolutionChecks) {
+TEST(ConstraintSolverTest, TestSolutionChecks) {
   {
     ConstraintSystem CS;
     // x + y <= 10, x >= 5, y >= 6, x <= 10, y <= 10
@@ -79,4 +79,75 @@ TEST(ConstraintSloverTest, TestSolutionChecks) {
     EXPECT_TRUE(CS.mayHaveSolution());
   }
 }
+
+TEST(ConstraintSolverTest, IsConditionImplied) {
+  {
+    // For the test below, we assume we know
+    // x <= 5 && y <= 3
+    ConstraintSystem CS;
+    CS.addVariableRow({5, 1, 0});
+    CS.addVariableRow({3, 0, 1});
+
+    // x + y <= 6 does not hold.
+    EXPECT_FALSE(CS.isConditionImplied({6, 1, 1}));
+    // x + y <= 7 does not hold.
+    EXPECT_FALSE(CS.isConditionImplied({7, 1, 1}));
+    // x + y <= 8 does hold.
+    EXPECT_TRUE(CS.isConditionImplied({8, 1, 1}));
+
+    // 2 * x + y <= 12 does hold.
+    EXPECT_FALSE(CS.isConditionImplied({12, 2, 1}));
+    // 2 * x + y <= 13 does hold.
+    EXPECT_TRUE(CS.isConditionImplied({13, 2, 1}));
+
+    //  x + y <= 12 does hold.
+    EXPECT_FALSE(CS.isConditionImplied({12, 2, 1}));
+    // 2 * x + y <= 13 does hold.
+    EXPECT_TRUE(CS.isConditionImplied({13, 2, 1}));
+
+    // x <= y == x - y <= 0 does not hold.
+    EXPECT_FALSE(CS.isConditionImplied({0, 1, -1}));
+    // y <= x == -x + y <= 0 does not hold.
+    EXPECT_FALSE(CS.isConditionImplied({0, -1, 1}));
+  }
+
+  {
+    // For the test below, we assume we know
+    // x + 1 <= y + 1 == x - y <= 0
+    ConstraintSystem CS;
+    CS.addVariableRow({0, 1, -1});
+
+    // x <= y == x - y <= 0 does hold.
+    EXPECT_TRUE(CS.isConditionImplied({0, 1, -1}));
+    // y <= x == -x + y <= 0 does not hold.
+    EXPECT_FALSE(CS.isConditionImplied({0, -1, 1}));
+
+    // x <= y + 10 == x - y <= 10 does hold.
+    EXPECT_TRUE(CS.isConditionImplied({10, 1, -1}));
+    // x + 10 <= y == x - y <= -10 does NOT hold.
+    EXPECT_FALSE(CS.isConditionImplied({-10, 1, -1}));
+  }
+
+  {
+    // For the test below, we assume we know
+    // x <= y == x - y <= 0
+    // y <= z == y - x <= 0
+    ConstraintSystem CS;
+    CS.addVariableRow({0, 1, -1, 0});
+    CS.addVariableRow({0, 0, 1, -1});
+
+    // z <= y == -y + z <= 0 does not hold.
+    EXPECT_FALSE(CS.isConditionImplied({0, 0, -1, 1}));
+    // x <= z == x - z <= 0 does hold.
+    EXPECT_TRUE(CS.isConditionImplied({0, 1, 0, -1}));
+  }
+}
+
+TEST(ConstraintSolverTest, IsConditionImpliedOverflow) {
+  ConstraintSystem CS;
+  // Make sure isConditionImplied returns false when there is an overflow.
+  int64_t Limit = std::numeric_limits<int64_t>::max();
+  CS.addVariableRow({Limit - 1, Limit - 2, Limit - 3});
+  EXPECT_FALSE(CS.isConditionImplied({Limit - 1, Limit - 2, Limit - 3}));
+}
 } // namespace