[SMTChecker] Add option divModWithSlacks

Changelog.md

@@ -10,6 +10,7 @@ Compiler Features:
  * Yul Optimizer: Move function arguments and return variables to memory with the experimental Stack Limit Evader (which is not enabled by default).
  * 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``.
 
 
 Bugfixes:

docs/smtchecker.rst

@@ -509,7 +509,17 @@ which has the following form:
         "source2.sol": ["contract2", "contract3"]
     }
 
-.. _smtchecker_engines:
+Division and Modulo With Slack Variables
+========================================
+
+Spacer, the default Horn solver used by the SMTChecker, often dislikes division
+and modulo operations inside Horn rules. Because of that, by default the
+Solidity division and modulo operations are encoded using the constraint
+``a = b * d + m`` where ``d = a / b`` and ``m = a % b``.
+However, other solvers, such as Eldarica, prefer the syntactically precise operations.
+The command line flag ``--model-checker-div-mod-no-slacks`` and the JSON option
+``settings.modelChecker.divModNoSlacks`` can be used to toggle the encoding
+depending on the used solver preferences.
 
 Natspec Function Abstraction
 ============================
@@ -523,6 +533,8 @@ body of the function is not used, and when called, the function will:
 - Return a nondeterministic value, and either keep the state variables unchanged if the abstracted function is view/pure, or also set the state variables to nondeterministic values otherwise. This can be used via the annotation ``/// @custom:smtchecker abstract-function-nondet``.
 - Act as an uninterpreted function. This means that the semantics of the function (given by the body) are ignored, and the only property this function has is that given the same input it guarantees the same output. This is currently under development and will be available via the annotation ``/// @custom:smtchecker abstract-function-uf``.
 
+.. _smtchecker_engines:
+
 Model Checking Engines
 ======================
 

docs/using-the-compiler.rst

@@ -400,6 +400,12 @@ Input Description
             "source1.sol": ["contract1"],
             "source2.sol": ["contract2", "contract3"]
           },
+          // Choose whether division and modulo operations should be replaced by
+          // multiplication with slack variables. Default is `true`.
+          // Using `false` here is recommended if you are using the CHC engine
+          // and not using Spacer as the Horn solver (using Eldarica, for example).
+          // See the Formal Verification section for a more detailed explanation of this option.
+          "divModWithSlacks": true,
           // Choose which model checker engine to use: all (default), bmc, chc, none.
           "engine": "chc",
           // Choose whether to output all unproved targets. The default is `false`.

libsolidity/formal/ModelCheckerSettings.h

