diff --git a/test/libsolutil/LP.cpp b/test/libsolutil/LP.cpp index 0c998ff70..72c461587 100644 --- a/test/libsolutil/LP.cpp +++ b/test/libsolutil/LP.cpp @@ -23,8 +23,12 @@ #include #include +#include + #include +#include + using namespace std; using namespace solidity::smtutil; using namespace solidity::util; @@ -41,6 +45,37 @@ public: m_solvingState.variableNames.emplace_back(""); } + LinearExpression linearExpression(vector _factors) + { + LinearExpression lexp; + lexp.resize(_factors.size()); + for (auto&& [index, value]: _factors | ranges::views::enumerate) + lexp[index] = rational{value}; + return lexp; + } + + void addFuzzerInput(vector> _constraints) + { + size_t totalNumVariables = 0; + for (auto c: _constraints) + { + bool equality = static_cast(c[0]); + vector factors(c.begin() + 1, c.end()); + m_solvingState.constraints.push_back( + { + linearExpression(factors), + equality + } + ); + auto it = find_if(factors.rbegin(), factors.rend(), [](auto const& _i) { return _i != 0; }); + size_t numVariablesInConstraint = factors.size() - 1 - static_cast(distance(factors.rbegin(), it)); + if (totalNumVariables < numVariablesInConstraint) + totalNumVariables = numVariablesInConstraint; + } + for (size_t i = 0; i < totalNumVariables; i++) + m_solvingState.variableNames.emplace_back("x" + to_string(i)); + } + LinearExpression constant(rational _value) { return LinearExpression::factorForVariable(0, _value); @@ -153,6 +188,23 @@ BOOST_AUTO_TEST_CASE(fuzzer) sat(); } +BOOST_AUTO_TEST_CASE(fuzzer3) +{ + addFuzzerInput( + { + {1,-1,0,0,0,0,90,9}, + {0,0,0,0,-76,0,0,74}, + {0,0,0,0,0,31,0,0,0,0,-71}, + {0,0,5,0,-85,60}, + {1,0,0,-9,0,0,63,-31,-2,0,-78}, + {0,0,50,-70,2,-76,94}, + {1,1,0,-3,51}, + {1,0,0,-33,0,0,0,60} + } + ); + infeasible(); +} + BOOST_AUTO_TEST_CASE(fuzzer2) { /* diff --git a/test/tools/ossfuzz/lpsolver/FuzzerSolverInterface.cpp b/test/tools/ossfuzz/lpsolver/FuzzerSolverInterface.cpp index 11800684d..ee69022ef 100644 --- a/test/tools/ossfuzz/lpsolver/FuzzerSolverInterface.cpp +++ b/test/tools/ossfuzz/lpsolver/FuzzerSolverInterface.cpp @@ -48,6 +48,18 @@ void FuzzerSolverInterface::addLPConstraint(pair> _constraint) m_lpSolvingState.constraints.push_back({linearExpression(move(_constraint.second)), _constraint.first}); } +void FuzzerSolverInterface::addLPVariable(string _varName) +{ + if ( + find( + m_lpSolvingState.variableNames.begin(), + m_lpSolvingState.variableNames.end(), + _varName + ) == m_lpSolvingState.variableNames.end() + ) + m_lpSolvingState.variableNames.emplace_back(_varName); +} + void FuzzerSolverInterface::addZ3Constraint(pair> _constraint) { bool isEquality = _constraint.first; @@ -57,6 +69,8 @@ void FuzzerSolverInterface::addZ3Constraint(pair> _constraint) if (index != 0 && value != 0) { string varName = "x" + to_string(index - 1); + // Add variable name to LP solving state to aid debugging + addLPVariable(varName); expr var = m_z3Ctx.real_const(varName.c_str()); expr factor = m_z3Ctx.int_val(value); reduce = reduce + var * factor; @@ -105,9 +119,13 @@ string FuzzerSolverInterface::checkZ3Result() bool FuzzerSolverInterface::differentialCheck(vector>> _constraints) { - addLPConstraints(_constraints); addZ3Constraints(_constraints); string z3Result = checkZ3Result(); + // There is no point in continuing if z3 (the quicker solver) returns + // unknown. + if (z3Result == "unknown") + return true; + addLPConstraints(_constraints); string lpResult = checkLPResult(); bool checkFailed = ((z3Result == "infeasible") && (lpResult == "feasible")) || ((z3Result == "feasible") && (lpResult == "infeasible")); diff --git a/test/tools/ossfuzz/lpsolver/FuzzerSolverInterface.h b/test/tools/ossfuzz/lpsolver/FuzzerSolverInterface.h index 9e4bc3649..6123ccde1 100644 --- a/test/tools/ossfuzz/lpsolver/FuzzerSolverInterface.h +++ b/test/tools/ossfuzz/lpsolver/FuzzerSolverInterface.h @@ -75,6 +75,9 @@ private: /// @returns Z3 result as string. std::string z3Result(z3::check_result _result); + /// Adds variable name to LP solver solving state. + void addLPVariable(std::string _varName); + solidity::util::LPSolver m_lpSolver; solidity::util::SolvingState m_lpSolvingState; z3::context m_z3Ctx;