From efb0d4253c33269a9f59c2a4c71a44cba3888927 Mon Sep 17 00:00:00 2001 From: Martin Blicha Date: Mon, 26 Jun 2023 11:55:31 +0200 Subject: [PATCH] Use callback properly in SMTLib2 interface --- libsmtutil/SMTLib2Interface.cpp | 136 +++++++++++++++++++------------- libsmtutil/SMTLib2Interface.h | 9 +-- libsolidity/formal/BMC.cpp | 2 +- 3 files changed, 83 insertions(+), 64 deletions(-) diff --git a/libsmtutil/SMTLib2Interface.cpp b/libsmtutil/SMTLib2Interface.cpp index 62e9d70bd..888949e36 100644 --- a/libsmtutil/SMTLib2Interface.cpp +++ b/libsmtutil/SMTLib2Interface.cpp @@ -39,17 +39,14 @@ using namespace solidity::frontend; using namespace solidity::smtutil; SMTLib2Interface::SMTLib2Interface( - std::map _queryResponses, + [[maybe_unused]] std::map _queryResponses, ReadCallback::Callback _smtCallback, SMTSolverChoice _enabledSolvers, - std::optional _queryTimeout, - bool _dumpQuery + std::optional _queryTimeout ): SolverInterface(_queryTimeout), - m_queryResponses(std::move(_queryResponses)), m_smtCallback(std::move(_smtCallback)), - m_enabledSolvers(_enabledSolvers), - m_dumpQuery(_dumpQuery) + m_enabledSolvers(_enabledSolvers) { reset(); } @@ -117,28 +114,88 @@ void SMTLib2Interface::addAssertion(Expression const& _expr) write("(assert " + toSExpr(_expr) + ")"); } +namespace { // Helpers for querying solvers using SMT callback + auto resultFromSolverResponse (std::string const& response) { + CheckResult result; + // TODO proper parsing + if (boost::starts_with(response, "sat\n")) + result = CheckResult::SATISFIABLE; + else if (boost::starts_with(response, "unsat\n")) + result = CheckResult::UNSATISFIABLE; + else if (boost::starts_with(response, "unknown\n")) + result = CheckResult::UNKNOWN; + else + result = CheckResult::ERROR; + return result; + } + + bool solverAnswered(CheckResult result) + { + return result == CheckResult::SATISFIABLE || result == CheckResult::UNSATISFIABLE; + } + + std::vector parseValues(std::string::const_iterator _start, std::string::const_iterator _end) + { + std::vector values; + while (_start < _end) + { + auto valStart = find(_start, _end, ' '); + if (valStart < _end) + ++valStart; + auto valEnd = find(valStart, _end, ')'); + values.emplace_back(valStart, valEnd); + _start = find(valEnd, _end, '('); + } + + return values; + } + + std::vector parseValues(string const& solverAnswer) + { + return parseValues(find(solverAnswer.cbegin(), solverAnswer.cend(), '\n'), solverAnswer.cend()); + } +} + std::pair> SMTLib2Interface::check(std::vector const& _expressionsToEvaluate) { - std::string response = querySolver( - boost::algorithm::join(m_accumulatedOutput, "\n") + - checkSatAndGetValuesCommand(_expressionsToEvaluate) - ); + auto query = boost::algorithm::join(m_accumulatedOutput, "\n") + + checkSatAndGetValuesCommand(_expressionsToEvaluate); - CheckResult result; - // TODO proper parsing - if (boost::starts_with(response, "sat\n")) - result = CheckResult::SATISFIABLE; - else if (boost::starts_with(response, "unsat\n")) - result = CheckResult::UNSATISFIABLE; - else if (boost::starts_with(response, "unknown\n")) - result = CheckResult::UNKNOWN; - else - result = CheckResult::ERROR; + std::vector solverCommands; + if (m_enabledSolvers.z3) + solverCommands.emplace_back("z3"); + if (m_enabledSolvers.cvc4) + solverCommands.emplace_back("cvc4"); - std::vector values; - if (result == CheckResult::SATISFIABLE && !_expressionsToEvaluate.empty()) - values = parseValues(find(response.cbegin(), response.cend(), '\n'), response.cend()); - return std::make_pair(result, values); + CheckResult lastResult = CheckResult::ERROR; + std::vector finalValues; + for (auto const& s: solverCommands) + { + auto callBackResult = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery) + ' ' + s, query); + if (not callBackResult.success) + continue; + auto const& response = callBackResult.responseOrErrorMessage; + CheckResult result = resultFromSolverResponse(response); + if (solverAnswered(result)) + { + if (!solverAnswered(lastResult)) + { + lastResult = result; + finalValues = parseValues(response); + } + else if (lastResult != result) + { + lastResult = CheckResult::CONFLICTING; + break; + } + } + else if (result == CheckResult::UNKNOWN && lastResult == CheckResult::ERROR) + lastResult = result; + } + if (lastResult == CheckResult::ERROR) { + m_unhandledQueries.push_back(query); + } + return std::make_pair(lastResult, finalValues); } std::string SMTLib2Interface::toSExpr(Expression const& _expr) @@ -295,37 +352,6 @@ std::string SMTLib2Interface::checkSatAndGetValuesCommand(std::vector SMTLib2Interface::parseValues(std::string::const_iterator _start, std::string::const_iterator _end) -{ - std::vector values; - while (_start < _end) - { - auto valStart = find(_start, _end, ' '); - if (valStart < _end) - ++valStart; - auto valEnd = find(valStart, _end, ')'); - values.emplace_back(valStart, valEnd); - _start = find(valEnd, _end, '('); - } - - return values; -} - -std::string SMTLib2Interface::querySolver(std::string const& _input) -{ - h256 inputHash = keccak256(_input); - if (m_queryResponses.count(inputHash)) - return m_queryResponses.at(inputHash); - if (m_smtCallback) - { - auto result = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery), _input); - if (result.success) - return result.responseOrErrorMessage; - } - m_unhandledQueries.push_back(_input); - return "unknown\n"; -} - std::string SMTLib2Interface::dumpQuery(std::vector const& _expressionsToEvaluate) { return boost::algorithm::join(m_accumulatedOutput, "\n") + diff --git a/libsmtutil/SMTLib2Interface.h b/libsmtutil/SMTLib2Interface.h index 910065b10..91430a8d4 100644 --- a/libsmtutil/SMTLib2Interface.h +++ b/libsmtutil/SMTLib2Interface.h @@ -45,8 +45,7 @@ public: std::map _queryResponses = {}, frontend::ReadCallback::Callback _smtCallback = {}, SMTSolverChoice _enabledSolvers = SMTSolverChoice::All(), - std::optional _queryTimeout = {}, - bool _printQuery = false + std::optional _queryTimeout = {} ); void reset() override; @@ -78,10 +77,6 @@ private: void write(std::string _data); std::string checkSatAndGetValuesCommand(std::vector const& _expressionsToEvaluate); - std::vector parseValues(std::string::const_iterator _start, std::string::const_iterator _end); - - /// Communicates with the solver via the callback. Throws SMTSolverError on error. - std::string querySolver(std::string const& _input); std::vector m_accumulatedOutput; std::map m_variables; @@ -92,12 +87,10 @@ private: /// otherwise solvers cannot parse the queries. std::vector> m_userSorts; - std::map m_queryResponses; std::vector m_unhandledQueries; frontend::ReadCallback::Callback m_smtCallback; SMTSolverChoice m_enabledSolvers; - bool m_dumpQuery; }; } diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index c455ddc70..e879abfa1 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -44,7 +44,7 @@ BMC::BMC( ): SMTEncoder(_context, _settings, _errorReporter, _unsupportedErrorReporter, _charStreamProvider), m_interface(std::make_unique( - _smtlib2Responses, _smtCallback, _settings.solvers, _settings.timeout, _settings.printQuery + _smtlib2Responses, _smtCallback, _settings.solvers, _settings.timeout )) { solAssert(!_settings.printQuery || _settings.solvers == smtutil::SMTSolverChoice::SMTLIB2(), "Only SMTLib2 solver can be enabled to print queries");