Merge pull request #9910 from ethereum/smt_addmulmod

[SMTChecker] Support addmod and mulmod

Changelog.md

@@ -1,5 +1,7 @@
 ### 0.7.3 (unreleased)
 
+Compiler Features:
+ * SMTChecker: Support ``addmod`` and ``mulmod``.
 
 
 ### 0.7.2 (2020-09-28)

libsolidity/formal/BMC.cpp

@@ -390,8 +390,6 @@ void BMC::endVisit(FunctionCall const& _funCall)
 	case FunctionType::Kind::SHA256:
 	case FunctionType::Kind::RIPEMD160:
 	case FunctionType::Kind::BlockHash:
-	case FunctionType::Kind::AddMod:
-	case FunctionType::Kind::MulMod:
 		SMTEncoder::endVisit(_funCall);
 		abstractFunctionCall(_funCall);
 		break;
@@ -410,6 +408,9 @@ void BMC::endVisit(FunctionCall const& _funCall)
 		);
 		break;
 	}
+	case FunctionType::Kind::AddMod:
+	case FunctionType::Kind::MulMod:
+		[[fallthrough]];
 	default:
 		SMTEncoder::endVisit(_funCall);
 		break;
@@ -443,6 +444,18 @@ void BMC::visitRequire(FunctionCall const& _funCall)
 		);
 }
 
+void BMC::visitAddMulMod(FunctionCall const& _funCall)
+{
+	solAssert(_funCall.arguments().at(2), "");
+	addVerificationTarget(
+		VerificationTarget::Type::DivByZero,
+		expr(*_funCall.arguments().at(2)),
+		&_funCall
+	);
+
+	SMTEncoder::visitAddMulMod(_funCall);
+}
+
 void BMC::inlineFunctionCall(FunctionCall const& _funCall)
 {
 	solAssert(shouldInlineFunctionCall(_funCall), "");

libsolidity/formal/BMC.h

@@ -95,6 +95,7 @@ private:
 	//@{
 	void visitAssert(FunctionCall const& _funCall);
 	void visitRequire(FunctionCall const& _funCall);
+	void visitAddMulMod(FunctionCall const& _funCall) override;
 	/// Visits the FunctionDefinition of the called function
 	/// if available and inlines the return value.
 	void inlineFunctionCall(FunctionCall const& _funCall);

libsolidity/formal/CHC.cpp

@@ -497,6 +497,24 @@ void CHC::visitAssert(FunctionCall const& _funCall)
 	m_context.addAssertion(errorFlag().currentValue() == previousError);
 }
 
+void CHC::visitAddMulMod(FunctionCall const& _funCall)
+{
+	auto previousError = errorFlag().currentValue();
+	errorFlag().increaseIndex();
+
+	addVerificationTarget(
+		&_funCall,
+		VerificationTarget::Type::DivByZero,
+		errorFlag().currentValue()
+	);
+
+	solAssert(_funCall.arguments().at(2), "");
+	smtutil::Expression target = expr(*_funCall.arguments().at(2)) == 0 && errorFlag().currentValue() == newErrorId(_funCall);
+	m_context.addAssertion((errorFlag().currentValue() == previousError) || target);
+
+	SMTEncoder::visitAddMulMod(_funCall);
+}
+
 void CHC::internalFunctionCall(FunctionCall const& _funCall)
 {
 	solAssert(m_currentContract, "");
@@ -1158,6 +1176,11 @@ void CHC::checkVerificationTargets()
 					errorReporterId = overflowErrorId;
 				}
 			}
+			else if (target.type == VerificationTarget::Type::DivByZero)
+			{
+				satMsg = "Division by zero happens here.";
+				errorReporterId = 4281_error;
+			}
 			else
 				solAssert(false, "");
 

libsolidity/formal/CHC.h

@@ -83,6 +83,7 @@ private:
 	void endVisit(Continue const& _node) override;
 
 	void visitAssert(FunctionCall const& _funCall);
+	void visitAddMulMod(FunctionCall const& _funCall) override;
 	void internalFunctionCall(FunctionCall const& _funCall);
 	void externalFunctionCall(FunctionCall const& _funCall);
 	void unknownFunctionCall(FunctionCall const& _funCall);

libsolidity/formal/SMTEncoder.cpp

@@ -632,8 +632,10 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
 	case FunctionType::Kind::SHA256:
 	case FunctionType::Kind::RIPEMD160:
 	case FunctionType::Kind::BlockHash:
+		break;
 	case FunctionType::Kind::AddMod:
 	case FunctionType::Kind::MulMod:
+		visitAddMulMod(_funCall);
 		break;
 	case FunctionType::Kind::Send:
 	case FunctionType::Kind::Transfer:
