[SMTChecker] Support tuple type declaration

Changelog.md

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

libsolidity/formal/SMTChecker.cpp

@@ -383,17 +383,41 @@ void SMTChecker::endVisit(Assignment const& _assignment)
 
 void SMTChecker::endVisit(TupleExpression const& _tuple)
 {
-	if (
+	if (_tuple.isInlineArray())
-		_tuple.isInlineArray() ||
-		_tuple.components().size() != 1 ||
-		!isSupportedType(_tuple.components()[0]->annotation().type->category())
-	)
 		m_errorReporter.warning(
 			_tuple.location(),
-			"Assertion checker does not yet implement tuples and inline arrays."
+			"Assertion checker does not yet implement inline arrays."
 		);
+	else if (_tuple.annotation().type->category() == Type::Category::Tuple)
+	{
+		createExpr(_tuple);
+		vector<shared_ptr<SymbolicVariable>> components;
+		for (auto const& component: _tuple.components())
+			if (component)
+			{
+				if (auto varDecl = identifierToVariable(*component))
+					components.push_back(m_variables[varDecl]);
+				else
+				{
+					solAssert(knownExpr(*component), "");
+					components.push_back(m_expressions[component.get()]);
+				}
+			}
+			else
+				components.push_back(nullptr);
+		solAssert(components.size() == _tuple.components().size(), "");
+		auto const& symbTuple = dynamic_pointer_cast<SymbolicTupleVariable>(m_expressions[&_tuple]);
+		solAssert(symbTuple, "");
+		symbTuple->setComponents(move(components));
+	}
 	else
-		defineExpr(_tuple, expr(*_tuple.components()[0]));
+	{
+		/// Parenthesized expressions are also TupleExpression regardless their type.
+		auto const& components = _tuple.components();
+		solAssert(components.size() == 1, "");
+		if (isSupportedType(components.front()->annotation().type->category()))
+			defineExpr(_tuple, expr(*components.front()));
+	}
 }
 
 void SMTChecker::addOverflowTarget(

libsolidity/formal/SymbolicTypes.cpp

@@ -99,7 +99,8 @@ bool dev::solidity::isSupportedType(Type::Category _category)
 	return isNumber(_category) ||
 		isBool(_category) ||
 		isMapping(_category) ||
-		isArray(_category);
+		isArray(_category) ||
+		isTuple(_category);
 }
 
 bool dev::solidity::isSupportedTypeDeclaration(Type::Category _category)
@@ -151,6 +152,8 @@ pair<bool, shared_ptr<SymbolicVariable>> dev::solidity::newSymbolicVariable(
 		var = make_shared<SymbolicMappingVariable>(type, _uniqueName, _solver);
 	else if (isArray(_type.category()))
 		var = make_shared<SymbolicArrayVariable>(type, _uniqueName, _solver);
+	else if (isTuple(_type.category()))
+		var = make_shared<SymbolicTupleVariable>(type, _uniqueName, _solver);
 	else
 		solAssert(false, "");
 	return make_pair(abstract, var);
@@ -226,6 +229,11 @@ bool dev::solidity::isArray(Type::Category _category)
 	return _category == Type::Category::Array;
 }
 
+bool dev::solidity::isTuple(Type::Category _category)
+{
+	return _category == Type::Category::Tuple;
+}
+
 smt::Expression dev::solidity::minValue(IntegerType const& _type)
 {
 	return smt::Expression(_type.minValue());

libsolidity/formal/SymbolicTypes.h

@@ -51,6 +51,7 @@ bool isBool(Type::Category _category);
 bool isFunction(Type::Category _category);
 bool isMapping(Type::Category _category);
 bool isArray(Type::Category _category);
+bool isTuple(Type::Category _category);
 
 /// Returns a new symbolic variable, according to _type.
 /// Also returns whether the type is abstract or not,

libsolidity/formal/SymbolicVariables.cpp

@@ -173,3 +173,21 @@ SymbolicEnumVariable::SymbolicEnumVariable(
 {
 	solAssert(isEnum(m_type->category()), "");
 }
+
+SymbolicTupleVariable::SymbolicTupleVariable(
+	TypePointer _type,
+	string _uniqueName,
+	smt::SolverInterface& _interface
+):
+	SymbolicVariable(move(_type), move(_uniqueName), _interface)
+{
+	solAssert(isTuple(m_type->category()), "");
+}
+
+void SymbolicTupleVariable::setComponents(vector<shared_ptr<SymbolicVariable>> _components)
+{
+	solAssert(m_components.empty(), "");
+	auto const& tupleType = dynamic_cast<TupleType const*>(m_type);
+	solAssert(_components.size() == tupleType->components().size(), "");
+	m_components = move(_components);
+}

libsolidity/formal/SymbolicVariables.h

@@ -187,5 +187,28 @@ public:
 	);
 };
 
+/**
+ * Specialization of SymbolicVariable for Tuple
+ */
+class SymbolicTupleVariable: public SymbolicVariable
+{
+public:
+	SymbolicTupleVariable(
+		TypePointer _type,
+		std::string _uniqueName,
+		smt::SolverInterface& _interface
+	);
+
+	std::vector<std::shared_ptr<SymbolicVariable>> const& components()
+	{
+		return m_components;
+	}
+
+	void setComponents(std::vector<std::shared_ptr<SymbolicVariable>> _components);
+
+private:
+	std::vector<std::shared_ptr<SymbolicVariable>> m_components;
+};
+
 }
 }

test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple.sol

@@ -12,4 +12,3 @@ contract C
 }
 
 // ----
-// Warning: (153-156): Assertion checker does not yet implement tuples and inline arrays.

test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple_fail.sol

@@ -12,5 +12,4 @@ contract C
 }
 
 // ----
-// Warning: (153-156): Assertion checker does not yet implement tuples and inline arrays.
 // Warning: (163-176): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/address_transfer.sol

@@ -12,5 +12,4 @@ contract C
 }
 // ----
 // Warning: (131-146): Insufficient funds happens here
-// Warning: (131-146): Assertion checker does not yet implement this type.
 // Warning: (195-219): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/address_transfer_2.sol

@@ -15,7 +15,5 @@ contract C
 }
 // ----
 // Warning: (217-232): Insufficient funds happens here
-// Warning: (217-232): Assertion checker does not yet implement this type.
 // Warning: (236-251): Insufficient funds happens here
-// Warning: (236-251): Assertion checker does not yet implement this type.
 // Warning: (295-324): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/address_transfer_insufficient.sol

@@ -12,7 +12,5 @@ contract C
 }
 // ----
 // Warning: (134-149): Insufficient funds happens here
-// Warning: (134-149): Assertion checker does not yet implement this type.
 // Warning: (153-169): Insufficient funds happens here
-// Warning: (153-169): Assertion checker does not yet implement this type.
 // Warning: (213-237): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/array_literal_1.sol

@@ -8,5 +8,5 @@ contract C
 }
 // ----
 // Warning: (76-96): Unused local variable.
-// Warning: (99-114): Assertion checker does not yet implement tuples and inline arrays.
+// Warning: (99-114): Assertion checker does not yet implement inline arrays.
 // Warning: (99-114): Internal error: Expression undefined for SMT solver.

test/libsolidity/smtCheckerTests/types/tuple_assignment_compound.sol

@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public pure {
+		uint a = 1;
+		uint b = 3;
+		a += ((((b))));
+		assert(a == 3);
+	}
+}
+// ----
+// Warning: (122-136): Assertion violation happens here