Merge pull request ethereum#9709 from ethereum/smt_fix_tuple_3

[SMTChecker] Fix ICE on tuples of one element of tuple type

Author: Leonardo

Changelog.md

@@ -22,6 +22,7 @@ Bugfixes:
  * SMTChecker: Fix internal error on fixed bytes index access.
  * SMTChecker: Fix internal error on lvalue unary operators with tuples.
  * SMTChecker: Fix internal error on tuple assignment.
+ * SMTChecker: Fix internal error on tuples of one element that have tuple type.
  * SMTChecker: Fix soundness of array ``pop``.
  * References Resolver: Fix internal bug when using constructor for library.
  * Yul Optimizer: Make function inlining order more resilient to whether or not unrelated source files are present.

libsolidity/formal/SMTEncoder.cpp

@@ -420,8 +420,11 @@ void SMTEncoder::endVisit(TupleExpression const& _tuple)
 			_tuple.location(),
 			"Assertion checker does not yet implement inline arrays."
 		);
-	else if (_tuple.annotation().type->category() == Type::Category::Tuple)
+	else if (_tuple.components().size() == 1)
+		defineExpr(_tuple, expr(*_tuple.components().front()));
+	else
 	{
+		solAssert(_tuple.annotation().type->category() == Type::Category::Tuple, "");
 		auto const& symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(_tuple));
 		solAssert(symbTuple, "");
 		auto const& symbComponents = symbTuple->components();
@@ -445,13 +448,6 @@ void SMTEncoder::endVisit(TupleExpression const& _tuple)
 			}
 		}
 	}
-	else
-	{
-		/// Parenthesized expressions are also TupleExpression regardless their type.
-		auto const& components = _tuple.components();
-		solAssert(components.size() == 1, "");
-		defineExpr(_tuple, expr(*components.front()));
-	}
 }
 
 void SMTEncoder::endVisit(UnaryOperation const& _op)

test/libsolidity/smtCheckerTests/types/tuple_extra_parens_7.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+contract C {
+	function g() internal pure returns (uint, uint) {
+		return (2, 3);
+	}
+	function f() public {
+		(address(1).call(""));
+		(uint x, uint y) = ((g()));
+		assert(x == 2);
+		assert(y == 3);
+	}
+}
+// ----
+// Warning 5084: (142-152): Type conversion is not yet fully supported and might yield false positives.