Merge pull request #10545 from ethereum/modelCheckerSettingsMove

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

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:

docs/using-the-compiler.rst

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

libsolidity/interface/StandardCompiler.cpp

@@ -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();
 	}
 

scripts/bytecodecompare/prepare_report.py

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

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'] } }
+                    outputSelection: { '*': { '*': ['evm.bytecode.object', 'metadata'] } },
-                },
+                    "modelChecker": { "engine": "none" }
-                "modelCheckerSettings": {
-                    "engine": "none"
                 }
             }
             var result = JSON.parse(compiler.compile(JSON.stringify(input)))

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"
+		}
 	}
 }

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"
+		}
 	}
 }

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"
+		}
 	}
 }

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"
+		}
 	}
 }

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
+		}
 	}
 }

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",
+		"modelChecker":
-		"timeout": 1000
+		{
+			"engine": "bmc",
+			"timeout": 1000
+		}
 	}
 }

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",
+		"modelChecker":
-		"timeout": 1000
+		{
+			"engine": "chc",
+			"timeout": 1000
+		}
 	}
 }

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",
+		"modelChecker":
-		"atimeout": 1
+		{
+			"engine": "chc",
+			"atimeout": 1
+		}
 	}
 }

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"
+		}
 	}
 }

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"}]}