Change settings.modelChecker.targets to take an array instead of string

Changelog.md

@@ -18,6 +18,7 @@ Compiler Features:
  * SMTChecker: Report local variables in CHC counterexamples.
  * SMTChecker: Report out of bounds index access for arrays and fixed bytes.
  * Standard JSON: Model checker option ``settings.modelChecker.targets`` also accepts ``outOfBounds``.
+ * Standard JSON: Model checker option ``settings.modelChecker.targets`` takes an array of string targets instead of string of comma separated targets.
  * Yul Optimizer: Added a new step FunctionSpecializer, that specializes a function with its literal arguments.
  * Yul EVM Code Transform: Stack Optimization: Reuse slots of unused function arguments and defer allocating stack slots for return variables until after expression statements and assignments that do not reference them.
  * NatSpec: Allow ``@notice`` tag on non-public state variables and local variable declarations. The documentation will only be part of the AST, under the field ``documentation``.

docs/smtchecker.rst

@@ -448,10 +448,13 @@ the JSON option ``settings.modelChecker.timeout=<time>``, where 0 means no timeo
 Verification Targets
 ====================
 
-The types of verification targets created by the SMTChecker can also be customized via
+The types of verification targets created by the SMTChecker can also be
-the CLI option ``--model-checker-target <targets>`` or the JSON option
+customized via the CLI option ``--model-checker-target <targets>`` or the JSON
-``settings.modelChecker.targets=<targets>``, where ``<targets>`` is a no-space-comma-separated
+option ``settings.modelChecker.targets=<targets>``.
-list of one or more verification targets. The keywords that represent the targets are:
+In the CLI case, ``<targets>`` is a no-space-comma-separated list of one or
+more verification targets, and an array of one or more targets as strings in
+the JSON input.
+The keywords that represent the targets are:
 
 - Assertions: ``assert``.
 - Arithmetic underflow: ``underflow``.
@@ -461,8 +464,7 @@ list of one or more verification targets. The keywords that represent the target
 - Popping an empty array: ``popEmptyArray``.
 - Out of bounds array/fixed bytes index access: ``outOfBounds``.
 - Insufficient funds for a transfer: ``balance``.
-- All of the above: ``all``.
+- All of the above: ``default`` (CLI only).
-- None of the above: ``none``.
 
 A common subset of targets might be, for example:
 ``--model-checker-targets assert,overflow``.

docs/using-the-compiler.rst

@@ -374,16 +374,16 @@ Input Description
             "MyContract": [ "abi", "evm.bytecode.opcodes" ]
           }
         },
