cerc-io/solidity
10
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Rebase on rational solver.

Browse Source
This commit is contained in:
Bhargava Shastry 2022-03-01 10:57:11 +01:00
parent 9826efa461
commit de338e60de
3 changed files with 11 additions and 32 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

28
test/libsolutil/LP.cpp
View File

@ -61,14 +61,9 @@ public:
{ {
bool equality = static_cast<bool>(c[0]); bool equality = static_cast<bool>(c[0]);
vector<int> factors(c.begin() + 1, c.end()); vector<int> factors(c.begin() + 1, c.end());
m_solvingState.constraints.push_back( m_solvingState.constraints.push_back({linearExpression(factors), equality});
{ auto it = find_if(factors.rbegin(), factors.rend(), [](auto const& _i) { return _i != 0; });
linearExpression(factors), size_t numVariablesInConstraint = factors.size() - 1 - static_cast<size_t>(distance(factors.rbegin(), it));
equality
}
);
auto it = find_if(factors.rbegin(), factors.rend(), [](auto const& _i) { return _i != 0; });
size_t numVariablesInConstraint = factors.size() - 1 - static_cast<size_t>(distance(factors.rbegin(), it));
if (totalNumVariables < numVariablesInConstraint) if (totalNumVariables < numVariablesInConstraint)
totalNumVariables = numVariablesInConstraint; totalNumVariables = numVariablesInConstraint;
} }
@ -150,14 +145,6 @@ public:
BOOST_CHECK_MESSAGE(suppliedReason == _reason, "Reasons are different"); BOOST_CHECK_MESSAGE(suppliedReason == _reason, "Reasons are different");
} }
void sat()
{
auto [result, model] = m_solver.check(m_solvingState);
for (auto const& [var, value]: model)
cout << var << " = " << value << endl;
BOOST_REQUIRE(result == LPResult::Feasible);
}
protected: protected:
size_t variableIndex(string const& _name) size_t variableIndex(string const& _name)
{ {
@ -179,15 +166,6 @@ protected:
BOOST_FIXTURE_TEST_SUITE(LP, LPTestFramework, *boost::unit_test::label("nooptions")) BOOST_FIXTURE_TEST_SUITE(LP, LPTestFramework, *boost::unit_test::label("nooptions"))
BOOST_AUTO_TEST_CASE(fuzzer)
{
auto x = variable("x", -6);
auto y = variable("y", -6);
// expected result: -6x -6y = 8 is unsat since x >= 0 and y >= 0 are implied
addEQConstraint(x + y, constant(8));
sat();
}
BOOST_AUTO_TEST_CASE(fuzzer3) BOOST_AUTO_TEST_CASE(fuzzer3)
{ {
addFuzzerInput( addFuzzerInput(

6
test/tools/ossfuzz/lpsolver/FuzzerSolverInterface.cpp
View File

@ -45,7 +45,9 @@ LinearExpression FuzzerSolverInterface::linearExpression(vector<int> _factors)
void FuzzerSolverInterface::addLPConstraint(pair<bool, vector<int>> _constraint) void FuzzerSolverInterface::addLPConstraint(pair<bool, vector<int>> _constraint)
{ {
m_lpSolvingState.constraints.push_back({linearExpression(move(_constraint.second)), _constraint.first}); m_lpSolvingState.constraints.push_back(
{linearExpression(move(_constraint.second)), _constraint.first, {}}
);
} }
void FuzzerSolverInterface::addLPVariable(string _varName) void FuzzerSolverInterface::addLPVariable(string _varName)
@ -95,7 +97,7 @@ void FuzzerSolverInterface::addZ3Constraints(vector<pair<bool, vector<int>>> _co
addZ3Constraint(c); addZ3Constraint(c);
} }
solution FuzzerSolverInterface::checkLP() Solution FuzzerSolverInterface::checkLP()
{ {
return m_lpSolver.check(m_lpSolvingState); return m_lpSolver.check(m_lpSolvingState);
} }

9
test/tools/ossfuzz/lpsolver/FuzzerSolverInterface.h
View File

@ -28,10 +28,9 @@
namespace solidity::test::fuzzer::lpsolver namespace solidity::test::fuzzer::lpsolver
{ {
using solution = std::pair< using Model = std::map<std::string, solidity::util::rational>;
solidity::util::LPResult, using ReasonSet = std::set<size_t>;
std::map<std::string, solidity::util::rational> using Solution = std::pair<solidity::util::LPResult, std::variant<Model, ReasonSet>>;
>;
class FuzzerSolverInterface class FuzzerSolverInterface
{ {
@ -54,7 +53,7 @@ public:
solidity::util::LinearExpression linearExpression(std::vector<int> _factors); solidity::util::LinearExpression linearExpression(std::vector<int> _factors);
/// Queries LP solver and @returns solution. /// Queries LP solver and @returns solution.
solution checkLP(); Solution checkLP();
/// Queries Z3 solver and @returns solution. /// Queries Z3 solver and @returns solution.
z3::check_result checkZ3(); z3::check_result checkZ3();