From dcd0c32ad587fbb884ceb76e043e1c2714f556ca Mon Sep 17 00:00:00 2001 From: Ramkumar Ramachandra Date: Tue, 16 Jul 2024 12:09:38 +0100 Subject: [PATCH] ConstraintElimination: use DynamicAPInt To automatically handle overflows correctly and make the transform more powerful, replace uses of int64_t with DynamicAPInt in ConstraintElimination and ConstraintSystem. --- llvm/include/llvm/Analysis/ConstraintSystem.h | 50 +++++----- llvm/lib/Analysis/ConstraintSystem.cpp | 35 +++---- .../Scalar/ConstraintElimination.cpp | 49 ++++----- .../constraint-overflow.ll | 3 +- .../ConstraintElimination/overflows.ll | 3 +- .../Analysis/ConstraintSystemTest.cpp | 99 ++++++++++--------- 6 files changed, 123 insertions(+), 116 deletions(-) diff --git a/llvm/include/llvm/Analysis/ConstraintSystem.h b/llvm/include/llvm/Analysis/ConstraintSystem.h index 7b02b618f7cb44..7711336b1d6353 100644 --- a/llvm/include/llvm/Analysis/ConstraintSystem.h +++ b/llvm/include/llvm/Analysis/ConstraintSystem.h @@ -9,38 +9,35 @@ #ifndef LLVM_ANALYSIS_CONSTRAINTSYSTEM_H #define LLVM_ANALYSIS_CONSTRAINTSYSTEM_H -#include "llvm/ADT/APInt.h" #include "llvm/ADT/ArrayRef.h" #include "llvm/ADT/DenseMap.h" +#include "llvm/ADT/DynamicAPInt.h" #include "llvm/ADT/SmallVector.h" -#include "llvm/Support/MathExtras.h" - -#include namespace llvm { class Value; class ConstraintSystem { struct Entry { - int64_t Coefficient; + DynamicAPInt Coefficient; uint16_t Id; - Entry(int64_t Coefficient, uint16_t Id) + Entry(const DynamicAPInt &Coefficient, uint16_t Id) : Coefficient(Coefficient), Id(Id) {} }; - static int64_t getConstPart(const Entry &E) { + static DynamicAPInt getConstPart(const Entry &E) { if (E.Id == 0) return E.Coefficient; - return 0; + return DynamicAPInt{0}; } - static int64_t getLastCoefficient(ArrayRef Row, uint16_t Id) { + static DynamicAPInt getLastCoefficient(ArrayRef Row, uint16_t Id) { if (Row.empty()) - return 0; + return DynamicAPInt{0}; if (Row.back().Id == Id) return Row.back().Coefficient; - return 0; + return DynamicAPInt{0}; } size_t NumVariables = 0; @@ -74,11 +71,12 @@ class ConstraintSystem { ConstraintSystem(const DenseMap &Value2Index) : NumVariables(Value2Index.size()), Value2Index(Value2Index) {} - bool addVariableRow(ArrayRef R) { + bool addVariableRow(ArrayRef R) { assert(Constraints.empty() || R.size() == NumVariables); // If all variable coefficients are 0, the constraint does not provide any // usable information. - if (all_of(ArrayRef(R).drop_front(1), [](int64_t C) { return C == 0; })) + if (all_of(ArrayRef(R).drop_front(1), + [](const DynamicAPInt &C) { return C == 0; })) return false; SmallVector NewRow; @@ -98,10 +96,11 @@ class ConstraintSystem { return Value2Index; } - bool addVariableRowFill(ArrayRef R) { + bool addVariableRowFill(ArrayRef R) { // If all variable coefficients are 0, the constraint does not provide any // usable information. - if (all_of(ArrayRef(R).drop_front(1), [](int64_t C) { return C == 0; })) + if (all_of(ArrayRef(R).drop_front(1), + [](const DynamicAPInt &C) { return C == 0; })) return false; NumVariables = std::max(R.size(), NumVariables); @@ -111,7 +110,7 @@ class ConstraintSystem { /// Returns true if there may be a solution for the constraints in the system. bool mayHaveSolution(); - static SmallVector negate(SmallVector R) { + static SmallVector negate(SmallVector R) { // The negated constraint R is obtained by multiplying by -1 and adding 1 to // the constant. R[0] += 1; @@ -122,11 +121,11 @@ class ConstraintSystem { /// original vector. /// /// \param R The vector of coefficients to be negated. - static SmallVector negateOrEqual(SmallVector R) { + static SmallVector + negateOrEqual(SmallVector R) { // The negated constraint R is obtained by multiplying by -1. for (auto &C : R) - if (MulOverflow(C, int64_t(-1), C)) - return {}; + C *= -1; return R; } @@ -134,19 +133,18 @@ class ConstraintSystem { /// modify the original vector. /// /// \param R The vector of coefficients to be converted. - static SmallVector toStrictLessThan(SmallVector R) { + static SmallVector + toStrictLessThan(SmallVector R) { // The strict less than is obtained by subtracting 1 from the constant. - if (SubOverflow(R[0], int64_t(1), R[0])) { - return {}; - } + R[0] -= 1; return R; } - bool isConditionImplied(SmallVector R) const; + bool isConditionImplied(SmallVector R) const; - SmallVector getLastConstraint() const { + SmallVector getLastConstraint() const { assert(!Constraints.empty() && "Constraint system is empty"); - SmallVector Result(NumVariables, 0); + SmallVector Result(NumVariables, DynamicAPInt{0}); for (auto &Entry : Constraints.back()) Result[Entry.Id] = Entry.Coefficient; return Result; diff --git a/llvm/lib/Analysis/ConstraintSystem.cpp b/llvm/lib/Analysis/ConstraintSystem.cpp index e4c9dcc7544e99..bb21936c4218ee 100644 --- a/llvm/lib/Analysis/ConstraintSystem.cpp +++ b/llvm/lib/Analysis/ConstraintSystem.cpp @@ -7,8 +7,8 @@ //===----------------------------------------------------------------------===// #include "llvm/Analysis/ConstraintSystem.h" +#include "llvm/ADT/DynamicAPInt.h" #include "llvm/ADT/SmallVector.h" -#include "llvm/Support/MathExtras.h" #include "llvm/ADT/StringExtras.h" #include "llvm/IR/Value.h" #include "llvm/Support/Debug.h" @@ -55,8 +55,8 @@ bool ConstraintSystem::eliminateUsingFM() { if (R1 == R2) continue; - int64_t UpperLast = getLastCoefficient(RemainingRows[R2], LastIdx); - int64_t LowerLast = getLastCoefficient(RemainingRows[R1], LastIdx); + DynamicAPInt UpperLast = getLastCoefficient(RemainingRows[R2], LastIdx); + DynamicAPInt LowerLast = getLastCoefficient(RemainingRows[R1], LastIdx); assert( UpperLast != 0 && LowerLast != 0 && "RemainingRows should only contain rows where the variable is != 0"); @@ -79,9 +79,9 @@ bool ConstraintSystem::eliminateUsingFM() { while (true) { if (IdxUpper >= UpperRow.size() || IdxLower >= LowerRow.size()) break; - int64_t M1, M2, N; - int64_t UpperV = 0; - int64_t LowerV = 0; + DynamicAPInt M1, M2, N; + DynamicAPInt UpperV{0}; + DynamicAPInt LowerV{0}; uint16_t CurrentId = std::numeric_limits::max(); if (IdxUpper < UpperRow.size()) { CurrentId = std::min(UpperRow[IdxUpper].Id, CurrentId); @@ -94,18 +94,13 @@ bool ConstraintSystem::eliminateUsingFM() { UpperV = UpperRow[IdxUpper].Coefficient; IdxUpper++; } - - if (MulOverflow(UpperV, -1 * LowerLast, M1)) - return false; + M1 = UpperV * (-LowerLast); if (IdxLower < LowerRow.size() && LowerRow[IdxLower].Id == CurrentId) { LowerV = LowerRow[IdxLower].Coefficient; IdxLower++; } - - if (MulOverflow(LowerV, UpperLast, M2)) - return false; - if (AddOverflow(M1, M2, N)) - return false; + M2 = LowerV * UpperLast; + N = M1 + M2; if (N == 0) continue; NR.emplace_back(N, CurrentId); @@ -170,15 +165,15 @@ void ConstraintSystem::dump() const { continue; std::string Coefficient; if (E.Coefficient != 1) - Coefficient = std::to_string(E.Coefficient) + " * "; + Coefficient = std::to_string(int64_t{E.Coefficient}) + " * "; Parts.push_back(Coefficient + Names[E.Id - 1]); } // assert(!Parts.empty() && "need to have at least some parts"); - int64_t ConstPart = 0; + DynamicAPInt ConstPart{0}; if (Row[0].Id == 0) ConstPart = Row[0].Coefficient; LLVM_DEBUG(dbgs() << join(Parts, std::string(" + ")) - << " <= " << std::to_string(ConstPart) << "\n"); + << " <= " << std::to_string(int64_t{ConstPart}) << "\n"); } #endif } @@ -191,10 +186,12 @@ bool ConstraintSystem::mayHaveSolution() { return HasSolution; } -bool ConstraintSystem::isConditionImplied(SmallVector R) const { +bool ConstraintSystem::isConditionImplied( + SmallVector R) const { // If all variable coefficients are 0, we have 'C >= 0'. If the constant is >= // 0, R is always true, regardless of the system. - if (all_of(ArrayRef(R).drop_front(1), [](int64_t C) { return C == 0; })) + if (all_of(ArrayRef(R).drop_front(1), + [](const DynamicAPInt &C) { return C == 0; })) return R[0] >= 0; // If there is no solution with the negation of R added to the system, the diff --git a/llvm/lib/Transforms/Scalar/ConstraintElimination.cpp b/llvm/lib/Transforms/Scalar/ConstraintElimination.cpp index c31173879af1e6..0a5b6548b3629b 100644 --- a/llvm/lib/Transforms/Scalar/ConstraintElimination.cpp +++ b/llvm/lib/Transforms/Scalar/ConstraintElimination.cpp @@ -12,6 +12,7 @@ //===----------------------------------------------------------------------===// #include "llvm/Transforms/Scalar/ConstraintElimination.h" +#include "llvm/ADT/DynamicAPInt.h" #include "llvm/ADT/STLExtras.h" #include "llvm/ADT/ScopeExit.h" #include "llvm/ADT/SmallVector.h" @@ -221,17 +222,17 @@ struct StackEntry { }; struct ConstraintTy { - SmallVector Coefficients; + SmallVector Coefficients; SmallVector Preconditions; - SmallVector> ExtraInfo; + SmallVector> ExtraInfo; bool IsSigned = false; ConstraintTy() = default; - ConstraintTy(SmallVector Coefficients, bool IsSigned, bool IsEq, - bool IsNe) + ConstraintTy(SmallVector Coefficients, bool IsSigned, + bool IsEq, bool IsNe) : Coefficients(std::move(Coefficients)), IsSigned(IsSigned), IsEq(IsEq), IsNe(IsNe) {} @@ -278,8 +279,9 @@ class ConstraintInfo { auto &Value2Index = getValue2Index(false); // Add Arg > -1 constraints to unsigned system for all function arguments. for (Value *Arg : FunctionArgs) { - ConstraintTy VarPos(SmallVector(Value2Index.size() + 1, 0), - false, false, false); + ConstraintTy VarPos( + SmallVector(Value2Index.size() + 1, DynamicAPInt{0}), + false, false, false); VarPos.Coefficients[Value2Index[Arg]] = -1; UnsignedCS.addVariableRow(VarPos.Coefficients); } @@ -663,8 +665,8 @@ ConstraintInfo::getConstraint(CmpInst::Predicate Pred, Value *Op0, Value *Op1, Preconditions, IsSigned, DL); auto BDec = decompose(Op1->stripPointerCastsSameRepresentation(), Preconditions, IsSigned, DL); - int64_t Offset1 = ADec.Offset; - int64_t Offset2 = BDec.Offset; + DynamicAPInt Offset1{ADec.Offset}; + DynamicAPInt Offset2{BDec.Offset}; Offset1 *= -1; auto &VariablesA = ADec.Vars; @@ -692,7 +694,8 @@ ConstraintInfo::getConstraint(CmpInst::Predicate Pred, Value *Op0, Value *Op1, // Build result constraint, by first adding all coefficients from A and then // subtracting all coefficients from B. ConstraintTy Res( - SmallVector(Value2Index.size() + NewVariables.size() + 1, 0), + SmallVector(Value2Index.size() + NewVariables.size() + 1, + DynamicAPInt{0}), IsSigned, IsEq, IsNe); // Collect variables that are known to be positive in all uses in the // constraint. @@ -706,27 +709,24 @@ ConstraintInfo::getConstraint(CmpInst::Predicate Pred, Value *Op0, Value *Op1, } for (const auto &KV : VariablesB) { - if (SubOverflow(R[GetOrAddIndex(KV.Variable)], KV.Coefficient, - R[GetOrAddIndex(KV.Variable)])) - return {}; + R[GetOrAddIndex(KV.Variable)] = + R[GetOrAddIndex(KV.Variable)] - KV.Coefficient; auto I = KnownNonNegativeVariables.insert({KV.Variable, KV.IsKnownNonNegative}); I.first->second &= KV.IsKnownNonNegative; } - int64_t OffsetSum; - if (AddOverflow(Offset1, Offset2, OffsetSum)) - return {}; + DynamicAPInt OffsetSum; + OffsetSum = Offset1 + Offset2; if (Pred == (IsSigned ? CmpInst::ICMP_SLT : CmpInst::ICMP_ULT)) - if (AddOverflow(OffsetSum, int64_t(-1), OffsetSum)) - return {}; + OffsetSum += -1; R[0] = OffsetSum; Res.Preconditions = std::move(Preconditions); // Remove any (Coefficient, Variable) entry where the Coefficient is 0 for new // variables. while (!NewVariables.empty()) { - int64_t Last = R.back(); + DynamicAPInt Last = R.back(); if (Last != 0) break; R.pop_back(); @@ -739,7 +739,8 @@ ConstraintInfo::getConstraint(CmpInst::Predicate Pred, Value *Op0, Value *Op1, if (!KV.second || (!Value2Index.contains(KV.first) && !NewIndexMap.contains(KV.first))) continue; - SmallVector C(Value2Index.size() + NewVariables.size() + 1, 0); + SmallVector C(Value2Index.size() + NewVariables.size() + 1, + DynamicAPInt{0}); C[GetOrAddIndex(KV.first)] = -1; Res.ExtraInfo.push_back(C); } @@ -756,8 +757,9 @@ ConstraintTy ConstraintInfo::getConstraintForSolving(CmpInst::Predicate Pred, (Pred == CmpInst::ICMP_UGE && Op1 == NullC)) { auto &Value2Index = getValue2Index(false); // Return constraint that's trivially true. - return ConstraintTy(SmallVector(Value2Index.size(), 0), false, - false, false); + return ConstraintTy( + SmallVector(Value2Index.size(), DynamicAPInt{0}), + false, false, false); } // If both operands are known to be non-negative, change signed predicates to @@ -892,7 +894,7 @@ void ConstraintInfo::transferToOtherSystem( #ifndef NDEBUG -static void dumpConstraint(ArrayRef C, +static void dumpConstraint(ArrayRef C, const DenseMap &Value2Index) { ConstraintSystem CS(Value2Index); CS.addVariableRowFill(C); @@ -1590,7 +1592,8 @@ void ConstraintInfo::addFact(CmpInst::Predicate Pred, Value *A, Value *B, if (!R.IsSigned) { for (Value *V : NewVariables) { - ConstraintTy VarPos(SmallVector(Value2Index.size() + 1, 0), + ConstraintTy VarPos(SmallVector(Value2Index.size() + 1, + DynamicAPInt{0}), false, false, false); VarPos.Coefficients[Value2Index[V]] = -1; CSToUse.addVariableRow(VarPos.Coefficients); diff --git a/llvm/test/Transforms/ConstraintElimination/constraint-overflow.ll b/llvm/test/Transforms/ConstraintElimination/constraint-overflow.ll index 88f87f4afab286..efb89fd0512d96 100644 --- a/llvm/test/Transforms/ConstraintElimination/constraint-overflow.ll +++ b/llvm/test/Transforms/ConstraintElimination/constraint-overflow.ll @@ -13,8 +13,7 @@ define i32 @f(i64 %a3, i64 %numElements) { ; CHECK-NEXT: [[CMP:%.*]] = icmp ugt i64 [[A1]], [[A3]] ; CHECK-NEXT: br i1 [[CMP]], label [[IF_END_I:%.*]], label [[ABORT:%.*]] ; CHECK: if.end.i: -; CHECK-NEXT: [[CMP2_NOT_I:%.*]] = icmp ult i64 [[A1]], [[A3]] -; CHECK-NEXT: br i1 [[CMP2_NOT_I]], label [[ABORT]], label [[EXIT:%.*]] +; CHECK-NEXT: br i1 false, label [[ABORT]], label [[EXIT:%.*]] ; CHECK: abort: ; CHECK-NEXT: ret i32 -1 ; CHECK: exit: diff --git a/llvm/test/Transforms/ConstraintElimination/overflows.ll b/llvm/test/Transforms/ConstraintElimination/overflows.ll index 556ae0c56f9aad..f60291cc846cec 100644 --- a/llvm/test/Transforms/ConstraintElimination/overflows.ll +++ b/llvm/test/Transforms/ConstraintElimination/overflows.ll @@ -23,8 +23,7 @@ define i1 @test_overflow_in_negate_constraint(i8 %x, i64 %y) { ; CHECK-NEXT: bb: ; CHECK-NEXT: [[ZEXT:%.*]] = zext i8 [[X]] to i64 ; CHECK-NEXT: [[SHL:%.*]] = shl nuw nsw i64 [[ZEXT]], 63 -; CHECK-NEXT: [[ICMP:%.*]] = icmp uge i64 [[Y]], [[SHL]] -; CHECK-NEXT: ret i1 [[ICMP]] +; CHECK-NEXT: ret i1 true ; bb: %zext = zext i8 %x to i64 diff --git a/llvm/unittests/Analysis/ConstraintSystemTest.cpp b/llvm/unittests/Analysis/ConstraintSystemTest.cpp index febeb982c87af8..567d5cf9494e53 100644 --- a/llvm/unittests/Analysis/ConstraintSystemTest.cpp +++ b/llvm/unittests/Analysis/ConstraintSystemTest.cpp @@ -7,21 +7,31 @@ //===----------------------------------------------------------------------===// #include "llvm/Analysis/ConstraintSystem.h" +#include "llvm/ADT/DynamicAPInt.h" +#include "llvm/ADT/SmallVector.h" #include "gtest/gtest.h" +#include using namespace llvm; namespace { +SmallVector toDynamicAPIntVec(std::initializer_list IL) { + SmallVector Ret; + Ret.reserve(IL.size()); + for (auto El : IL) + Ret.emplace_back(El); + return Ret; +} TEST(ConstraintSolverTest, TestSolutionChecks) { { ConstraintSystem CS; // x + y <= 10, x >= 5, y >= 6, x <= 10, y <= 10 - CS.addVariableRow({10, 1, 1}); - CS.addVariableRow({-5, -1, 0}); - CS.addVariableRow({-6, 0, -1}); - CS.addVariableRow({10, 1, 0}); - CS.addVariableRow({10, 0, 1}); + CS.addVariableRow(toDynamicAPIntVec({10, 1, 1})); + CS.addVariableRow(toDynamicAPIntVec({-5, -1, 0})); + CS.addVariableRow(toDynamicAPIntVec({-6, 0, -1})); + CS.addVariableRow(toDynamicAPIntVec({10, 1, 0})); + CS.addVariableRow(toDynamicAPIntVec({10, 0, 1})); EXPECT_FALSE(CS.mayHaveSolution()); } @@ -29,11 +39,11 @@ TEST(ConstraintSolverTest, TestSolutionChecks) { { ConstraintSystem CS; // x + y <= 10, x >= 2, y >= 3, x <= 10, y <= 10 - CS.addVariableRow({10, 1, 1}); - CS.addVariableRow({-2, -1, 0}); - CS.addVariableRow({-3, 0, -1}); - CS.addVariableRow({10, 1, 0}); - CS.addVariableRow({10, 0, 1}); + CS.addVariableRow(toDynamicAPIntVec({10, 1, 1})); + CS.addVariableRow(toDynamicAPIntVec({-2, -1, 0})); + CS.addVariableRow(toDynamicAPIntVec({-3, 0, -1})); + CS.addVariableRow(toDynamicAPIntVec({10, 1, 0})); + CS.addVariableRow(toDynamicAPIntVec({10, 0, 1})); EXPECT_TRUE(CS.mayHaveSolution()); } @@ -41,9 +51,9 @@ TEST(ConstraintSolverTest, TestSolutionChecks) { { ConstraintSystem CS; // x + y <= 10, x >= 10, y >= 10; does not have a solution. - CS.addVariableRow({10, 1, 1}); - CS.addVariableRow({-10, -1, 0}); - CS.addVariableRow({-10, 0, -1}); + CS.addVariableRow(toDynamicAPIntVec({10, 1, 1})); + CS.addVariableRow(toDynamicAPIntVec({-10, -1, 0})); + CS.addVariableRow(toDynamicAPIntVec({-10, 0, -1})); EXPECT_FALSE(CS.mayHaveSolution()); } @@ -51,9 +61,9 @@ TEST(ConstraintSolverTest, TestSolutionChecks) { { ConstraintSystem CS; // x + y >= 20, 10 >= x, 10 >= y; does HAVE a solution. - CS.addVariableRow({-20, -1, -1}); - CS.addVariableRow({-10, -1, 0}); - CS.addVariableRow({-10, 0, -1}); + CS.addVariableRow(toDynamicAPIntVec({-20, -1, -1})); + CS.addVariableRow(toDynamicAPIntVec({-10, -1, 0})); + CS.addVariableRow(toDynamicAPIntVec({-10, 0, -1})); EXPECT_TRUE(CS.mayHaveSolution()); } @@ -62,9 +72,9 @@ TEST(ConstraintSolverTest, TestSolutionChecks) { ConstraintSystem CS; // 2x + y + 3z <= 10, 2x + y >= 10, y >= 1 - CS.addVariableRow({10, 2, 1, 3}); - CS.addVariableRow({-10, -2, -1, 0}); - CS.addVariableRow({-1, 0, 0, -1}); + CS.addVariableRow(toDynamicAPIntVec({10, 2, 1, 3})); + CS.addVariableRow(toDynamicAPIntVec({-10, -2, -1, 0})); + CS.addVariableRow(toDynamicAPIntVec({-1, 0, 0, -1})); EXPECT_FALSE(CS.mayHaveSolution()); } @@ -73,8 +83,8 @@ TEST(ConstraintSolverTest, TestSolutionChecks) { ConstraintSystem CS; // 2x + y + 3z <= 10, 2x + y >= 10 - CS.addVariableRow({10, 2, 1, 3}); - CS.addVariableRow({-10, -2, -1, 0}); + CS.addVariableRow(toDynamicAPIntVec({10, 2, 1, 3})); + CS.addVariableRow(toDynamicAPIntVec({-10, -2, -1, 0})); EXPECT_TRUE(CS.mayHaveSolution()); } @@ -85,47 +95,47 @@ 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}); + CS.addVariableRow(toDynamicAPIntVec({5, 1, 0})); + CS.addVariableRow(toDynamicAPIntVec({3, 0, 1})); // x + y <= 6 does not hold. - EXPECT_FALSE(CS.isConditionImplied({6, 1, 1})); + EXPECT_FALSE(CS.isConditionImplied(toDynamicAPIntVec({6, 1, 1}))); // x + y <= 7 does not hold. - EXPECT_FALSE(CS.isConditionImplied({7, 1, 1})); + EXPECT_FALSE(CS.isConditionImplied(toDynamicAPIntVec({7, 1, 1}))); // x + y <= 8 does hold. - EXPECT_TRUE(CS.isConditionImplied({8, 1, 1})); + EXPECT_TRUE(CS.isConditionImplied(toDynamicAPIntVec({8, 1, 1}))); // 2 * x + y <= 12 does hold. - EXPECT_FALSE(CS.isConditionImplied({12, 2, 1})); + EXPECT_FALSE(CS.isConditionImplied(toDynamicAPIntVec({12, 2, 1}))); // 2 * x + y <= 13 does hold. - EXPECT_TRUE(CS.isConditionImplied({13, 2, 1})); + EXPECT_TRUE(CS.isConditionImplied(toDynamicAPIntVec({13, 2, 1}))); // x + y <= 12 does hold. - EXPECT_FALSE(CS.isConditionImplied({12, 2, 1})); + EXPECT_FALSE(CS.isConditionImplied(toDynamicAPIntVec({12, 2, 1}))); // 2 * x + y <= 13 does hold. - EXPECT_TRUE(CS.isConditionImplied({13, 2, 1})); + EXPECT_TRUE(CS.isConditionImplied(toDynamicAPIntVec({13, 2, 1}))); // x <= y == x - y <= 0 does not hold. - EXPECT_FALSE(CS.isConditionImplied({0, 1, -1})); + EXPECT_FALSE(CS.isConditionImplied(toDynamicAPIntVec({0, 1, -1}))); // y <= x == -x + y <= 0 does not hold. - EXPECT_FALSE(CS.isConditionImplied({0, -1, 1})); + EXPECT_FALSE(CS.isConditionImplied(toDynamicAPIntVec({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}); + CS.addVariableRow(toDynamicAPIntVec({0, 1, -1})); // x <= y == x - y <= 0 does hold. - EXPECT_TRUE(CS.isConditionImplied({0, 1, -1})); + EXPECT_TRUE(CS.isConditionImplied(toDynamicAPIntVec({0, 1, -1}))); // y <= x == -x + y <= 0 does not hold. - EXPECT_FALSE(CS.isConditionImplied({0, -1, 1})); + EXPECT_FALSE(CS.isConditionImplied(toDynamicAPIntVec({0, -1, 1}))); // x <= y + 10 == x - y <= 10 does hold. - EXPECT_TRUE(CS.isConditionImplied({10, 1, -1})); + EXPECT_TRUE(CS.isConditionImplied(toDynamicAPIntVec({10, 1, -1}))); // x + 10 <= y == x - y <= -10 does NOT hold. - EXPECT_FALSE(CS.isConditionImplied({-10, 1, -1})); + EXPECT_FALSE(CS.isConditionImplied(toDynamicAPIntVec({-10, 1, -1}))); } { @@ -133,21 +143,22 @@ TEST(ConstraintSolverTest, IsConditionImplied) { // x <= y == x - y <= 0 // y <= z == y - x <= 0 ConstraintSystem CS; - CS.addVariableRow({0, 1, -1, 0}); - CS.addVariableRow({0, 0, 1, -1}); + CS.addVariableRow(toDynamicAPIntVec({0, 1, -1, 0})); + CS.addVariableRow(toDynamicAPIntVec({0, 0, 1, -1})); // z <= y == -y + z <= 0 does not hold. - EXPECT_FALSE(CS.isConditionImplied({0, 0, -1, 1})); + EXPECT_FALSE(CS.isConditionImplied(toDynamicAPIntVec({0, 0, -1, 1}))); // x <= z == x - z <= 0 does hold. - EXPECT_TRUE(CS.isConditionImplied({0, 1, 0, -1})); + EXPECT_TRUE(CS.isConditionImplied(toDynamicAPIntVec({0, 1, 0, -1}))); } } TEST(ConstraintSolverTest, IsConditionImpliedOverflow) { ConstraintSystem CS; - // Make sure isConditionImplied returns false when there is an overflow. + // Make sure overflows are automatically handled by DynamicAPInt. 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})); + CS.addVariableRow(toDynamicAPIntVec({Limit - 1, Limit - 2, Limit - 3})); + EXPECT_TRUE(CS.isConditionImplied( + toDynamicAPIntVec({Limit - 1, Limit - 2, Limit - 3}))); } } // namespace