+        // The modelChecker object is experimental and subject to changes.
         "modelChecker":
         {
           // Choose which model checker engine to use: all (default), bmc, chc, none.
           "engine": "chc",
-          // Choose which targets should be checked: all (default), constantCondition,
+          // Choose which targets should be checked: constantCondition,
           // underflow, overflow, divByZero, balance, assert, popEmptyArray, outOfBounds.
+          // If the option is not given all targets are checked by default.
           // See the Formal Verification section for the targets description.
-          // Multiple targets can be selected at the same time, separated by a comma
+          "targets": ["underflow", "overflow", "assert"],
-          // without spaces:
-          "targets": "underflow,overflow,assert",
           // Timeout for each SMT query in milliseconds.
           // If this option is not given, the SMTChecker will use a deterministic
           // resource limit by default.

libsolidity/formal/ModelCheckerSettings.cpp

@@ -26,22 +26,22 @@ using namespace ranges;
 using namespace solidity;
 using namespace solidity::frontend;
 
+using TargetType = VerificationTargetType;
+map<string, TargetType> const ModelCheckerTargets::targetStrings{
+	{"constantCondition", TargetType::ConstantCondition},
+	{"underflow", TargetType::Underflow},
+	{"overflow", TargetType::Overflow},
+	{"divByZero", TargetType::DivByZero},
+	{"balance", TargetType::Balance},
+	{"assert", TargetType::Assert},
+	{"popEmptyArray", TargetType::PopEmptyArray},
+	{"outOfBounds", TargetType::OutOfBounds}
+};
+
 std::optional<ModelCheckerTargets> ModelCheckerTargets::fromString(string const& _targets)
 {
-	using TargetType = VerificationTargetType;
-	static map<string, TargetType> const targetStrings{
-		{"constantCondition", TargetType::ConstantCondition},
-		{"underflow", TargetType::Underflow},
-		{"overflow", TargetType::Overflow},
-		{"divByZero", TargetType::DivByZero},
-		{"balance", TargetType::Balance},
-		{"assert", TargetType::Assert},
-		{"popEmptyArray", TargetType::PopEmptyArray},
-		{"outOfBounds", TargetType::OutOfBounds}
-	};
-
 	set<TargetType> chosenTargets;
-	if (_targets == "all")
+	if (_targets == "default")
 		for (auto&& v: targetStrings | views::values)
 			chosenTargets.insert(v);
 	else
@@ -54,3 +54,11 @@ std::optional<ModelCheckerTargets> ModelCheckerTargets::fromString(string const&
 
 	return ModelCheckerTargets{chosenTargets};
 }
+
+bool ModelCheckerTargets::setFromString(string const& _target)
+{
+	if (!targetStrings.count(_target))
+		return false;
+	targets.insert(targetStrings.at(_target));
+	return true;
+}

libsolidity/formal/ModelCheckerSettings.h

@@ -58,12 +58,18 @@ enum class VerificationTargetType { ConstantCondition, Underflow, Overflow, Unde
 
 struct ModelCheckerTargets
 {
-	static ModelCheckerTargets All() { return *fromString("all"); }
+	static ModelCheckerTargets All() { return *fromString("default"); }
-	static ModelCheckerTargets None() { return {}; }
 
 	static std::optional<ModelCheckerTargets> fromString(std::string const& _targets);
 
 	bool has(VerificationTargetType _type) const { return targets.count(_type); }
+
+	/// @returns true if the @p _target is valid,
+	/// and false otherwise.
+	bool setFromString(std::string const& _target);
+
+	static std::map<std::string, VerificationTargetType> const targetStrings;
+
 	std::set<VerificationTargetType> targets;
 };
 

libsolidity/interface/StandardCompiler.cpp

@@ -913,12 +913,23 @@ std::variant<StandardCompiler::InputsAndSettings, Json::Value> StandardCompiler:
 
 	if (modelCheckerSettings.isMember("targets"))
 	{
-		if (!modelCheckerSettings["targets"].isString())
+		auto const& targetsArray = modelCheckerSettings["targets"];
-			return formatFatalError("JSONError", "settings.modelChecker.targets must be a string.");
+		if (!targetsArray.isArray())
-		std::optional<ModelCheckerTargets> targets = ModelCheckerTargets::fromString(modelCheckerSettings["targets"].asString());
+			return formatFatalError("JSONError", "settings.modelChecker.targets must be an array.");
-		if (!targets)
+
-			return formatFatalError("JSONError", "Invalid model checker targets requested.");
+		ModelCheckerTargets targets;
-		ret.modelCheckerSettings.targets = *targets;
+		for (auto const& t: targetsArray)
+		{
+			if (!t.isString())
+				return formatFatalError("JSONError", "Every target in settings.modelChecker.targets must be a string.");
+			if (!targets.setFromString(t.asString()))
+				return formatFatalError("JSONError", "Invalid model checker targets requested.");
+		}
+
+		if (targets.targets.empty())
+			return formatFatalError("JSONError", "settings.modelChecker.targets must be a non-empty array.");
+
+		ret.modelCheckerSettings.targets = targets;
 	}
 
 	if (modelCheckerSettings.isMember("timeout"))

solc/CommandLineInterface.cpp

@@ -1060,7 +1060,7 @@ General Information)").c_str(),
 		)
 		(
 			g_strModelCheckerTargets.c_str(),
-			po::value<string>()->value_name("all,constantCondition,underflow,overflow,divByZero,balance,assert,popEmptyArray,outOfBounds")->default_value("all"),
+			po::value<string>()->value_name("default,constantCondition,underflow,overflow,divByZero,balance,assert,popEmptyArray,outOfBounds")->default_value("default"),
 			"Select model checker verification targets. "
 			"Multiple targets can be selected at the same time, separated by a comma "
 			"and no spaces."

test/cmdlineTests/model_checker_targets_all/args

@@ -1 +1 @@
---model-checker-engine all --model-checker-targets all
+--model-checker-engine all --model-checker-targets default

test/cmdlineTests/model_checker_targets_all_bmc/args

@@ -1 +1 @@
---model-checker-engine bmc --model-checker-targets all
+--model-checker-engine bmc --model-checker-targets default

test/cmdlineTests/model_checker_targets_all_chc/args

@@ -1 +1 @@
---model-checker-engine chc --model-checker-targets all
+--model-checker-engine chc --model-checker-targets default

test/cmdlineTests/standard_model_checker_targets_all/input.json

@@ -23,8 +23,7 @@
 	{
 		"modelChecker":
 		{
-			"engine": "all",
+			"engine": "all"
-			"targets": "all"
 		}
 	}
 }

test/cmdlineTests/standard_model_checker_targets_all_bmc/input.json

@@ -23,8 +23,7 @@
 	{
 		"modelChecker":
 		{
-			"engine": "bmc",
+			"engine": "bmc"
-			"targets": "all"
 		}
 	}
 }

