Merge pull request #11256 from ethereum/smt_target_array

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

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",
-			"targets": "all"
+			"engine": "all"
 		}
 	}
 }

test/cmdlineTests/standard_model_checker_targets_all_bmc/input.json

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

test/cmdlineTests/standard_model_checker_targets_all_chc/input.json

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

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