Merge pull request #11755 from ethereum/smt_default_no_overflow

[SMTChecker] Do not create targets for underoverflow by default for Sol >=0.8

Author: Leonardo

Changelog.md

@@ -11,6 +11,7 @@ Compiler Features:
  * Commandline Interface: option ``--pretty-json`` works also with ``--standard--json``.
  * SMTChecker: Unproved targets are hidden by default, and the SMTChecker only states how many unproved targets there are. They can be listed using the command line option ``--model-checker-show-unproved`` or the JSON option ``settings.modelChecker.showUnproved``.
  * SMTChecker: new setting to enable/disable encoding of division and modulo with slack variables. The command line option is ``--model-checker-div-mod-slacks`` and the JSON option is ``settings.modelChecker.divModWithSlacks``.
+ * SMTChecker: Do not check underflow and overflow by default.
 
 
 Bugfixes:

docs/smtchecker.rst

@@ -34,6 +34,9 @@ The other verification targets that the SMTChecker checks at compile time are:
 - Out of bounds index access.
 - Insufficient funds for a transfer.
 
+All the targets above are automatically checked by default if all engines are
+enabled, except underflow and overflow for Solidity >=0.8.7.
+
 The potential warnings that the SMTChecker reports are:
 
 - ``<failing  property> happens here.``. This means that the SMTChecker proved that a certain property fails. A counterexample may be given, however in complex situations it may also not show a counterexample. This result may also be a false positive in certain cases, when the SMT encoding adds abstractions for Solidity code that is either hard or impossible to express.
@@ -93,8 +96,10 @@ Overflow
     }
 
 The contract above shows an overflow check example.
-The SMTChecker will, by default, check every reachable arithmetic operation
-in the contract for potential underflow and overflow.
+The SMTChecker does not check underflow and overflow by default for Solidity >=0.8.7,
+so we need to use the command line option ``--model-checker-targets "underflow,overflow"``
+or the JSON option ``settings.modelChecker.targets = ["underflow", "overflow"]``.
+See :ref:`this section for targets configuration<smtchecker_targets>`.
 Here, it reports the following:
 
 .. code-block:: text
@@ -447,6 +452,8 @@ If the SMTChecker does not manage to solve the contract properties with the defa
 a timeout can be given in milliseconds via the CLI option ``--model-checker-timeout <time>`` or
 the JSON option ``settings.modelChecker.timeout=<time>``, where 0 means no timeout.
 
+.. _smtchecker_targets:
+
 Verification Targets
 ====================
 
@@ -471,6 +478,8 @@ The keywords that represent the targets are:
 A common subset of targets might be, for example:
 ``--model-checker-targets assert,overflow``.
 
+All targets are checked by default, except underflow and overflow for Solidity >=0.8.7.
+
 There is no precise heuristic on how and when to split verification targets,
 but it can be useful especially when dealing with large contracts.
 

docs/using-the-compiler.rst

@@ -415,7 +415,8 @@ Input Description
           "solvers": ["cvc4", "smtlib2", "z3"],
           // 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.
+          // If the option is not given all targets are checked by default,
+          // except underflow/overflow for Solidity >=0.8.7.
           // See the Formal Verification section for the targets description.
           "targets": ["underflow", "overflow", "assert"],
           // Timeout for each SMT query in milliseconds.

libsolidity/formal/ModelCheckerSettings.cpp

