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_strModelCheckerDivModSlacks = "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_strModelCheckerDivModSlacks.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_strModelCheckerDivModSlacks))
+		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_strModelCheckerDivModSlacks) ||
 		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/err

@@ -0,0 +1 @@
+Compiler run successful, no output requested.

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/err

@@ -0,0 +1 @@
+Compiler run successful, no output requested.

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/err

@@ -0,0 +1 @@
+Compiler run successful, no output requested.

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/err

@@ -0,0 +1 @@
+Compiler run successful, no output requested.

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/solc/CommandLineParser.cpp

@@ -79,14 +79,7 @@ BOOST_AUTO_TEST_CASE(no_options)
 	CommandLineOptions expectedOptions;
 	expectedOptions.input.paths = {"contract.sol"};
 	expectedOptions.modelChecker.initialize = true;
-	expectedOptions.modelChecker.settings = {
-		ModelCheckerContracts::Default(),
-		ModelCheckerEngine::None(),
-		false,
-		smtutil::SMTSolverChoice::All(),
-		ModelCheckerTargets::Default(),
-		nullopt,
-	};
+	expectedOptions.modelChecker.settings = {};
 
 	stringstream sout, serr;
 	optional<CommandLineOptions> parsedOptions = parseCommandLine(commandLine, sout, serr);
@@ -151,6 +144,7 @@ BOOST_AUTO_TEST_CASE(cli_mode_options)
 			"--optimize-runs=1000",
 			"--yul-optimizations=agf",
 			"--model-checker-contracts=contract1.yul:A,contract2.yul:B",
+			"--model-checker-div-mod-no-slacks",
 			"--model-checker-engine=bmc",
 			"--model-checker-show-unproved=true",
 			"--model-checker-solvers=z3,smtlib2",
@@ -210,6 +204,7 @@ BOOST_AUTO_TEST_CASE(cli_mode_options)
 		expectedOptions.modelChecker.initialize = true;
 		expectedOptions.modelChecker.settings = {
 			{{{"contract1.yul", {"A"}}, {"contract2.yul", {"B"}}}},
+			true,
 			{true, false},
 			true,
 			{false, true, true},
@@ -281,6 +276,7 @@ BOOST_AUTO_TEST_CASE(assembly_mode_options)
 			"--model-checker-contracts="   // Ignored in assembly mode
 				"contract1.yul:A,"
 				"contract2.yul:B",
+			"--model-checker-div-mod-no-slacks", // Ignored in assembly mode
 			"--model-checker-engine=bmc",  // Ignored in assembly mode
 			"--model-checker-show-unproved=true", // Ignored in assembly mode
 			"--model-checker-solvers=z3,smtlib2", // Ignored in assembly mode
@@ -380,6 +376,7 @@ BOOST_AUTO_TEST_CASE(standard_json_mode_options)
 		"--model-checker-contracts="       // Ignored in Standard JSON mode
 			"contract1.yul:A,"
 			"contract2.yul:B",
+		"--model-checker-div-mod-no-slacks", // Ignored in Standard JSON mode
 		"--model-checker-engine=bmc",      // Ignored in Standard JSON mode
 		"--model-checker-show-unproved=true",      // Ignored in Standard JSON mode
 		"--model-checker-solvers=z3,smtlib2", // Ignored in Standard JSON mode

test/tools/fuzzer_common.cpp

@@ -104,6 +104,7 @@ void FuzzerUtil::testCompiler(
 		forceSMT(_input);
 		compiler.setModelCheckerSettings({
 			frontend::ModelCheckerContracts::Default(),
+			/*divModWithSlacks*/true,
 			frontend::ModelCheckerEngine::All(),
 			/*showUnproved=*/false,
 			smtutil::SMTSolverChoice::All(),