Merge pull request #6649 from ethereum/smt_tuple_asgn

[SMTChecker] Support tuple assignment

Changelog.md

@@ -6,7 +6,7 @@ Language Features:
 
 Compiler Features:
  * SMTChecker: Support inherited state variables.
- * SMTChecker: Support tuple declarations.
+ * SMTChecker: Support tuple assignments.
 
 
 Bugfixes:

libsolidity/formal/SMTChecker.cpp

@@ -368,13 +368,29 @@ void SMTChecker::endVisit(Assignment const& _assignment)
 		);
 	else
 	{
-		auto rightHandSide = compoundOps.count(op) ?
+		vector<smt::Expression> rightArguments;
-			compoundAssignment(_assignment) :
+		if (_assignment.rightHandSide().annotation().type->category() == Type::Category::Tuple)
-			expr(_assignment.rightHandSide());
+		{
-		defineExpr(_assignment, rightHandSide);
+			auto const& symbTuple = dynamic_pointer_cast<SymbolicTupleVariable>(m_expressions[&_assignment.rightHandSide()]);
+			solAssert(symbTuple, "");
+			for (auto const& component: symbTuple->components())
+			{
+				/// Right hand side tuple component cannot be empty.
+				solAssert(component, "");
+				rightArguments.push_back(component->currentValue());
+			}
+		}
+		else
+		{
+			auto rightHandSide = compoundOps.count(op) ?
+				compoundAssignment(_assignment) :
+				expr(_assignment.rightHandSide());
+			defineExpr(_assignment, rightHandSide);
+			rightArguments.push_back(expr(_assignment));
+		}
 		assignment(
 			_assignment.leftHandSide(),
-			expr(_assignment),
+			rightArguments,
 			_assignment.annotation().type,
 			_assignment.location()
 		);
@@ -1250,7 +1266,7 @@ smt::Expression SMTChecker::division(smt::Expression _left, smt::Expression _rig
 
 void SMTChecker::assignment(
 	Expression const& _left,
-	smt::Expression const& _right,
+	vector<smt::Expression> const& _right,
 	TypePointer const& _type,
 	langutil::SourceLocation const& _location
 )
@@ -1261,9 +1277,23 @@ void SMTChecker::assignment(
 			"Assertion checker does not yet implement type " + _type->toString()
 		);
 	else if (auto varDecl = identifierToVariable(_left))
-		assignment(*varDecl, _right, _location);
+	{
+		solAssert(_right.size() == 1, "");
+		assignment(*varDecl, _right.front(), _location);
+	}
 	else if (dynamic_cast<IndexAccess const*>(&_left))
-		arrayIndexAssignment(_left, _right);
+	{
+		solAssert(_right.size() == 1, "");
+		arrayIndexAssignment(_left, _right.front());
+	}
+	else if (auto tuple = dynamic_cast<TupleExpression const*>(&_left))
+	{
+		auto const& components = tuple->components();
+		solAssert(_right.size() == components.size(), "");
+		for (unsigned i = 0; i < _right.size(); ++i)
+			if (auto component = components.at(i))
+				assignment(*component, {_right.at(i)}, component->annotation().type, component->location());
+	}
 	else
 		m_errorReporter.warning(
 			_location,

libsolidity/formal/SMTChecker.h

@@ -141,7 +141,7 @@ private:
 	/// Will also be used for assignments of tuple components.
 	void assignment(
 		Expression const& _left,
-		smt::Expression const& _right,
+		std::vector<smt::Expression> const& _right,
 		TypePointer const& _type,
 		langutil::SourceLocation const& _location
 	);

test/libsolidity/smtCheckerTests/types/tuple_assignment.sol

@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function g() public pure {
+		uint x;
+		uint y;
+		(x, y) = (2, 4);
+		assert(x == 2);
+		assert(y == 4);
+	}
+}

test/libsolidity/smtCheckerTests/types/tuple_assignment_array.sol

@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint[] a;
+	function g(uint x, uint y) public {
+		require(x != y);
+		(a[x], a[y]) = (2, 4);
+		assert(a[x] == 2);
+		assert(a[y] == 4);
+	}
+}

test/libsolidity/smtCheckerTests/types/tuple_assignment_array_empty.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint[] a;
+	function g(uint x, uint y) public {
+		require(x != y);
+		(, a[y]) = (2, 4);
+		assert(a[x] == 2);
+		assert(a[y] == 4);
+	}
+}
+// ----
+// Warning: (136-153): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/tuple_assignment_empty.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function g() public pure {
+		uint x;
+		uint y;
+		(x, ) = (2, 4);
+		assert(x == 2);
+		assert(y == 4);
+	}
+}
+// ----
+// Warning: (132-146): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/tuple_declarations.sol

@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function g() public pure {
+		(uint x, uint y) = (2, 4);
+		assert(x == 2);
+		assert(y == 4);
+	}
+}
+// ----
+// Warning: (76-101): Assertion checker does not yet support such variable declarations.
+// Warning: (105-119): Assertion violation happens here