RPCS3/llvm-mirror
1
0
Fork 0
mirror of https://github.com/RPCS3/llvm-mirror.git synced 2024-11-21 18:22:53 +01:00
Code Issues Projects Releases Wiki Activity

[ConstraintSolver] Add isConditionImplied helper.

Browse Source 
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
This commit is contained in:
Florian Hahn 2020-09-15 13:50:11 +01:00
parent 7977b42a57
commit 4727133524
3 changed files with 93 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
include/llvm/Analysis/ConstraintSystem.h
View File

@ -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

10
lib/Analysis/ConstraintSystem.cpp
View File

@ -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();
}

73
unittests/Analysis/ConstraintSystemTest.cpp
View File

@ -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