Merge pull request #9515 from ethereum/smt_fix_extra_parens

[SMTChecker] Fix ICE when tuples have extra effectless parens

Changelog.md

@@ -35,6 +35,7 @@ Bugfixes:
  * Inheritance: Disallow public state variables overwriting ``pure`` functions.
  * NatSpec: Constructors and functions have consistent userdoc output.
  * SMTChecker: Fix internal error when assigning to a 1-tuple.
+ * SMTChecker: Fix internal error when tuples have extra effectless parenthesis.
  * State Mutability: Constant public state variables are considered ``pure`` functions.
  * Type Checker: Fixing deduction issues on function types when function call has named arguments.
  * Immutables: Fix internal compiler error when immutables are not assigned.

libsolidity/formal/SMTEncoder.cpp

@@ -1470,7 +1470,7 @@ void SMTEncoder::assignment(
 
 void SMTEncoder::tupleAssignment(Expression const& _left, Expression const& _right)
 {
-	auto lTuple = dynamic_cast<TupleExpression const*>(&_left);
+	auto lTuple = dynamic_cast<TupleExpression const*>(innermostTuple(dynamic_cast<TupleExpression const&>(_left)));
 	solAssert(lTuple, "");
 
 	auto const& lComponents = lTuple->components();

test/libsolidity/smtCheckerTests/types/tuple_extra_parens_1.sol

@@ -0,0 +1,7 @@
+pragma experimental SMTChecker;
+contract C {
+	function f2() public pure returns(int) {
+		int a;
+		((, a)) = (1, 2);
+	}
+}

test/libsolidity/smtCheckerTests/types/tuple_extra_parens_2.sol

@@ -0,0 +1,7 @@
+pragma experimental SMTChecker;
+contract C {
+	function f2() public pure returns(int) {
+		int a;
+		(((, a),)) = ((1, 2), 3);
+	}
+}

test/libsolidity/smtCheckerTests/types/tuple_extra_parens_3.sol

@@ -0,0 +1,7 @@
+pragma experimental SMTChecker;
+contract C {
+	function f2() public pure returns(int) {
+		int a;
+		(((((((, a),)))))) = ((1, 2), 3);
+	}
+}

test/libsolidity/smtCheckerTests/types/tuple_extra_parens_4.sol

@@ -0,0 +1,7 @@
+pragma experimental SMTChecker;
+contract C {
+	function f2() public pure returns(int) {
+		int a;
+		((((((, a)))),)) = ((1, 2), 3);
+	}
+}

test/libsolidity/smtCheckerTests/types/tuple_extra_parens_5.sol

@@ -0,0 +1,7 @@
+pragma experimental SMTChecker;
+contract C {
+	function f2() public pure returns(int) {
+		int a;
+		((((((((((((, a))))))),))))) = ((1, 2), 3);
+	}
+}

test/libsolidity/smtCheckerTests/types/tuple_extra_parens_6.sol

@@ -0,0 +1,6 @@
+pragma experimental SMTChecker;
+contract C {
+	function f() public pure {
+		(((,))) = ((2),3);
+	}
+}