@@ -112,6 +112,13 @@ struct ModelCheckerTargets
 struct ModelCheckerSettings
 {
 	ModelCheckerContracts contracts = ModelCheckerContracts::Default();
+	/// Currently division and modulo are replaced by multiplication with slack vars, such that
+	/// a / b <=> a = b * k + m
+	/// where k and m are slack variables.
+	/// This is the default because Spacer prefers that over precise / and mod.
+	/// This option allows disabling this mechanism since other solvers
+	/// might prefer the precise encoding.
+	bool divModNoSlacks = false;
 	ModelCheckerEngine engine = ModelCheckerEngine::None();
 	bool showUnproved = false;
 	smtutil::SMTSolverChoice solvers = smtutil::SMTSolverChoice::All();
@@ -123,6 +130,7 @@ struct ModelCheckerSettings
 	{
 		return
 			contracts == _other.contracts &&
+			divModNoSlacks == _other.divModNoSlacks &&
 			engine == _other.engine &&
 			showUnproved == _other.showUnproved &&
 			solvers == _other.solvers &&

libsolidity/formal/SMTEncoder.cpp

@@ -1916,6 +1916,9 @@ pair<smtutil::Expression, smtutil::Expression> SMTEncoder::divModWithSlacks(
 	IntegerType const& _type
 )
 {
+	if (m_settings.divModNoSlacks)
+		return {_left / _right, _left % _right};
+
 	IntegerType const* intType = &_type;
 	string suffix = "div_mod_" + to_string(m_context.newUniqueId());
 	smt::SymbolicIntVariable dSymb(intType, intType, "d_" + suffix, m_context);

libsolidity/interface/StandardCompiler.cpp

@@ -442,7 +442,7 @@ std::optional<Json::Value> checkSettingsKeys(Json::Value const& _input)
 
 std::optional<Json::Value> checkModelCheckerSettingsKeys(Json::Value const& _input)
 {
-	static set<string> keys{"contracts", "engine", "showUnproved", "solvers", "targets", "timeout"};
+	static set<string> keys{"contracts", "divModNoSlacks", "engine", "showUnproved", "solvers", "targets", "timeout"};
 	return checkKeys(_input, keys, "modelChecker");
 }
 
@@ -941,6 +941,14 @@ std::variant<StandardCompiler::InputsAndSettings, Json::Value> StandardCompiler:
 		ret.modelCheckerSettings.contracts = {move(sourceContracts)};
 	}
 
+	if (modelCheckerSettings.isMember("divModNoSlacks"))
+	{
+		auto const& divModNoSlacks = modelCheckerSettings["divModNoSlacks"];
+		if (!divModNoSlacks.isBool())
+			return formatFatalError("JSONError", "settings.modelChecker.divModNoSlacks must be a Boolean.");
+		ret.modelCheckerSettings.divModNoSlacks = divModNoSlacks.asBool();
+	}
+
 	if (modelCheckerSettings.isMember("engine"))
 	{
 		if (!modelCheckerSettings["engine"].isString())

solc/CommandLineParser.cpp

@@ -86,6 +86,7 @@ static string const g_strMetadata = "metadata";
 static string const g_strMetadataHash = "metadata-hash";
 static string const g_strMetadataLiteral = "metadata-literal";
 static string const g_strModelCheckerContracts = "model-checker-contracts";
+static string const g_strModelCheckerDivModNoSlacks = "model-checker-div-mod-no-slacks";
 static string const g_strModelCheckerEngine = "model-checker-engine";
 static string const g_strModelCheckerShowUnproved = "model-checker-show-unproved";
 static string const g_strModelCheckerSolvers = "model-checker-solvers";
@@ -720,6 +721,11 @@ General Information)").c_str(),
 			"Multiple pairs <source>:<contract> can be selected at the same time, separated by a comma "
 			"and no spaces."
 		)
+		(
+			g_strModelCheckerDivModNoSlacks.c_str(),
+			"Encode division and modulo operations with their precise operators"
+			" instead of multiplication with slack variables."
+		)
 		(
 			g_strModelCheckerEngine.c_str(),
 			po::value<string>()->value_name("all,bmc,chc,none")->default_value("none"),
@@ -1092,6 +1098,9 @@ General Information)").c_str(),
 		m_options.modelChecker.settings.contracts = move(*contracts);
 	}
 
+	if (m_args.count(g_strModelCheckerDivModNoSlacks))
+		m_options.modelChecker.settings.divModNoSlacks = true;
+
 	if (m_args.count(g_strModelCheckerEngine))
 	{
 		string engineStr = m_args[g_strModelCheckerEngine].as<string>();
@@ -1140,6 +1149,7 @@ General Information)").c_str(),
 	m_options.metadata.literalSources = (m_args.count(g_strMetadataLiteral) > 0);
 	m_options.modelChecker.initialize =
 		m_args.count(g_strModelCheckerContracts) ||
+		m_args.count(g_strModelCheckerDivModNoSlacks) ||
 		m_args.count(g_strModelCheckerEngine) ||
 		m_args.count(g_strModelCheckerShowUnproved) ||
 		m_args.count(g_strModelCheckerSolvers) ||

test/cmdlineTests/model_checker_divModSlacks_default_all/args

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

test/cmdlineTests/model_checker_divModSlacks_default_all/input.sol

@@ -0,0 +1,8 @@
+// SPDX-License-Identifier: GPL-3.0
+pragma solidity >=0.0;
+contract C {
+	function f(uint a, uint b) public pure returns (uint, uint) {
+		require(b != 0);
+		return (a / b, a % b);
+	}
+}

