From 77698f8108e6fad115d46d37fdc6de0592607a4a Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Tue, 29 Nov 2022 13:14:40 +0100 Subject: [PATCH] Fix internal error when deleting struct member of function type --- Changelog.md | 1 + libsolidity/formal/SMTEncoder.cpp | 19 ++++++++----------- .../abi/abi_encode_function.sol | 1 - .../functions/getters/function.sol | 5 +++-- .../functions/getters/struct_4.sol | 3 ++- .../imports/import_library_2.sol | 2 +- .../operators/delete_function_type_1.sol | 16 ++++++++++++++++ .../operators/delete_function_type_2.sol | 13 +++++++++++++ .../operators/delete_function_type_3.sol | 19 +++++++++++++++++++ .../types/address_transfer.sol | 2 +- .../types/array_dynamic_2_fail.sol | 2 +- .../types/array_dynamic_3_fail.sol | 2 +- 12 files changed, 66 insertions(+), 19 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/operators/delete_function_type_1.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/delete_function_type_2.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/delete_function_type_3.sol diff --git a/Changelog.md b/Changelog.md index f075e4c32..17294f6b2 100644 --- a/Changelog.md +++ b/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) diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index adae21412..eea459737 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/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(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(_memberAccess.annotation().type); + if (functionType && functionType->hasDeclaration()) + defineExpr(_memberAccess, functionType->externalIdentifier()); - createExpr(_memberAccess); + return true; + } Expression const* memberExpr = innermostTuple(_memberAccess.expression()); diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_function.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_function.sol index 1a3c71982..2bce234d4 100644 --- a/test/libsolidity/smtCheckerTests/abi/abi_encode_function.sol +++ b/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. diff --git a/test/libsolidity/smtCheckerTests/functions/getters/function.sol b/test/libsolidity/smtCheckerTests/functions/getters/function.sol index 95680f13d..a5339f7a8 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/function.sol +++ b/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 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 8364: (140-146): Assertion checker does not yet implement type function () view external returns (function () external returns (uint256)) +// Warning 6328: (152-170): CHC: Assertion violation happens here. +// Warning 6328: (262-278): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/getters/struct_4.sol b/test/libsolidity/smtCheckerTests/functions/getters/struct_4.sol index 73c2fcc57..3e300edbb 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/struct_4.sol +++ b/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. diff --git a/test/libsolidity/smtCheckerTests/imports/import_library_2.sol b/test/libsolidity/smtCheckerTests/imports/import_library_2.sol index 4d33d4002..acf2acda4 100644 --- a/test/libsolidity/smtCheckerTests/imports/import_library_2.sol +++ b/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. diff --git a/test/libsolidity/smtCheckerTests/operators/delete_function_type_1.sol b/test/libsolidity/smtCheckerTests/operators/delete_function_type_1.sol new file mode 100644 index 000000000..b6bc1f6a0 --- /dev/null +++ b/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. diff --git a/test/libsolidity/smtCheckerTests/operators/delete_function_type_2.sol b/test/libsolidity/smtCheckerTests/operators/delete_function_type_2.sol new file mode 100644 index 000000000..ee7497aca --- /dev/null +++ b/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. diff --git a/test/libsolidity/smtCheckerTests/operators/delete_function_type_3.sol b/test/libsolidity/smtCheckerTests/operators/delete_function_type_3.sol new file mode 100644 index 000000000..b334b982e --- /dev/null +++ b/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. diff --git a/test/libsolidity/smtCheckerTests/types/address_transfer.sol b/test/libsolidity/smtCheckerTests/types/address_transfer.sol index 654c24969..89e8ae102 100644 --- a/test/libsolidity/smtCheckerTests/types/address_transfer.sol +++ b/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. diff --git a/test/libsolidity/smtCheckerTests/types/array_dynamic_2_fail.sol b/test/libsolidity/smtCheckerTests/types/array_dynamic_2_fail.sol index 8de55bc9b..fc53eb69b 100644 --- a/test/libsolidity/smtCheckerTests/types/array_dynamic_2_fail.sol +++ b/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. diff --git a/test/libsolidity/smtCheckerTests/types/array_dynamic_3_fail.sol b/test/libsolidity/smtCheckerTests/types/array_dynamic_3_fail.sol index 53ac92a7c..a98511ed1 100644 --- a/test/libsolidity/smtCheckerTests/types/array_dynamic_3_fail.sol +++ b/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.