cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Deprecate pragma experimental SMTChecker

Browse Source
This commit is contained in:
Leonardo Alt 2021-03-31 17:09:37 +02:00
parent 0cc0cabd30
commit b753cb6120
7 changed files with 46 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libsolidity/formal/BMC.cpp
View File

@ -61,8 +61,6 @@ BMC::BMC(
void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<VerificationTargetType>> _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))

6
libsolidity/formal/CHC.cpp
View File

@ -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();

39
libsolidity/formal/ModelChecker.cpp
View File

@ -21,6 +21,8 @@
#include <libsmtutil/Z3Interface.h>
#endif
#include <range/v3/algorithm/any_of.hpp>
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<shared_ptr<SourceUnit>> 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<PragmaDirective>(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)

5
libsolidity/formal/ModelChecker.h
View File

@ -55,6 +55,9 @@ public:
smtutil::SMTSolverChoice _enabledSolvers = smtutil::SMTSolverChoice::All()
);
// TODO This should be removed for 0.9.0.
void enableAllEnginesIfPragmaPresent(std::vector<std::shared_ptr<SourceUnit>> 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.

2
libsolidity/formal/ModelCheckerSettings.h
View File

@ -69,7 +69,7 @@ struct ModelCheckerTargets
struct ModelCheckerSettings
{
ModelCheckerEngine engine = ModelCheckerEngine::All();
ModelCheckerEngine engine = ModelCheckerEngine::None();
ModelCheckerTargets targets = ModelCheckerTargets::All();
std::optional<unsigned> timeout;
};

1
libsolidity/interface/CompilerStack.cpp
View File

@ -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);

2
solc/CommandLineInterface.cpp
View File

@ -1055,7 +1055,7 @@ General Information)").c_str(),
smtCheckerOptions.add_options()
(
g_strModelCheckerEngine.c_str(),
po::value<string>()->value_name("all,bmc,chc,none")->default_value("all"),
po::value<string>()->value_name("all,bmc,chc,none")->default_value("none"),
"Select model checker engine."
)
(