Merge pull request #13762 from ethereum/smt_fix_delete

Fix internal error when deleting struct member of function type

Changelog.md

@@ -27,6 +27,7 @@ Bugfixes:
  * SMTChecker: Fix internal error on multiple wrong SMTChecker natspec entries.
  * SMTChecker: Fix internal error on chain assignments using static fully specified state variables.
  * SMTChecker: Fix internal error when using user defined types as mapping indices or struct members.
+ * SMTChecker: Fix internal error when deleting struct member of function type.
 
 
 ### 0.8.17 (2022-09-08)

libsolidity/formal/SMTEncoder.cpp

@@ -586,15 +586,6 @@ bool SMTEncoder::visit(FunctionCall const& _funCall)
 			arg->accept(*this);
 		return false;
 	}
-	else if (funType.kind() == FunctionType::Kind::ABIEncodeCall)
-	{
-		auto fun = _funCall.arguments().front();
-		createExpr(*fun);
-		auto const* functionType = dynamic_cast<FunctionType const*>(fun->annotation().type);
-		if (functionType->hasDeclaration())
-			defineExpr(*fun, functionType->externalIdentifier());
-		return true;
-	}
 
 	// We do not really need to visit the expression in a wrap/unwrap no-op call,
 	// so we just ignore the function call expression to avoid "unsupported" warnings.
@@ -1323,11 +1314,17 @@ void SMTEncoder::endVisit(Return const& _return)
 
 bool SMTEncoder::visit(MemberAccess const& _memberAccess)
 {
+	createExpr(_memberAccess);
+
 	auto const& accessType = _memberAccess.annotation().type;
 	if (accessType->category() == Type::Category::Function)
-		return true;
+	{
+		auto const* functionType = dynamic_cast<FunctionType const*>(_memberAccess.annotation().type);
+		if (functionType && functionType->hasDeclaration())
+			defineExpr(_memberAccess, functionType->externalIdentifier());
 
-	createExpr(_memberAccess);
+		return true;
+	}
 
 	Expression const* memberExpr = innermostTuple(_memberAccess.expression());
 

test/libsolidity/smtCheckerTests/abi/abi_encode_function.sol

@@ -6,4 +6,3 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6031: (54-60): Internal error: Expression undefined for SMT solver.

test/libsolidity/smtCheckerTests/functions/getters/function.sol

@@ -15,5 +15,6 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (152-170): CHC: Assertion violation happens here.\nCounterexample:\ng = 0\ne = 0\n\nTransaction trace:\nC.constructor()\nState: g = 0\nC.f()\n    e() -- untrusted external call\n    g() -- untrusted external call
+// Warning 8364: (140-146): Assertion checker does not yet implement type function () view external returns (function () external returns (uint256))
-// Warning 6328: (262-278): CHC: Assertion violation happens here.\nCounterexample:\ng = 0\ne = 0\n\nTransaction trace:\nC.constructor()\nState: g = 0\nC.f()\n    e() -- untrusted external call\n    g() -- untrusted external call\n    e() -- untrusted external call
+// Warning 6328: (152-170): CHC: Assertion violation happens here.
+// Warning 6328: (262-278): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/getters/struct_4.sol

@@ -19,4 +19,5 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 2072: (146-183): Unused local variable.
-// Warning 6328: (234-269): CHC: Assertion violation happens here.\nCounterexample:\ns = {d: 0, f: 0}\nd = 0\nf = 0\n\nTransaction trace:\nC.constructor()\nState: s = {d: 0, f: 0}\nC.test()
+// Warning 8364: (187-193): Assertion checker does not yet implement type function () view external returns (contract D,function () external returns (uint256))
+// Warning 6328: (234-269): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/imports/import_library_2.sol

@@ -25,4 +25,4 @@ contract ERC20 {
 // ====
 // SMTEngine: all
 // ----
-// Warning 3944: (ERC20.sol:157-162): CHC: Underflow (resulting value less than 0) happens here.\nCounterexample:\n\namount = 1\n\nTransaction trace:\nERC20.constructor()\nERC20.transferFrom(1){ msg.sender: 0x52f6 }\n    SafeMath.sub(0, 1) -- internal call
+// Warning 3944: (ERC20.sol:157-162): CHC: Underflow (resulting value less than 0) happens here.

test/libsolidity/smtCheckerTests/operators/delete_function_type_1.sol

@@ -0,0 +1,16 @@
+struct S {
+    function() e;
+}
+
+contract C {
+    S s;
+    function() f;
+
+    constructor() {
+        delete s.e;
+        assert(s.e == f); // should fail for now because function pointer comparisons are not supported
+    }
+}
+// ----
+// Warning 7229: (128-136): Assertion checker does not yet implement the type function () for comparisons
+// Warning 6328: (121-137): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/delete_function_type_2.sol

@@ -0,0 +1,13 @@
+contract C {
+    mapping (uint => function()) m;
+    function() f;
+
+    constructor() {
+        m[2] = f;
+        delete m[2];
+        assert(m[2] == f); // should fail for now because function pointer comparisons are not supported
+    }
+}
+// ----
+// Warning 7229: (142-151): Assertion checker does not yet implement the type function () for comparisons
+// Warning 6328: (135-152): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/delete_function_type_3.sol

@@ -0,0 +1,19 @@
+contract C {
+    function()[] arr;
+    function() f;
+
+    constructor() {
+        arr.push();
+        arr.push();
+        arr[1] = f;
+        delete arr[1];
+        assert(arr[1] == f); // should fail for now because function pointer comparisons are not supported
+    }
+}
+// ----
+// Warning 8364: (82-90): Assertion checker does not yet implement type function (function ()[] storage pointer) returns (function ())
+// Warning 8364: (102-110): Assertion checker does not yet implement type function (function ()[] storage pointer) returns (function ())
+// Warning 7229: (172-183): Assertion checker does not yet implement the type function () for comparisons
+// Warning 6368: (149-155): CHC: Out of bounds access happens here.
+// Warning 6368: (172-178): CHC: Out of bounds access happens here.
+// Warning 6328: (165-184): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/types/address_transfer.sol

@@ -11,5 +11,5 @@ contract C
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (162-186): CHC: Assertion violation happens here.\nCounterexample:\n\na = 0x0\nx = 100\n\nTransaction trace:\nC.constructor()\nC.f(0x0)
+// Warning 6328: (162-186): CHC: Assertion violation happens here.
 // Warning 1236: (98-113): BMC: Insufficient funds happens here.

test/libsolidity/smtCheckerTests/types/array_dynamic_2_fail.sol

@@ -15,4 +15,4 @@ contract C
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (245-270): CHC: Assertion violation happens here.\nCounterexample:\narray = [[200]]\nx = 0\ny = 0\nz = 0\nt = 0\n\nTransaction trace:\nC.constructor()\nState: array = []\nC.a()\nState: array = [[0]]\nC.f(0, 0, 0, 0)
+// Warning 6328: (245-270): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/types/array_dynamic_3_fail.sol

@@ -16,4 +16,4 @@ contract C
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (318-346): CHC: Assertion violation happens here.\nCounterexample:\narray = [[[200]]]\nx = 0\ny = 0\nz = 0\nt = 0\nw = 0\nv = 0\n\nTransaction trace:\nC.constructor()\nState: array = []\nC.p()\nState: array = [[[0]]]\nC.f(0, 0, 0, 0, 0, 0)
+// Warning 6328: (318-346): CHC: Assertion violation happens here.