test/cmdlineTests/model_checker_divModSlacks_default_bmc/args

@@ -0,0 +1 @@
+--model-checker-engine bmc

test/cmdlineTests/model_checker_divModSlacks_default_bmc/input.sol

@@ -0,0 +1,8 @@
+// SPDX-License-Identifier: GPL-3.0
+pragma solidity >=0.0;
+contract C {
+	function f(uint a, uint b) public pure returns (uint, uint) {
+		require(b != 0);
+		return (a / b, a % b);
+	}
+}

test/cmdlineTests/model_checker_divModSlacks_default_chc/args

@@ -0,0 +1 @@
+--model-checker-engine chc

test/cmdlineTests/model_checker_divModSlacks_default_chc/input.sol

@@ -0,0 +1,8 @@
+// SPDX-License-Identifier: GPL-3.0
+pragma solidity >=0.0;
+contract C {
+	function f(uint a, uint b) public pure returns (uint, uint) {
+		require(b != 0);
+		return (a / b, a % b);
+	}
+}

test/cmdlineTests/model_checker_divModSlacks_false_all/args

@@ -0,0 +1 @@
+--model-checker-engine all --model-checker-div-mod-no-slacks

test/cmdlineTests/model_checker_divModSlacks_false_all/err

@@ -0,0 +1,13 @@
+Warning: CHC: Error trying to invoke SMT solver.
+ --> model_checker_divModSlacks_false_all/input.sol:6:11:
+  |
+6 | 		return (a / b, a % b);
+  | 		        ^^^^^
+
+Warning: CHC: Error trying to invoke SMT solver.
+ --> model_checker_divModSlacks_false_all/input.sol:6:18:
+  |
+6 | 		return (a / b, a % b);
+  | 		               ^^^^^
+
+Warning: CHC: 2 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.

test/cmdlineTests/model_checker_divModSlacks_false_all/input.sol

@@ -0,0 +1,8 @@
+// SPDX-License-Identifier: GPL-3.0
+pragma solidity >=0.0;
+contract C {
+	function f(uint a, uint b) public pure returns (uint, uint) {
+		require(b != 0);
+		return (a / b, a % b);
+	}
+}

test/cmdlineTests/model_checker_divModSlacks_false_bmc/args

@@ -0,0 +1 @@
+--model-checker-engine bmc --model-checker-div-mod-no-slacks

test/cmdlineTests/model_checker_divModSlacks_false_bmc/input.sol

@@ -0,0 +1,8 @@
+// SPDX-License-Identifier: GPL-3.0
+pragma solidity >=0.0;
+contract C {
+	function f(uint a, uint b) public pure returns (uint, uint) {
+		require(b != 0);
+		return (a / b, a % b);
+	}
+}

test/cmdlineTests/model_checker_divModSlacks_false_chc/args

@@ -0,0 +1 @@
+--model-checker-engine chc --model-checker-div-mod-no-slacks

test/cmdlineTests/model_checker_divModSlacks_false_chc/err

@@ -0,0 +1,13 @@
+Warning: CHC: Error trying to invoke SMT solver.
+ --> model_checker_divModSlacks_false_chc/input.sol:6:11:
+  |
+6 | 		return (a / b, a % b);
+  | 		        ^^^^^
+
+Warning: CHC: Error trying to invoke SMT solver.
+ --> model_checker_divModSlacks_false_chc/input.sol:6:18:
+  |
+6 | 		return (a / b, a % b);
+  | 		               ^^^^^
+
+Warning: CHC: 2 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.

test/cmdlineTests/model_checker_divModSlacks_false_chc/input.sol

@@ -0,0 +1,8 @@
+// SPDX-License-Identifier: GPL-3.0
+pragma solidity >=0.0;
+contract C {
+	function f(uint a, uint b) public pure returns (uint, uint) {
+		require(b != 0);
+		return (a / b, a % b);
+	}
+}

