Merge pull request #10038 from blishko/issue-9197

[SMTChecker] Encoding div and mod operations with slack variables

libsolidity/formal/SMTEncoder.cpp

@@ -755,11 +755,12 @@ void SMTEncoder::visitAddMulMod(FunctionCall const& _funCall)
 	auto y = expr(*args.at(1));
 	auto k = expr(*args.at(2));
 	m_context.addAssertion(k != 0);
+	auto const& intType = dynamic_cast<IntegerType const&>(*_funCall.annotation().type);
 
 	if (kind == FunctionType::Kind::AddMod)
-		defineExpr(_funCall, (x + y) % k);
+		defineExpr(_funCall, divModWithSlacks(x + y, k, intType).second);
 	else
-		defineExpr(_funCall, (x * y) % k);
+		defineExpr(_funCall, divModWithSlacks(x * y, k, intType).second);
 }
 
 void SMTEncoder::visitObjectCreation(FunctionCall const& _funCall)
@@ -1490,8 +1491,8 @@ pair<smtutil::Expression, smtutil::Expression> SMTEncoder::arithmeticOperation(
 		case Token::Add: return _left + _right;
 		case Token::Sub: return _left - _right;
 		case Token::Mul: return _left * _right;
-		case Token::Div: return division(_left, _right, *intType);
+		case Token::Div: return divModWithSlacks(_left, _right, *intType).first;
-		case Token::Mod: return _left % _right;
+		case Token::Mod: return divModWithSlacks(_left, _right, *intType).second;
 		default: solAssert(false, "");
 		}
 	}();
@@ -1693,13 +1694,30 @@ void SMTEncoder::bitwiseNotOperation(UnaryOperation const& _op)
 	defineExpr(_op, smtutil::Expression::bv2int(~bvOperand, isSigned));
 }
 
-smtutil::Expression SMTEncoder::division(smtutil::Expression _left, smtutil::Expression _right, IntegerType const& _type)
+pair<smtutil::Expression, smtutil::Expression> SMTEncoder::divModWithSlacks(
+	smtutil::Expression _left,
+	smtutil::Expression _right,
+	IntegerType const& _type
+)
 {
-	// Signed division in SMTLIB2 rounds differently for negative division.
+	IntegerType const* intType = &_type;
+	string suffix = "div_mod_" + to_string(m_context.newUniqueId());
+	smt::SymbolicIntVariable d(intType, intType, "d_" + suffix, m_context);
+	smt::SymbolicIntVariable r(intType, intType, "r_" + suffix, m_context);
+
+	// x / y = d and x % y = r iff d * y + r = x and
+	// either x >= 0 and 0 <= r < abs(y) (or just 0 <= r < y for unsigned)
+	// or     x < 0 and -abs(y) < r <= 0
+	m_context.addAssertion(((d.currentValue() * _right) + r.currentValue()) == _left);
 	if (_type.isSigned())
-		return signedDivisionEVM(_left, _right);
+		m_context.addAssertion(
-	else
+			(_left >= 0 && 0 <= r.currentValue() && r.currentValue() < smtutil::abs(_right)) ||
-		return _left / _right;
+			(_left < 0 && (0 - smtutil::abs(_right)) < r.currentValue() && r.currentValue() <= 0)
+		);
+	else // unsigned version
+		m_context.addAssertion(0 <= r.currentValue() && r.currentValue() < _right);
+
+	return {d.currentValue(), r.currentValue()};
 }
 
 void SMTEncoder::assignment(

libsolidity/formal/SMTEncoder.h

@@ -36,6 +36,7 @@
 #include <string>
 #include <unordered_map>
 #include <vector>
+#include <utility>
 
 namespace solidity::langutil
 {
@@ -174,9 +175,14 @@ protected:
 		std::vector<smtutil::Expression> const& _elementValues
 	);
 
-	/// Division expression in the given type. Requires special treatment because
+	/// @returns a pair of expressions representing _left / _right and _left mod _right, respectively.
-	/// of rounding for signed division.
+	/// Uses slack variables and additional constraints to express the results using only operations
-	smtutil::Expression division(smtutil::Expression _left, smtutil::Expression _right, IntegerType const& _type);
+	/// more friendly to the SMT solver (multiplication, addition, subtraction and comparison).
+	std::pair<smtutil::Expression, smtutil::Expression>	divModWithSlacks(
+		smtutil::Expression _left,
+		smtutil::Expression _right,
+		IntegerType const& _type
+	);
 
 	void assignment(VariableDeclaration const& _variable, Expression const& _value);
 	/// Handles assignments to variables of different types.

scripts/error_codes.py

@@ -220,7 +220,7 @@ def examine_id_coverage(top_dir, source_id_to_file_names, new_ids_only=False):
             return False
 
     old_source_only_ids = {
-        "1123", "1133", "1220", "1584", "1823", "1950",
+        "1123", "1133", "1218", "1220", "1584", "1823", "1950",
         "1988", "2418", "2461", "2512", "2592", "2657", "2800", "2842", "2856",
         "3263", "3356", "3441", "3682", "3876",
         "3893", "4010", "4281", "4802", "4805", "4828",

test/libsolidity/smtCheckerTests/math/addmod_1.sol

@@ -12,10 +12,5 @@ contract C {
 	}
 }
 // ----
-// Warning 1218: (83-108): CHC: Error trying to invoke SMT solver.
-// Warning 1218: (141-166): CHC: Error trying to invoke SMT solver.
-// Warning 1218: (76-114): CHC: Error trying to invoke SMT solver.
-// Warning 1218: (170-184): CHC: Error trying to invoke SMT solver.
-// Warning 1218: (263-278): CHC: Error trying to invoke SMT solver.
 // Warning 3046: (141-166): BMC: Division by zero happens here.
 // Warning 3046: (263-278): BMC: Division by zero happens here.

test/libsolidity/smtCheckerTests/math/addmod_mulmod.sol

@@ -9,8 +9,5 @@ contract C {
 	}
 }
 // ----
