Merge pull request #6405 from ethereum/smt_compound_assignment

[SMTChecker] Support arithmetic compound assignment operators.

Changelog.md

@@ -4,6 +4,7 @@ Language Features:
 
 
 Compiler Features:
+ * SMTChecker: Support arithmetic compound assignment operators.
  * Yul: Adds break and continue keywords to for-loop syntax.
 
 

libsolidity/formal/SMTChecker.cpp

@@ -26,6 +26,7 @@
 #include <boost/range/adaptor/map.hpp>
 #include <boost/range/adaptors.hpp>
 #include <boost/algorithm/string/replace.hpp>
+#include <boost/optional.hpp>
 
 using namespace std;
 using namespace dev;
@@ -333,27 +334,59 @@ void SMTChecker::endVisit(VariableDeclarationStatement const& _varDecl)
 
 void SMTChecker::endVisit(Assignment const& _assignment)
 {
-	if (_assignment.assignmentOperator() != Token::Assign)
+	static map<Token, Token> const compoundToArithmetic{
+		{Token::AssignAdd, Token::Add},
+		{Token::AssignSub, Token::Sub},
+		{Token::AssignMul, Token::Mul},
+		{Token::AssignDiv, Token::Div}
+	};
+	Token op = _assignment.assignmentOperator();
+	if (op != Token::Assign && !compoundToArithmetic.count(op))
 		m_errorReporter.warning(
 			_assignment.location(),
-			"Assertion checker does not yet implement compound assignment."
+			"Assertion checker does not yet implement this assignment operator."
 		);
 	else if (!isSupportedType(_assignment.annotation().type->category()))
 		m_errorReporter.warning(
 			_assignment.location(),
 			"Assertion checker does not yet implement type " + _assignment.annotation().type->toString()
 		);
-	else if (Identifier const* identifier = dynamic_cast<Identifier const*>(&_assignment.leftHandSide()))
+	else if (
+		dynamic_cast<Identifier const*>(&_assignment.leftHandSide()) ||
+		dynamic_cast<IndexAccess const*>(&_assignment.leftHandSide())
+	)
 	{
-		VariableDeclaration const& decl = dynamic_cast<VariableDeclaration const&>(*identifier->annotation().referencedDeclaration);
+		boost::optional<smt::Expression> leftHandSide;
-		solAssert(knownVariable(decl), "");
+		VariableDeclaration const* decl = nullptr;
-		assignment(decl, _assignment.rightHandSide(), _assignment.location());
+		auto identifier = dynamic_cast<Identifier const*>(&_assignment.leftHandSide());
-		defineExpr(_assignment, expr(_assignment.rightHandSide()));
+		if (identifier)
+		{
+			decl = dynamic_cast<VariableDeclaration const*>(identifier->annotation().referencedDeclaration);
+			solAssert(decl, "");
+			solAssert(knownVariable(*decl), "");
+			leftHandSide = currentValue(*decl);
 		}
-	else if (dynamic_cast<IndexAccess const*>(&_assignment.leftHandSide()))
+		else
-	{
+			leftHandSide = expr(_assignment.leftHandSide());
-		arrayIndexAssignment(_assignment);
+
-		defineExpr(_assignment, expr(_assignment.rightHandSide()));
+		solAssert(leftHandSide, "");
+		smt::Expression rightHandSide =
+			compoundToArithmetic.count(op) ?
+				arithmeticOperation(
+					compoundToArithmetic.at(op),
+					*leftHandSide,
+					expr(_assignment.rightHandSide()),
+					_assignment.annotation().type,
+					_assignment.location()
+				) :
+				expr(_assignment.rightHandSide())
+		;
+		defineExpr(_assignment, rightHandSide);
+
+		if (identifier)
+			assignment(*decl, _assignment, _assignment.location());
+		else
+			arrayIndexAssignment(_assignment, expr(_assignment));
 	}
 	else
 		m_errorReporter.warning(
@@ -878,7 +911,7 @@ void SMTChecker::arrayAssignment()
 	m_arrayAssignmentHappened = true;
 }
 
-void SMTChecker::arrayIndexAssignment(Assignment const& _assignment)
+void SMTChecker::arrayIndexAssignment(Assignment const& _assignment, smt::Expression const& _rightHandSide)
 {
 	auto const& indexAccess = dynamic_cast<IndexAccess const&>(_assignment.leftHandSide());
 	if (auto const& id = dynamic_cast<Identifier const*>(&indexAccess.baseExpression()))
@@ -918,7 +951,7 @@ void SMTChecker::arrayIndexAssignment(Assignment const& _assignment)
 		smt::Expression store = smt::Expression::store(
 			m_variables[&varDecl]->currentValue(),
 			expr(*indexAccess.indexExpression()),
-			expr(_assignment.rightHandSide())
+			_rightHandSide
 		);
 		m_interface->addAssertion(newValue(varDecl) == store);
 		// Update the SMT select value after the assignment,
@@ -999,54 +1032,13 @@ void SMTChecker::arithmeticOperation(BinaryOperation const& _op)
 	case Token::Mul:
 	case Token::Div:
 	{
-		solAssert(_op.annotation().commonType, "");
+		defineExpr(_op, arithmeticOperation(
-		if (_op.annotation().commonType->category() != Type::Category::Integer)
+			_op.getOperator(),
-		{
+			expr(_op.leftExpression()),
-			m_errorReporter.warning(
+			expr(_op.rightExpression()),
-				_op.location(),
-				"Assertion checker does not yet implement this operator on non-integer types."
-			);
-			break;
-		}
-		auto const& intType = dynamic_cast<IntegerType const&>(*_op.annotation().commonType);
-		smt::Expression left(expr(_op.leftExpression()));
-		smt::Expression right(expr(_op.rightExpression()));
-		Token op = _op.getOperator();
-		smt::Expression value(
-			op == Token::Add ? left + right :
-			op == Token::Sub ? left - right :
-			op == Token::Div ? division(left, right, intType) :
-			/*op == Token::Mul*/ left * right
-		);
-
-		if (_op.getOperator() == Token::Div)
-		{
-			checkCondition(right == 0, _op.location(), "Division by zero", "<result>", &right);
-			m_interface->addAssertion(right != 0);
-		}
-
-		addOverflowTarget(
-			OverflowTarget::Type::All,
 			_op.annotation().commonType,
-			value,
 			_op.location()
-		);
-
-		smt::Expression intValueRange = (0 - minValue(intType)) + maxValue(intType) + 1;
-		defineExpr(_op, smt::Expression::ite(
-			value > maxValue(intType) || value < minValue(intType),
-			value % intValueRange,
-			value
 		));
-		if (intType.isSigned())
-		{
-			defineExpr(_op, smt::Expression::ite(
-				expr(_op) > maxValue(intType),
-				expr(_op) - intValueRange,
-				expr(_op)
-			));
-		}
-
 		break;
 	}
 	default:
@@ -1057,6 +1049,63 @@ void SMTChecker::arithmeticOperation(BinaryOperation const& _op)
 	}
 }
 
+smt::Expression SMTChecker::arithmeticOperation(
+	Token _op,
+	smt::Expression const& _left,
+	smt::Expression const& _right,
+	TypePointer const& _commonType,
+	langutil::SourceLocation const& _location
+)
+{
+	static set<Token> validOperators{
+		Token::Add,
+		Token::Sub,
+		Token::Mul,
+		Token::Div
+	};
+	solAssert(validOperators.count(_op), "");
+	solAssert(_commonType, "");
+	solAssert(_commonType->category() == Type::Category::Integer, "");
+
+	auto const& intType = dynamic_cast<IntegerType const&>(*_commonType);
+	smt::Expression value(
+		_op == Token::Add ? _left + _right :
+		_op == Token::Sub ? _left - _right :
+		_op == Token::Div ? division(_left, _right, intType) :
+		/*op == Token::Mul*/ _left * _right
+	);
+
+	if (_op == Token::Div)
+	{
+		checkCondition(_right == 0, _location, "Division by zero", "<result>", &_right);
+		m_interface->addAssertion(_right != 0);
+	}
+
+	addOverflowTarget(
+		OverflowTarget::Type::All,
+		_commonType,
+		value,
+		_location
+	);
+
+	smt::Expression intValueRange = (0 - minValue(intType)) + maxValue(intType) + 1;
+	value = smt::Expression::ite(
+		value > maxValue(intType) || value < minValue(intType),
+		value % intValueRange,
+		value
+	);
+	if (intType.isSigned())
+	{
+		value = smt::Expression::ite(
+			value > maxValue(intType),
+			value - intValueRange,
+			value
+		);
+	}
+
+	return value;
+}
+
 void SMTChecker::compareOperation(BinaryOperation const& _op)
 {
 	solAssert(_op.annotation().commonType, "");
@@ -1177,7 +1226,7 @@ void SMTChecker::checkCondition(
 	SourceLocation const& _location,
 	string const& _description,
 	string const& _additionalValueName,
-	smt::Expression* _additionalValue
+	smt::Expression const* _additionalValue
 )
 {
 	m_interface->push();

libsolidity/formal/SMTChecker.h

@@ -92,6 +92,16 @@ private:
 	/// Symbolic _expr is the rational literal.
 	bool shortcutRationalNumber(Expression const& _expr);
 	void arithmeticOperation(BinaryOperation const& _op);
+	/// @returns _op(_left, _right).
+	/// Used by the function above, compound assignments and
+	/// unary increment/decrement.
+	smt::Expression arithmeticOperation(
+		Token _op,
+		smt::Expression const& _left,
+		smt::Expression const& _right,
+		TypePointer const& _commonType,
+		langutil::SourceLocation const& _location
+	);
 	void compareOperation(BinaryOperation const& _op);
 	void booleanOperation(BinaryOperation const& _op);
 
@@ -117,7 +127,7 @@ private:
 	/// while aliasing is not supported.
 	void arrayAssignment();
 	/// Handles assignment to SMT array index.
-	void arrayIndexAssignment(Assignment const& _assignment);
+	void arrayIndexAssignment(Assignment const& _assignment, smt::Expression const& _rightHandSide);
 
 	/// Division expression in the given type. Requires special treatment because
 	/// of rounding for signed division.
@@ -141,7 +151,7 @@ private:
 		langutil::SourceLocation const& _location,
 		std::string const& _description,
 		std::string const& _additionalValueName = "",
-		smt::Expression* _additionalValue = nullptr
+		smt::Expression const* _additionalValue = nullptr
 	);
 	/// Checks that a boolean condition is not constant. Do not warn if the expression
 	/// is a literal constant.

test/libsolidity/SMTChecker.cpp

@@ -188,6 +188,48 @@ BOOST_AUTO_TEST_CASE(division_truncates_correctly)
 	CHECK_SUCCESS_NO_WARNINGS(text);
 }
 
+BOOST_AUTO_TEST_CASE(compound_assignment_division)
+{
+	string text = R"(
+		contract C {
+			function f(uint x) public pure {
+				require(x == 2);
+				uint y = 10;
+				y /= y / x;
+				assert(y == x);
+				assert(y == 0);
+			}
+		}
+	)";
+	CHECK_WARNING(text, "Assertion violation");
+	text = R"(
+		contract C {
+			uint[] array;
+			function f(uint x, uint p) public {
+				require(x == 2);
+				require(array[p] == 10);
+				array[p] /= array[p] / x;
+				assert(array[p] == x);
+				assert(array[p] == 0);
+			}
+		}
+	)";
+	CHECK_WARNING(text, "Assertion violation");
+	text = R"(
+		contract C {
+			mapping (uint => uint) map;
+			function f(uint x, uint p) public {
+				require(x == 2);
+				require(map[p] == 10);
+				map[p] /= map[p] / x;
+				assert(map[p] == x);
+				assert(map[p] == 0);
+			}
+		}
+	)";
+	CHECK_WARNING(text, "Assertion violation");
+}
+
 BOOST_AUTO_TEST_SUITE_END()
 
 }

