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 for smtchecker trusted external calls

Browse Source
This commit is contained in:
Leo Alt 2021-10-12 11:32:02 +02:00
parent d4e4189a85
commit 397bd7da4f
2 changed files with 28 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
libsolidity/interface/StandardCompiler.cpp
View File

@ -445,7 +445,7 @@ std::optional<Json::Value> checkSettingsKeys(Json::Value const& _input)
std::optional<Json::Value> checkModelCheckerSettingsKeys(Json::Value const& _input)
{
static set<string> keys{"contracts", "divModNoSlacks", "engine", "invariants", "showUnproved", "solvers", "targets", "timeout"};
static set<string> keys{"contracts", "divModNoSlacks", "engine", "extCalls", "invariants", "showUnproved", "solvers", "targets", "timeout"};
return checkKeys(_input, keys, "modelChecker");
}
@ -987,6 +987,16 @@ std::variant<StandardCompiler::InputsAndSettings, Json::Value> StandardCompiler:
ret.modelCheckerSettings.engine = *engine;
}
if (modelCheckerSettings.isMember("extCalls"))
{
if (!modelCheckerSettings["extCalls"].isString())
return formatFatalError("JSONError", "settings.modelChecker.extCalls must be a string.");
std::optional<ModelCheckerExtCalls> extCalls = ModelCheckerExtCalls::fromString(modelCheckerSettings["extCalls"].asString());
if (!extCalls)
return formatFatalError("JSONError", "Invalid model checker extCalls requested.");
ret.modelCheckerSettings.externalCalls = *extCalls;
}
if (modelCheckerSettings.isMember("invariants"))
{
auto const& invariantsArray = modelCheckerSettings["invariants"];

17
solc/CommandLineParser.cpp
View File

@ -67,6 +67,7 @@ static string const g_strMetadataLiteral = "metadata-literal";
static string const g_strModelCheckerContracts = "model-checker-contracts";
static string const g_strModelCheckerDivModNoSlacks = "model-checker-div-mod-no-slacks";
static string const g_strModelCheckerEngine = "model-checker-engine";
static string const g_strModelCheckerExtCalls = "model-checker-ext-calls";
static string const g_strModelCheckerInvariants = "model-checker-invariants";
static string const g_strModelCheckerShowUnproved = "model-checker-show-unproved";
static string const g_strModelCheckerSolvers = "model-checker-solvers";
@ -800,6 +801,12 @@ General Information)").c_str(),
po::value<string>()->value_name("all,bmc,chc,none")->default_value("none"),
"Select model checker engine."
)
(
g_strModelCheckerExtCalls.c_str(),
po::value<string>()->value_name("untrusted,trusted")->default_value("untrusted"),
"Select whether to assume (trusted) that external calls always invoke"
" the code given by the type of the contract, if that code is available."
)
(
g_strModelCheckerInvariants.c_str(),
po::value<string>()->value_name("default,all,contract,reentrancy")->default_value("default"),
@ -1219,6 +1226,15 @@ void CommandLineParser::processArgs()
m_options.modelChecker.settings.engine = *engine;
}
if (m_args.count(g_strModelCheckerExtCalls))
{
string mode = m_args[g_strModelCheckerExtCalls].as<string>();
optional<ModelCheckerExtCalls> extCallsMode = ModelCheckerExtCalls::fromString(mode);
if (!extCallsMode)
solThrow(CommandLineValidationError, "Invalid option for --" + g_strModelCheckerExtCalls + ": " + mode);
m_options.modelChecker.settings.externalCalls = *extCallsMode;
}
if (m_args.count(g_strModelCheckerInvariants))
{
string invsStr = m_args[g_strModelCheckerInvariants].as<string>();
@ -1257,6 +1273,7 @@ void CommandLineParser::processArgs()
m_args.count(g_strModelCheckerContracts) ||
m_args.count(g_strModelCheckerDivModNoSlacks) ||
m_args.count(g_strModelCheckerEngine) ||
m_args.count(g_strModelCheckerExtCalls) ||
m_args.count(g_strModelCheckerInvariants) ||
m_args.count(g_strModelCheckerShowUnproved) ||
m_args.count(g_strModelCheckerSolvers) ||