From f4b849972ca4acae5de9634dede8f7a17753814f Mon Sep 17 00:00:00 2001 From: Martin Blicha Date: Mon, 26 Jun 2023 13:41:17 +0200 Subject: [PATCH] Remove smtlib2 solver option --- libsmtutil/CHCSmtLib2Interface.cpp | 2 +- libsmtutil/SolverInterface.h | 22 ++++++++-------------- libsolidity/formal/BMC.cpp | 9 ++------- libsolidity/formal/CHC.cpp | 8 +++----- libsolidity/formal/ModelChecker.cpp | 2 +- libsolidity/interface/StandardCompiler.cpp | 3 --- solc/CommandLineParser.cpp | 4 +--- test/solc/CommandLineParser.cpp | 6 +++--- 8 files changed, 19 insertions(+), 37 deletions(-) diff --git a/libsmtutil/CHCSmtLib2Interface.cpp b/libsmtutil/CHCSmtLib2Interface.cpp index d4b697bcf..80051f500 100644 --- a/libsmtutil/CHCSmtLib2Interface.cpp +++ b/libsmtutil/CHCSmtLib2Interface.cpp @@ -183,7 +183,7 @@ 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 || m_enabledSolvers.z3); + smtAssert(m_enabledSolvers.eld || m_enabledSolvers.z3); smtAssert(m_smtCallback, "Callback must be set!"); std::string solverBinary = [&](){ if (m_enabledSolvers.eld) diff --git a/libsmtutil/SolverInterface.h b/libsmtutil/SolverInterface.h index 4a21f1841..6778a4371 100644 --- a/libsmtutil/SolverInterface.h +++ b/libsmtutil/SolverInterface.h @@ -43,15 +43,13 @@ struct SMTSolverChoice { bool cvc4 = false; bool eld = false; - bool smtlib2 = false; bool z3 = false; - static constexpr SMTSolverChoice All() noexcept { return {true, true, true, true}; } - static constexpr SMTSolverChoice CVC4() noexcept { return {true, false, false, false}; } - static constexpr SMTSolverChoice ELD() noexcept { return {false, true, false, false}; } - static constexpr SMTSolverChoice SMTLIB2() noexcept { return {false, false, true, false}; } - static constexpr SMTSolverChoice Z3() noexcept { return {false, false, false, true}; } - static constexpr SMTSolverChoice None() noexcept { return {false, false, false, false}; } + static constexpr SMTSolverChoice All() noexcept { return {true, true, true}; } + static constexpr SMTSolverChoice CVC4() noexcept { return {true, false, false}; } + static constexpr SMTSolverChoice ELD() noexcept { return {false, true, false}; } + static constexpr SMTSolverChoice Z3() noexcept { return {false, false, true}; } + static constexpr SMTSolverChoice None() noexcept { return {false, false, false}; } static std::optional fromString(std::string const& _solvers) { @@ -67,7 +65,6 @@ struct SMTSolverChoice { cvc4 &= _other.cvc4; eld &= _other.eld; - smtlib2 &= _other.smtlib2; z3 &= _other.z3; return *this; } @@ -84,29 +81,26 @@ struct SMTSolverChoice { return cvc4 == _other.cvc4 && eld == _other.eld && - smtlib2 == _other.smtlib2 && z3 == _other.z3; } bool setSolver(std::string const& _solver) { - static std::set const solvers{"cvc4", "eld", "smtlib2", "z3"}; + static std::set const solvers{"cvc4", "eld", "z3"}; if (!solvers.count(_solver)) return false; if (_solver == "cvc4") cvc4 = true; if (_solver == "eld") eld = true; - else if (_solver == "smtlib2") - smtlib2 = true; else if (_solver == "z3") z3 = true; return true; } bool none() const noexcept { return !some(); } - bool some() const noexcept { return cvc4 || eld || smtlib2 || z3; } - bool all() const noexcept { return cvc4 && eld && smtlib2 && z3; } + bool some() const noexcept { return cvc4 || eld || z3; } + bool all() const noexcept { return cvc4 && eld && z3; } }; enum class CheckResult diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index e879abfa1..8ece98388 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -47,7 +47,6 @@ BMC::BMC( _smtlib2Responses, _smtCallback, _settings.solvers, _settings.timeout )) { - solAssert(!_settings.printQuery || _settings.solvers == smtutil::SMTSolverChoice::SMTLIB2(), "Only SMTLib2 solver can be enabled to print queries"); if (m_settings.solvers.cvc4 || m_settings.solvers.z3) if (!_smtlib2Responses.empty()) m_errorReporter.warning( @@ -62,7 +61,7 @@ BMC::BMC( void BMC::analyze(SourceUnit const& _source, std::map, smt::EncodingContext::IdCompare> _solvedTargets) { // At this point every enabled solver is available. - if (!m_settings.solvers.cvc4 && !m_settings.solvers.smtlib2 && !m_settings.solvers.z3) + if (!m_settings.solvers.cvc4 && !m_settings.solvers.z3) { m_errorReporter.warning( 7710_error, @@ -121,11 +120,7 @@ void BMC::analyze(SourceUnit const& _source, std::mapunhandledQueries().empty() && - m_interface->solvers() == 1 && - m_settings.solvers.smtlib2 - ) + if (!m_interface->unhandledQueries().empty()) m_errorReporter.warning( 8084_error, SourceLocation(), diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 9f75a8ca3..5f97ccc6b 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -66,14 +66,12 @@ CHC::CHC( SMTEncoder(_context, _settings, _errorReporter, _unsupportedErrorReporter, _charStreamProvider), m_smtlib2Responses(_smtlib2Responses), m_smtCallback(_smtCallback) -{ - solAssert(!_settings.printQuery || _settings.solvers == smtutil::SMTSolverChoice::SMTLIB2(), "Only SMTLib2 solver can be enabled to print queries"); -} +{} void CHC::analyze(SourceUnit const& _source) { // At this point every enabled solver is available. - if (!m_settings.solvers.eld && !m_settings.solvers.smtlib2 && !m_settings.solvers.z3) + if (!m_settings.solvers.eld && !m_settings.solvers.z3) { m_errorReporter.warning( 7649_error, @@ -1168,7 +1166,7 @@ void CHC::resetSourceAnalysis() m_blockCounter = 0; // At this point every enabled solver is available. - solAssert(m_settings.solvers.smtlib2 || m_settings.solvers.eld || m_settings.solvers.z3); + solAssert(m_settings.solvers.eld || m_settings.solvers.z3); if (!m_interface) m_interface = std::make_unique(m_smtlib2Responses, m_smtCallback, m_settings.solvers, m_settings.timeout); diff --git a/libsolidity/formal/ModelChecker.cpp b/libsolidity/formal/ModelChecker.cpp index 1644e6a92..eb90694b2 100644 --- a/libsolidity/formal/ModelChecker.cpp +++ b/libsolidity/formal/ModelChecker.cpp @@ -162,7 +162,7 @@ std::vector ModelChecker::unhandledQueries() SMTSolverChoice ModelChecker::availableSolvers() { - smtutil::SMTSolverChoice available = smtutil::SMTSolverChoice::SMTLIB2(); + smtutil::SMTSolverChoice available = smtutil::SMTSolverChoice::None(); #if defined(__linux) || defined(__APPLE__) available.eld = !boost::process::search_path("eld").empty(); available.z3 = !boost::process::search_path("z3").empty(); diff --git a/libsolidity/interface/StandardCompiler.cpp b/libsolidity/interface/StandardCompiler.cpp index c46be3b22..1e0b34a60 100644 --- a/libsolidity/interface/StandardCompiler.cpp +++ b/libsolidity/interface/StandardCompiler.cpp @@ -1094,9 +1094,6 @@ std::variant StandardCompiler: if (!printQuery.isBool()) return formatFatalError(Error::Type::JSONError, "settings.modelChecker.printQuery must be a Boolean value."); - if (!(ret.modelCheckerSettings.solvers == smtutil::SMTSolverChoice::SMTLIB2())) - return formatFatalError(Error::Type::JSONError, "Only SMTLib2 solver can be enabled to print queries"); - ret.modelCheckerSettings.printQuery = printQuery.asBool(); } diff --git a/solc/CommandLineParser.cpp b/solc/CommandLineParser.cpp index 53f481ae8..264602c88 100644 --- a/solc/CommandLineParser.cpp +++ b/solc/CommandLineParser.cpp @@ -853,7 +853,7 @@ General Information)").c_str(), ) ( g_strModelCheckerSolvers.c_str(), - po::value()->value_name("cvc4,eld,z3,smtlib2")->default_value("z3"), + po::value()->value_name("cvc4,eld,z3")->default_value("z3"), "Select model checker solvers." ) ( @@ -1323,8 +1323,6 @@ void CommandLineParser::processArgs() if (m_args.count(g_strModelCheckerPrintQuery)) { - if (!(m_options.modelChecker.settings.solvers == smtutil::SMTSolverChoice::SMTLIB2())) - solThrow(CommandLineValidationError, "Only SMTLib2 solver can be enabled to print queries"); m_options.modelChecker.settings.printQuery = true; } diff --git a/test/solc/CommandLineParser.cpp b/test/solc/CommandLineParser.cpp index 43cef9d27..818ae8af5 100644 --- a/test/solc/CommandLineParser.cpp +++ b/test/solc/CommandLineParser.cpp @@ -151,7 +151,7 @@ BOOST_AUTO_TEST_CASE(cli_mode_options) "--model-checker-show-proved-safe", "--model-checker-show-unproved", "--model-checker-show-unsupported", - "--model-checker-solvers=z3,smtlib2", + "--model-checker-solvers=z3", "--model-checker-targets=underflow,divByZero", "--model-checker-timeout=5" }; @@ -221,7 +221,7 @@ BOOST_AUTO_TEST_CASE(cli_mode_options) true, true, true, - {false, false, true, true}, + {false, false, true}, {{VerificationTargetType::Underflow, VerificationTargetType::DivByZero}}, 5, }; @@ -413,7 +413,7 @@ BOOST_AUTO_TEST_CASE(invalid_options_input_modes_combinations) {"--model-checker-div-mod-no-slacks", {"--assemble", "--yul", "--strict-assembly", "--standard-json", "--link"}}, {"--model-checker-engine=bmc", {"--assemble", "--yul", "--strict-assembly", "--standard-json", "--link"}}, {"--model-checker-invariants=contract,reentrancy", {"--assemble", "--yul", "--strict-assembly", "--standard-json", "--link"}}, - {"--model-checker-solvers=z3,smtlib2", {"--assemble", "--yul", "--strict-assembly", "--standard-json", "--link"}}, + {"--model-checker-solvers=z3", {"--assemble", "--yul", "--strict-assembly", "--standard-json", "--link"}}, {"--model-checker-timeout=5", {"--assemble", "--yul", "--strict-assembly", "--standard-json", "--link"}}, {"--model-checker-contracts=contract1.yul:A,contract2.yul:B", {"--assemble", "--yul", "--strict-assembly", "--standard-json", "--link"}}, {"--model-checker-targets=underflow,divByZero", {"--assemble", "--yul", "--strict-assembly", "--standard-json", "--link"}}