From 15269067b57cabfaba2de86671c2a9844810fce9 Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Thu, 28 Mar 2019 12:43:20 +0100
Subject: [PATCH] Support arithmetic compound assignment operators

---
 Changelog.md                      |  1 +
 libsolidity/formal/SMTChecker.cpp | 61 ++++++++++++++++++++++++-------
 libsolidity/formal/SMTChecker.h   |  2 +-
 3 files changed, 49 insertions(+), 15 deletions(-)

diff --git a/Changelog.md b/Changelog.md
index 5d46ee6f6..8744665a4 100644
--- a/Changelog.md
+++ b/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.
 
 
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index db9aa7c55..a9592370d 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/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);
-		solAssert(knownVariable(decl), "");
-		assignment(decl, _assignment.rightHandSide(), _assignment.location());
-		defineExpr(_assignment, expr(_assignment.rightHandSide()));
-	}
-	else if (dynamic_cast<IndexAccess const*>(&_assignment.leftHandSide()))
-	{
-		arrayIndexAssignment(_assignment);
-		defineExpr(_assignment, expr(_assignment.rightHandSide()));
+		boost::optional<smt::Expression> leftHandSide;
+		VariableDeclaration const* decl = nullptr;
+		auto identifier = dynamic_cast<Identifier const*>(&_assignment.leftHandSide());
+		if (identifier)
+		{
+			decl = dynamic_cast<VariableDeclaration const*>(identifier->annotation().referencedDeclaration);
+			solAssert(decl, "");
+			solAssert(knownVariable(*decl), "");
+			leftHandSide = currentValue(*decl);
+		}
+		else
+			leftHandSide = expr(_assignment.leftHandSide());
+
+		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(
@@ -890,7 +923,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()))
@@ -930,7 +963,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,
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index 9c5ba761b..4d4f67b21 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -123,7 +123,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.