From 6c8ecfa82c1cd6dcac0f1f951525451874205dad Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Wed, 19 May 2021 17:35:19 +0200 Subject: [PATCH] Add option to choose solver --- .circleci/config.yml | 4 +- docs/smtchecker.rst | 33 +++++ libsmtutil/SMTPortfolio.cpp | 12 +- libsmtutil/SolverInterface.h | 70 ++++++++- libsolidity/formal/BMC.cpp | 53 +++++-- libsolidity/formal/BMC.h | 1 - libsolidity/formal/CHC.cpp | 54 ++++--- libsolidity/formal/CHC.h | 4 - libsolidity/formal/ModelChecker.cpp | 11 +- libsolidity/formal/ModelChecker.h | 3 +- libsolidity/formal/ModelCheckerSettings.h | 2 + libsolidity/interface/CompilerStack.cpp | 11 +- libsolidity/interface/CompilerStack.h | 3 - libsolidity/interface/StandardCompiler.cpp | 20 ++- scripts/error_codes.py | 3 +- solc/CommandLineParser.cpp | 19 +++ .../model_checker_solvers_all/args | 1 + .../model_checker_solvers_all/err | 12 ++ .../model_checker_solvers_all/input.sol | 7 + .../model_checker_solvers_all_implicit/args | 1 + .../model_checker_solvers_all_implicit/err | 12 ++ .../input.sol | 7 + .../model_checker_solvers_smtlib2/args | 1 + .../model_checker_solvers_smtlib2/err | 3 + .../model_checker_solvers_smtlib2/input.sol | 7 + .../model_checker_solvers_wrong/args | 1 + .../model_checker_solvers_wrong/err | 1 + .../model_checker_solvers_wrong/exit | 1 + .../model_checker_solvers_wrong/input.sol | 7 + .../model_checker_solvers_wrong2/args | 1 + .../model_checker_solvers_wrong2/err | 1 + .../model_checker_solvers_wrong2/exit | 1 + .../model_checker_solvers_wrong2/input.sol | 7 + .../model_checker_solvers_z3/args | 1 + .../cmdlineTests/model_checker_solvers_z3/err | 12 ++ .../model_checker_solvers_z3/input.sol | 7 + .../model_checker_solvers_z3_smtlib2/args | 1 + .../model_checker_solvers_z3_smtlib2/err | 12 ++ .../input.sol | 7 + .../input.json | 17 +++ .../output.json | 21 +++ .../input.json | 18 +++ .../output.json | 5 + .../input.json | 18 +++ .../output.json | 138 ++++++++++++++++++ .../input.json | 18 +++ .../output.json | 21 +++ .../input.json | 18 +++ .../output.json | 21 +++ test/externalTests/solc-js/solc-js.sh | 6 +- test/libsolidity/SMTCheckerTest.cpp | 19 +-- test/solc/CommandLineParser.cpp | 6 + test/tools/fuzzer_common.cpp | 2 +- 53 files changed, 650 insertions(+), 92 deletions(-) create mode 100644 test/cmdlineTests/model_checker_solvers_all/args create mode 100644 test/cmdlineTests/model_checker_solvers_all/err create mode 100644 test/cmdlineTests/model_checker_solvers_all/input.sol create mode 100644 test/cmdlineTests/model_checker_solvers_all_implicit/args create mode 100644 test/cmdlineTests/model_checker_solvers_all_implicit/err create mode 100644 test/cmdlineTests/model_checker_solvers_all_implicit/input.sol create mode 100644 test/cmdlineTests/model_checker_solvers_smtlib2/args create mode 100644 test/cmdlineTests/model_checker_solvers_smtlib2/err create mode 100644 test/cmdlineTests/model_checker_solvers_smtlib2/input.sol create mode 100644 test/cmdlineTests/model_checker_solvers_wrong/args create mode 100644 test/cmdlineTests/model_checker_solvers_wrong/err create mode 100644 test/cmdlineTests/model_checker_solvers_wrong/exit create mode 100644 test/cmdlineTests/model_checker_solvers_wrong/input.sol create mode 100644 test/cmdlineTests/model_checker_solvers_wrong2/args create mode 100644 test/cmdlineTests/model_checker_solvers_wrong2/err create mode 100644 test/cmdlineTests/model_checker_solvers_wrong2/exit create mode 100644 test/cmdlineTests/model_checker_solvers_wrong2/input.sol create mode 100644 test/cmdlineTests/model_checker_solvers_z3/args create mode 100644 test/cmdlineTests/model_checker_solvers_z3/err create mode 100644 test/cmdlineTests/model_checker_solvers_z3/input.sol create mode 100644 test/cmdlineTests/model_checker_solvers_z3_smtlib2/args create mode 100644 test/cmdlineTests/model_checker_solvers_z3_smtlib2/err create mode 100644 test/cmdlineTests/model_checker_solvers_z3_smtlib2/input.sol create mode 100644 test/cmdlineTests/standard_model_checker_solvers_all/input.json create mode 100644 test/cmdlineTests/standard_model_checker_solvers_all/output.json create mode 100644 test/cmdlineTests/standard_model_checker_solvers_none/input.json create mode 100644 test/cmdlineTests/standard_model_checker_solvers_none/output.json create mode 100644 test/cmdlineTests/standard_model_checker_solvers_smtlib2/input.json create mode 100644 test/cmdlineTests/standard_model_checker_solvers_smtlib2/output.json create mode 100644 test/cmdlineTests/standard_model_checker_solvers_z3/input.json create mode 100644 test/cmdlineTests/standard_model_checker_solvers_z3/output.json create mode 100644 test/cmdlineTests/standard_model_checker_solvers_z3_smtlib2/input.json create mode 100644 test/cmdlineTests/standard_model_checker_solvers_z3_smtlib2/output.json diff --git a/.circleci/config.yml b/.circleci/config.yml index 93e9f93bd..11198a089 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -811,7 +811,7 @@ jobs: t_ems_solcjs: docker: - - image: buildpack-deps:latest + - image: << pipeline.parameters.ubuntu-2004-docker-image >> environment: TERM: xterm steps: @@ -822,7 +822,7 @@ jobs: name: Install test dependencies command: | apt-get update - apt-get install -qqy --no-install-recommends nodejs npm cvc4 + apt-get install -qqy --no-install-recommends nodejs npm - run: name: Test solcjs no_output_timeout: 30m diff --git a/docs/smtchecker.rst b/docs/smtchecker.rst index a4580ce4d..f3a9e2e81 100644 --- a/docs/smtchecker.rst +++ b/docs/smtchecker.rst @@ -558,6 +558,39 @@ calls assume the called code is unknown and can do anything. The CHC engine is much more powerful than BMC in terms of what it can prove, and might require more computing resources. +SMT and Horn solvers +==================== + +The two engines detailed above use automated theorem provers as their logical +backends. BMC uses an SMT solver, whereas CHC uses a Horn solver. Often the +same tool can act as both, as seen in `z3 `_, +which is primarily an SMT solver and makes `Spacer +`_ available as a Horn solver, and `Eldarica +`_ which does both. + +The user can choose which solvers should be used, if available, via the CLI +option ``--model-checker-solvers {all,cvc4,smtlib2,z3}`` or the JSON option +``settings.modelChecker.solvers=[smtlib2,z3]``, where: + +- ``cvc4`` is only available if the ``solc`` binary is compiled with it. Only BMC uses ``cvc4``. +- ``smtlib2`` outputs SMT/Horn queries in the `smtlib2 `_ format. + These can be used together with the compiler's `callback mechanism `_ so that + any solver binary from the system can be employed to synchronously return the results of the queries to the compiler. + This is currently the only way to use Eldarica, for example, since it does not have a C++ API. + This can be used by both BMC and CHC depending on which solvers are called. +- ``z3`` is available + + - if ``solc`` is compiled with it; + - if a dynamic ``z3`` library of version 4.8.x is installed in a Linux system (from Solidity 0.7.6); + - statically in ``soljson.js`` (from Solidity 0.6.9), that is, the Javascript binary of the compiler. + +Since both BMC and CHC use ``z3``, and ``z3`` is available in a greater variety +of environments, including in the browser, most users will almost never need to be +concerned about this option. More advanced users might apply this option to try +alternative solvers on more complex problems. + +Please note that certain combinations of chosen engine and solver will lead to +the SMTChecker doing nothing, for example choosing CHC and ``cvc4``. ******************************* Abstraction and False Positives diff --git a/libsmtutil/SMTPortfolio.cpp b/libsmtutil/SMTPortfolio.cpp index de00c1f79..aec9b0a1c 100644 --- a/libsmtutil/SMTPortfolio.cpp +++ b/libsmtutil/SMTPortfolio.cpp @@ -40,7 +40,8 @@ SMTPortfolio::SMTPortfolio( ): SolverInterface(_queryTimeout) { - m_solvers.emplace_back(make_unique(move(_smtlib2Responses), move(_smtCallback), m_queryTimeout)); + if (_enabledSolvers.smtlib2) + m_solvers.emplace_back(make_unique(move(_smtlib2Responses), move(_smtCallback), m_queryTimeout)); #ifdef HAVE_Z3 if (_enabledSolvers.z3 && Z3Interface::available()) m_solvers.emplace_back(make_unique(m_queryTimeout)); @@ -143,10 +144,11 @@ pair> SMTPortfolio::check(vector const& vector SMTPortfolio::unhandledQueries() { // This code assumes that the constructor guarantees that - // SmtLib2Interface is in position 0. - smtAssert(!m_solvers.empty(), ""); - smtAssert(dynamic_cast(m_solvers.front().get()), ""); - return m_solvers.front()->unhandledQueries(); + // 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) diff --git a/libsmtutil/SolverInterface.h b/libsmtutil/SolverInterface.h index 6eb6982fb..21648c245 100644 --- a/libsmtutil/SolverInterface.h +++ b/libsmtutil/SolverInterface.h @@ -23,10 +23,13 @@ #include +#include + #include #include #include #include +#include #include #include @@ -36,16 +39,71 @@ namespace solidity::smtutil struct SMTSolverChoice { bool cvc4 = false; + bool smtlib2 = false; bool z3 = false; - static constexpr SMTSolverChoice All() { return {true, true}; } - static constexpr SMTSolverChoice CVC4() { return {true, false}; } - static constexpr SMTSolverChoice Z3() { return {false, true}; } - static constexpr SMTSolverChoice None() { return {false, false}; } + static constexpr SMTSolverChoice All() { return {true, true, true}; } + static constexpr SMTSolverChoice CVC4() { return {true, false, false}; } + static constexpr SMTSolverChoice SMTLIB2() { return {false, true, false}; } + static constexpr SMTSolverChoice Z3() { return {false, false, true}; } + static constexpr SMTSolverChoice None() { return {false, false, false}; } + + static std::optional fromString(std::string const& _solvers) + { + SMTSolverChoice solvers; + if (_solvers == "all") + { + smtAssert(solvers.setSolver("cvc4"), ""); + smtAssert(solvers.setSolver("smtlib2"), ""); + smtAssert(solvers.setSolver("z3"), ""); + } + else + for (auto&& s: _solvers | ranges::views::split(',') | ranges::to>()) + if (!solvers.setSolver(s)) + return {}; + + return solvers; + } + + SMTSolverChoice& operator&(SMTSolverChoice const& _other) + { + cvc4 &= _other.cvc4; + smtlib2 &= _other.smtlib2; + z3 &= _other.z3; + return *this; + } + + SMTSolverChoice& operator&=(SMTSolverChoice const& _other) + { + return *this & _other; + } + + bool operator!=(SMTSolverChoice const& _other) const noexcept { return !(*this == _other); } + + bool operator==(SMTSolverChoice const& _other) const noexcept + { + return cvc4 == _other.cvc4 && + smtlib2 == _other.smtlib2 && + z3 == _other.z3; + } + + bool setSolver(std::string const& _solver) + { + static std::set const solvers{"cvc4", "smtlib2", "z3"}; + if (!solvers.count(_solver)) + return false; + if (_solver == "cvc4") + cvc4 = true; + else if (_solver == "smtlib2") + smtlib2 = true; + else if (_solver == "z3") + z3 = true; + return true; + } bool none() { return !some(); } - bool some() { return cvc4 || z3; } - bool all() { return cvc4 && z3; } + bool some() { return cvc4 || smtlib2 || z3; } + bool all() { return cvc4 && smtlib2 && z3; } }; enum class CheckResult diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index e86906ff9..eee9988ed 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -40,16 +40,15 @@ BMC::BMC( ErrorReporter& _errorReporter, map const& _smtlib2Responses, ReadCallback::Callback const& _smtCallback, - smtutil::SMTSolverChoice _enabledSolvers, ModelCheckerSettings const& _settings, CharStreamProvider const& _charStreamProvider ): SMTEncoder(_context, _settings, _charStreamProvider), - m_interface(make_unique(_smtlib2Responses, _smtCallback, _enabledSolvers, _settings.timeout)), + m_interface(make_unique(_smtlib2Responses, _smtCallback, _settings.solvers, _settings.timeout)), m_outerErrorReporter(_errorReporter) { #if defined (HAVE_Z3) || defined (HAVE_CVC4) - if (_enabledSolvers.some()) + if (m_settings.solvers.cvc4 || m_settings.solvers.z3) if (!_smtlib2Responses.empty()) m_errorReporter.warning( 5622_error, @@ -63,6 +62,20 @@ BMC::BMC( void BMC::analyze(SourceUnit const& _source, map> _solvedTargets) { + if (m_interface->solvers() == 0) + { + if (!m_noSolverWarning) + { + m_noSolverWarning = true; + m_outerErrorReporter.warning( + 7710_error, + SourceLocation(), + "BMC analysis was not possible since no SMT solver was found and enabled." + ); + } + return; + } + if (SMTEncoder::analyze(_source)) { m_solvedTargets = move(_solvedTargets); @@ -75,11 +88,14 @@ void BMC::analyze(SourceUnit const& _source, mapsolvers() > 0, ""); // If this check is true, Z3 and CVC4 are not available // and the query answers were not provided, since SMTPortfolio - // guarantees that SmtLib2Interface is the first solver. - if (!m_interface->unhandledQueries().empty() && m_interface->solvers() == 1) + // guarantees that SmtLib2Interface is the first solver, if enabled. + if ( + !m_interface->unhandledQueries().empty() && + m_interface->solvers() == 1 && + m_settings.solvers.smtlib2 + ) { if (!m_noSolverWarning) { @@ -87,7 +103,8 @@ void BMC::analyze(SourceUnit const& _source, map sortedModel; - for (size_t i = 0; i < values.size(); ++i) - if (expressionsToEvaluate.at(i).name != values.at(i)) - sortedModel[expressionNames.at(i)] = values.at(i); - for (auto const& eval: sortedModel) - modelMessage << " " << eval.first << " = " << eval.second << "\n"; + std::ostringstream modelMessage; + // Sometimes models have complex smtlib2 expressions that SMTLib2Interface fails to parse. + if (values.size() == expressionNames.size()) + { + modelMessage << "Counterexample:\n"; + map sortedModel; + for (size_t i = 0; i < values.size(); ++i) + if (expressionsToEvaluate.at(i).name != values.at(i)) + sortedModel[expressionNames.at(i)] = values.at(i); + + for (auto const& eval: sortedModel) + modelMessage << " " << eval.first << " = " << eval.second << "\n"; + } m_errorReporter.warning( _errorHappens, diff --git a/libsolidity/formal/BMC.h b/libsolidity/formal/BMC.h index fae2ecf45..c1b89347c 100644 --- a/libsolidity/formal/BMC.h +++ b/libsolidity/formal/BMC.h @@ -62,7 +62,6 @@ public: langutil::ErrorReporter& _errorReporter, std::map const& _smtlib2Responses, ReadCallback::Callback const& _smtCallback, - smtutil::SMTSolverChoice _enabledSolvers, ModelCheckerSettings const& _settings, langutil::CharStreamProvider const& _charStreamProvider ); diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 10e066f60..00657922d 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -56,26 +56,38 @@ CHC::CHC( ErrorReporter& _errorReporter, [[maybe_unused]] map const& _smtlib2Responses, [[maybe_unused]] ReadCallback::Callback const& _smtCallback, - SMTSolverChoice _enabledSolvers, ModelCheckerSettings const& _settings, CharStreamProvider const& _charStreamProvider ): SMTEncoder(_context, _settings, _charStreamProvider), - m_outerErrorReporter(_errorReporter), - m_enabledSolvers(_enabledSolvers) + m_outerErrorReporter(_errorReporter) { - bool usesZ3 = _enabledSolvers.z3; + bool usesZ3 = m_settings.solvers.z3; #ifdef HAVE_Z3 usesZ3 = usesZ3 && Z3Interface::available(); #else usesZ3 = false; #endif - if (!usesZ3) + if (!usesZ3 && m_settings.solvers.smtlib2) m_interface = make_unique(_smtlib2Responses, _smtCallback, m_settings.timeout); } void CHC::analyze(SourceUnit const& _source) { + if (!m_settings.solvers.z3 && !m_settings.solvers.smtlib2) + { + if (!m_noSolverWarning) + { + m_noSolverWarning = true; + m_outerErrorReporter.warning( + 7649_error, + SourceLocation(), + "CHC analysis was not possible since no Horn solver was enabled." + ); + } + return; + } + if (SMTEncoder::analyze(_source)) { resetSourceAnalysis(); @@ -92,6 +104,8 @@ void CHC::analyze(SourceUnit const& _source) } bool ranSolver = true; + // If ranSolver is true here it's because an SMT solver callback was + // actually given and the queries were solved. if (auto const* smtLibInterface = dynamic_cast(m_interface.get())) ranSolver = smtLibInterface->unhandledQueries().empty(); if (!ranSolver && !m_noSolverWarning) @@ -103,7 +117,8 @@ void CHC::analyze(SourceUnit const& _source) #ifdef HAVE_Z3_DLOPEN "CHC analysis was not possible since libz3.so." + to_string(Z3_MAJOR_VERSION) + "." + to_string(Z3_MINOR_VERSION) + " was not found." #else - "CHC analysis was not possible since no integrated z3 SMT solver was found." + "CHC analysis was not possible. No Horn solver was available." + " None of the installed solvers was enabled." #endif ); } @@ -933,7 +948,7 @@ void CHC::resetSourceAnalysis() bool usesZ3 = false; #ifdef HAVE_Z3 - usesZ3 = m_enabledSolvers.z3 && Z3Interface::available(); + usesZ3 = m_settings.solvers.z3 && Z3Interface::available(); if (usesZ3) { /// z3::fixedpoint does not have a reset mechanism, so we need to create another. @@ -1427,20 +1442,23 @@ pair CHC::query(smtutil::Expression c case CheckResult::SATISFIABLE: { #ifdef HAVE_Z3 - // Even though the problem is SAT, Spacer's pre processing makes counterexamples incomplete. - // We now disable those optimizations and check whether we can still solve the problem. - auto* spacer = dynamic_cast(m_interface.get()); - solAssert(spacer, ""); - spacer->setSpacerOptions(false); + if (m_settings.solvers.z3) + { + // Even though the problem is SAT, Spacer's pre processing makes counterexamples incomplete. + // We now disable those optimizations and check whether we can still solve the problem. + auto* spacer = dynamic_cast(m_interface.get()); + solAssert(spacer, ""); + spacer->setSpacerOptions(false); - CheckResult resultNoOpt; - CHCSolverInterface::CexGraph cexNoOpt; - tie(resultNoOpt, cexNoOpt) = m_interface->query(_query); + CheckResult resultNoOpt; + CHCSolverInterface::CexGraph cexNoOpt; + tie(resultNoOpt, cexNoOpt) = m_interface->query(_query); - if (resultNoOpt == CheckResult::SATISFIABLE) - cex = move(cexNoOpt); + if (resultNoOpt == CheckResult::SATISFIABLE) + cex = move(cexNoOpt); - spacer->setSpacerOptions(true); + spacer->setSpacerOptions(true); + } #endif break; } diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index 6886c2c7f..3aab9268d 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -56,7 +56,6 @@ public: langutil::ErrorReporter& _errorReporter, std::map const& _smtlib2Responses, ReadCallback::Callback const& _smtCallback, - smtutil::SMTSolverChoice _enabledSolvers, ModelCheckerSettings const& _settings, langutil::CharStreamProvider const& _charStreamProvider ); @@ -393,9 +392,6 @@ private: /// ErrorReporter that comes from CompilerStack. langutil::ErrorReporter& m_outerErrorReporter; - - /// SMT solvers that are chosen at runtime. - smtutil::SMTSolverChoice m_enabledSolvers; }; } diff --git a/libsolidity/formal/ModelChecker.cpp b/libsolidity/formal/ModelChecker.cpp index e17c7f4df..1aac80248 100644 --- a/libsolidity/formal/ModelChecker.cpp +++ b/libsolidity/formal/ModelChecker.cpp @@ -35,14 +35,13 @@ ModelChecker::ModelChecker( langutil::CharStreamProvider const& _charStreamProvider, map const& _smtlib2Responses, ModelCheckerSettings _settings, - ReadCallback::Callback const& _smtCallback, - smtutil::SMTSolverChoice _enabledSolvers + ReadCallback::Callback const& _smtCallback ): m_errorReporter(_errorReporter), - m_settings(_settings), + m_settings(move(_settings)), m_context(), - m_bmc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers, m_settings, _charStreamProvider), - m_chc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers, m_settings, _charStreamProvider) + m_bmc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, m_settings, _charStreamProvider), + m_chc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, m_settings, _charStreamProvider) { } @@ -135,7 +134,7 @@ vector ModelChecker::unhandledQueries() solidity::smtutil::SMTSolverChoice ModelChecker::availableSolvers() { - smtutil::SMTSolverChoice available = smtutil::SMTSolverChoice::None(); + smtutil::SMTSolverChoice available = smtutil::SMTSolverChoice::SMTLIB2(); #ifdef HAVE_Z3 available.z3 = solidity::smtutil::Z3Interface::available(); #endif diff --git a/libsolidity/formal/ModelChecker.h b/libsolidity/formal/ModelChecker.h index 0bf2b4ffc..8156e39e7 100644 --- a/libsolidity/formal/ModelChecker.h +++ b/libsolidity/formal/ModelChecker.h @@ -52,8 +52,7 @@ public: langutil::CharStreamProvider const& _charStreamProvider, std::map const& _smtlib2Responses, ModelCheckerSettings _settings = ModelCheckerSettings{}, - ReadCallback::Callback const& _smtCallback = ReadCallback::Callback(), - smtutil::SMTSolverChoice _enabledSolvers = smtutil::SMTSolverChoice::All() + ReadCallback::Callback const& _smtCallback = ReadCallback::Callback() ); // TODO This should be removed for 0.9.0. diff --git a/libsolidity/formal/ModelCheckerSettings.h b/libsolidity/formal/ModelCheckerSettings.h index cfcd31d2c..edd8f0800 100644 --- a/libsolidity/formal/ModelCheckerSettings.h +++ b/libsolidity/formal/ModelCheckerSettings.h @@ -113,6 +113,7 @@ struct ModelCheckerSettings { ModelCheckerContracts contracts = ModelCheckerContracts::Default(); ModelCheckerEngine engine = ModelCheckerEngine::None(); + smtutil::SMTSolverChoice solvers = smtutil::SMTSolverChoice::All(); ModelCheckerTargets targets = ModelCheckerTargets::Default(); std::optional timeout; @@ -122,6 +123,7 @@ struct ModelCheckerSettings return contracts == _other.contracts && engine == _other.engine && + solvers == _other.solvers && targets == _other.targets && timeout == _other.timeout; } diff --git a/libsolidity/interface/CompilerStack.cpp b/libsolidity/interface/CompilerStack.cpp index 93ddd4122..f32b47d2a 100644 --- a/libsolidity/interface/CompilerStack.cpp +++ b/libsolidity/interface/CompilerStack.cpp @@ -95,7 +95,6 @@ static int g_compilerStackCounts = 0; CompilerStack::CompilerStack(ReadCallback::Callback _readFile): m_readFile{std::move(_readFile)}, - m_enabledSMTSolvers{smtutil::SMTSolverChoice::All()}, m_errorReporter{m_errorList} { // Because TypeProvider is currently a singleton API, we must ensure that @@ -228,13 +227,6 @@ void CompilerStack::setModelCheckerSettings(ModelCheckerSettings _settings) m_modelCheckerSettings = _settings; } -void CompilerStack::setSMTSolverChoice(smtutil::SMTSolverChoice _enabledSMTSolvers) -{ - if (m_stackState >= ParsedAndImported) - BOOST_THROW_EXCEPTION(CompilerError() << errinfo_comment("Must set enabled SMT solvers before parsing.")); - m_enabledSMTSolvers = _enabledSMTSolvers; -} - void CompilerStack::setLibraries(std::map const& _libraries) { if (m_stackState >= ParsedAndImported) @@ -299,7 +291,6 @@ void CompilerStack::reset(bool _keepSettings) m_viaIR = false; m_evmVersion = langutil::EVMVersion(); m_modelCheckerSettings = ModelCheckerSettings{}; - m_enabledSMTSolvers = smtutil::SMTSolverChoice::All(); m_generateIR = false; m_generateEwasm = false; m_revertStrings = RevertStrings::Default; @@ -555,7 +546,7 @@ bool CompilerStack::analyze() if (noErrors) { - ModelChecker modelChecker(m_errorReporter, *this, m_smtlib2Responses, m_modelCheckerSettings, m_readFile, m_enabledSMTSolvers); + ModelChecker modelChecker(m_errorReporter, *this, m_smtlib2Responses, m_modelCheckerSettings, m_readFile); auto allSources = applyMap(m_sourceOrder, [](Source const* _source) { return _source->ast; }); modelChecker.enableAllEnginesIfPragmaPresent(allSources); modelChecker.checkRequestedSourcesAndContracts(allSources); diff --git a/libsolidity/interface/CompilerStack.h b/libsolidity/interface/CompilerStack.h index 77b2fe4de..efdae0c36 100644 --- a/libsolidity/interface/CompilerStack.h +++ b/libsolidity/interface/CompilerStack.h @@ -176,8 +176,6 @@ public: /// Set model checker settings. void setModelCheckerSettings(ModelCheckerSettings _settings); - /// Set which SMT solvers should be enabled. - void setSMTSolverChoice(smtutil::SMTSolverChoice _enabledSolvers); /// Sets the requested contract names by source. /// If empty, no filtering is performed and every contract @@ -480,7 +478,6 @@ private: bool m_viaIR = false; langutil::EVMVersion m_evmVersion; ModelCheckerSettings m_modelCheckerSettings; - smtutil::SMTSolverChoice m_enabledSMTSolvers; std::map> m_requestedContractNames; bool m_generateEvmBytecode = true; bool m_generateIR = false; diff --git a/libsolidity/interface/StandardCompiler.cpp b/libsolidity/interface/StandardCompiler.cpp index b27e7d08d..70ed10d27 100644 --- a/libsolidity/interface/StandardCompiler.cpp +++ b/libsolidity/interface/StandardCompiler.cpp @@ -442,7 +442,7 @@ std::optional checkSettingsKeys(Json::Value const& _input) std::optional checkModelCheckerSettingsKeys(Json::Value const& _input) { - static set keys{"contracts", "engine", "targets", "timeout"}; + static set keys{"contracts", "engine", "solvers", "targets", "timeout"}; return checkKeys(_input, keys, "modelChecker"); } @@ -951,6 +951,24 @@ std::variant StandardCompiler: ret.modelCheckerSettings.engine = *engine; } + if (modelCheckerSettings.isMember("solvers")) + { + auto const& solversArray = modelCheckerSettings["solvers"]; + if (!solversArray.isArray()) + return formatFatalError("JSONError", "settings.modelChecker.solvers must be an array."); + + smtutil::SMTSolverChoice solvers; + for (auto const& s: solversArray) + { + if (!s.isString()) + return formatFatalError("JSONError", "Every target in settings.modelChecker.solvers must be a string."); + if (!solvers.setSolver(s.asString())) + return formatFatalError("JSONError", "Invalid model checker solvers requested."); + } + + ret.modelCheckerSettings.solvers = solvers; + } + if (modelCheckerSettings.isMember("targets")) { auto const& targetsArray = modelCheckerSettings["targets"]; diff --git a/scripts/error_codes.py b/scripts/error_codes.py index ffb95b889..b5c7887a1 100755 --- a/scripts/error_codes.py +++ b/scripts/error_codes.py @@ -227,7 +227,8 @@ def examine_id_coverage(top_dir, source_id_to_file_names, new_ids_only=False): "1988", "2066", "3356", "3893", "3996", "4010", "4802", "5272", "5622", "7128", "7400", - "7589", "7593", "8065", "8084", "8140", + "7589", "7593", "7649", "7710", + "8065", "8084", "8140", "8312", "8592", "9134", "9609", } diff --git a/solc/CommandLineParser.cpp b/solc/CommandLineParser.cpp index ed2f2c9b3..5a1daed1e 100644 --- a/solc/CommandLineParser.cpp +++ b/solc/CommandLineParser.cpp @@ -87,6 +87,7 @@ static string const g_strMetadataHash = "metadata-hash"; static string const g_strMetadataLiteral = "metadata-literal"; static string const g_strModelCheckerContracts = "model-checker-contracts"; static string const g_strModelCheckerEngine = "model-checker-engine"; +static string const g_strModelCheckerSolvers = "model-checker-solvers"; static string const g_strModelCheckerTargets = "model-checker-targets"; static string const g_strModelCheckerTimeout = "model-checker-timeout"; static string const g_strNatspecDev = "devdoc"; @@ -723,6 +724,11 @@ General Information)").c_str(), po::value()->value_name("all,bmc,chc,none")->default_value("none"), "Select model checker engine." ) + ( + g_strModelCheckerSolvers.c_str(), + po::value()->value_name("all,cvc4,z3,smtlib2")->default_value("all"), + "Select model checker solvers." + ) ( g_strModelCheckerTargets.c_str(), po::value()->value_name("default,constantCondition,underflow,overflow,divByZero,balance,assert,popEmptyArray,outOfBounds")->default_value("default"), @@ -1089,6 +1095,18 @@ General Information)").c_str(), m_options.modelChecker.settings.engine = *engine; } + if (m_args.count(g_strModelCheckerSolvers)) + { + string solversStr = m_args[g_strModelCheckerSolvers].as(); + optional solvers = smtutil::SMTSolverChoice::fromString(solversStr); + if (!solvers) + { + serr() << "Invalid option for --" << g_strModelCheckerSolvers << ": " << solversStr << endl; + return false; + } + m_options.modelChecker.settings.solvers = *solvers; + } + if (m_args.count(g_strModelCheckerTargets)) { string targetsStr = m_args[g_strModelCheckerTargets].as(); @@ -1108,6 +1126,7 @@ General Information)").c_str(), m_options.modelChecker.initialize = m_args.count(g_strModelCheckerContracts) || m_args.count(g_strModelCheckerEngine) || + m_args.count(g_strModelCheckerSolvers) || m_args.count(g_strModelCheckerTargets) || m_args.count(g_strModelCheckerTimeout); m_options.output.experimentalViaIR = (m_args.count(g_strExperimentalViaIR) > 0); diff --git a/test/cmdlineTests/model_checker_solvers_all/args b/test/cmdlineTests/model_checker_solvers_all/args new file mode 100644 index 000000000..4f09ccbe9 --- /dev/null +++ b/test/cmdlineTests/model_checker_solvers_all/args @@ -0,0 +1 @@ +--model-checker-engine all --model-checker-solvers all diff --git a/test/cmdlineTests/model_checker_solvers_all/err b/test/cmdlineTests/model_checker_solvers_all/err new file mode 100644 index 000000000..3db918e25 --- /dev/null +++ b/test/cmdlineTests/model_checker_solvers_all/err @@ -0,0 +1,12 @@ +Warning: CHC: Assertion violation happens here. +Counterexample: + +x = 0 + +Transaction trace: +test.constructor() +test.f(0) + --> model_checker_solvers_all/input.sol:5:3: + | +5 | assert(x > 0); + | ^^^^^^^^^^^^^ diff --git a/test/cmdlineTests/model_checker_solvers_all/input.sol b/test/cmdlineTests/model_checker_solvers_all/input.sol new file mode 100644 index 000000000..7d05ef6e5 --- /dev/null +++ b/test/cmdlineTests/model_checker_solvers_all/input.sol @@ -0,0 +1,7 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; +contract test { + function f(uint x) public pure { + assert(x > 0); + } +} \ No newline at end of file diff --git a/test/cmdlineTests/model_checker_solvers_all_implicit/args b/test/cmdlineTests/model_checker_solvers_all_implicit/args new file mode 100644 index 000000000..5aeb1490e --- /dev/null +++ b/test/cmdlineTests/model_checker_solvers_all_implicit/args @@ -0,0 +1 @@ +--model-checker-engine all diff --git a/test/cmdlineTests/model_checker_solvers_all_implicit/err b/test/cmdlineTests/model_checker_solvers_all_implicit/err new file mode 100644 index 000000000..7fffab4ef --- /dev/null +++ b/test/cmdlineTests/model_checker_solvers_all_implicit/err @@ -0,0 +1,12 @@ +Warning: CHC: Assertion violation happens here. +Counterexample: + +x = 0 + +Transaction trace: +test.constructor() +test.f(0) + --> model_checker_solvers_all_implicit/input.sol:5:3: + | +5 | assert(x > 0); + | ^^^^^^^^^^^^^ diff --git a/test/cmdlineTests/model_checker_solvers_all_implicit/input.sol b/test/cmdlineTests/model_checker_solvers_all_implicit/input.sol new file mode 100644 index 000000000..7d05ef6e5 --- /dev/null +++ b/test/cmdlineTests/model_checker_solvers_all_implicit/input.sol @@ -0,0 +1,7 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; +contract test { + function f(uint x) public pure { + assert(x > 0); + } +} \ No newline at end of file diff --git a/test/cmdlineTests/model_checker_solvers_smtlib2/args b/test/cmdlineTests/model_checker_solvers_smtlib2/args new file mode 100644 index 000000000..3d90e9161 --- /dev/null +++ b/test/cmdlineTests/model_checker_solvers_smtlib2/args @@ -0,0 +1 @@ +--model-checker-engine all --model-checker-solvers smtlib2 diff --git a/test/cmdlineTests/model_checker_solvers_smtlib2/err b/test/cmdlineTests/model_checker_solvers_smtlib2/err new file mode 100644 index 000000000..9a156ff90 --- /dev/null +++ b/test/cmdlineTests/model_checker_solvers_smtlib2/err @@ -0,0 +1,3 @@ +Warning: CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled. + +Warning: BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled. diff --git a/test/cmdlineTests/model_checker_solvers_smtlib2/input.sol b/test/cmdlineTests/model_checker_solvers_smtlib2/input.sol new file mode 100644 index 000000000..7d05ef6e5 --- /dev/null +++ b/test/cmdlineTests/model_checker_solvers_smtlib2/input.sol @@ -0,0 +1,7 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; +contract test { + function f(uint x) public pure { + assert(x > 0); + } +} \ No newline at end of file diff --git a/test/cmdlineTests/model_checker_solvers_wrong/args b/test/cmdlineTests/model_checker_solvers_wrong/args new file mode 100644 index 000000000..542502ee3 --- /dev/null +++ b/test/cmdlineTests/model_checker_solvers_wrong/args @@ -0,0 +1 @@ +--model-checker-engine all --model-checker-solvers ultraSolver diff --git a/test/cmdlineTests/model_checker_solvers_wrong/err b/test/cmdlineTests/model_checker_solvers_wrong/err new file mode 100644 index 000000000..bf2df0a70 --- /dev/null +++ b/test/cmdlineTests/model_checker_solvers_wrong/err @@ -0,0 +1 @@ +Invalid option for --model-checker-solvers: ultraSolver diff --git a/test/cmdlineTests/model_checker_solvers_wrong/exit b/test/cmdlineTests/model_checker_solvers_wrong/exit new file mode 100644 index 000000000..d00491fd7 --- /dev/null +++ b/test/cmdlineTests/model_checker_solvers_wrong/exit @@ -0,0 +1 @@ +1 diff --git a/test/cmdlineTests/model_checker_solvers_wrong/input.sol b/test/cmdlineTests/model_checker_solvers_wrong/input.sol new file mode 100644 index 000000000..7d05ef6e5 --- /dev/null +++ b/test/cmdlineTests/model_checker_solvers_wrong/input.sol @@ -0,0 +1,7 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; +contract test { + function f(uint x) public pure { + assert(x > 0); + } +} \ No newline at end of file diff --git a/test/cmdlineTests/model_checker_solvers_wrong2/args b/test/cmdlineTests/model_checker_solvers_wrong2/args new file mode 100644 index 000000000..a20c99800 --- /dev/null +++ b/test/cmdlineTests/model_checker_solvers_wrong2/args @@ -0,0 +1 @@ +--model-checker-engine all --model-checker-solvers z3, smtlib2 diff --git a/test/cmdlineTests/model_checker_solvers_wrong2/err b/test/cmdlineTests/model_checker_solvers_wrong2/err new file mode 100644 index 000000000..1bdd53068 --- /dev/null +++ b/test/cmdlineTests/model_checker_solvers_wrong2/err @@ -0,0 +1 @@ +"smtlib2" is not found. diff --git a/test/cmdlineTests/model_checker_solvers_wrong2/exit b/test/cmdlineTests/model_checker_solvers_wrong2/exit new file mode 100644 index 000000000..d00491fd7 --- /dev/null +++ b/test/cmdlineTests/model_checker_solvers_wrong2/exit @@ -0,0 +1 @@ +1 diff --git a/test/cmdlineTests/model_checker_solvers_wrong2/input.sol b/test/cmdlineTests/model_checker_solvers_wrong2/input.sol new file mode 100644 index 000000000..7d05ef6e5 --- /dev/null +++ b/test/cmdlineTests/model_checker_solvers_wrong2/input.sol @@ -0,0 +1,7 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; +contract test { + function f(uint x) public pure { + assert(x > 0); + } +} \ No newline at end of file diff --git a/test/cmdlineTests/model_checker_solvers_z3/args b/test/cmdlineTests/model_checker_solvers_z3/args new file mode 100644 index 000000000..ff27293ea --- /dev/null +++ b/test/cmdlineTests/model_checker_solvers_z3/args @@ -0,0 +1 @@ +--model-checker-engine all --model-checker-solvers z3 diff --git a/test/cmdlineTests/model_checker_solvers_z3/err b/test/cmdlineTests/model_checker_solvers_z3/err new file mode 100644 index 000000000..67349d8e1 --- /dev/null +++ b/test/cmdlineTests/model_checker_solvers_z3/err @@ -0,0 +1,12 @@ +Warning: CHC: Assertion violation happens here. +Counterexample: + +x = 0 + +Transaction trace: +test.constructor() +test.f(0) + --> model_checker_solvers_z3/input.sol:5:3: + | +5 | assert(x > 0); + | ^^^^^^^^^^^^^ diff --git a/test/cmdlineTests/model_checker_solvers_z3/input.sol b/test/cmdlineTests/model_checker_solvers_z3/input.sol new file mode 100644 index 000000000..7d05ef6e5 --- /dev/null +++ b/test/cmdlineTests/model_checker_solvers_z3/input.sol @@ -0,0 +1,7 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; +contract test { + function f(uint x) public pure { + assert(x > 0); + } +} \ No newline at end of file diff --git a/test/cmdlineTests/model_checker_solvers_z3_smtlib2/args b/test/cmdlineTests/model_checker_solvers_z3_smtlib2/args new file mode 100644 index 000000000..889888874 --- /dev/null +++ b/test/cmdlineTests/model_checker_solvers_z3_smtlib2/args @@ -0,0 +1 @@ +--model-checker-engine all --model-checker-solvers z3,smtlib2 diff --git a/test/cmdlineTests/model_checker_solvers_z3_smtlib2/err b/test/cmdlineTests/model_checker_solvers_z3_smtlib2/err new file mode 100644 index 000000000..5699afcde --- /dev/null +++ b/test/cmdlineTests/model_checker_solvers_z3_smtlib2/err @@ -0,0 +1,12 @@ +Warning: CHC: Assertion violation happens here. +Counterexample: + +x = 0 + +Transaction trace: +test.constructor() +test.f(0) + --> model_checker_solvers_z3_smtlib2/input.sol:5:3: + | +5 | assert(x > 0); + | ^^^^^^^^^^^^^ diff --git a/test/cmdlineTests/model_checker_solvers_z3_smtlib2/input.sol b/test/cmdlineTests/model_checker_solvers_z3_smtlib2/input.sol new file mode 100644 index 000000000..7d05ef6e5 --- /dev/null +++ b/test/cmdlineTests/model_checker_solvers_z3_smtlib2/input.sol @@ -0,0 +1,7 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; +contract test { + function f(uint x) public pure { + assert(x > 0); + } +} \ No newline at end of file diff --git a/test/cmdlineTests/standard_model_checker_solvers_all/input.json b/test/cmdlineTests/standard_model_checker_solvers_all/input.json new file mode 100644 index 000000000..db9f2232d --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_solvers_all/input.json @@ -0,0 +1,17 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract C { function f(uint x) public pure { assert(x > 0); } }" + } + }, + "settings": + { + "modelChecker": + { + "engine": "all" + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_solvers_all/output.json b/test/cmdlineTests/standard_model_checker_solvers_all/output.json new file mode 100644 index 000000000..12dfe5871 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_solvers_all/output.json @@ -0,0 +1,21 @@ +{"errors":[{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here. +Counterexample: + +x = 0 + +Transaction trace: +C.constructor() +C.f(0) + --> A:4:47: + | +4 | contract C { function f(uint x) public pure { assert(x > 0); } } + | ^^^^^^^^^^^^^ + +","message":"CHC: Assertion violation happens here. +Counterexample: + +x = 0 + +Transaction trace: +C.constructor() +C.f(0)","severity":"warning","sourceLocation":{"end":119,"file":"A","start":106},"type":"Warning"}],"sources":{"A":{"id":0}}} diff --git a/test/cmdlineTests/standard_model_checker_solvers_none/input.json b/test/cmdlineTests/standard_model_checker_solvers_none/input.json new file mode 100644 index 000000000..07cbb88ac --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_solvers_none/input.json @@ -0,0 +1,18 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract C { function f(uint x) public pure { assert(x > 0); } }" + } + }, + "settings": + { + "modelChecker": + { + "engine": "all", + "solvers": [] + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_solvers_none/output.json b/test/cmdlineTests/standard_model_checker_solvers_none/output.json new file mode 100644 index 000000000..b237fadce --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_solvers_none/output.json @@ -0,0 +1,5 @@ +{"errors":[{"component":"general","errorCode":"7649","formattedMessage":"Warning: CHC analysis was not possible since no Horn solver was enabled. + +","message":"CHC analysis was not possible since no Horn solver was enabled.","severity":"warning","type":"Warning"},{"component":"general","errorCode":"7710","formattedMessage":"Warning: BMC analysis was not possible since no SMT solver was found and enabled. + +","message":"BMC analysis was not possible since no SMT solver was found and enabled.","severity":"warning","type":"Warning"}],"sources":{"A":{"id":0}}} diff --git a/test/cmdlineTests/standard_model_checker_solvers_smtlib2/input.json b/test/cmdlineTests/standard_model_checker_solvers_smtlib2/input.json new file mode 100644 index 000000000..8903ec016 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_solvers_smtlib2/input.json @@ -0,0 +1,18 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract C { function f(uint x) public pure { assert(x > 0); } }" + } + }, + "settings": + { + "modelChecker": + { + "engine": "all", + "solvers": ["smtlib2"] + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_solvers_smtlib2/output.json b/test/cmdlineTests/standard_model_checker_solvers_smtlib2/output.json new file mode 100644 index 000000000..2ab2d6b5e --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_solvers_smtlib2/output.json @@ -0,0 +1,138 @@ +{"auxiliaryInputRequested":{"smtlib2queries":{"0x4ee925df3426fec84707cea517cc52ed216229bfde71458a69e7edeece2c071e":"(set-option :produce-models true) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) +(declare-fun |x_3_0| () Int) +(declare-fun |expr_7_0| () Int) +(declare-fun |expr_8_0| () Int) +(declare-fun |expr_9_1| () Bool) + +(assert (and (and (and true true) (and (= expr_9_1 (> expr_7_0 expr_8_0)) (and (=> (and true true) true) (and (= expr_8_0 0) (and (=> (and true true) (and (>= expr_7_0 0) (<= expr_7_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_7_0 x_3_0) (and (and (>= x_3_0 0) (<= x_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 3017696395)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 179)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 222)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 100)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 139)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))) (not expr_9_1))) +(declare-const |EVALEXPR_0| Int) +(assert (= |EVALEXPR_0| x_3_0)) +(check-sat) +(get-value (|EVALEXPR_0| )) +","0x540d6953fff999f72ca33d8af8b900986dc012a365fc1b8572aa9d9978f1392b":"(set-logic HORN) + +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |interface_0_C_14_0| (Int |abi_type| |crypto_type| |state_type| ) Bool) +(declare-fun |nondet_interface_1_C_14_0| (Int Int |abi_type| |crypto_type| |state_type| |state_type| ) Bool) +(declare-fun |summary_constructor_2_C_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) +(assert +(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (state_0 |state_type|) (this_0 Int) (tx_0 |tx_type|)) +(=> (= error_0 0) (nondet_interface_1_C_14_0 error_0 this_0 abi_0 crypto_0 state_0 state_0)))) + + +(declare-fun |summary_3_function_f__13_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int ) Bool) +(assert +(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int)) +(=> (and (and (nondet_interface_1_C_14_0 error_0 this_0 abi_0 crypto_0 state_0 state_1) true) (and (= error_0 0) (summary_3_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 x_3_0 state_2 x_3_1))) (nondet_interface_1_C_14_0 error_1 this_0 abi_0 crypto_0 state_0 state_2)))) + + +(declare-fun |block_4_function_f__13_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int ) Bool) +(declare-fun |block_5_f_12_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int ) Bool) +(assert +(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int)) +(block_4_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1))) + + +(assert +(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int)) +(=> (and (and (block_4_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1) (and (and (and (and (= state_1 state_0) (= error_0 0)) true) (and true (= x_3_1 x_3_0))) true)) true) (block_5_f_12_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1)))) + + +(declare-fun |block_6_return_function_f__13_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int ) Bool) +(declare-fun |block_7_function_f__13_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int ) Bool) +(assert +(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int)) +(=> (and (and (block_5_f_12_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1) (and (= expr_9_1 (> expr_7_0 expr_8_0)) (and (=> true true) (and (= expr_8_0 0) (and (=> true (and (>= expr_7_0 0) (<= expr_7_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_7_0 x_3_1) (and (and (>= x_3_1 0) (<= x_3_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true))))))) (and (not expr_9_1) (= error_1 1))) (block_7_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1)))) + + +(assert +(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int)) +(=> (block_7_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1) (summary_3_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1)))) + + +(assert +(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int)) +(=> (and (and (block_5_f_12_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1) (and (= error_1 error_0) (and (= expr_9_1 (> expr_7_0 expr_8_0)) (and (=> true true) (and (= expr_8_0 0) (and (=> true (and (>= expr_7_0 0) (<= expr_7_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_7_0 x_3_1) (and (and (>= x_3_1 0) (<= x_3_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true)))))))) true) (block_6_return_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1)))) + + +(assert +(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int)) +(=> (and (and (block_6_return_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1) true) true) (summary_3_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1)))) + + +(assert +(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int)) +(=> (and (and (interface_0_C_14_0 this_0 abi_0 crypto_0 state_0) true) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 3017696395)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 179)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 222)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 100)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 139)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) (summary_3_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1)) (= error_0 0))) (interface_0_C_14_0 this_0 abi_0 crypto_0 state_1)))) + + +(declare-fun |contract_initializer_8_C_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) +(declare-fun |contract_initializer_entry_9_C_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) +(assert +(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int)) +(=> (and (and (= state_1 state_0) (= error_0 0)) true) (contract_initializer_entry_9_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) + + +(declare-fun |contract_initializer_after_init_10_C_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) +(assert +(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int)) +(=> (and (and (contract_initializer_entry_9_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) true) true) (contract_initializer_after_init_10_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) + + +(assert +(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int)) +(=> (and (and (contract_initializer_after_init_10_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) true) true) (contract_initializer_8_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) + + +(declare-fun |implicit_constructor_entry_11_C_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) +(assert +(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int)) +(=> (and (and (and (= state_1 state_0) (= error_0 0)) true) true) (implicit_constructor_entry_11_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) + + +(assert +(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int)) +(=> (and (and (implicit_constructor_entry_11_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) (and (contract_initializer_8_C_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 state_2) true)) (> error_1 0)) (summary_constructor_2_C_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 state_2)))) + + +(assert +(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int)) +(=> (and (and (implicit_constructor_entry_11_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) (and (= error_1 0) (and (contract_initializer_8_C_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 state_2) true))) true) (summary_constructor_2_C_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 state_2)))) + + +(assert +(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int)) +(=> (and (and (summary_constructor_2_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) true) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (= (|msg.value| tx_0) 0)) (= error_0 0))) (interface_0_C_14_0 this_0 abi_0 crypto_0 state_1)))) + + +(declare-fun |error_target_2_0| () Bool) +(assert +(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int)) +(=> (and (and (interface_0_C_14_0 this_0 abi_0 crypto_0 state_0) true) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 3017696395)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 179)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 222)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 100)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 139)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) (summary_3_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1)) (= error_0 1))) error_target_2_0))) + + +(assert +(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int)) +(=> error_target_2_0 false))) +(check-sat)"}},"errors":[{"component":"general","errorCode":"3996","formattedMessage":"Warning: CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled. + +","message":"CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled.","severity":"warning","type":"Warning"},{"component":"general","errorCode":"8084","formattedMessage":"Warning: BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled. + +","message":"BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled.","severity":"warning","type":"Warning"}],"sources":{"A":{"id":0}}} diff --git a/test/cmdlineTests/standard_model_checker_solvers_z3/input.json b/test/cmdlineTests/standard_model_checker_solvers_z3/input.json new file mode 100644 index 000000000..91db9ad7f --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_solvers_z3/input.json @@ -0,0 +1,18 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract C { function f(uint x) public pure { assert(x > 0); } }" + } + }, + "settings": + { + "modelChecker": + { + "engine": "all", + "solvers": ["z3"] + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_solvers_z3/output.json b/test/cmdlineTests/standard_model_checker_solvers_z3/output.json new file mode 100644 index 000000000..12dfe5871 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_solvers_z3/output.json @@ -0,0 +1,21 @@ +{"errors":[{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here. +Counterexample: + +x = 0 + +Transaction trace: +C.constructor() +C.f(0) + --> A:4:47: + | +4 | contract C { function f(uint x) public pure { assert(x > 0); } } + | ^^^^^^^^^^^^^ + +","message":"CHC: Assertion violation happens here. +Counterexample: + +x = 0 + +Transaction trace: +C.constructor() +C.f(0)","severity":"warning","sourceLocation":{"end":119,"file":"A","start":106},"type":"Warning"}],"sources":{"A":{"id":0}}} diff --git a/test/cmdlineTests/standard_model_checker_solvers_z3_smtlib2/input.json b/test/cmdlineTests/standard_model_checker_solvers_z3_smtlib2/input.json new file mode 100644 index 000000000..19913a562 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_solvers_z3_smtlib2/input.json @@ -0,0 +1,18 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract C { function f(uint x) public pure { assert(x > 0); } }" + } + }, + "settings": + { + "modelChecker": + { + "engine": "all", + "solvers": ["z3", "smtlib2"] + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_solvers_z3_smtlib2/output.json b/test/cmdlineTests/standard_model_checker_solvers_z3_smtlib2/output.json new file mode 100644 index 000000000..12dfe5871 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_solvers_z3_smtlib2/output.json @@ -0,0 +1,21 @@ +{"errors":[{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here. +Counterexample: + +x = 0 + +Transaction trace: +C.constructor() +C.f(0) + --> A:4:47: + | +4 | contract C { function f(uint x) public pure { assert(x > 0); } } + | ^^^^^^^^^^^^^ + +","message":"CHC: Assertion violation happens here. +Counterexample: + +x = 0 + +Transaction trace: +C.constructor() +C.f(0)","severity":"warning","sourceLocation":{"end":119,"file":"A","start":106},"type":"Warning"}],"sources":{"A":{"id":0}}} diff --git a/test/externalTests/solc-js/solc-js.sh b/test/externalTests/solc-js/solc-js.sh index 9cc753959..3762ba7a2 100755 --- a/test/externalTests/solc-js/solc-js.sh +++ b/test/externalTests/solc-js/solc-js.sh @@ -47,8 +47,10 @@ function solcjs_test cp -Rf "$SOLCJS_INPUT_DIR/DAO" test/ printLog "Copying SMTChecker tests..." - cp -Rf "$TEST_DIR"/test/libsolidity/smtCheckerTests test/ - rm -rf test/smtCheckerTests/imports + # We do not copy all tests because that takes too long. + cp -Rf "$TEST_DIR"/test/libsolidity/smtCheckerTests/external_calls test/smtCheckerTests/ + cp -Rf "$TEST_DIR"/test/libsolidity/smtCheckerTests/loops test/smtCheckerTests/ + cp -Rf "$TEST_DIR"/test/libsolidity/smtCheckerTests/invariants test/smtCheckerTests/ # Update version (needed for some tests) echo "Updating package.json to version $VERSION" diff --git a/test/libsolidity/SMTCheckerTest.cpp b/test/libsolidity/SMTCheckerTest.cpp index bdc408b9f..961baab70 100644 --- a/test/libsolidity/SMTCheckerTest.cpp +++ b/test/libsolidity/SMTCheckerTest.cpp @@ -29,21 +29,13 @@ SMTCheckerTest::SMTCheckerTest(string const& _filename): SyntaxTest(_filename, E { auto const& choice = m_reader.stringSetting("SMTSolvers", "any"); if (choice == "any") - m_enabledSolvers = smtutil::SMTSolverChoice::All(); - else if (choice == "z3") - m_enabledSolvers = smtutil::SMTSolverChoice::Z3(); - else if (choice == "cvc4") - m_enabledSolvers = smtutil::SMTSolverChoice::CVC4(); + m_modelCheckerSettings.solvers = smtutil::SMTSolverChoice::All(); else if (choice == "none") - m_enabledSolvers = smtutil::SMTSolverChoice::None(); - else + m_modelCheckerSettings.solvers = smtutil::SMTSolverChoice::None(); + else if (!m_modelCheckerSettings.solvers.setSolver(choice)) BOOST_THROW_EXCEPTION(runtime_error("Invalid SMT solver choice.")); - auto available = ModelChecker::availableSolvers(); - if (!available.z3) - m_enabledSolvers.z3 = false; - if (!available.cvc4) - m_enabledSolvers.cvc4 = false; + m_modelCheckerSettings.solvers &= ModelChecker::availableSolvers(); auto engine = ModelCheckerEngine::fromString(m_reader.stringSetting("SMTEngine", "all")); if (engine) @@ -51,7 +43,7 @@ SMTCheckerTest::SMTCheckerTest(string const& _filename): SyntaxTest(_filename, E else BOOST_THROW_EXCEPTION(runtime_error("Invalid SMT engine choice.")); - if (m_enabledSolvers.none() || m_modelCheckerSettings.engine.none()) + if (m_modelCheckerSettings.solvers.none() || m_modelCheckerSettings.engine.none()) m_shouldRun = false; auto const& ignoreCex = m_reader.stringSetting("SMTIgnoreCex", "no"); @@ -66,7 +58,6 @@ SMTCheckerTest::SMTCheckerTest(string const& _filename): SyntaxTest(_filename, E TestCase::TestResult SMTCheckerTest::run(ostream& _stream, string const& _linePrefix, bool _formatted) { setupCompiler(); - compiler().setSMTSolverChoice(m_enabledSolvers); compiler().setModelCheckerSettings(m_modelCheckerSettings); parseAndAnalyze(); filterObtainedErrors(); diff --git a/test/solc/CommandLineParser.cpp b/test/solc/CommandLineParser.cpp index 3f12b85fd..21ef80894 100644 --- a/test/solc/CommandLineParser.cpp +++ b/test/solc/CommandLineParser.cpp @@ -27,6 +27,7 @@ #include #include +#include #include #include @@ -82,6 +83,7 @@ BOOST_AUTO_TEST_CASE(no_options) expectedOptions.modelChecker.settings = { ModelCheckerContracts::Default(), ModelCheckerEngine::None(), + smtutil::SMTSolverChoice::All(), ModelCheckerTargets::Default(), nullopt, }; @@ -150,6 +152,7 @@ BOOST_AUTO_TEST_CASE(cli_mode_options) "--yul-optimizations=agf", "--model-checker-contracts=contract1.yul:A,contract2.yul:B", "--model-checker-engine=bmc", + "--model-checker-solvers=z3,smtlib2", "--model-checker-targets=underflow,divByZero", "--model-checker-timeout=5", }; @@ -207,6 +210,7 @@ BOOST_AUTO_TEST_CASE(cli_mode_options) expectedOptions.modelChecker.settings = { {{{"contract1.yul", {"A"}}, {"contract2.yul", {"B"}}}}, {true, false}, + {false, true, true}, {{VerificationTargetType::Underflow, VerificationTargetType::DivByZero}}, 5, }; @@ -276,6 +280,7 @@ BOOST_AUTO_TEST_CASE(assembly_mode_options) "contract1.yul:A," "contract2.yul:B", "--model-checker-engine=bmc", // Ignored in assembly mode + "--model-checker-solvers=z3,smtlib2", // Ignored in assembly mode "--model-checker-targets=" // Ignored in assembly mode "underflow," "divByZero", @@ -372,6 +377,7 @@ BOOST_AUTO_TEST_CASE(standard_json_mode_options) "contract1.yul:A," "contract2.yul:B", "--model-checker-engine=bmc", // Ignored in Standard JSON mode + "--model-checker-solvers=z3,smtlib2", // Ignored in Standard JSON mode "--model-checker-targets=" // Ignored in Standard JSON mode "underflow," "divByZero", diff --git a/test/tools/fuzzer_common.cpp b/test/tools/fuzzer_common.cpp index 99a3775e1..ef85288b0 100644 --- a/test/tools/fuzzer_common.cpp +++ b/test/tools/fuzzer_common.cpp @@ -16,7 +16,6 @@ */ // SPDX-License-Identifier: GPL-3.0 -#include "libsolidity/formal/ModelCheckerSettings.h" #include #include @@ -105,6 +104,7 @@ void FuzzerUtil::testCompiler( compiler.setModelCheckerSettings({ frontend::ModelCheckerContracts::Default(), frontend::ModelCheckerEngine::All(), + smtutil::SMTSolverChoice::All(), frontend::ModelCheckerTargets::Default(), /*timeout=*/1 });