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 negate(SmallVector 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 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 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::max(); + CS.addVariableRow({Limit - 1, Limit - 2, Limit - 3}); + EXPECT_FALSE(CS.isConditionImplied({Limit - 1, Limit - 2, Limit - 3})); +} } // namespace