From cb1e6b3179e1581324133b339215762d7fc1c6b0 Mon Sep 17 00:00:00 2001 From: Bhargava Shastry Date: Mon, 7 Feb 2022 15:25:22 +0100 Subject: [PATCH] Support models. --- test/tools/ossfuzz/LPSolverFuzzer.cpp | 61 ++++++++++++++--- .../lpsolver/FuzzerSolverInterface.cpp | 66 ++++++++++++++++++- .../ossfuzz/lpsolver/FuzzerSolverInterface.h | 23 ++++++- 3 files changed, 138 insertions(+), 12 deletions(-) diff --git a/test/tools/ossfuzz/LPSolverFuzzer.cpp b/test/tools/ossfuzz/LPSolverFuzzer.cpp index 2083c8295..eb0e78fcd 100644 --- a/test/tools/ossfuzz/LPSolverFuzzer.cpp +++ b/test/tools/ossfuzz/LPSolverFuzzer.cpp @@ -16,6 +16,8 @@ */ // SPDX-License-Identifier: GPL-3.0 +#include + #include #include #include @@ -23,11 +25,40 @@ #include #include +using namespace solidity::test::fuzzer::lpsolver; using namespace std; // Prototype as we can't use the FuzzerInterface.h header. extern "C" int LLVMFuzzerTestOneInput(uint8_t const* _data, size_t _size); +namespace +{ +#ifdef DEBUG +void printConstraints(vector>> _constraints) +{ + for (auto& i: _constraints) + { + cout << (i.first ? "=" : "<="); + for (auto& j: i.second) + cout << "," << j; + cout << endl; + } +} +#endif + +bool validConstraints(vector>> _constraints) +{ + // Zero input constraints is an invalid input + if (_constraints.size() < 1) + return false; + // Incomplete constraints are invalid + for (auto c: _constraints) + if (c.second.empty()) + return false; + return true; +} +} + extern "C" int LLVMFuzzerTestOneInput(uint8_t const* _data, size_t _size) { // Parse CSV input @@ -54,16 +85,26 @@ extern "C" int LLVMFuzzerTestOneInput(uint8_t const* _data, size_t _size) constraints.emplace_back(constraint); } - // Debug - for (auto& i: constraints) + if (!validConstraints(constraints)) + return 0; + else { - cout << (i.first ? "=" : "<="); - for (auto& j: i.second) - cout << "," << j; - cout << endl; - } + // TODO: Z3 on constraints provided by fuzzer interface and comparing its outcome + // with LP solver. + FuzzerSolverInterface solverWithoutModels(/*supportModels=*/false); + FuzzerSolverInterface solverWithModels(/*supportModels=*/true); - // TODO: Invoke LP solver and Z3 on constraints provided by fuzzer interface, - // comparing their outcomes. - return 0; + solverWithoutModels.addConstraints(constraints); + string resultWithoutModels = solverWithoutModels.checkResult(); + solverWithModels.addConstraints(constraints); + string resultWithModels = solverWithModels.checkResult(); + + if (resultWithoutModels != resultWithModels) + { + cout << resultWithoutModels << endl; + cout << resultWithModels << endl; + solAssert(false, "LP result without models did not match with result with models."); + } + return 0; + } } diff --git a/test/tools/ossfuzz/lpsolver/FuzzerSolverInterface.cpp b/test/tools/ossfuzz/lpsolver/FuzzerSolverInterface.cpp index 4e82d71d8..fc7cb3ffa 100644 --- a/test/tools/ossfuzz/lpsolver/FuzzerSolverInterface.cpp +++ b/test/tools/ossfuzz/lpsolver/FuzzerSolverInterface.cpp @@ -19,7 +19,8 @@ using namespace solidity::test::fuzzer::lpsolver; using namespace solidity::util; using namespace std; -FuzzerSolverInterface::FuzzerSolverInterface() +FuzzerSolverInterface::FuzzerSolverInterface(bool _supportModels): + m_solver(_supportModels) { m_solvingState.variableNames.emplace_back(""); } @@ -53,11 +54,74 @@ void FuzzerSolverInterface::addEQConstraint(LinearExpression _lhs) m_solvingState.constraints.push_back({move(_lhs), true}); } +LinearExpression FuzzerSolverInterface::linearExpression(vector _factors) +{ + bool first = true; + unsigned count = 0; + LinearExpression lexp; + for (auto f: _factors) + { + if (first) + { + first = false; + lexp += constant(f); + } + else + lexp += variable(f, "x" + to_string(count++)); + } + return lexp; +} + +void FuzzerSolverInterface::addEQConstraint(vector _factors) +{ + addEQConstraint(linearExpression(_factors)); +} + +void FuzzerSolverInterface::addLEConstraint(vector _factors) +{ + addLEConstraint(linearExpression(_factors)); +} + +void FuzzerSolverInterface::addConstraint(pair> _constraint) +{ + if (_constraint.first) + addEQConstraint(_constraint.second); + else + addLEConstraint(_constraint.second); +} + +void FuzzerSolverInterface::addConstraints(vector>> _constraints) +{ + for (auto c: _constraints) + addConstraint(c); +} + solution FuzzerSolverInterface::check() { return m_solver.check(m_solvingState); } +string FuzzerSolverInterface::checkResult() +{ + auto r = check(); + return lpResult(r.first); +} + +string FuzzerSolverInterface::lpResult(LPResult _result) +{ + switch (_result) + { + case LPResult::Unknown: + return "unknown"; + case LPResult::Unbounded: + return "unbounded"; + case LPResult::Feasible: + return "feasible"; + case LPResult::Infeasible: + return "infeasible"; + } +} + size_t FuzzerSolverInterface::variableIndex(string const& _name) { if (m_solvingState.variableNames.empty()) diff --git a/test/tools/ossfuzz/lpsolver/FuzzerSolverInterface.h b/test/tools/ossfuzz/lpsolver/FuzzerSolverInterface.h index 655926ad1..a93c5a040 100644 --- a/test/tools/ossfuzz/lpsolver/FuzzerSolverInterface.h +++ b/test/tools/ossfuzz/lpsolver/FuzzerSolverInterface.h @@ -34,7 +34,7 @@ using solution = std::pair< class FuzzerSolverInterface { public: - FuzzerSolverInterface(); + FuzzerSolverInterface(bool _supportModels); /// @returns constant rational. solidity::util::LinearExpression constant(solidity::util::rational _rationalConstant); @@ -57,13 +57,34 @@ public: /// Adds equal-to-zero constraint to solver. void addEQConstraint(solidity::util::LinearExpression _lhs); + /// Adds less-than-equal constraint from vector of factors. + void addLEConstraint(std::vector _factors); + + /// Adds equal-to constraint from vector of factors. + void addEQConstraint(std::vector _factors); + + /// Adds @param _constraint to LP solver. + void addConstraint(std::pair> _constraint); + + /// Adds @param _constraints to LP solver. + void addConstraints(std::vector>> _constraints); + + /// @returns linear expression created from @param _factors. + solidity::util::LinearExpression linearExpression(std::vector _factors); + /// Queries LP solver and @returns solution. solution check(); + /// Queries LP solver and @returns sat result as string. + std::string checkResult(); + private: /// Adds variable if necessary to LP solver state and @returns index of variable. size_t variableIndex(std::string const& _name); + /// @returns LP result as string. + std::string lpResult(solidity::util::LPResult _result); + solidity::util::LPSolver m_solver; solidity::util::SolvingState m_solvingState; };