@@ -40,9 +40,16 @@ map<string, TargetType> const ModelCheckerTargets::targetStrings{
 std::optional<ModelCheckerTargets> ModelCheckerTargets::fromString(string const& _targets)
 {
 	set<TargetType> chosenTargets;
-	if (_targets == "default")
+	if (_targets == "default" || _targets == "all")
+	{
+		bool all = _targets == "all";
 		for (auto&& v: targetStrings | ranges::views::values)
+		{
+			if (!all && (v == TargetType::Underflow || v == TargetType::Overflow))
+				continue;
 			chosenTargets.insert(v);
+		}
+	}
 	else
 		for (auto&& t: _targets | ranges::views::split(',') | ranges::to<vector<string>>())
 		{

libsolidity/formal/ModelCheckerSettings.h

@@ -91,7 +91,10 @@ enum class VerificationTargetType { ConstantCondition, Underflow, Overflow, Unde
 
 struct ModelCheckerTargets
 {
+	/// Adds the default targets, that is, all except underflow and overflow.
 	static ModelCheckerTargets Default() { return *fromString("default"); }
+	/// Adds all targets, including underflow and overflow.
+	static ModelCheckerTargets All() { return *fromString("all"); }
 
 	static std::optional<ModelCheckerTargets> fromString(std::string const& _targets);
 

solc/CommandLineParser.cpp

@@ -743,10 +743,10 @@ General Information)").c_str(),
 		)
 		(
 			g_strModelCheckerTargets.c_str(),
-			po::value<string>()->value_name("default,constantCondition,underflow,overflow,divByZero,balance,assert,popEmptyArray,outOfBounds")->default_value("default"),
+			po::value<string>()->value_name("default,all,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."
+			"Multiple targets can be selected at the same time, separated by a comma and no spaces."
+			" By default all targets except underflow and overflow are selected."
 		)
 		(
 			g_strModelCheckerTimeout.c_str(),

test/cmdlineTests/model_checker_targets_all_all_engines/args

@@ -0,0 +1 @@
+--model-checker-engine all --model-checker-targets all

test/cmdlineTests/model_checker_targets_all/err renamed to test/cmdlineTests/model_checker_targets_all_all_engines/err

@@ -8,7 +8,7 @@ Transaction trace:
 test.constructor()
 State: arr = []
 test.f(0, 0)
- --> model_checker_targets_all/input.sol:7:3:
+ --> model_checker_targets_all_all_engines/input.sol:7:3:
   |
 7 | 		--x;
   | 		^^^
@@ -23,7 +23,7 @@ Transaction trace:
 test.constructor()
 State: arr = []
 test.f(0, 2)
- --> model_checker_targets_all/input.sol:8:3:
+ --> model_checker_targets_all_all_engines/input.sol:8:3:
   |
 8 | 		x + type(uint).max;
   | 		^^^^^^^^^^^^^^^^^^
@@ -38,7 +38,7 @@ Transaction trace:
 test.constructor()
 State: arr = []
 test.f(0, 1)
- --> model_checker_targets_all/input.sol:9:3:
+ --> model_checker_targets_all_all_engines/input.sol:9:3:
   |
 9 | 		2 / x;
   | 		^^^^^
@@ -53,7 +53,7 @@ Transaction trace:
 test.constructor()
 State: arr = []
 test.f(0, 1)
-  --> model_checker_targets_all/input.sol:11:3:
+  --> model_checker_targets_all_all_engines/input.sol:11:3:
    |
 11 | 		assert(x > 0);
    | 		^^^^^^^^^^^^^
@@ -68,7 +68,7 @@ Transaction trace:
 test.constructor()
 State: arr = []
 test.f(0, 1)
-  --> model_checker_targets_all/input.sol:12:3:
+  --> model_checker_targets_all_all_engines/input.sol:12:3:
    |
 12 | 		arr.pop();
    | 		^^^^^^^^^
@@ -83,20 +83,20 @@ Transaction trace:
 test.constructor()
 State: arr = []
 test.f(0, 1)
-  --> model_checker_targets_all/input.sol:13:3:
+  --> model_checker_targets_all_all_engines/input.sol:13:3:
    |
 13 | 		arr[x];
    | 		^^^^^^
 
 Warning: BMC: Condition is always true.
- --> model_checker_targets_all/input.sol:6:11:
+ --> model_checker_targets_all_all_engines/input.sol:6:11:
   |
 6 | 		require(x >= 0);
   | 		        ^^^^^^
 Note: Callstack:
 
 Warning: BMC: Insufficient funds happens here.
-  --> model_checker_targets_all/input.sol:10:3:
+  --> model_checker_targets_all_all_engines/input.sol:10:3:
    |
 10 | 		a.transfer(x);
    | 		^^^^^^^^^^^^^

test/cmdlineTests/model_checker_targets_all/input.sol renamed to test/cmdlineTests/model_checker_targets_all_all_engines/input.sol

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