-// Warning 1218: (118-143): CHC: Error trying to invoke SMT solver.
-// Warning 1218: (183-208): CHC: Error trying to invoke SMT solver.
-// Warning 1218: (219-233): CHC: Error trying to invoke SMT solver.
 // Warning 6838: (93-143): BMC: Condition is always false.
 // Warning 6838: (158-208): BMC: Condition is always false.

test/libsolidity/smtCheckerTests/math/addmod_mulmod_zero.sol

@@ -22,15 +22,5 @@ contract C {
 }
 // ----
 // Warning 6321: (253-260): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable.
-// Warning 1218: (94-109): CHC: Error trying to invoke SMT solver.
-// Warning 1218: (113-126): CHC: Error trying to invoke SMT solver.
-// Warning 1218: (180-195): CHC: Error trying to invoke SMT solver.
-// Warning 1218: (199-212): CHC: Error trying to invoke SMT solver.
-// Warning 1218: (275-290): CHC: Error trying to invoke SMT solver.
-// Warning 1218: (303-318): CHC: Error trying to invoke SMT solver.
-// Warning 1218: (349-364): CHC: Error trying to invoke SMT solver.
-// Warning 1218: (377-392): CHC: Error trying to invoke SMT solver.
-// Warning 1218: (322-336): CHC: Error trying to invoke SMT solver.
-// Warning 1218: (396-410): CHC: Error trying to invoke SMT solver.
 // Warning 3046: (94-109): BMC: Division by zero happens here.
 // Warning 3046: (180-195): BMC: Division by zero happens here.

test/libsolidity/smtCheckerTests/math/addmulmod.sol

@@ -17,8 +17,3 @@ contract C {
 	}
 }
 // ----
-// Warning 1218: (158-174): CHC: Error trying to invoke SMT solver.
-// Warning 1218: (178-192): CHC: Error trying to invoke SMT solver.
-// Warning 1218: (309-325): CHC: Error trying to invoke SMT solver.
-// Warning 1218: (329-343): CHC: Error trying to invoke SMT solver.
-// Warning 7812: (329-343): BMC: Assertion violation might happen here.

test/libsolidity/smtCheckerTests/math/mulmod_1.sol

@@ -12,10 +12,5 @@ contract C {
 	}
 }
 // ----
-// Warning 1218: (83-108): CHC: Error trying to invoke SMT solver.
-// Warning 1218: (141-166): CHC: Error trying to invoke SMT solver.
-// Warning 1218: (76-114): CHC: Error trying to invoke SMT solver.
-// Warning 1218: (170-184): CHC: Error trying to invoke SMT solver.
-// Warning 1218: (263-278): CHC: Error trying to invoke SMT solver.
 // Warning 3046: (141-166): BMC: Division by zero happens here.
 // Warning 3046: (263-278): BMC: Division by zero happens here.

test/libsolidity/smtCheckerTests/operators/compound_assignment_division_1.sol

@@ -9,6 +9,4 @@ contract C {
 	}
 }
 // ----
-// Warning 1218: (129-143): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (147-161): CHC: Assertion violation happens here.
-// Warning 1218: (147-161): CHC: Error trying to invoke SMT solver.
-// Warning 4661: (147-161): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/compound_assignment_division_2.sol

@@ -10,6 +10,4 @@ contract C {
 	}
 }
 // ----
