Merge pull request #13754 from ethereum/smt_fix_assignment

Fix internal error in assignment chains

Changelog.md

@@ -25,6 +25,7 @@ Bugfixes:
  * SMTChecker: Improved readability for large integers that are powers of two or almost powers of two in error messages.
  * SMTChecker: Fix internal error when a public library function is called internally.
  * SMTChecker: Fix internal error on multiple wrong SMTChecker natspec entries.
+ * SMTChecker: Fix internal error on chain assignments using static fully specified state variables.
 
 
 ### 0.8.17 (2022-09-08)

libsolidity/formal/SMTEncoder.cpp

@@ -2757,7 +2757,9 @@ VariableDeclaration const* SMTEncoder::identifierToVariable(Expression const& _e
 		}
 	// But we are interested in "contract.var", because that is the same as just "var".
 	if (auto const* memberAccess = dynamic_cast<MemberAccess const*>(&_expr))
-		if (dynamic_cast<ContractDefinition const*>(expressionToDeclaration(memberAccess->expression())))
+		if (dynamic_cast<ContractDefinition const*>(expressionToDeclaration(
+			*cleanExpression(memberAccess->expression())
+		)))
 			if (auto const* varDecl = dynamic_cast<VariableDeclaration const*>(memberAccess->annotation().referencedDeclaration))
 			{
 				solAssert(m_context.knownVariable(*varDecl), "");

test/libsolidity/smtCheckerTests/operators/assignment_chain_tuple_contract_1.sol

@@ -0,0 +1,10 @@
+contract C {
+    string public name = (C).name = type(C).name;
+
+    function f() external view {
+        assert(keccak256(bytes(name)) == keccak256(bytes("C"))); // should fail because SMTChecker doesn't support type(C).name
+    }
+}
+// ----
+// Warning 7507: (49-61): Assertion checker does not yet support this expression.
+// Warning 6328: (105-160): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()

test/libsolidity/smtCheckerTests/operators/assignment_chain_tuple_contract_2.sol

@@ -0,0 +1,13 @@
+contract C {
+    uint x = ((((C)))).x = ((C)).x = 2;
+
+    function f() external view {
+        assert(x == 2); // should hold
+    }
+
+    function g() external view {
+        assert(x != 2); // should fail
+    }
+}
+// ----
+// Warning 6328: (174-188): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor()\nState: x = 2\nC.g()

test/libsolidity/smtCheckerTests/operators/assignment_chain_tuple_contract_3.sol

@@ -0,0 +1,22 @@
+contract C {
+    uint x = ((((C)))).x = ((C)).x = 2;
+
+    function f() external view {
+        assert(x == 2); // should fail for D
+    }
+
+    function g() external view {
+        assert(x != 2); // should fail for C
+    }
+}
+
+contract D is C {
+    uint y = ((C)).x = 3;
+
+    function h() external view {
+        assert(y == 3); // should hold
+    }
+}
+// ----
+// Warning 6328: (95-109): CHC: Assertion violation happens here.\nCounterexample:\ny = 3, x = 3\n\nTransaction trace:\nD.constructor()\nState: y = 3, x = 3\nC.f()
+// Warning 6328: (180-194): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor()\nState: x = 2\nC.g()