diff --git a/test/tools/ossfuzz/CMakeLists.txt b/test/tools/ossfuzz/CMakeLists.txt index e9e95d108..22b6b567a 100644 --- a/test/tools/ossfuzz/CMakeLists.txt +++ b/test/tools/ossfuzz/CMakeLists.txt @@ -28,7 +28,7 @@ if (OSSFUZZ) LPSolverFuzzer.cpp LPSolverCustomMutatorInterface.cpp ) - target_link_libraries(lpsolver_ossfuzz PRIVATE solutil lpsolvergen) + target_link_libraries(lpsolver_ossfuzz PRIVATE solutil lpsolvergen z3) set_target_properties(lpsolver_ossfuzz PROPERTIES LINK_FLAGS ${LIB_FUZZING_ENGINE}) add_executable(solc_ossfuzz diff --git a/test/tools/ossfuzz/LPSolverFuzzer.cpp b/test/tools/ossfuzz/LPSolverFuzzer.cpp index 43ebb463c..c23667339 100644 --- a/test/tools/ossfuzz/LPSolverFuzzer.cpp +++ b/test/tools/ossfuzz/LPSolverFuzzer.cpp @@ -113,21 +113,12 @@ extern "C" int LLVMFuzzerTestOneInput(uint8_t const* _data, size_t _size) auto constraints = parseConstraints(input); if (constraints.has_value()) { - // TODO: Z3 on constraints provided by fuzzer interface and comparing its outcome - // with LP solver. - FuzzerSolverInterface solverWithoutModels(/*supportModels=*/false); FuzzerSolverInterface solverWithModels(/*supportModels=*/true); - - solverWithoutModels.addConstraints(constraints.value()); - string resultWithoutModels = solverWithoutModels.checkResult(); - solverWithModels.addConstraints(constraints.value()); - string resultWithModels = solverWithModels.checkResult(); - - if (resultWithoutModels != resultWithModels) + if (!solverWithModels.differentialCheck(constraints.value())) { - cout << resultWithoutModels << endl; - cout << resultWithModels << endl; - solAssert(false, "LP result without models did not match with result with models."); + cout << solverWithModels.m_lpResult << endl; + cout << solverWithModels.m_z3Result << endl; + solAssert(false, "LP result did not match with z3 result."); } } } diff --git a/test/tools/ossfuzz/lpsolver/FuzzerSolverInterface.cpp b/test/tools/ossfuzz/lpsolver/FuzzerSolverInterface.cpp index 365e42af8..11800684d 100644 --- a/test/tools/ossfuzz/lpsolver/FuzzerSolverInterface.cpp +++ b/test/tools/ossfuzz/lpsolver/FuzzerSolverInterface.cpp @@ -17,14 +17,21 @@ #include +#include + using namespace solidity::test::fuzzer::lpsolver; using namespace solidity::util; using namespace std; +using namespace z3; FuzzerSolverInterface::FuzzerSolverInterface(bool _supportModels): - m_solver(_supportModels) + m_lpSolver(_supportModels), + m_z3Solver(m_z3Ctx) { - m_solvingState.variableNames.emplace_back(""); + m_lpSolvingState.variableNames.emplace_back(""); + params z3Params(m_z3Ctx); + z3Params.set(":timeout", static_cast(10)); // in milliseconds + m_z3Solver.set(z3Params); } LinearExpression FuzzerSolverInterface::linearExpression(vector _factors) @@ -36,26 +43,75 @@ LinearExpression FuzzerSolverInterface::linearExpression(vector _factors) return lexp; } -void FuzzerSolverInterface::addConstraint(pair> _constraint) +void FuzzerSolverInterface::addLPConstraint(pair> _constraint) { - m_solvingState.constraints.push_back({linearExpression(move(_constraint.second)), _constraint.first}); + m_lpSolvingState.constraints.push_back({linearExpression(move(_constraint.second)), _constraint.first}); } -void FuzzerSolverInterface::addConstraints(vector>> _constraints) +void FuzzerSolverInterface::addZ3Constraint(pair> _constraint) +{ + bool isEquality = _constraint.first; + expr reduce = m_z3Ctx.real_val(0); + for (auto&& [index, value]: _constraint.second | ranges::views::enumerate) + { + if (index != 0 && value != 0) + { + string varName = "x" + to_string(index - 1); + expr var = m_z3Ctx.real_const(varName.c_str()); + expr factor = m_z3Ctx.int_val(value); + reduce = reduce + var * factor; + m_z3Solver.add(var >= 0); + } + } + if (isEquality) + m_z3Solver.add(reduce == _constraint.second[0]); + else + m_z3Solver.add(reduce <= _constraint.second[0]); +} + +void FuzzerSolverInterface::addLPConstraints(vector>> _constraints) { for (auto c: _constraints) - addConstraint(c); + addLPConstraint(c); } -solution FuzzerSolverInterface::check() +void FuzzerSolverInterface::addZ3Constraints(vector>> _constraints) { - return m_solver.check(m_solvingState); + for (auto c: _constraints) + addZ3Constraint(c); } -string FuzzerSolverInterface::checkResult() +solution FuzzerSolverInterface::checkLP() { - auto r = check(); - return lpResult(r.first); + return m_lpSolver.check(m_lpSolvingState); +} + +check_result FuzzerSolverInterface::checkZ3() +{ + return m_z3Solver.check(); +} + +string FuzzerSolverInterface::checkLPResult() +{ + m_lpResult = lpResult(checkLP().first); + return m_lpResult; +} + +string FuzzerSolverInterface::checkZ3Result() +{ + m_z3Result = z3Result(checkZ3()); + return m_z3Result; +} + +bool FuzzerSolverInterface::differentialCheck(vector>> _constraints) +{ + addLPConstraints(_constraints); + addZ3Constraints(_constraints); + string z3Result = checkZ3Result(); + string lpResult = checkLPResult(); + bool checkFailed = ((z3Result == "infeasible") && (lpResult == "feasible")) || + ((z3Result == "feasible") && (lpResult == "infeasible")); + return !checkFailed; } string FuzzerSolverInterface::lpResult(LPResult _result) @@ -72,3 +128,18 @@ string FuzzerSolverInterface::lpResult(LPResult _result) return "infeasible"; } } + +string FuzzerSolverInterface::z3Result(check_result _result) +{ + switch (_result) + { + case check_result::unsat: + return "infeasible"; + case check_result::sat: + return "feasible"; + case check_result::unknown: + return "unknown"; + default: + solAssert(false, "Invalid Z3 result"); + } +} diff --git a/test/tools/ossfuzz/lpsolver/FuzzerSolverInterface.h b/test/tools/ossfuzz/lpsolver/FuzzerSolverInterface.h index 114821f7e..9e4bc3649 100644 --- a/test/tools/ossfuzz/lpsolver/FuzzerSolverInterface.h +++ b/test/tools/ossfuzz/lpsolver/FuzzerSolverInterface.h @@ -21,6 +21,8 @@ #include #include +#include + #include namespace solidity::test::fuzzer::lpsolver @@ -37,25 +39,48 @@ public: FuzzerSolverInterface(bool _supportModels); /// Adds @param _constraint to LP solver. - void addConstraint(std::pair> _constraint); + void addLPConstraint(std::pair> _constraint); + + /// Adds @param _constraint to Z3 solver. + void addZ3Constraint(std::pair> _constraint); /// Adds @param _constraints to LP solver. - void addConstraints(std::vector>> _constraints); + void addLPConstraints(std::vector>> _constraints); + + /// Adds @param _constraints to Z3 solver. + void addZ3Constraints(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(); + solution checkLP(); + + /// Queries Z3 solver and @returns solution. + z3::check_result checkZ3(); /// Queries LP solver and @returns sat result as string. - std::string checkResult(); + std::string checkLPResult(); + /// Queries Z3 solver and @returns sat result as string. + std::string checkZ3Result(); + + /// @returns true if both the LP and the Z3 solver return an identical result on + /// @param _constraints, false otherwise. + bool differentialCheck(std::vector>> _constraints); private: /// @returns LP result as string. std::string lpResult(solidity::util::LPResult _result); - solidity::util::LPSolver m_solver; - solidity::util::SolvingState m_solvingState; + /// @returns Z3 result as string. + std::string z3Result(z3::check_result _result); + + solidity::util::LPSolver m_lpSolver; + solidity::util::SolvingState m_lpSolvingState; + z3::context m_z3Ctx; + z3::solver m_z3Solver; +public: + std::string m_lpResult; + std::string m_z3Result; }; }