From b753cb6120b758c8db73c6f9f9b8745b3413dcdb Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Wed, 31 Mar 2021 17:09:37 +0200 Subject: [PATCH] Deprecate pragma experimental SMTChecker --- libsolidity/formal/BMC.cpp | 2 -- libsolidity/formal/CHC.cpp | 6 ---- libsolidity/formal/ModelChecker.cpp | 39 ++++++++++++++++++++++- libsolidity/formal/ModelChecker.h | 5 +++ libsolidity/formal/ModelCheckerSettings.h | 2 +- libsolidity/interface/CompilerStack.cpp | 1 + solc/CommandLineInterface.cpp | 2 +- 7 files changed, 46 insertions(+), 11 deletions(-) diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index 1caf3228a..f6630f0da 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -61,8 +61,6 @@ BMC::BMC( void BMC::analyze(SourceUnit const& _source, map> _solvedTargets) { - solAssert(_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker), ""); - /// This is currently used to abort analysis of SourceUnits /// containing file level functions or constants. if (SMTEncoder::analyze(_source)) diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 6812e2a99..65e29870b 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -76,8 +76,6 @@ CHC::CHC( void CHC::analyze(SourceUnit const& _source) { - solAssert(_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker), ""); - /// This is currently used to abort analysis of SourceUnits /// containing file level functions or constants. if (SMTEncoder::analyze(_source)) @@ -1430,10 +1428,6 @@ void CHC::verificationTargetEncountered( return; solAssert(m_currentContract || m_currentFunction, ""); - SourceUnit const* source = m_currentContract ? sourceUnitContaining(*m_currentContract) : sourceUnitContaining(*m_currentFunction); - solAssert(source, ""); - if (!source->annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker)) - return; bool scopeIsFunction = m_currentFunction && !m_currentFunction->isConstructor(); auto errorId = newErrorId(); diff --git a/libsolidity/formal/ModelChecker.cpp b/libsolidity/formal/ModelChecker.cpp index dadc05a04..b26fc9352 100644 --- a/libsolidity/formal/ModelChecker.cpp +++ b/libsolidity/formal/ModelChecker.cpp @@ -21,6 +21,8 @@ #include #endif +#include + using namespace std; using namespace solidity; using namespace solidity::util; @@ -34,6 +36,7 @@ ModelChecker::ModelChecker( ReadCallback::Callback const& _smtCallback, smtutil::SMTSolverChoice _enabledSolvers ): + m_errorReporter(_errorReporter), m_settings(_settings), m_context(), m_bmc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers, m_settings), @@ -41,9 +44,43 @@ ModelChecker::ModelChecker( { } +// TODO This should be removed for 0.9.0. +void ModelChecker::enableAllEnginesIfPragmaPresent(vector> const& _sources) +{ + bool hasPragma = ranges::any_of(_sources, [](auto _source) { + return _source && _source->annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker); + }); + if (hasPragma) + m_settings.engine = ModelCheckerEngine::All(); +} + void ModelChecker::analyze(SourceUnit const& _source) { - if (!_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker)) + // TODO This should be removed for 0.9.0. + if (_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker)) + { + PragmaDirective const* smtPragma = nullptr; + for (auto node: _source.nodes()) + if (auto pragma = dynamic_pointer_cast(node)) + if ( + pragma->literals().size() >= 2 && + pragma->literals().at(1) == "SMTChecker" + ) + { + smtPragma = pragma.get(); + break; + } + solAssert(smtPragma, ""); + m_errorReporter.warning( + 5523_error, + smtPragma->location(), + "The SMTChecker pragma has been deprecated and will be removed in the future. " + "Please use the \"model checker engine\" compiler setting to activate the SMTChecker instead. " + "If the pragma is enabled, all engines will be used." + ); + } + + if (m_settings.engine.none()) return; if (m_settings.engine.chc) diff --git a/libsolidity/formal/ModelChecker.h b/libsolidity/formal/ModelChecker.h index 572f47083..9c594394b 100644 --- a/libsolidity/formal/ModelChecker.h +++ b/libsolidity/formal/ModelChecker.h @@ -55,6 +55,9 @@ public: smtutil::SMTSolverChoice _enabledSolvers = smtutil::SMTSolverChoice::All() ); + // TODO This should be removed for 0.9.0. + void enableAllEnginesIfPragmaPresent(std::vector> const& _sources); + void analyze(SourceUnit const& _sources); /// This is used if the SMT solver is not directly linked into this binary. @@ -66,6 +69,8 @@ public: static smtutil::SMTSolverChoice availableSolvers(); private: + langutil::ErrorReporter& m_errorReporter; + ModelCheckerSettings m_settings; /// Stores the context of the encoding. diff --git a/libsolidity/formal/ModelCheckerSettings.h b/libsolidity/formal/ModelCheckerSettings.h index 0a1f338ff..a9eba20d5 100644 --- a/libsolidity/formal/ModelCheckerSettings.h +++ b/libsolidity/formal/ModelCheckerSettings.h @@ -69,7 +69,7 @@ struct ModelCheckerTargets struct ModelCheckerSettings { - ModelCheckerEngine engine = ModelCheckerEngine::All(); + ModelCheckerEngine engine = ModelCheckerEngine::None(); ModelCheckerTargets targets = ModelCheckerTargets::All(); std::optional timeout; }; diff --git a/libsolidity/interface/CompilerStack.cpp b/libsolidity/interface/CompilerStack.cpp index a48270074..30f09d5cd 100644 --- a/libsolidity/interface/CompilerStack.cpp +++ b/libsolidity/interface/CompilerStack.cpp @@ -547,6 +547,7 @@ bool CompilerStack::analyze() if (noErrors) { ModelChecker modelChecker(m_errorReporter, m_smtlib2Responses, m_modelCheckerSettings, m_readFile, m_enabledSMTSolvers); + modelChecker.enableAllEnginesIfPragmaPresent(applyMap(m_sourceOrder, [](Source const* _source) { return _source->ast; })); for (Source const* source: m_sourceOrder) if (source->ast) modelChecker.analyze(*source->ast); diff --git a/solc/CommandLineInterface.cpp b/solc/CommandLineInterface.cpp index d7ada29f3..d0c9e81ee 100644 --- a/solc/CommandLineInterface.cpp +++ b/solc/CommandLineInterface.cpp @@ -1055,7 +1055,7 @@ General Information)").c_str(), smtCheckerOptions.add_options() ( g_strModelCheckerEngine.c_str(), - po::value()->value_name("all,bmc,chc,none")->default_value("all"), + po::value()->value_name("all,bmc,chc,none")->default_value("none"), "Select model checker engine." ) (