From 96a230af507187aa42d849a95f45cb551a61cd80 Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Mon, 2 Mar 2020 22:10:15 +0100
Subject: [PATCH] [SMTChecker] Fix ICEs with tuples

---
 Changelog.md                                      |  1 +
 libsolidity/formal/SMTEncoder.cpp                 | 15 +++++++++++----
 .../smtCheckerTests/types/function_in_tuple_1.sol | 10 ++++++++++
 .../smtCheckerTests/types/function_in_tuple_2.sol | 10 ++++++++++
 .../types/tuple_single_element_1.sol              |  9 +++++++++
 .../types/tuple_single_element_2.sol              |  9 +++++++++
 .../types/tuple_single_non_tuple_element.sol      |  9 +++++++++
 7 files changed, 59 insertions(+), 4 deletions(-)
 create mode 100644 test/libsolidity/smtCheckerTests/types/function_in_tuple_1.sol
 create mode 100644 test/libsolidity/smtCheckerTests/types/function_in_tuple_2.sol
 create mode 100644 test/libsolidity/smtCheckerTests/types/tuple_single_element_1.sol
 create mode 100644 test/libsolidity/smtCheckerTests/types/tuple_single_element_2.sol
 create mode 100644 test/libsolidity/smtCheckerTests/types/tuple_single_non_tuple_element.sol

diff --git a/Changelog.md b/Changelog.md
index f151365ae..fc5d3d0d3 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -11,6 +11,7 @@ Compiler Features:
 Bugfixes:
  * isoltest: Added new keyword `wei` to express function value in semantic tests
  * Standard-JSON-Interface: Fix a bug related to empty filenames and imports.
+ * SMTChecker: Fix internal errors when analysing tuples.
 
 
 ### 0.6.3 (2020-02-18)
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index ac81a5d87..3b2f48816 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -407,19 +407,26 @@ void SMTEncoder::endVisit(TupleExpression const& _tuple)
 		auto const& symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(_tuple));
 		solAssert(symbTuple, "");
 		auto const& symbComponents = symbTuple->components();
-		auto const& tupleComponents = _tuple.components();
-		solAssert(symbComponents.size() == _tuple.components().size(), "");
+		auto const* tupleComponents = &_tuple.components();
+		while (tupleComponents->size() == 1)
+		{
+			auto innerTuple = dynamic_pointer_cast<TupleExpression>(tupleComponents->front());
+			solAssert(innerTuple, "");
+			tupleComponents = &innerTuple->components();
+		}
+		solAssert(symbComponents.size() == tupleComponents->size(), "");
 		for (unsigned i = 0; i < symbComponents.size(); ++i)
 		{
 			auto sComponent = symbComponents.at(i);
-			auto tComponent = tupleComponents.at(i);
+			auto tComponent = tupleComponents->at(i);
 			if (sComponent && tComponent)
 			{
 				if (auto varDecl = identifierToVariable(*tComponent))
 					m_context.addAssertion(sComponent->currentValue() == currentValue(*varDecl));
 				else
 				{
-					solAssert(m_context.knownExpression(*tComponent), "");
+					if (!m_context.knownExpression(*tComponent))
+						createExpr(*tComponent);
 					m_context.addAssertion(sComponent->currentValue() == expr(*tComponent));
 				}
 			}
diff --git a/test/libsolidity/smtCheckerTests/types/function_in_tuple_1.sol b/test/libsolidity/smtCheckerTests/types/function_in_tuple_1.sol
new file mode 100644
index 000000000..4d1d954f7
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/function_in_tuple_1.sol
@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract K {
+	function f() public pure {
+		(abi.encode, 2);
+	}
+}
+// ----
+// Warning: (76-91): Statement has no effect.
+// Warning: (77-80): Assertion checker does not yet implement type abi
diff --git a/test/libsolidity/smtCheckerTests/types/function_in_tuple_2.sol b/test/libsolidity/smtCheckerTests/types/function_in_tuple_2.sol
new file mode 100644
index 000000000..5b9c2f41c
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/function_in_tuple_2.sol
@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract K {
+	function f() public pure {
+		(abi.encode, "");
+	}
+}
+// ----
+// Warning: (76-92): Statement has no effect.
+// Warning: (77-80): Assertion checker does not yet implement type abi
diff --git a/test/libsolidity/smtCheckerTests/types/tuple_single_element_1.sol b/test/libsolidity/smtCheckerTests/types/tuple_single_element_1.sol
new file mode 100644
index 000000000..f14ca9bc1
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/tuple_single_element_1.sol
@@ -0,0 +1,9 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		(("", 2));
+	}
+}
+// ----
+// Warning: (76-85): Statement has no effect.
diff --git a/test/libsolidity/smtCheckerTests/types/tuple_single_element_2.sol b/test/libsolidity/smtCheckerTests/types/tuple_single_element_2.sol
new file mode 100644
index 000000000..29b9c9747
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/tuple_single_element_2.sol
@@ -0,0 +1,9 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		(("", ""));
+	}
+}
+// ----
+// Warning: (76-86): Statement has no effect.
diff --git a/test/libsolidity/smtCheckerTests/types/tuple_single_non_tuple_element.sol b/test/libsolidity/smtCheckerTests/types/tuple_single_non_tuple_element.sol
new file mode 100644
index 000000000..2a99a552e
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/tuple_single_non_tuple_element.sol
@@ -0,0 +1,9 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		(2);
+	}
+}
+// ----
+// Warning: (76-79): Statement has no effect.