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

Move standard-json "modelCheckerSettings" key to "settings.modelChecker".

Browse Source
This commit is contained in:
Daniel Kirchner 2020-12-09 15:15:49 +01:00
parent 44b7301048
commit e691b7402a
15 changed files with 70 additions and 46 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -13,6 +13,7 @@ Compiler Features:
* SMTChecker: Support getters.
* SMTChecker: Support named arguments in function calls.
* SMTChecker: Support struct constructor.
* Standard-Json: Move the recently introduced ``modelCheckerSettings`` key to ``settings.modelChecker``.
* Standard-Json: Properly filter the requested output artifacts.
Bugfixes:

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

@ -369,16 +369,16 @@ Input Description
"MyContract": [ "abi", "evm.bytecode.opcodes" ]
}
},
},
"modelCheckerSettings":
{
// Choose which model checker engine to use: all (default), bmc, chc, none.
"engine": "chc",
// Timeout for each SMT query in milliseconds.
// If this option is not given, the SMTChecker will use a deterministic
// resource limit by default.
// A given timeout of 0 means no resource/time restrictions for any query.
"timeout": 20000
"modelChecker":
{
// Choose which model checker engine to use: all (default), bmc, chc, none.
"engine": "chc",
// Timeout for each SMT query in milliseconds.
// If this option is not given, the SMTChecker will use a deterministic
// resource limit by default.
// A given timeout of 0 means no resource/time restrictions for any query.
"timeout": 20000
}
}
}

12
libsolidity/interface/StandardCompiler.cpp
View File

@ -409,7 +409,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", "modelCheckerSettings", "settings", "sources"};
static set<string> keys{"auxiliaryInput", "language", "settings", "sources"};
return checkKeys(_input, keys, "root");
}
@ -427,14 +427,14 @@ 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", "viaIR"};
static set<string> keys{"parserErrorRecovery", "debug", "evmVersion", "libraries", "metadata", "modelChecker", "optimizer", "outputSelection", "remappings", "stopAfter", "viaIR"};
return checkKeys(_input, keys, "settings");
}
std::optional<Json::Value> checkModelCheckerSettingsKeys(Json::Value const& _input)
{
static set<string> keys{"engine", "timeout"};
return checkKeys(_input, keys, "modelCheckerSettings");
return checkKeys(_input, keys, "modelChecker");
}
std::optional<Json::Value> checkOptimizerKeys(Json::Value const& _input)
@ -892,7 +892,7 @@ std::variant<StandardCompiler::InputsAndSettings, Json::Value> StandardCompiler:
"Requested output selection conflicts with \"settings.stopAfter\"."
);
Json::Value const& modelCheckerSettings = _input.get("modelCheckerSettings", Json::Value());
Json::Value const& modelCheckerSettings = settings.get("modelChecker", Json::Value());
if (auto result = checkModelCheckerSettingsKeys(modelCheckerSettings))
return *result;
@ -900,7 +900,7 @@ std::variant<StandardCompiler::InputsAndSettings, Json::Value> StandardCompiler:
if (modelCheckerSettings.isMember("engine"))
{
if (!modelCheckerSettings["engine"].isString())
return formatFatalError("JSONError", "modelCheckerSettings.engine must be a string.");
return formatFatalError("JSONError", "settings.modelChecker.engine must be a string.");
std::optional<ModelCheckerEngine> engine = ModelCheckerEngine::fromString(modelCheckerSettings["engine"].asString());
if (!engine)
return formatFatalError("JSONError", "Invalid model checker engine requested.");
@ -910,7 +910,7 @@ std::variant<StandardCompiler::InputsAndSettings, Json::Value> StandardCompiler:
if (modelCheckerSettings.isMember("timeout"))
{
if (!modelCheckerSettings["timeout"].isUInt())
return formatFatalError("JSONError", "modelCheckerSettings.timeout must be an unsigned integer.");
return formatFatalError("JSONError", "settings.modelChecker.timeout must be an unsigned integer.");
ret.modelCheckerSettings.timeout = modelCheckerSettings["timeout"].asUInt();
}

6
scripts/bytecodecompare/prepare_report.py
View File

@ -19,10 +19,8 @@ for optimize in [False, True]:
'optimizer': {
'enabled': optimize
},
'outputSelection': {'*': {'*': ['evm.bytecode.object', 'metadata']}}
},
'modelCheckerSettings': {
"engine": 'none'
'outputSelection': {'*': {'*': ['evm.bytecode.object', 'metadata']}},
'modelChecker': { "engine": 'none' }
}
}
args = [SOLC_BIN, '--standard-json']