test/libsolidity/smtCheckerTests/operators/compound_add.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x) public pure {
+		require(x < 100);
+		uint y = 100;
+		y += y + x;
+		assert(y < 300);
+		assert(y < 110);
+	}
+}
+// ----
+// Warning: (151-166): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/compound_add_array_index.sol

@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint[] array;
+	function f(uint x, uint p) public {
+		require(x < 100);
+		require(array[p] == 100);
+		array[p] += array[p] + x;
+		assert(array[p] < 300);
+		assert(array[p] < 110);
+	}
+}
+// ----
+// Warning: (202-224): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/compound_add_chain.sol

@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public pure {
+		uint a = 1;
+		uint b = 3;
+		uint c = 7;
+		a += b += c;
+		assert(b ==  10 && a == 11);
+		a += (b += c);
+		assert(b ==  17 && a == 28);
+		a += a += a;
+		assert(a == 112);
+	}
+}

test/libsolidity/smtCheckerTests/operators/compound_add_mapping.sol

@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	mapping (uint => uint) map;
+	function f(uint x, uint p) public {
+		require(x < 100);
+		require(map[p] == 100);
+		map[p] += map[p] + x;
+		assert(map[p] < 300);
+		assert(map[p] < 110);
+	}
+}
+// ----
+// Warning: (208-228): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/compound_mul.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x) public pure {
+		require(x < 10);
+		uint y = 10;
+		y *= y + x;
+		assert(y <= 190);
+		assert(y < 50);
+	}
+}
+// ----
+// Warning: (150-164): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/compound_mul_array_index.sol

