Merge pull request #10064 from ethereum/smt_engine

Move modelCheckerSettings out of settings in StandardCompiler

Author: chriseth

Changelog.md

@@ -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:

docs/using-the-compiler.rst

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

libsolidity/interface/StandardCompiler.cpp

@@ -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;

test/cmdlineTests/standard_model_checker_engine_all/input.json

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

test/cmdlineTests/standard_model_checker_engine_bmc/input.json

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

test/cmdlineTests/standard_model_checker_engine_chc/input.json

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

test/cmdlineTests/standard_model_checker_engine_none/input.json

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