6
scripts/bytecodecompare/storebytecode.sh
View File

@ -66,10 +66,8 @@ for (var optimize of [false, true])
sources: inputs,
settings: {
optimizer: { enabled: optimize },
outputSelection: { '*': { '*': ['evm.bytecode.object', 'metadata'] } }
},
"modelCheckerSettings": {
"engine": "none"
outputSelection: { '*': { '*': ['evm.bytecode.object', 'metadata'] } },
"modelChecker": { "engine": "none" }
}
}
var result = JSON.parse(compiler.compile(JSON.stringify(input)))

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

@ -7,8 +7,11 @@
"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); } }"
}
},
"modelCheckerSettings":
"settings":
{
"engine": "all"
"modelChecker":
{
"engine": "all"
}
}
}

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

@ -7,8 +7,11 @@
"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); } }"
}
},
"modelCheckerSettings":
"settings":
{
"engine": "bmc"
"modelChecker":
{
"engine": "bmc"
}
}
}

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

@ -7,8 +7,11 @@
"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); } }"
}
},
"modelCheckerSettings":
"settings":
{
"engine": "chc"
"modelChecker":
{
"engine": "chc"
}
}
}

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

@ -7,8 +7,11 @@
"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); } }"
}
},
"modelCheckerSettings":
"settings":
{
"engine": "none"
"modelChecker":
{
"engine": "none"
}
}
}

7
test/cmdlineTests/standard_model_checker_timeout_all/input.json
View File

@ -7,8 +7,11 @@
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {\nfunction f(uint x, uint y, uint k) public pure {\nrequire(k > 0); require(x % k == 0); require(y % k == 0); uint r = mulmod(x, y, k); assert(r % k == 0);}}"
}
},
"modelCheckerSettings":
"settings":
{
"timeout": 1000
"modelChecker":
{
"timeout": 1000
}
}
}

9
test/cmdlineTests/standard_model_checker_timeout_bmc/input.json
View File

@ -7,9 +7,12 @@
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {\nfunction f(uint x, uint y, uint k) public pure {\nrequire(k > 0); require(x % k == 0); require(y % k == 0); uint r = mulmod(x, y, k); assert(r % k == 0);}}"
}
},
"modelCheckerSettings":
"settings":
{
"engine": "bmc",
"timeout": 1000
"modelChecker":
{
"engine": "bmc",
"timeout": 1000
}
}
}

9
test/cmdlineTests/standard_model_checker_timeout_chc/input.json
View File

@ -7,9 +7,12 @@
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {\nfunction f(uint x, uint y, uint k) public pure {\nrequire(k > 0); require(x % k == 0); require(y % k == 0); uint r = mulmod(x, y, k); assert(r % k == 0);}}"
}
},
"modelCheckerSettings":
"settings":
{
"engine": "chc",
"timeout": 1000
"modelChecker":
{
"engine": "chc",
"timeout": 1000
}
}
}

9
test/cmdlineTests/standard_model_checker_timeout_wrong_key/input.json
View File

@ -7,9 +7,12 @@
"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); } }"
}
},
"modelCheckerSettings":
"settings":
{
"engine": "chc",
"atimeout": 1
"modelChecker":
{
"engine": "chc",
"atimeout": 1
}
}
}

7
test/cmdlineTests/standard_model_checker_timeout_wrong_value/input.json
View File

@ -7,8 +7,11 @@
"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); } }"
}
},
"modelCheckerSettings":
"settings":
{
"timeout": "asd"
"modelChecker":
{
"timeout": "asd"
}
}
}

2
test/cmdlineTests/standard_model_checker_timeout_wrong_value/output.json
View File

@ -1 +1 @@
{"errors":[{"component":"general","formattedMessage":"modelCheckerSettings.timeout must be an unsigned integer.","message":"modelCheckerSettings.timeout must be an unsigned integer.","severity":"error","type":"JSONError"}]}
{"errors":[{"component":"general","formattedMessage":"settings.modelChecker.timeout must be an unsigned integer.","message":"settings.modelChecker.timeout must be an unsigned integer.","severity":"error","type":"JSONError"}]}