From e691b7402a210281a8a9e397b8b9c5e4f5dc1ea3 Mon Sep 17 00:00:00 2001 From: Daniel Kirchner Date: Wed, 9 Dec 2020 15:15:49 +0100 Subject: [PATCH] Move standard-json "modelCheckerSettings" key to "settings.modelChecker". --- Changelog.md | 1 + docs/using-the-compiler.rst | 20 +++++++++---------- libsolidity/interface/StandardCompiler.cpp | 12 +++++------ scripts/bytecodecompare/prepare_report.py | 6 ++---- scripts/bytecodecompare/storebytecode.sh | 6 ++---- .../input.json | 7 +++++-- .../input.json | 7 +++++-- .../input.json | 7 +++++-- .../input.json | 7 +++++-- .../input.json | 7 +++++-- .../input.json | 9 ++++++--- .../input.json | 9 ++++++--- .../input.json | 9 ++++++--- .../input.json | 7 +++++-- .../output.json | 2 +- 15 files changed, 70 insertions(+), 46 deletions(-) diff --git a/Changelog.md b/Changelog.md index 7d2095bb4..52d7e8234 100644 --- a/Changelog.md +++ b/Changelog.md @@ -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: diff --git a/docs/using-the-compiler.rst b/docs/using-the-compiler.rst index 8504f3e0f..b1ddc76c3 100644 --- a/docs/using-the-compiler.rst +++ b/docs/using-the-compiler.rst @@ -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 + } } } diff --git a/libsolidity/interface/StandardCompiler.cpp b/libsolidity/interface/StandardCompiler.cpp index d46a01701..9bf080b47 100644 --- a/libsolidity/interface/StandardCompiler.cpp +++ b/libsolidity/interface/StandardCompiler.cpp @@ -409,7 +409,7 @@ std::optional checkKeys(Json::Value const& _input, set cons std::optional checkRootKeys(Json::Value const& _input) { - static set keys{"auxiliaryInput", "language", "modelCheckerSettings", "settings", "sources"}; + static set keys{"auxiliaryInput", "language", "settings", "sources"}; return checkKeys(_input, keys, "root"); } @@ -427,14 +427,14 @@ std::optional checkAuxiliaryInputKeys(Json::Value const& _input) std::optional checkSettingsKeys(Json::Value const& _input) { - static set keys{"parserErrorRecovery", "debug", "evmVersion", "libraries", "metadata", "optimizer", "outputSelection", "remappings", "stopAfter", "viaIR"}; + static set keys{"parserErrorRecovery", "debug", "evmVersion", "libraries", "metadata", "modelChecker", "optimizer", "outputSelection", "remappings", "stopAfter", "viaIR"}; return checkKeys(_input, keys, "settings"); } std::optional checkModelCheckerSettingsKeys(Json::Value const& _input) { static set keys{"engine", "timeout"}; - return checkKeys(_input, keys, "modelCheckerSettings"); + return checkKeys(_input, keys, "modelChecker"); } std::optional checkOptimizerKeys(Json::Value const& _input) @@ -892,7 +892,7 @@ std::variant 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: 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 engine = ModelCheckerEngine::fromString(modelCheckerSettings["engine"].asString()); if (!engine) return formatFatalError("JSONError", "Invalid model checker engine requested."); @@ -910,7 +910,7 @@ std::variant 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(); } diff --git a/scripts/bytecodecompare/prepare_report.py b/scripts/bytecodecompare/prepare_report.py index 4f231d2d1..2697b940b 100755 --- a/scripts/bytecodecompare/prepare_report.py +++ b/scripts/bytecodecompare/prepare_report.py @@ -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'] diff --git a/scripts/bytecodecompare/storebytecode.sh b/scripts/bytecodecompare/storebytecode.sh index d9b04ae54..bddc6aa56 100755 --- a/scripts/bytecodecompare/storebytecode.sh +++ b/scripts/bytecodecompare/storebytecode.sh @@ -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))) diff --git a/test/cmdlineTests/standard_model_checker_engine_all/input.json b/test/cmdlineTests/standard_model_checker_engine_all/input.json index 6dbf3647f..e39baccbc 100644 --- a/test/cmdlineTests/standard_model_checker_engine_all/input.json +++ b/test/cmdlineTests/standard_model_checker_engine_all/input.json @@ -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" + } } } diff --git a/test/cmdlineTests/standard_model_checker_engine_bmc/input.json b/test/cmdlineTests/standard_model_checker_engine_bmc/input.json index 7395c5b12..944d64147 100644 --- a/test/cmdlineTests/standard_model_checker_engine_bmc/input.json +++ b/test/cmdlineTests/standard_model_checker_engine_bmc/input.json @@ -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" + } } } diff --git a/test/cmdlineTests/standard_model_checker_engine_chc/input.json b/test/cmdlineTests/standard_model_checker_engine_chc/input.json index 1a46cb917..bda610936 100644 --- a/test/cmdlineTests/standard_model_checker_engine_chc/input.json +++ b/test/cmdlineTests/standard_model_checker_engine_chc/input.json @@ -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" + } } } diff --git a/test/cmdlineTests/standard_model_checker_engine_none/input.json b/test/cmdlineTests/standard_model_checker_engine_none/input.json index a66a757ac..cbb146060 100644 --- a/test/cmdlineTests/standard_model_checker_engine_none/input.json +++ b/test/cmdlineTests/standard_model_checker_engine_none/input.json @@ -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" + } } } diff --git a/test/cmdlineTests/standard_model_checker_timeout_all/input.json b/test/cmdlineTests/standard_model_checker_timeout_all/input.json index a9c901b78..a0de7e267 100644 --- a/test/cmdlineTests/standard_model_checker_timeout_all/input.json +++ b/test/cmdlineTests/standard_model_checker_timeout_all/input.json @@ -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 + } } } diff --git a/test/cmdlineTests/standard_model_checker_timeout_bmc/input.json b/test/cmdlineTests/standard_model_checker_timeout_bmc/input.json index 83441ca59..0cf2c2182 100644 --- a/test/cmdlineTests/standard_model_checker_timeout_bmc/input.json +++ b/test/cmdlineTests/standard_model_checker_timeout_bmc/input.json @@ -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 + } } } diff --git a/test/cmdlineTests/standard_model_checker_timeout_chc/input.json b/test/cmdlineTests/standard_model_checker_timeout_chc/input.json index f88d1745b..2e54455fb 100644 --- a/test/cmdlineTests/standard_model_checker_timeout_chc/input.json +++ b/test/cmdlineTests/standard_model_checker_timeout_chc/input.json @@ -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 + } } } diff --git a/test/cmdlineTests/standard_model_checker_timeout_wrong_key/input.json b/test/cmdlineTests/standard_model_checker_timeout_wrong_key/input.json index 7b1c26f56..b0196d3be 100644 --- a/test/cmdlineTests/standard_model_checker_timeout_wrong_key/input.json +++ b/test/cmdlineTests/standard_model_checker_timeout_wrong_key/input.json @@ -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 + } } } diff --git a/test/cmdlineTests/standard_model_checker_timeout_wrong_value/input.json b/test/cmdlineTests/standard_model_checker_timeout_wrong_value/input.json index 21a5a2e73..86a17c1d9 100644 --- a/test/cmdlineTests/standard_model_checker_timeout_wrong_value/input.json +++ b/test/cmdlineTests/standard_model_checker_timeout_wrong_value/input.json @@ -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" + } } } diff --git a/test/cmdlineTests/standard_model_checker_timeout_wrong_value/output.json b/test/cmdlineTests/standard_model_checker_timeout_wrong_value/output.json index 4bd0dde9a..c3a54e514 100644 --- a/test/cmdlineTests/standard_model_checker_timeout_wrong_value/output.json +++ b/test/cmdlineTests/standard_model_checker_timeout_wrong_value/output.json @@ -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"}]}