@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint[] array;
+	function f(uint x, uint p) public {
+		require(x < 10);
+		require(array[p] == 10);
+		array[p] *= array[p] + x;
+		assert(array[p] <= 190);
+		assert(array[p] < 50);
+	}
+}
+// ----
+// Warning: (201-222): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/compound_mul_mapping.sol

@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	mapping (uint => uint) map;
+	function f(uint x, uint p) public {
+		require(x < 10);
+		require(map[p] == 10);
+		map[p] *= map[p] + x;
+		assert(map[p] <= 190);
+		assert(map[p] < 50);
+	}
+}
+// ----
+// Warning: (207-226): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/compound_sub.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x) public pure {
+		require(x < 100);
+		uint y = 200;
+		y -= y - x;
+		assert(y >= 0);
+		assert(y < 90);
+	}
+}
+// ----
+// Warning: (150-164): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/compound_sub_array_index.sol

@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint[] array;
+	function f(uint x, uint p) public {
+		require(x < 100);
+		require(array[p] == 200);
+		array[p] -= array[p] - x;
+		assert(array[p] >= 0);
+		assert(array[p] < 90);
+	}
+}
+// ----
+// Warning: (201-222): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/compound_sub_mapping.sol

@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	mapping (uint => uint) map;
+	function f(uint x, uint p) public {
+		require(x < 100);
+		require(map[p] == 200);
+		map[p] -= map[p] - x;
+		assert(map[p] >= 0);
+		assert(map[p] < 90);
+	}
+}
+// ----
+// Warning: (207-226): Assertion violation happens here