test/cmdlineTests/standard_model_checker_divModSlacks_default_all/input.json

@@ -0,0 +1,22 @@
+{
+	"language": "Solidity",
+	"sources":
+	{
+		"A":
+		{
+			"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract C {
+					function f(uint a, uint b) public pure returns (uint, uint) {
+						require(b != 0);
+						return (a / b, a % b);
+					}
+			}"
+		}
+	},
+	"settings":
+	{
+		"modelChecker":
+		{
+			"engine": "all"
+		}
+	}
+}

test/cmdlineTests/standard_model_checker_divModSlacks_default_all/output.json

@@ -0,0 +1,49 @@
+{"auxiliaryInputRequested":{"smtlib2queries":{"0x10763dfdad96614fe8fcaf54161ed2be500bbaa57bda8e2d706b675f1290f13b":"(set-option :produce-models true)
+(set-logic ALL)
+(declare-fun |error_0| () Int)
+(declare-fun |this_0| () Int)
+(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
+(declare-fun |state_0| () |state_type|)
+(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
+(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
+(declare-fun |tx_0| () |tx_type|)
+(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
+(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
+(declare-fun |crypto_0| () |crypto_type|)
+(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
+(declare-fun |abi_0| () |abi_type|)
+(declare-fun |a_3_0| () Int)
+(declare-fun |b_5_0| () Int)
+(declare-fun |_8_0| () Int)
+(declare-fun |_10_0| () Int)
+(declare-fun |expr_13_0| () Int)
+(declare-fun |expr_14_0| () Int)
+(declare-fun |expr_15_1| () Bool)
+
+(assert (and (and (and true true) (and (= expr_15_1 (not (= expr_13_0 expr_14_0))) (and (=> (and true true) true) (and (= expr_14_0 0) (and (=> (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 b_5_0) (and (= _10_0 0) (and (= _8_0 0) (and (and (>= b_5_0 0) (<= b_5_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_3_0 0) (<= a_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 332507694)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 19)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 209)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 170)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 46)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))))))))) expr_15_1))
+(check-sat)
+","0xa0332f5d2cf85238fd31e652cfbcc1d2a774996d4d2368d02b71c393eb375f0e":"(set-option :produce-models true)
+(set-logic ALL)
+(declare-fun |error_0| () Int)
+(declare-fun |this_0| () Int)
+(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
+(declare-fun |state_0| () |state_type|)
+(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
+(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
+(declare-fun |tx_0| () |tx_type|)
+(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
+(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
+(declare-fun |crypto_0| () |crypto_type|)
+(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
+(declare-fun |abi_0| () |abi_type|)
+(declare-fun |a_3_0| () Int)
+(declare-fun |b_5_0| () Int)
+(declare-fun |_8_0| () Int)
+(declare-fun |_10_0| () Int)
+(declare-fun |expr_13_0| () Int)
+(declare-fun |expr_14_0| () Int)
+(declare-fun |expr_15_1| () Bool)
+
+(assert (and (and (and true true) (and (= expr_15_1 (not (= expr_13_0 expr_14_0))) (and (=> (and true true) true) (and (= expr_14_0 0) (and (=> (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 b_5_0) (and (= _10_0 0) (and (= _8_0 0) (and (and (>= b_5_0 0) (<= b_5_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_3_0 0) (<= a_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 332507694)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 19)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 209)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 170)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 46)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))))))))) (not expr_15_1)))
+(check-sat)
+"}},"sources":{"A":{"id":0}}}

test/cmdlineTests/standard_model_checker_divModSlacks_default_bmc/input.json

@@ -0,0 +1,22 @@
+{
+	"language": "Solidity",
+	"sources":
+	{
+		"A":
+		{
+			"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract C {
+					function f(uint a, uint b) public pure returns (uint, uint) {
+						require(b != 0);
+						return (a / b, a % b);
+					}
+			}"
+		}
+	},
+	"settings":
+	{
+		"modelChecker":
+		{
+			"engine": "bmc"
+		}
+	}
+}