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

Merge pull request #10064 from ethereum/smt_engine

Browse Source 
Move modelCheckerSettings out of settings in StandardCompiler
This commit is contained in:
chriseth 2020-10-19 13:37:14 +02:00 committed by GitHub
commit df24a4eb5a
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
7 changed files with 30 additions and 16 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Changelog.md
View File

@ -14,7 +14,7 @@ Compiler Features:
* SMTChecker: Support ``keccak256``, ``sha256``, ``ripemd160`` and ``ecrecover`` in the CHC engine.
* Control Flow Graph: Print warning for non-empty functions with unnamed return parameters that are not assigned a value in all code paths.
* Command Line Interface: New option ``model-checker-engine`` allows to choose a specific SMTChecker engine. Options are ``all`` (default), ``bmc``, ``chc`` and ``none``.
* Standard JSON: New option ``settings.modelCheckerEngine`` allows to choose a specific SMTChecker engine. Options are ``all`` (default), ``bmc``, ``chc`` and ``none``.
* Standard JSON: New option ``modelCheckerSettings.engine`` allows to choose a specific SMTChecker engine. Options are ``all`` (default), ``bmc``, ``chc`` and ``none``.
Bugfixes:

5
docs/using-the-compiler.rst
View File

@ -342,8 +342,11 @@ Input Description
"MyContract": [ "abi", "evm.bytecode.opcodes" ]
}
},
},
"modelCheckerSettings":
{
// Choose which model checker engine to use: all (default), bmc, chc, none.
"modelCheckerEngine": "chc"
"engine": "chc"
}
}

23
libsolidity/interface/StandardCompiler.cpp
View File

@ -396,7 +396,7 @@ std::optional<Json::Value> checkKeys(Json::Value const& _input, set<string> cons
std::optional<Json::Value> checkRootKeys(Json::Value const& _input)
{
static set<string> keys{"auxiliaryInput", "language", "settings", "sources"};
static set<string> keys{"auxiliaryInput", "language", "modelCheckerSettings", "settings", "sources"};
return checkKeys(_input, keys, "root");
}
@ -414,10 +414,16 @@ 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", "modelCheckerEngine"};
static set<string> keys{"parserErrorRecovery", "debug", "evmVersion", "libraries", "metadata", "optimizer", "outputSelection", "remappings", "stopAfter"};
return checkKeys(_input, keys, "settings");
}
std::optional<Json::Value> checkModelCheckerSettingsKeys(Json::Value const& _input)
{
static set<string> keys{"engine"};
return checkKeys(_input, keys, "modelCheckerSettings");
}
std::optional<Json::Value> checkOptimizerKeys(Json::Value const& _input)
{
static set<string> keys{"details", "enabled", "runs"};
@ -867,11 +873,16 @@ std::variant<StandardCompiler::InputsAndSettings, Json::Value> StandardCompiler:
"Requested output selection conflicts with \"settings.stopAfter\"."
);
if (settings.isMember("modelCheckerEngine"))
Json::Value const& modelCheckerSettings = _input.get("modelCheckerSettings", Json::Value());
if (auto result = checkModelCheckerSettingsKeys(modelCheckerSettings))
return *result;
if (modelCheckerSettings.isMember("engine"))
{
if (!settings["modelCheckerEngine"].isString())
return formatFatalError("JSONError", "modelCheckerEngine must be a string.");
std::optional<ModelCheckerEngine> engine = ModelCheckerEngine::fromString(settings["modelCheckerEngine"].asString());
if (!modelCheckerSettings["engine"].isString())
return formatFatalError("JSONError", "modelCheckerSettings.engine must be a string.");
std::optional<ModelCheckerEngine> engine = ModelCheckerEngine::fromString(modelCheckerSettings["engine"].asString());
if (!engine)
return formatFatalError("JSONError", "Invalid model checker engine requested.");
ret.modelCheckerEngine = *engine;

4
test/cmdlineTests/standard_model_checker_engine_all/input.json
View File

@ -7,8 +7,8 @@
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract C { function f(uint x) public pure { assert(x > 0); } }"
}
},
"settings":
"modelCheckerSettings":
{
"modelCheckerEngine": "all"
"engine": "all"
}
}

4
test/cmdlineTests/standard_model_checker_engine_bmc/input.json
View File

@ -7,8 +7,8 @@
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract C { function f(uint x) public pure { assert(x > 0); } }"
}
},
"settings":
"modelCheckerSettings":
{
"modelCheckerEngine": "bmc"
"engine": "bmc"
}
}

4
test/cmdlineTests/standard_model_checker_engine_chc/input.json
View File

@ -7,8 +7,8 @@
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract C { function f(uint x) public pure { assert(x > 0); } }"
}
},
"settings":
"modelCheckerSettings":
{
"modelCheckerEngine": "chc"
"engine": "chc"
}
}

4
test/cmdlineTests/standard_model_checker_engine_none/input.json
View File

@ -7,8 +7,8 @@
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract C { function f(uint x) public pure { assert(x > 0); } }"
}
},
"settings":
"modelCheckerSettings":
{
"modelCheckerEngine": "none"
"engine": "none"
}
}