cerc-io/solidity
10
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 invariants option to CLI and JSON

Browse Source
This commit is contained in:
Leo Alt 2021-10-06 11:51:22 +02:00
parent d419c30ca6
commit 3118fb3666
2 changed files with 43 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

23
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) std::optional<Json::Value> checkModelCheckerSettingsKeys(Json::Value const& _input)
{ {
static set<string> keys{"contracts", "divModNoSlacks", "engine", "showUnproved", "solvers", "targets", "timeout"}; static set<string> keys{"contracts", "divModNoSlacks", "engine", "invariants", "showUnproved", "solvers", "targets", "timeout"};
return checkKeys(_input, keys, "modelChecker"); return checkKeys(_input, keys, "modelChecker");
} }
@ -987,6 +987,27 @@ std::variant<StandardCompiler::InputsAndSettings, Json::Value> StandardCompiler:
ret.modelCheckerSettings.engine = *engine; ret.modelCheckerSettings.engine = *engine;
} }
if (modelCheckerSettings.isMember("invariants"))
{
auto const& invariantsArray = modelCheckerSettings["invariants"];
if (!invariantsArray.isArray())
return formatFatalError("JSONError", "settings.modelChecker.invariants must be an array.");
ModelCheckerInvariants invariants;
for (auto const& i: invariantsArray)
{
if (!i.isString())
return formatFatalError("JSONError", "Every invariant type in settings.modelChecker.invariants must be a string.");
if (!invariants.setFromString(i.asString()))
return formatFatalError("JSONError", "Invalid model checker invariants requested.");
}
if (invariants.invariants.empty())
return formatFatalError("JSONError", "settings.modelChecker.invariants must be a non-empty array.");
ret.modelCheckerSettings.invariants = invariants;
}
if (modelCheckerSettings.isMember("showUnproved")) if (modelCheckerSettings.isMember("showUnproved"))
{ {
auto const& showUnproved = modelCheckerSettings["showUnproved"]; auto const& showUnproved = modelCheckerSettings["showUnproved"];

21
solc/CommandLineParser.cpp
View File

@ -78,6 +78,7 @@ static string const g_strMetadataLiteral = "metadata-literal";
static string const g_strModelCheckerContracts = "model-checker-contracts"; static string const g_strModelCheckerContracts = "model-checker-contracts";
static string const g_strModelCheckerDivModNoSlacks = "model-checker-div-mod-no-slacks"; static string const g_strModelCheckerDivModNoSlacks = "model-checker-div-mod-no-slacks";
static string const g_strModelCheckerEngine = "model-checker-engine"; static string const g_strModelCheckerEngine = "model-checker-engine";
static string const g_strModelCheckerInvariants = "model-checker-invariants";
static string const g_strModelCheckerShowUnproved = "model-checker-show-unproved"; static string const g_strModelCheckerShowUnproved = "model-checker-show-unproved";
static string const g_strModelCheckerSolvers = "model-checker-solvers"; static string const g_strModelCheckerSolvers = "model-checker-solvers";
static string const g_strModelCheckerTargets = "model-checker-targets"; static string const g_strModelCheckerTargets = "model-checker-targets";
@ -801,6 +802,13 @@ General Information)").c_str(),
po::value<string>()->value_name("all,bmc,chc,none")->default_value("none"), po::value<string>()->value_name("all,bmc,chc,none")->default_value("none"),
"Select model checker engine." "Select model checker engine."
) )
(
g_strModelCheckerInvariants.c_str(),
po::value<string>()->value_name("default,all,contract,reentrancy")->default_value("default"),
"Select whether to report inferred contract inductive invariants."
" Multiple types of invariants can be selected at the same time, separated by a comma and no spaces."
" By default no invariants are reported."
)
( (
g_strModelCheckerShowUnproved.c_str(), g_strModelCheckerShowUnproved.c_str(),
"Show all unproved targets separately." "Show all unproved targets separately."
@ -1253,6 +1261,18 @@ bool CommandLineParser::processArgs()
m_options.modelChecker.settings.engine = *engine; m_options.modelChecker.settings.engine = *engine;
} }
if (m_args.count(g_strModelCheckerInvariants))
{
string invsStr = m_args[g_strModelCheckerInvariants].as<string>();
optional<ModelCheckerInvariants> invs = ModelCheckerInvariants::fromString(invsStr);
if (!invs)
{
serr() << "Invalid option for --" << g_strModelCheckerInvariants << ": " << invsStr << endl;
return false;
}
m_options.modelChecker.settings.invariants = *invs;
}
if (m_args.count(g_strModelCheckerShowUnproved)) if (m_args.count(g_strModelCheckerShowUnproved))
m_options.modelChecker.settings.showUnproved = true; m_options.modelChecker.settings.showUnproved = true;
@ -1288,6 +1308,7 @@ bool CommandLineParser::processArgs()
m_args.count(g_strModelCheckerContracts) || m_args.count(g_strModelCheckerContracts) ||
m_args.count(g_strModelCheckerDivModNoSlacks) || m_args.count(g_strModelCheckerDivModNoSlacks) ||
m_args.count(g_strModelCheckerEngine) || m_args.count(g_strModelCheckerEngine) ||
m_args.count(g_strModelCheckerInvariants) ||
m_args.count(g_strModelCheckerShowUnproved) || m_args.count(g_strModelCheckerShowUnproved) ||
m_args.count(g_strModelCheckerSolvers) || m_args.count(g_strModelCheckerSolvers) ||
m_args.count(g_strModelCheckerTargets) || m_args.count(g_strModelCheckerTargets) ||