cerc-io/solidity
11
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

Add CLI option to choose model checker engine

Browse Source
This commit is contained in:
Leonardo Alt
2020-10-16 15:01:47 +01:00
parent 23314fc96c
commit 4e49135318
34 changed files with 315 additions and 12 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/BMC.cpp
+3 -2
View File
@@ -836,7 +836,7 @@ void BMC::checkCondition(
"\nNote that some information is erased after the execution of loops.\n"
"You can re-introduce information using require().";
if (m_externalFunctionCallHappened)
extraComment+=
extraComment +=
"\nNote that external function calls are not inlined,"
" even if the source code of the function is available."
" This is due to the possibility that the actual called contract"
@@ -854,7 +854,7 @@ void BMC::checkCondition(
if (_callStack.size())
{
std::ostringstream modelMessage;
modelMessage << "\nCounterexample:\n";
modelMessage << "Counterexample:\n";
solAssert(values.size() == expressionNames.size(), "");
map<string, string> sortedModel;
for (size_t i = 0; i < values.size(); ++i)
@@ -863,6 +863,7 @@ void BMC::checkCondition(
for (auto const& eval: sortedModel)
modelMessage << " " << eval.first << " = " << eval.second << "\n";
m_errorReporter.warning(
_errorHappens,
_location,
libsolidity/formal/CHC.cpp
+6 -2
View File
@@ -1298,7 +1298,7 @@ void CHC::checkAndReportTarget(
_errorReporterId,
_scope->location(),
"CHC: " + _satMsg,
SecondarySourceLocation().append("\nCounterexample:\n" + *cex, SourceLocation{})
SecondarySourceLocation().append("Counterexample:\n" + *cex, SourceLocation{})
);
else
m_outerErrorReporter.warning(
@@ -1402,9 +1402,13 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
}
}
else
{
auto modelMsg = formatVariableModel(*stateVars, stateValues, ", ");
/// We report the state after every tx in the trace except for the last, which is reported
/// first in the code above.
path.emplace_back("State: " + formatVariableModel(*stateVars, stateValues, ", "));
if (!modelMsg.empty())
path.emplace_back("State: " + modelMsg);
}
string txCex = summaryPredicate->formatSummaryCall(summaryArgs);
path.emplace_back(txCex);
libsolidity/formal/ModelChecker.cpp
+6 -2
View File
@@ -27,9 +27,11 @@ using namespace solidity::frontend;
ModelChecker::ModelChecker(
ErrorReporter& _errorReporter,
map<h256, string> const& _smtlib2Responses,
ModelCheckerEngine _engine,
ReadCallback::Callback const& _smtCallback,
smtutil::SMTSolverChoice _enabledSolvers
):
m_engine(_engine),
m_context(),
m_bmc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers),
m_chc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers)
@@ -41,13 +43,15 @@ void ModelChecker::analyze(SourceUnit const& _source)
if (!_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker))
return;
m_chc.analyze(_source);
if (m_engine.chc)
m_chc.analyze(_source);
auto solvedTargets = m_chc.safeTargets();
for (auto const& target: m_chc.unsafeTargets())
solvedTargets[target.first] += target.second;
m_bmc.analyze(_source, solvedTargets);
if (m_engine.bmc)
m_bmc.analyze(_source, solvedTargets);
}
vector<string> ModelChecker::unhandledQueries()
libsolidity/formal/ModelChecker.h
+33
View File
@@ -32,6 +32,8 @@
#include <libsmtutil/SolverInterface.h>
#include <liblangutil/ErrorReporter.h>
#include <optional>
namespace solidity::langutil
{
class ErrorReporter;
@@ -41,6 +43,34 @@ struct SourceLocation;
namespace solidity::frontend
{
struct ModelCheckerEngine
{
bool bmc = false;
bool chc = false;
static constexpr ModelCheckerEngine All() { return {true, true}; }
static constexpr ModelCheckerEngine BMC() { return {true, false}; }
static constexpr ModelCheckerEngine CHC() { return {false, true}; }
static constexpr ModelCheckerEngine None() { return {false, false}; }
bool none() const { return !any(); }
bool any() const { return bmc || chc; }
bool all() const { return bmc && chc; }
static std::optional<ModelCheckerEngine> fromString(std::string const& _engine)
{
static std::map<std::string, ModelCheckerEngine> engineMap{
{"all", All()},
{"bmc", BMC()},
{"chc", CHC()},
{"none", None()}
};
if (engineMap.count(_engine))
return engineMap.at(_engine);
return {};
}
};
class ModelChecker
{
public:
@@ -49,6 +79,7 @@ public:
ModelChecker(
langutil::ErrorReporter& _errorReporter,
std::map<solidity::util::h256, std::string> const& _smtlib2Responses,
ModelCheckerEngine _engine = ModelCheckerEngine::All(),
ReadCallback::Callback const& _smtCallback = ReadCallback::Callback(),
smtutil::SMTSolverChoice _enabledSolvers = smtutil::SMTSolverChoice::All()
);
@@ -64,6 +95,8 @@ public:
static smtutil::SMTSolverChoice availableSolvers();
private:
ModelCheckerEngine m_engine;
/// Stores the context of the encoding.
smt::EncodingContext m_context;
libsolidity/formal/SMTEncoder.cpp
+1 -1
View File
@@ -2114,7 +2114,7 @@ SecondarySourceLocation SMTEncoder::callStackMessage(vector<CallStackEntry> cons
{
SecondarySourceLocation callStackLocation;
solAssert(!_callStack.empty(), "");
callStackLocation.append("Callstack: ", SourceLocation());
callStackLocation.append("Callstack:", SourceLocation());
for (auto const& call: _callStack | boost::adaptors::reversed)
if (call.second)
callStackLocation.append("", call.second->location());
libsolidity/interface/CompilerStack.cpp
+10 -1
View File
@@ -87,6 +87,7 @@ static int g_compilerStackCounts = 0;
CompilerStack::CompilerStack(ReadCallback::Callback _readFile):
m_readFile{std::move(_readFile)},
m_modelCheckerEngine{ModelCheckerEngine::All()},
m_enabledSMTSolvers{smtutil::SMTSolverChoice::All()},
m_errorReporter{m_errorList}
{
@@ -138,6 +139,13 @@ void CompilerStack::setEVMVersion(langutil::EVMVersion _version)
m_evmVersion = _version;
}
void CompilerStack::setModelCheckerEngine(ModelCheckerEngine _engine)
{
if (m_stackState >= ParsedAndImported)
BOOST_THROW_EXCEPTION(CompilerError() << errinfo_comment("Must set enabled model checking engines before parsing."));
m_modelCheckerEngine = _engine;
}
void CompilerStack::setSMTSolverChoice(smtutil::SMTSolverChoice _enabledSMTSolvers)
{
if (m_stackState >= ParsedAndImported)
@@ -207,6 +215,7 @@ void CompilerStack::reset(bool _keepSettings)
m_remappings.clear();
m_libraries.clear();
m_evmVersion = langutil::EVMVersion();
m_modelCheckerEngine = ModelCheckerEngine::All();
m_enabledSMTSolvers = smtutil::SMTSolverChoice::All();
m_generateIR = false;
m_generateEwasm = false;
@@ -443,7 +452,7 @@ bool CompilerStack::analyze()
if (noErrors)
{
ModelChecker modelChecker(m_errorReporter, m_smtlib2Responses, m_readFile, m_enabledSMTSolvers);
ModelChecker modelChecker(m_errorReporter, m_smtlib2Responses, m_modelCheckerEngine, m_readFile, m_enabledSMTSolvers);
for (Source const* source: m_sourceOrder)
if (source->ast)
modelChecker.analyze(*source->ast);
libsolidity/interface/CompilerStack.h
+5
View File
@@ -29,6 +29,8 @@
#include <libsolidity/interface/Version.h>
#include <libsolidity/interface/DebugSettings.h>
#include <libsolidity/formal/ModelChecker.h>
#include <libsmtutil/SolverInterface.h>
#include <liblangutil/ErrorReporter.h>
@@ -165,6 +167,8 @@ public:
/// Must be set before parsing.
void setEVMVersion(langutil::EVMVersion _version = langutil::EVMVersion{});
/// Set which model checking engines should be used.
void setModelCheckerEngine(ModelCheckerEngine _engine);
/// Set which SMT solvers should be enabled.
void setSMTSolverChoice(smtutil::SMTSolverChoice _enabledSolvers);
@@ -452,6 +456,7 @@ private:
RevertStrings m_revertStrings = RevertStrings::Default;
State m_stopAfter = State::CompilationSuccessful;
langutil::EVMVersion m_evmVersion;
ModelCheckerEngine m_modelCheckerEngine;
smtutil::SMTSolverChoice m_enabledSMTSolvers;
std::map<std::string, std::set<std::string>> m_requestedContractNames;
bool m_generateEvmBytecode = true;
libsolidity/interface/StandardCompiler.cpp
+13 -1
View File
@@ -414,7 +414,7 @@ std::optional<Json::Value> checkAuxiliaryInputKeys(Json::Value const& _input)
std::optional<Json::Value> checkSettingsKeys(Json::Value const& _input)
{
static set<string> keys{"parserErrorRecovery", "debug", "evmVersion", "libraries", "metadata", "optimizer", "outputSelection", "remappings", "stopAfter"};
static set<string> keys{"parserErrorRecovery", "debug", "evmVersion", "libraries", "metadata", "optimizer", "outputSelection", "remappings", "stopAfter", "modelCheckerEngine"};
return checkKeys(_input, keys, "settings");
}
@@ -527,6 +527,7 @@ std::optional<Json::Value> checkOutputSelection(Json::Value const& _outputSelect
return std::nullopt;
}
/// Validates the optimizer settings and returns them in a parsed object.
/// On error returns the json-formatted error message.
std::variant<OptimiserSettings, Json::Value> parseOptimizerSettings(Json::Value const& _jsonInput)
@@ -866,6 +867,16 @@ std::variant<StandardCompiler::InputsAndSettings, Json::Value> StandardCompiler:
"Requested output selection conflicts with \"settings.stopAfter\"."
);
if (settings.isMember("modelCheckerEngine"))
{
if (!settings["modelCheckerEngine"].isString())
return formatFatalError("JSONError", "modelCheckerEngine must be a string.");
std::optional<ModelCheckerEngine> engine = ModelCheckerEngine::fromString(settings["modelCheckerEngine"].asString());
if (!engine)
return formatFatalError("JSONError", "Invalid model checker engine requested.");
ret.modelCheckerEngine = *engine;
}
return { std::move(ret) };
}
@@ -886,6 +897,7 @@ Json::Value StandardCompiler::compileSolidity(StandardCompiler::InputsAndSetting
compilerStack.useMetadataLiteralSources(_inputsAndSettings.metadataLiteralSources);
compilerStack.setMetadataHash(_inputsAndSettings.metadataHash);
compilerStack.setRequestedContractNames(requestedContractNames(_inputsAndSettings.outputSelection));
compilerStack.setModelCheckerEngine(_inputsAndSettings.modelCheckerEngine);
compilerStack.enableEvmBytecodeGeneration(isEvmBytecodeRequested(_inputsAndSettings.outputSelection));
compilerStack.enableIRGeneration(isIRRequested(_inputsAndSettings.outputSelection));
libsolidity/interface/StandardCompiler.h
+1
View File
@@ -71,6 +71,7 @@ private:
bool metadataLiteralSources = false;
CompilerStack::MetadataHash metadataHash = CompilerStack::MetadataHash::IPFS;
Json::Value outputSelection;
ModelCheckerEngine modelCheckerEngine = ModelCheckerEngine::All();
};
/// Parses the input json (and potentially invokes the read callback) and either returns