test/cmdlineTests/standard_model_checker_targets_all_chc/input.json

@@ -23,8 +23,7 @@
 	{
 		"modelChecker":
 		{
-			"engine": "chc",
+			"engine": "chc"
-			"targets": "all"
 		}
 	}
 }

test/cmdlineTests/standard_model_checker_targets_assert_bmc/input.json

@@ -24,7 +24,7 @@
 		"modelChecker":
 		{
 			"engine": "bmc",
-			"targets": "assert"
+			"targets": ["assert"]
 		}
 	}
 }

test/cmdlineTests/standard_model_checker_targets_assert_chc/input.json

@@ -24,7 +24,7 @@
 		"modelChecker":
 		{
 			"engine": "chc",
-			"targets": "assert"
+			"targets": ["assert"]
 		}
 	}
 }

test/cmdlineTests/standard_model_checker_targets_balance_bmc/input.json

@@ -24,7 +24,7 @@
 		"modelChecker":
 		{
 			"engine": "bmc",
-			"targets": "balance"
+			"targets": ["balance"]
 		}
 	}
 }

test/cmdlineTests/standard_model_checker_targets_balance_chc/input.json

@@ -24,7 +24,7 @@
 		"modelChecker":
 		{
 			"engine": "chc",
-			"targets": "balance"
+			"targets": ["balance"]
 		}
 	}
 }

test/cmdlineTests/standard_model_checker_targets_constantCondition_bmc/input.json

@@ -24,7 +24,7 @@
 		"modelChecker":
 		{
 			"engine": "bmc",
-			"targets": "constantCondition"
+			"targets": ["constantCondition"]
 		}
 	}
 }

test/cmdlineTests/standard_model_checker_targets_constantCondition_chc/input.json

@@ -24,7 +24,7 @@
 		"modelChecker":
 		{
 			"engine": "chc",
-			"targets": "constantCondition"
+			"targets": ["constantCondition"]
 		}
 	}
 }

test/cmdlineTests/standard_model_checker_targets_div_by_zero_bmc/input.json

@@ -24,7 +24,7 @@
 		"modelChecker":
 		{
 			"engine": "bmc",
-			"targets": "divByZero"
+			"targets": ["divByZero"]
 		}
 	}
 }

test/cmdlineTests/standard_model_checker_targets_div_by_zero_chc/input.json

@@ -24,7 +24,7 @@
 		"modelChecker":
 		{
 			"engine": "chc",
-			"targets": "divByZero"
+			"targets": ["divByZero"]
 		}
 	}
 }

test/cmdlineTests/standard_model_checker_targets_empty_array/input.json

@@ -24,7 +24,7 @@
 		"modelChecker":
 		{
 			"engine": "all",
-			"targets": "aaa,bbb"
+			"targets": []
 		}
 	}
 }

test/cmdlineTests/standard_model_checker_targets_empty_array/output.json

@@ -0,0 +1 @@
+{"errors":[{"component":"general","formattedMessage":"settings.modelChecker.targets must be a non-empty array.","message":"settings.modelChecker.targets must be a non-empty array.","severity":"error","type":"JSONError"}]}

test/cmdlineTests/standard_model_checker_targets_out_of_bounds_bmc/input.json

@@ -24,7 +24,7 @@
 		"modelChecker":
 		{
 			"engine": "bmc",
-			"targets": "outOfBounds"
+			"targets": ["outOfBounds"]
 		}
 	}
 }

test/cmdlineTests/standard_model_checker_targets_out_of_bounds_chc/input.json

@@ -24,7 +24,7 @@
 		"modelChecker":
 		{
 			"engine": "chc",
-			"targets": "outOfBounds"
+			"targets": ["outOfBounds"]
 		}
 	}
 }

test/cmdlineTests/standard_model_checker_targets_overflow_bmc/input.json

@@ -24,7 +24,7 @@
 		"modelChecker":
 		{
 			"engine": "bmc",
-			"targets": "overflow"
+			"targets": ["overflow"]
 		}
 	}
 }

test/cmdlineTests/standard_model_checker_targets_overflow_chc/input.json

@@ -24,7 +24,7 @@
 		"modelChecker":
 		{
 			"engine": "chc",
-			"targets": "overflow"
+			"targets": ["overflow"]
 		}
 	}
 }

test/cmdlineTests/standard_model_checker_targets_pop_empty_bmc/input.json

@@ -24,7 +24,7 @@
 		"modelChecker":
 		{
 			"engine": "bmc",
-			"targets": "popEmptyArray"
+			"targets": ["popEmptyArray"]
 		}
 	}
 }

test/cmdlineTests/standard_model_checker_targets_pop_empty_chc/input.json

