Refactor assignment handling

libsolidity/formal/SMTChecker.cpp

@@ -341,15 +341,15 @@ void SMTChecker::endVisit(VariableDeclarationStatement const& _varDecl)
 
 void SMTChecker::endVisit(Assignment const& _assignment)
 {
-	static map<Token, Token> const compoundToArithmetic{
+	static set<Token> const compoundOps{
-		{Token::AssignAdd, Token::Add},
+		Token::AssignAdd,
-		{Token::AssignSub, Token::Sub},
+		Token::AssignSub,
-		{Token::AssignMul, Token::Mul},
+		Token::AssignMul,
-		{Token::AssignDiv, Token::Div},
+		Token::AssignDiv,
-		{Token::AssignMod, Token::Mod}
+		Token::AssignMod
 	};
 	Token op = _assignment.assignmentOperator();
-	if (op != Token::Assign && !compoundToArithmetic.count(op))
+	if (op != Token::Assign && !compoundOps.count(op))
 		m_errorReporter.warning(
 			_assignment.location(),
 			"Assertion checker does not yet implement this assignment operator."
@@ -359,48 +359,19 @@ void SMTChecker::endVisit(Assignment const& _assignment)
 			_assignment.location(),
 			"Assertion checker does not yet implement type " + _assignment.annotation().type->toString()
 		);
-	else if (
-		dynamic_cast<Identifier const*>(&_assignment.leftHandSide()) ||
-		dynamic_cast<IndexAccess const*>(&_assignment.leftHandSide())
-	)
-	{
-		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());
+	{
-
+		auto rightHandSide = compoundOps.count(op) ?
-		solAssert(leftHandSide, "");
+			compoundAssignment(_assignment) :
-		smt::Expression rightHandSide =
+			expr(_assignment.rightHandSide());
-			compoundToArithmetic.count(op) ?
+		defineExpr(_assignment, rightHandSide);
-				arithmeticOperation(
+		assignment(
-					compoundToArithmetic.at(op),
+			_assignment.leftHandSide(),
-					*leftHandSide,
+			expr(_assignment),
-					expr(_assignment.rightHandSide()),
 			_assignment.annotation().type,
 			_assignment.location()
-				) :
-				expr(_assignment.rightHandSide())
-		;
-		defineExpr(_assignment, rightHandSide);
-
-		if (identifier)
-			assignment(*decl, _assignment, _assignment.location());
-		else
-			arrayIndexAssignment(_assignment.leftHandSide(), expr(_assignment));
-	}
-	else
-		m_errorReporter.warning(
-			_assignment.location(),
-			"Assertion checker does not yet implement such assignments."
 		);
+	}
 }
 
 void SMTChecker::endVisit(TupleExpression const& _tuple)
@@ -1237,6 +1208,50 @@ smt::Expression SMTChecker::division(smt::Expression _left, smt::Expression _rig
 		return _left / _right;
 }
 
+void SMTChecker::assignment(
+	Expression const& _left,
+	smt::Expression const& _right,
+	TypePointer const& _type,
+	langutil::SourceLocation const& _location
+)
+{
+	if (!isSupportedType(_type->category()))
+		m_errorReporter.warning(
+			_location,
+			"Assertion checker does not yet implement type " + _type->toString()
+		);
+	else if (auto varDecl = identifierToVariable(_left))
+		assignment(*varDecl, _right, _location);
+	else if (dynamic_cast<IndexAccess const*>(&_left))
+		arrayIndexAssignment(_left, _right);
+	else
+		m_errorReporter.warning(
+			_location,
+			"Assertion checker does not yet implement such assignments."
+		);
+}
+
+smt::Expression SMTChecker::compoundAssignment(Assignment const& _assignment)
+{
+	static map<Token, Token> const compoundToArithmetic{
+		{Token::AssignAdd, Token::Add},
+		{Token::AssignSub, Token::Sub},
+		{Token::AssignMul, Token::Mul},
+		{Token::AssignDiv, Token::Div},
+		{Token::AssignMod, Token::Mod}
+	};
+	Token op = _assignment.assignmentOperator();
+	solAssert(compoundToArithmetic.count(op), "");
+	auto decl = identifierToVariable(_assignment.leftHandSide());
+	return arithmeticOperation(
+		compoundToArithmetic.at(op),
+		decl ? currentValue(*decl) : expr(_assignment.leftHandSide()),
+		expr(_assignment.rightHandSide()),
+		_assignment.annotation().type,
+		_assignment.location()
+	);
+}
+
 void SMTChecker::assignment(VariableDeclaration const& _variable, Expression const& _value, SourceLocation const& _location)
 {
 	assignment(_variable, expr(_value), _location);
@@ -1811,3 +1826,16 @@ set<VariableDeclaration const*> SMTChecker::touchedVariables(ASTNode const& _nod
 	solAssert(!m_functionPath.empty(), "");
 	return m_variableUsage.touchedVariables(_node, m_functionPath);
 }
+
+VariableDeclaration const* SMTChecker::identifierToVariable(Expression const& _expr)
+{
+	if (auto identifier = dynamic_cast<Identifier const*>(&_expr))
+	{
+		if (auto decl = dynamic_cast<VariableDeclaration const*>(identifier->annotation().referencedDeclaration))
+		{
+			solAssert(knownVariable(*decl), "");
+			return decl;
+		}
+	}
+	return nullptr;
+}

libsolidity/formal/SMTChecker.h

@@ -135,7 +135,18 @@ private:
 	smt::Expression division(smt::Expression _left, smt::Expression _right, IntegerType const& _type);
 
 	void assignment(VariableDeclaration const& _variable, Expression const& _value, langutil::SourceLocation const& _location);
+	/// Handles assignments to variables of different types.
 	void assignment(VariableDeclaration const& _variable, smt::Expression const& _value, langutil::SourceLocation const& _location);
+	/// Handles assignments between generic expressions.
+	/// Will also be used for assignments of tuple components.
+	void assignment(
+		Expression const& _left,
+		smt::Expression const& _right,
+		TypePointer const& _type,
+		langutil::SourceLocation const& _location
+	);
+	/// Computes the right hand side of a compound assignment.
+	smt::Expression compoundAssignment(Assignment const& _assignment);
 
 	/// Maps a variable to an SSA index.
 	using VariableIndices = std::unordered_map<VariableDeclaration const*, int>;
@@ -274,6 +285,9 @@ private:
 	/// @returns variables that are touched in _node's subtree.
 	std::set<VariableDeclaration const*> touchedVariables(ASTNode const& _node);
 
+	/// @returns the VariableDeclaration referenced by an Identifier or nullptr.
+	VariableDeclaration const* identifierToVariable(Expression const& _expr);
+
 	std::shared_ptr<smt::SolverInterface> m_interface;
 	VariableUsage m_variableUsage;
 	bool m_loopExecutionHappened = false;