-// Warning 1218: (163-184): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (188-209): CHC: Assertion violation happens here.
-// Warning 1218: (188-209): CHC: Error trying to invoke SMT solver.
-// Warning 4661: (188-209): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/compound_assignment_division_3.sol

@@ -10,6 +10,4 @@ contract C {
 	}
 }
 // ----
-// Warning 1218: (171-190): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (194-213): CHC: Assertion violation happens here.
-// Warning 1218: (194-213): CHC: Error trying to invoke SMT solver.
-// Warning 4661: (194-213): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/division_3.sol

@@ -6,5 +6,4 @@ contract C {
 	}
 }
 // ----
-// Warning 1218: (127-132): CHC: Error trying to invoke SMT solver.
+// Warning 4984: (127-132): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.
-// Warning 2661: (127-132): BMC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.

test/libsolidity/smtCheckerTests/operators/division_4.sol

@@ -7,4 +7,3 @@ contract C {
 	}
 }
 // ----
-// Warning 1218: (147-152): CHC: Error trying to invoke SMT solver.

test/libsolidity/smtCheckerTests/operators/division_5.sol

@@ -10,4 +10,3 @@ contract C {
 	}
 }
 // ----
-// Warning 1218: (151-156): CHC: Error trying to invoke SMT solver.

test/libsolidity/smtCheckerTests/operators/division_6.sol

@@ -12,4 +12,3 @@ contract C {
 	}
 }
 // ----
-// Warning 1218: (265-270): CHC: Error trying to invoke SMT solver.

test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_1.sol

@@ -7,4 +7,3 @@ contract C {
 	}
 }
 // ----
-// Warning 1218: (107-125): CHC: Error trying to invoke SMT solver.

test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_2.sol

@@ -7,5 +7,3 @@ contract C {
 	}
 }
 // ----
-// Warning 1218: (112-117): CHC: Error trying to invoke SMT solver.
-// Warning 1218: (105-123): CHC: Error trying to invoke SMT solver.

test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_3.sol

@@ -7,5 +7,3 @@ contract C {
 	}
 }
 // ----
-// Warning 1218: (113-118): CHC: Error trying to invoke SMT solver.
-// Warning 1218: (106-125): CHC: Error trying to invoke SMT solver.

test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_4.sol

@@ -7,5 +7,3 @@ contract C {
 	}
 }
 // ----
-// Warning 1218: (113-118): CHC: Error trying to invoke SMT solver.
-// Warning 1218: (106-125): CHC: Error trying to invoke SMT solver.

test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_5.sol

@@ -7,5 +7,3 @@ contract C {
 	}
 }
 // ----
-// Warning 1218: (114-119): CHC: Error trying to invoke SMT solver.
-// Warning 1218: (107-125): CHC: Error trying to invoke SMT solver.

test/libsolidity/smtCheckerTests/operators/mod.sol

@@ -9,4 +9,3 @@ contract C {
 	}
 }
 // ----
-// Warning 1218: (166-182): CHC: Error trying to invoke SMT solver.

test/libsolidity/smtCheckerTests/operators/mod_even.sol

@@ -9,5 +9,3 @@ contract C
 	}
 }
 // ----
-// Warning 1218: (113-118): CHC: Error trying to invoke SMT solver.
-// Warning 1218: (122-142): CHC: Error trying to invoke SMT solver.

test/libsolidity/smtCheckerTests/operators/mod_n.sol

@@ -9,4 +9,3 @@ contract C
 	}
 }
 // ----
-// Warning 1218: (126-139): CHC: Error trying to invoke SMT solver.

test/libsolidity/smtCheckerTests/operators/mod_n_uint16.sol

@@ -9,4 +9,3 @@ contract C
 	}
 }
 // ----
-// Warning 1218: (130-149): CHC: Error trying to invoke SMT solver.

test/libsolidity/smtCheckerTests/operators/mod_signed.sol

@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+contract C {
+	function f(int x, int y) public pure {
+		require(y != 0);
+		require(x == 42);
+		int z1 = x % y;
+		int z2 = -x % y;
+		assert(z1 == -z2);
+		assert((x >= 0 && z1 >=0) || (x <= 0 && z1 <= 0));
+	}
+}
+// ----

test/libsolidity/smtCheckerTests/overflow/signed_div_overflow.sol

@@ -6,6 +6,5 @@ contract C  {
 	}
 }
 // ----
-// Warning 1218: (110-115): CHC: Error trying to invoke SMT solver.
+// Warning 4984: (110-115): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.
 // Warning 3046: (110-115): BMC: Division by zero happens here.
-// Warning 2661: (110-115): BMC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.