@@ -24,7 +24,7 @@
 		"modelChecker":
 		{
 			"engine": "chc",
-			"targets": "popEmptyArray"
+			"targets": ["popEmptyArray"]
 		}
 	}
 }

test/cmdlineTests/standard_model_checker_targets_underflow_bmc/input.json

@@ -24,7 +24,7 @@
 		"modelChecker":
 		{
 			"engine": "bmc",
-			"targets": "underflow"
+			"targets": ["underflow"]
 		}
 	}
 }

test/cmdlineTests/standard_model_checker_targets_underflow_chc/input.json

@@ -24,7 +24,7 @@
 		"modelChecker":
 		{
 			"engine": "chc",
-			"targets": "underflow"
+			"targets": ["underflow"]
 		}
 	}
 }

test/cmdlineTests/standard_model_checker_targets_underflow_overflow_assert_bmc/input.json

@@ -24,7 +24,7 @@
 		"modelChecker":
 		{
 			"engine": "bmc",
-			"targets": "underflow,overflow,assert"
+			"targets": ["underflow", "overflow", "assert"]
 		}
 	}
 }

test/cmdlineTests/standard_model_checker_targets_underflow_overflow_assert_chc/input.json

@@ -24,7 +24,7 @@
 		"modelChecker":
 		{
 			"engine": "chc",
-			"targets": "underflow,overflow,assert"
+			"targets": ["underflow", "overflow", "assert"]
 		}
 	}
 }

test/cmdlineTests/standard_model_checker_targets_underflow_overflow_bmc/input.json

@@ -24,7 +24,7 @@
 		"modelChecker":
 		{
 			"engine": "bmc",
-			"targets": "underflow,overflow"
+			"targets": ["underflow", "overflow"]
 		}
 	}
 }

test/cmdlineTests/standard_model_checker_targets_underflow_overflow_chc/input.json

@@ -24,7 +24,7 @@
 		"modelChecker":
 		{
 			"engine": "chc",
-			"targets": "underflow,overflow"
+			"targets": ["underflow", "overflow"]
 		}
 	}
 }

test/cmdlineTests/standard_model_checker_targets_wrong_target_types/input.json

@@ -0,0 +1,30 @@
+{
+	"language": "Solidity",
+	"sources":
+	{
+		"A":
+		{
+			"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test {
+					uint[] arr;
+					function f(address payable a, uint x) public {
+						require(x >= 0);
+						--x;
+						x + type(uint).max;
+						2 / x;
+						a.transfer(x);
+						assert(x > 0);
+						arr.pop();
+						arr[x];
+					}
+				}"
+		}
+	},
+	"settings":
+	{
+		"modelChecker":
+		{
+			"engine": "all",
+			"targets": [2]
+		}
+	}
+}

test/cmdlineTests/standard_model_checker_targets_wrong_target_types/output.json

@@ -0,0 +1 @@
+{"errors":[{"component":"general","formattedMessage":"Every target in settings.modelChecker.targets must be a string.","message":"Every target in settings.modelChecker.targets must be a string.","severity":"error","type":"JSONError"}]}

test/cmdlineTests/standard_model_checker_targets_wrong_target_types_2/input.json

@@ -0,0 +1,30 @@
+{
+	"language": "Solidity",
+	"sources":
+	{
+		"A":
+		{
+			"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test {
+					uint[] arr;
+					function f(address payable a, uint x) public {
+						require(x >= 0);
+						--x;
+						x + type(uint).max;
+						2 / x;
+						a.transfer(x);
+						assert(x > 0);
+						arr.pop();
+						arr[x];
+					}
+				}"
+		}
+	},
+	"settings":
+	{
+		"modelChecker":
+		{
+			"engine": "all",
+			"targets": "assert"
+		}
+	}
+}

test/cmdlineTests/standard_model_checker_targets_wrong_target_types_2/output.json

@@ -0,0 +1 @@
+{"errors":[{"component":"general","formattedMessage":"settings.modelChecker.targets must be an array.","message":"settings.modelChecker.targets must be an array.","severity":"error","type":"JSONError"}]}

test/cmdlineTests/standard_model_checker_targets_wrong_targets/input.json

@@ -0,0 +1,30 @@
+{
+	"language": "Solidity",
+	"sources":
+	{
+		"A":
+		{
+			"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test {
+					uint[] arr;
+					function f(address payable a, uint x) public {
+						require(x >= 0);
+						--x;
+						x + type(uint).max;
+						2 / x;
+						a.transfer(x);
+						assert(x > 0);
+						arr.pop();
+						arr[x];
+					}
+				}"
+		}
+	},
+	"settings":
+	{
+		"modelChecker":
+		{
+			"engine": "all",
+			"targets": ["aaa", "bbb"]
+		}
+	}
+}