@@ -738,6 +740,24 @@ void SMTEncoder::visitGasLeft(FunctionCall const& _funCall)
 		m_context.addAssertion(symbolicVar->currentValue() <= symbolicVar->valueAtIndex(index - 1));
 }
 
+void SMTEncoder::visitAddMulMod(FunctionCall const& _funCall)
+{
+	auto const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
+	auto kind = funType.kind();
+	solAssert(kind == FunctionType::Kind::AddMod || kind == FunctionType::Kind::MulMod, "");
+	auto const& args = _funCall.arguments();
+	solAssert(args.at(0) && args.at(1) && args.at(2), "");
+	auto x = expr(*args.at(0));
+	auto y = expr(*args.at(1));
+	auto k = expr(*args.at(2));
+	m_context.addAssertion(k != 0);
+
+	if (kind == FunctionType::Kind::AddMod)
+		defineExpr(_funCall, (x + y) % k);
+	else
+		defineExpr(_funCall, (x * y) % k);
+}
+
 void SMTEncoder::visitObjectCreation(FunctionCall const& _funCall)
 {
 	auto const& args = _funCall.arguments();

libsolidity/formal/SMTEncoder.h

@@ -137,6 +137,7 @@ protected:
 	void visitAssert(FunctionCall const& _funCall);
 	void visitRequire(FunctionCall const& _funCall);
 	void visitGasLeft(FunctionCall const& _funCall);
+	virtual void visitAddMulMod(FunctionCall const& _funCall);
 	void visitObjectCreation(FunctionCall const& _funCall);
 	void visitTypeConversion(FunctionCall const& _funCall);
 	void visitFunctionIdentifier(Identifier const& _identifier);

scripts/error_codes.py

@@ -223,7 +223,7 @@ def examine_id_coverage(top_dir, source_id_to_file_names, new_ids_only=False):
         "1123", "1133", "1220", "1584", "1823", "1950",
         "1988", "2418", "2461", "2512", "2592", "2657", "2800", "2842", "2856",
         "3263", "3356", "3441", "3682", "3876",
-        "3893", "3997", "4010", "4802", "4805", "4828",
+        "3893", "3997", "4010", "4281", "4802", "4805", "4828",
         "4904", "4990", "5052", "5073", "5170", "5188", "5272", "5333", "5347", "5473",
         "5622", "6041", "6052", "6272", "6708", "6792", "6931", "7110", "7128", "7186",
         "7589", "7593", "7653", "7812", "7885", "8065", "8084", "8140",

test/libsolidity/smtCheckerTests/math/addmod_1.sol

@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		assert(addmod(2**256 - 1, 10, 9) == 7);
+		uint y = 0;
+		uint x = addmod(2**256 - 1, 10, y);
+		assert(x == 1);
+	}
+	function g(uint x, uint y, uint k) public pure returns (uint) {
+		return addmod(x, y, k);
+	}
+}
+// ----
+// 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

@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function test() public pure {
+		uint x;
+		if ((2**255 + 2**255) % 7 != addmod(2**255, 2**255, 7)) x = 1;
+		if ((2**255 + 2**255) % 7 != addmod(2**255, 2**255, 7)) x = 2;
+		assert(x == 0);
+	}
+}
+// ----
+// 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

@@ -0,0 +1,35 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f(uint256 d) public pure {
+		uint x = addmod(1, 2, d);
+		assert(x < d);
+	}
+
+	function g(uint256 d) public pure {
+		uint x = mulmod(1, 2, d);
+		assert(x < d);
+	}
+
+	function h() public pure returns (uint256) {
+		uint x = mulmod(0, 1, 2);
+		uint y = mulmod(1, 0, 2);
+		assert(x == y);
+		uint z = addmod(0, 1, 2);
+		uint t = addmod(1, 0, 2);
+		assert(z == t);
+	}
+}
+// ----
+// 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

@@ -0,0 +1,24 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function test_addmod(uint x, uint y) public pure {
+		require(x % 13 == 0);
+		require(y % 13 == 0);
+
+		uint z = addmod(x, y, 13);
+		assert(z == 0);
+	}
+	function test_mulmod(uint x, uint y) public pure {
+		require(x % 13 == 0);
+		require(y % 13 == 0);
+
+		uint z = mulmod(x, y, 13);
+		assert(z == 0);
+	}
+}
+// ----
+// 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

@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		assert(mulmod(2**256 - 1, 2, 14) == 2);
+		uint y = 0;
+		uint x = mulmod(2**256 - 1, 10, y);
+		assert(x == 1);
+	}
+	function g(uint x, uint y, uint k) public pure returns (uint) {
+		return mulmod(x, y, k);
+	}
+}
+// ----
+// 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.