diff --git a/libsmtutil/CHCSmtLib2Interface.cpp b/libsmtutil/CHCSmtLib2Interface.cpp index 671ec9b51d6c..a267a843bb68 100644 --- a/libsmtutil/CHCSmtLib2Interface.cpp +++ b/libsmtutil/CHCSmtLib2Interface.cpp @@ -43,16 +43,14 @@ using namespace solidity::frontend; using namespace solidity::smtutil; CHCSmtLib2Interface::CHCSmtLib2Interface( - std::map const& _queryResponses, + std::map _queryResponses, ReadCallback::Callback _smtCallback, - SMTSolverChoice _enabledSolvers, std::optional _queryTimeout ): CHCSolverInterface(_queryTimeout), m_smtlib2(std::make_unique(_queryResponses, _smtCallback, m_queryTimeout)), m_queryResponses(std::move(_queryResponses)), - m_smtCallback(_smtCallback), - m_enabledSolvers(_enabledSolvers) + m_smtCallback(_smtCallback) { reset(); } @@ -186,9 +184,9 @@ std::string CHCSmtLib2Interface::querySolver(std::string const& _input) if (m_queryResponses.count(inputHash)) return m_queryResponses.at(inputHash); - smtAssert(m_enabledSolvers.smtlib2 || m_enabledSolvers.eld); if (m_smtCallback) { + setupSmtCallback(); auto result = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery), _input); if (result.success) return result.responseOrErrorMessage; diff --git a/libsmtutil/CHCSmtLib2Interface.h b/libsmtutil/CHCSmtLib2Interface.h index f7f656fd0b49..39131973bf7f 100644 --- a/libsmtutil/CHCSmtLib2Interface.h +++ b/libsmtutil/CHCSmtLib2Interface.h @@ -33,9 +33,8 @@ class CHCSmtLib2Interface: public CHCSolverInterface { public: explicit CHCSmtLib2Interface( - std::map const& _queryResponses = {}, + std::map _queryResponses = {}, frontend::ReadCallback::Callback _smtCallback = {}, - SMTSolverChoice _enabledSolvers = SMTSolverChoice::All(), std::optional _queryTimeout = {} ); @@ -59,7 +58,7 @@ class CHCSmtLib2Interface: public CHCSolverInterface auto const& sortNames() const { return m_smtlib2->sortNames(); } -private: +protected: std::string toSmtLibSort(SortPointer _sort); std::string toSmtLibSort(std::vector const& _sort); @@ -79,17 +78,19 @@ class CHCSmtLib2Interface: public CHCSolverInterface /// Translates CHC solver response with a model to our representation of invariants. Returns None on error. std::optional invariantsFromSolverResponse(std::string const& response) const; + /// Hook to setup external solver call + virtual void setupSmtCallback() {} + /// Used to access toSmtLibSort, SExpr, and handle variables. std::unique_ptr m_smtlib2; std::string m_accumulatedOutput; std::set m_variables; - std::map const& m_queryResponses; + std::map m_queryResponses; std::vector m_unhandledQueries; frontend::ReadCallback::Callback m_smtCallback; - SMTSolverChoice m_enabledSolvers; }; } diff --git a/libsmtutil/SMTLib2Interface.cpp b/libsmtutil/SMTLib2Interface.cpp index cfe1bc0bef2c..06ed26f2b26b 100644 --- a/libsmtutil/SMTLib2Interface.cpp +++ b/libsmtutil/SMTLib2Interface.cpp @@ -322,6 +322,7 @@ std::string SMTLib2Interface::querySolver(std::string const& _input) return m_queryResponses.at(inputHash); if (m_smtCallback) { + setupSmtCallback(); auto result = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery), _input); if (result.success) return result.responseOrErrorMessage; diff --git a/libsmtutil/SMTLib2Interface.h b/libsmtutil/SMTLib2Interface.h index fbfde664d579..d60a5bd250c5 100644 --- a/libsmtutil/SMTLib2Interface.h +++ b/libsmtutil/SMTLib2Interface.h @@ -71,7 +71,9 @@ class SMTLib2Interface: public SolverInterface std::string dumpQuery(std::vector const& _expressionsToEvaluate); -private: +protected: + virtual void setupSmtCallback() {} + void declareFunction(std::string const& _name, SortPointer const& _sort); void write(std::string _data); diff --git a/libsmtutil/SMTPortfolio.cpp b/libsmtutil/SMTPortfolio.cpp index 1435cc9d801c..196f02fdf99c 100644 --- a/libsmtutil/SMTPortfolio.cpp +++ b/libsmtutil/SMTPortfolio.cpp @@ -18,9 +18,6 @@ #include -#ifdef HAVE_Z3 -#include -#endif #include using namespace solidity; @@ -29,22 +26,12 @@ 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 + std::vector> _solvers, + std::optional _queryTimeout ): - SolverInterface(_queryTimeout) -{ - solAssert(!_printQuery || _enabledSolvers == smtutil::SMTSolverChoice::SMTLIB2(), "Only SMTLib2 solver can be enabled to print queries"); - if (_enabledSolvers.smtlib2 || _enabledSolvers.cvc5) - m_solvers.emplace_back(std::make_unique(std::move(_smtlib2Responses), std::move(_smtCallback), m_queryTimeout)); -#ifdef HAVE_Z3 - if (_enabledSolvers.z3 && Z3Interface::available()) - m_solvers.emplace_back(std::make_unique(m_queryTimeout)); -#endif -} + SolverInterface(_queryTimeout), m_solvers(std::move(_solvers)) +{} + void SMTPortfolio::reset() { diff --git a/libsmtutil/SMTPortfolio.h b/libsmtutil/SMTPortfolio.h index cdb33368e80a..5ffb37eb3286 100644 --- a/libsmtutil/SMTPortfolio.h +++ b/libsmtutil/SMTPortfolio.h @@ -42,13 +42,7 @@ class SMTPortfolio: public SolverInterface 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 - ); + SMTPortfolio(std::vector> solvers, std::optional _queryTimeout); void reset() override; diff --git a/libsolidity/CMakeLists.txt b/libsolidity/CMakeLists.txt index 3db857241f28..0b796035d313 100644 --- a/libsolidity/CMakeLists.txt +++ b/libsolidity/CMakeLists.txt @@ -109,6 +109,10 @@ set(sources formal/BMC.h formal/CHC.cpp formal/CHC.h + formal/Cvc5SMTLib2Interface.cpp + formal/Cvc5SMTLib2Interface.h + formal/EldaricaCHCSmtLib2Interface.cpp + formal/EldaricaCHCSmtLib2Interface.h formal/EncodingContext.cpp formal/EncodingContext.h formal/ExpressionFormatter.cpp diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index 0417c54e4b67..dd039626b084 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -18,9 +18,14 @@ #include +#include #include +#include #include +#ifdef HAVE_Z3 +#include +#endif #include #include @@ -35,6 +40,8 @@ using namespace solidity; using namespace solidity::util; using namespace solidity::langutil; using namespace solidity::frontend; +using namespace solidity::frontend::smt; +using namespace solidity::smtutil; BMC::BMC( smt::EncodingContext& _context, @@ -45,12 +52,19 @@ BMC::BMC( ModelCheckerSettings _settings, CharStreamProvider const& _charStreamProvider ): - SMTEncoder(_context, _settings, _errorReporter, _unsupportedErrorReporter, _charStreamProvider), - m_interface(std::make_unique( - _smtlib2Responses, _smtCallback, _settings.solvers, _settings.timeout, _settings.printQuery - )) + SMTEncoder(_context, _settings, _errorReporter, _unsupportedErrorReporter, _charStreamProvider) { - solAssert(!_settings.printQuery || _settings.solvers == smtutil::SMTSolverChoice::SMTLIB2(), "Only SMTLib2 solver can be enabled to print queries"); + solAssert(!_settings.printQuery || _settings.solvers == SMTSolverChoice::SMTLIB2(), "Only SMTLib2 solver can be enabled to print queries"); + std::vector> solvers; + if (_settings.solvers.smtlib2) + solvers.emplace_back(std::make_unique(_smtlib2Responses, _smtCallback, _settings.timeout)); + if (_settings.solvers.cvc5) + solvers.emplace_back(std::make_unique(_smtCallback, _settings.timeout)); +#ifdef HAVE_Z3 + if (_settings.solvers.z3 && Z3Interface::available()) + solvers.emplace_back(std::make_unique(_settings.timeout)); +#endif + m_interface = std::make_unique(std::move(solvers), _settings.timeout); #if defined (HAVE_Z3) if (m_settings.solvers.z3) if (!_smtlib2Responses.empty()) diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index c520d13f6b0f..66ebd47edb98 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -25,6 +25,7 @@ #endif #include +#include #include #include #include @@ -1289,15 +1290,23 @@ void CHC::resetSourceAnalysis() solAssert(false); #endif } - if (!m_settings.solvers.z3) + else { solAssert(m_settings.solvers.smtlib2 || m_settings.solvers.eld); - if (!m_interface) - m_interface = std::make_unique(m_smtlib2Responses, m_smtCallback, m_settings.solvers, m_settings.timeout); + { + if (m_settings.solvers.eld) + m_interface = std::make_unique( + m_smtCallback, + m_settings.timeout, + m_settings.invariants != ModelCheckerInvariants::None() + ); + else + m_interface = std::make_unique(m_smtlib2Responses, m_smtCallback, m_settings.timeout); + } auto smtlib2Interface = dynamic_cast(m_interface.get()); - solAssert(smtlib2Interface, ""); + solAssert(smtlib2Interface); smtlib2Interface->reset(); m_context.setSolver(smtlib2Interface->smtlib2Interface()); } diff --git a/libsolidity/formal/Cvc5SMTLib2Interface.cpp b/libsolidity/formal/Cvc5SMTLib2Interface.cpp new file mode 100644 index 000000000000..8a399c1356df --- /dev/null +++ b/libsolidity/formal/Cvc5SMTLib2Interface.cpp @@ -0,0 +1,35 @@ +/* + 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::frontend::smt; + +Cvc5SMTLib2Interface::Cvc5SMTLib2Interface( + frontend::ReadCallback::Callback _smtCallback, + std::optional _queryTimeout +): SMTLib2Interface({}, std::move(_smtCallback), _queryTimeout) +{ +} + +void Cvc5SMTLib2Interface::setupSmtCallback() { + if (auto* universalCallback = m_smtCallback.target()) + universalCallback->smtCommand().setCvc5(m_queryTimeout); +} diff --git a/libsolidity/formal/Cvc5SMTLib2Interface.h b/libsolidity/formal/Cvc5SMTLib2Interface.h new file mode 100644 index 000000000000..64bc364da1c8 --- /dev/null +++ b/libsolidity/formal/Cvc5SMTLib2Interface.h @@ -0,0 +1,37 @@ +/* + 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 + +namespace solidity::frontend::smt +{ + +class Cvc5SMTLib2Interface: public smtutil::SMTLib2Interface +{ +public: + explicit Cvc5SMTLib2Interface( + frontend::ReadCallback::Callback _smtCallback = {}, + std::optional _queryTimeout = {} + ); +private: + void setupSmtCallback() override; +}; + +} diff --git a/libsolidity/formal/EldaricaCHCSmtLib2Interface.cpp b/libsolidity/formal/EldaricaCHCSmtLib2Interface.cpp new file mode 100644 index 000000000000..4fa94539d8b8 --- /dev/null +++ b/libsolidity/formal/EldaricaCHCSmtLib2Interface.cpp @@ -0,0 +1,37 @@ +/* + 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::frontend::smt; + +EldaricaCHCSmtLib2Interface::EldaricaCHCSmtLib2Interface( + frontend::ReadCallback::Callback _smtCallback, + std::optional _queryTimeout, + bool computeInvariants +): CHCSmtLib2Interface({}, std::move(_smtCallback), _queryTimeout), m_computeInvariants(computeInvariants) +{ +} + +void EldaricaCHCSmtLib2Interface::setupSmtCallback() +{ + if (auto* universalCallback = m_smtCallback.target()) + universalCallback->smtCommand().setEldarica(m_queryTimeout, m_computeInvariants); +} diff --git a/libsolidity/formal/EldaricaCHCSmtLib2Interface.h b/libsolidity/formal/EldaricaCHCSmtLib2Interface.h new file mode 100644 index 000000000000..2c83b194ca7d --- /dev/null +++ b/libsolidity/formal/EldaricaCHCSmtLib2Interface.h @@ -0,0 +1,41 @@ +/* + 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 + +namespace solidity::frontend::smt +{ + +class EldaricaCHCSmtLib2Interface: public smtutil::CHCSmtLib2Interface +{ +public: + EldaricaCHCSmtLib2Interface( + frontend::ReadCallback::Callback _smtCallback, + std::optional _queryTimeout, + bool computeInvariants + ); + +private: + void setupSmtCallback() override; + + bool m_computeInvariants; +}; + +} diff --git a/libsolidity/interface/CompilerStack.cpp b/libsolidity/interface/CompilerStack.cpp index d5fe44ca167a..f9f1f0e64206 100644 --- a/libsolidity/interface/CompilerStack.cpp +++ b/libsolidity/interface/CompilerStack.cpp @@ -653,16 +653,7 @@ bool CompilerStack::analyzeLegacy(bool _noErrorsSoFar) // m_modelCheckerSettings is spread to engines and solver interfaces, // so we need to check whether the enabled ones are available before building the classes. if (m_modelCheckerSettings.engine.any()) - { m_modelCheckerSettings.solvers = ModelChecker::checkRequestedSolvers(m_modelCheckerSettings.solvers, m_errorReporter); - if (auto* universalCallback = m_readFile.target()) - { - if (m_modelCheckerSettings.solvers.eld) - universalCallback->smtCommand().setEldarica(m_modelCheckerSettings.timeout, m_modelCheckerSettings.invariants != ModelCheckerInvariants::None()); - if (m_modelCheckerSettings.solvers.cvc5) - universalCallback->smtCommand().setCvc5(m_modelCheckerSettings.timeout); - } - } ModelChecker modelChecker(m_errorReporter, *this, m_smtlib2Responses, m_modelCheckerSettings, m_readFile); modelChecker.checkRequestedSourcesAndContracts(allSources); diff --git a/test/cmdlineTests/model_checker_solvers_cvc5_eld/args b/test/cmdlineTests/model_checker_solvers_cvc5_eld/args new file mode 100644 index 000000000000..fb0c074ab2c4 --- /dev/null +++ b/test/cmdlineTests/model_checker_solvers_cvc5_eld/args @@ -0,0 +1 @@ +--model-checker-engine all --model-checker-solvers cvc5,eld diff --git a/test/cmdlineTests/model_checker_solvers_cvc5_eld/err b/test/cmdlineTests/model_checker_solvers_cvc5_eld/err new file mode 100644 index 000000000000..81a9f3a56342 --- /dev/null +++ b/test/cmdlineTests/model_checker_solvers_cvc5_eld/err @@ -0,0 +1,8 @@ +Info: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. + +Warning: BMC: Condition is always false. + --> model_checker_solvers_cvc5_eld/input.sol:6:7: + | +6 | if (y == 0) + | ^^^^^^ +Note: Callstack: diff --git a/test/cmdlineTests/model_checker_solvers_cvc5_eld/input.sol b/test/cmdlineTests/model_checker_solvers_cvc5_eld/input.sol new file mode 100644 index 000000000000..eae2d9b48594 --- /dev/null +++ b/test/cmdlineTests/model_checker_solvers_cvc5_eld/input.sol @@ -0,0 +1,10 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; +contract test { + function f() public pure { + uint y = 1; + if (y == 0) + revert(); + assert(y > 0); + } +}