[SMTChecker] Support mod

Changelog.md

@@ -14,6 +14,7 @@ Compiler Features:
  * SMTChecker: Support arithmetic compound assignment operators.
  * SMTChecker: Support unary increment and decrement for array and mapping access.
  * SMTChecker: Show unsupported warning for inline assembly blocks.
+ * SMTChecker: Support mod.
  * Optimizer: Add rule for shifts by constants larger than 255 for Constantinople.
  * Optimizer: Add rule to simplify certain ANDs and SHL combinations
  * Yul: Adds break and continue keywords to for-loop syntax.

libsolidity/formal/SMTChecker.cpp

@@ -347,7 +347,8 @@ void SMTChecker::endVisit(Assignment const& _assignment)
 		{Token::AssignAdd, Token::Add},
 		{Token::AssignSub, Token::Sub},
 		{Token::AssignMul, Token::Mul},
-		{Token::AssignDiv, Token::Div}
+		{Token::AssignDiv, Token::Div},
+		{Token::AssignMod, Token::Mod}
 	};
 	Token op = _assignment.assignmentOperator();
 	if (op != Token::Assign && !compoundToArithmetic.count(op))
@@ -1041,6 +1042,7 @@ void SMTChecker::arithmeticOperation(BinaryOperation const& _op)
 	case Token::Sub:
 	case Token::Mul:
 	case Token::Div:
+	case Token::Mod:
 	{
 		defineExpr(_op, arithmeticOperation(
 			_op.getOperator(),
@@ -1071,7 +1073,8 @@ smt::Expression SMTChecker::arithmeticOperation(
 		Token::Add,
 		Token::Sub,
 		Token::Mul,
-		Token::Div
+		Token::Div,
+		Token::Mod
 	};
 	solAssert(validOperators.count(_op), "");
 	solAssert(_commonType, "");
@@ -1082,10 +1085,11 @@ smt::Expression SMTChecker::arithmeticOperation(
 		_op == Token::Add ? _left + _right :
 		_op == Token::Sub ? _left - _right :
 		_op == Token::Div ? division(_left, _right, intType) :
-		/*op == Token::Mul*/ _left * _right
+		_op == Token::Mul ? _left * _right :
+		/*_op == Token::Mod*/ _left % _right
 	);
 
-	if (_op == Token::Div)
+	if (_op == Token::Div || _op == Token::Mod)
 	{
 		checkCondition(_right == 0, _location, "Division by zero", "<result>", &_right);
 		m_interface->addAssertion(_right != 0);

test/libsolidity/SMTChecker.cpp

@@ -230,6 +230,22 @@ BOOST_AUTO_TEST_CASE(compound_assignment_division)
 	CHECK_WARNING(text, "Assertion violation");
 }
 
+BOOST_AUTO_TEST_CASE(mod)
+{
+	string text = R"(
+		contract C {
+			function f(int x, int y) public pure {
+				require(y == -10);
+				require(x == 100);
+				int z1 = x % y;
+				int z2 = x % -y;
+				assert(z1 == z2);
+			}
+		}
+	)";
+	CHECK_SUCCESS_NO_WARNINGS(text);
+}
+
 BOOST_AUTO_TEST_SUITE_END()
 
 }

test/libsolidity/smtCheckerTests/operators/mod_even.sol

@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x) public pure {
+		require(x < 10000);
+		uint y = x * 2;
+		assert((y % 2) == 0);
+	}
+}

test/libsolidity/smtCheckerTests/operators/mod_n.sol

@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x, uint y) public pure {
+		require(y > 0);
+		uint z = x % y;
+		assert(z < y);
+	}
+}

test/libsolidity/smtCheckerTests/operators/mod_n_uint16.sol

@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint16 x, uint16 y) public pure {
+		require(y > 0);
+		uint z = x % y;
+		assert(z < 100_000);
+	}
+}