diff --git a/libsmtutil/CHCSmtLib2Interface.cpp b/libsmtutil/CHCSmtLib2Interface.cpp index 89cee2a3f..d4b697bcf 100644 --- a/libsmtutil/CHCSmtLib2Interface.cpp +++ b/libsmtutil/CHCSmtLib2Interface.cpp @@ -43,7 +43,7 @@ CHCSmtLib2Interface::CHCSmtLib2Interface( std::optional _queryTimeout ): CHCSolverInterface(_queryTimeout), - m_smtlib2(std::make_unique(_queryResponses, _smtCallback, m_queryTimeout)), + m_smtlib2(std::make_unique(_queryResponses, _smtCallback, _enabledSolvers, m_queryTimeout)), m_queryResponses(std::move(_queryResponses)), m_smtCallback(_smtCallback), m_enabledSolvers(_enabledSolvers) diff --git a/libsmtutil/CMakeLists.txt b/libsmtutil/CMakeLists.txt index 0c1afda8d..120996219 100644 --- a/libsmtutil/CMakeLists.txt +++ b/libsmtutil/CMakeLists.txt @@ -4,8 +4,6 @@ set(sources Exceptions.h SMTLib2Interface.cpp SMTLib2Interface.h - SMTPortfolio.cpp - SMTPortfolio.h SolverInterface.h Sorts.cpp Sorts.h diff --git a/libsmtutil/SMTLib2Interface.cpp b/libsmtutil/SMTLib2Interface.cpp index ac5645bf1..62e9d70bd 100644 --- a/libsmtutil/SMTLib2Interface.cpp +++ b/libsmtutil/SMTLib2Interface.cpp @@ -41,11 +41,15 @@ using namespace solidity::smtutil; SMTLib2Interface::SMTLib2Interface( std::map _queryResponses, ReadCallback::Callback _smtCallback, - std::optional _queryTimeout + SMTSolverChoice _enabledSolvers, + std::optional _queryTimeout, + bool _dumpQuery ): SolverInterface(_queryTimeout), m_queryResponses(std::move(_queryResponses)), - m_smtCallback(std::move(_smtCallback)) + m_smtCallback(std::move(_smtCallback)), + m_enabledSolvers(_enabledSolvers), + m_dumpQuery(_dumpQuery) { reset(); } diff --git a/libsmtutil/SMTLib2Interface.h b/libsmtutil/SMTLib2Interface.h index 9ef8e94a8..910065b10 100644 --- a/libsmtutil/SMTLib2Interface.h +++ b/libsmtutil/SMTLib2Interface.h @@ -44,7 +44,9 @@ public: explicit SMTLib2Interface( std::map _queryResponses = {}, frontend::ReadCallback::Callback _smtCallback = {}, - std::optional _queryTimeout = {} + SMTSolverChoice _enabledSolvers = SMTSolverChoice::All(), + std::optional _queryTimeout = {}, + bool _printQuery = false ); void reset() override; @@ -94,6 +96,8 @@ private: std::vector m_unhandledQueries; frontend::ReadCallback::Callback m_smtCallback; + SMTSolverChoice m_enabledSolvers; + bool m_dumpQuery; }; } diff --git a/libsmtutil/SMTPortfolio.cpp b/libsmtutil/SMTPortfolio.cpp deleted file mode 100644 index 89c2d410c..000000000 --- a/libsmtutil/SMTPortfolio.cpp +++ /dev/null @@ -1,153 +0,0 @@ -/* - This file is part of solidity. - - solidity is free software: you can redistribute it and/or modify - it under the terms of the GNU General Public License as published by - the Free Software Foundation, either version 3 of the License, or - (at your option) any later version. - - solidity is distributed in the hope that it will be useful, - but WITHOUT ANY WARRANTY; without even the implied warranty of - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - GNU General Public License for more details. - - You should have received a copy of the GNU General Public License - along with solidity. If not, see . -*/ -// SPDX-License-Identifier: GPL-3.0 - -#include - -#include - -using namespace solidity; -using namespace solidity::util; -using namespace solidity::frontend; -using namespace solidity::smtutil; - -SMTPortfolio::SMTPortfolio( - std::map _smtlib2Responses, - frontend::ReadCallback::Callback _smtCallback, - [[maybe_unused]] SMTSolverChoice _enabledSolvers, - std::optional _queryTimeout, - bool _printQuery -): - SolverInterface(_queryTimeout) -{ - solAssert(!_printQuery || _enabledSolvers == smtutil::SMTSolverChoice::SMTLIB2(), "Only SMTLib2 solver can be enabled to print queries"); - if (_enabledSolvers.smtlib2) - m_solvers.emplace_back(std::make_unique(std::move(_smtlib2Responses), std::move(_smtCallback), m_queryTimeout)); -} - -void SMTPortfolio::reset() -{ - for (auto const& s: m_solvers) - s->reset(); -} - -void SMTPortfolio::push() -{ - for (auto const& s: m_solvers) - s->push(); -} - -void SMTPortfolio::pop() -{ - for (auto const& s: m_solvers) - s->pop(); -} - -void SMTPortfolio::declareVariable(std::string const& _name, SortPointer const& _sort) -{ - smtAssert(_sort, ""); - for (auto const& s: m_solvers) - s->declareVariable(_name, _sort); -} - -void SMTPortfolio::addAssertion(Expression const& _expr) -{ - for (auto const& s: m_solvers) - s->addAssertion(_expr); -} - -/* - * Broadcasts the SMT query to all solvers and returns a single result. - * This comment explains how this result is decided. - * - * When a solver is queried, there are four possible answers: - * SATISFIABLE (SAT), UNSATISFIABLE (UNSAT), UNKNOWN, CONFLICTING, ERROR - * We say that a solver _answered_ the query if it returns either: - * SAT or UNSAT - * A solver did not answer the query if it returns either: - * UNKNOWN (it tried but couldn't solve it) or ERROR (crash, internal error, API error, etc). - * - * Ideally all solvers answer the query and agree on what the answer is - * (all say SAT or all say UNSAT). - * - * The actual logic as as follows: - * 1) If at least one solver answers the query, all the non-answer results are ignored. - * Here SAT/UNSAT is preferred over UNKNOWN since it's an actual answer, and over ERROR - * because one buggy solver/integration shouldn't break the portfolio. - * - * 2) If at least one solver answers SAT and at least one answers UNSAT, at least one of them is buggy - * and the result is CONFLICTING. - * In the future if we have more than 2 solvers enabled we could go with the majority. - * - * 3) If NO solver answers the query: - * If at least one solver returned UNKNOWN (where the rest returned ERROR), the result is UNKNOWN. - * This is preferred over ERROR since the SMTChecker might decide to abstract the query - * when it is told that this is a hard query to solve. - * - * If all solvers return ERROR, the result is ERROR. -*/ -std::pair> SMTPortfolio::check(std::vector const& _expressionsToEvaluate) -{ - CheckResult lastResult = CheckResult::ERROR; - std::vector finalValues; - for (auto const& s: m_solvers) - { - CheckResult result; - std::vector values; - tie(result, values) = s->check(_expressionsToEvaluate); - if (solverAnswered(result)) - { - if (!solverAnswered(lastResult)) - { - lastResult = result; - finalValues = std::move(values); - } - else if (lastResult != result) - { - lastResult = CheckResult::CONFLICTING; - break; - } - } - else if (result == CheckResult::UNKNOWN && lastResult == CheckResult::ERROR) - lastResult = result; - } - return std::make_pair(lastResult, finalValues); -} - -std::vector SMTPortfolio::unhandledQueries() -{ - // This code assumes that the constructor guarantees that - // SmtLib2Interface is in position 0, if enabled. - if (!m_solvers.empty()) - if (auto smtlib2 = dynamic_cast(m_solvers.front().get())) - return smtlib2->unhandledQueries(); - return {}; -} - -bool SMTPortfolio::solverAnswered(CheckResult result) -{ - return result == CheckResult::SATISFIABLE || result == CheckResult::UNSATISFIABLE; -} - -std::string SMTPortfolio::dumpQuery(std::vector const& _expressionsToEvaluate) -{ - // This code assumes that the constructor guarantees that - // SmtLib2Interface is in position 0, if enabled. - auto smtlib2 = dynamic_cast(m_solvers.front().get()); - solAssert(smtlib2, "Must use SMTLib2 solver to dump queries"); - return smtlib2->dumpQuery(_expressionsToEvaluate); -} diff --git a/libsmtutil/SMTPortfolio.h b/libsmtutil/SMTPortfolio.h deleted file mode 100644 index cdb33368e..000000000 --- a/libsmtutil/SMTPortfolio.h +++ /dev/null @@ -1,77 +0,0 @@ -/* - This file is part of solidity. - - solidity is free software: you can redistribute it and/or modify - it under the terms of the GNU General Public License as published by - the Free Software Foundation, either version 3 of the License, or - (at your option) any later version. - - solidity is distributed in the hope that it will be useful, - but WITHOUT ANY WARRANTY; without even the implied warranty of - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - GNU General Public License for more details. - - You should have received a copy of the GNU General Public License - along with solidity. If not, see . -*/ -// SPDX-License-Identifier: GPL-3.0 - -#pragma once - - -#include -#include -#include - -#include -#include - -namespace solidity::smtutil -{ - -/** - * The SMTPortfolio wraps all available solvers within a single interface, - * propagating the functionalities to all solvers. - * It also checks whether different solvers give conflicting answers - * to SMT queries. - */ -class SMTPortfolio: public SolverInterface -{ -public: - /// Noncopyable. - SMTPortfolio(SMTPortfolio const&) = delete; - SMTPortfolio& operator=(SMTPortfolio const&) = delete; - - SMTPortfolio( - std::map _smtlib2Responses = {}, - frontend::ReadCallback::Callback _smtCallback = {}, - SMTSolverChoice _enabledSolvers = SMTSolverChoice::All(), - std::optional _queryTimeout = {}, - bool _printQuery = false - ); - - void reset() override; - - void push() override; - void pop() override; - - void declareVariable(std::string const&, SortPointer const&) override; - - void addAssertion(Expression const& _expr) override; - - std::pair> check(std::vector const& _expressionsToEvaluate) override; - - std::vector unhandledQueries() override; - size_t solvers() override { return m_solvers.size(); } - - std::string dumpQuery(std::vector const& _expressionsToEvaluate); - -private: - static bool solverAnswered(CheckResult result); - - std::vector> m_solvers; - - std::vector m_assertions; -}; - -} diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index cb6b027f9..c455ddc70 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -20,7 +20,7 @@ #include -#include +#include #include #include @@ -43,7 +43,7 @@ BMC::BMC( CharStreamProvider const& _charStreamProvider ): SMTEncoder(_context, _settings, _errorReporter, _unsupportedErrorReporter, _charStreamProvider), - m_interface(std::make_unique( + m_interface(std::make_unique( _smtlib2Responses, _smtCallback, _settings.solvers, _settings.timeout, _settings.printQuery )) { @@ -1219,8 +1219,9 @@ BMC::checkSatisfiableAndGenerateModel(std::vector const& _e { if (m_settings.printQuery) { - auto portfolio = dynamic_cast(m_interface.get()); - std::string smtlibCode = portfolio->dumpQuery(_expressionsToEvaluate); + auto smtlibInterface = dynamic_cast(m_interface.get()); + solAssert(smtlibInterface, "Must use SMTLib2 solver to dump queries"); + std::string smtlibCode = smtlibInterface->dumpQuery(_expressionsToEvaluate); m_errorReporter.info( 6240_error, "BMC: Requested query:\n" + smtlibCode diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index d985e359e..656926a58 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -27,7 +27,6 @@ #include #include -#include #include #include