From 826fd90dcf51a8b89dda5362dd686159d0bd6a55 Mon Sep 17 00:00:00 2001 From: Pawel Gebal Date: Tue, 20 Jun 2023 19:38:30 +0200 Subject: [PATCH] Fix error in SMTChecker: Use rich indentifier instead of external identifier to ecnode member access to functions --- Changelog.md | 1 + libsolidity/formal/SMTEncoder.cpp | 6 +++++- .../functions/functions_library_internal.sol | 14 ++++++++++++++ 3 files changed, 20 insertions(+), 1 deletion(-) create mode 100644 test/libsolidity/smtCheckerTests/functions/functions_library_internal.sol diff --git a/Changelog.md b/Changelog.md index 7456a8a46..69bd02624 100644 --- a/Changelog.md +++ b/Changelog.md @@ -20,6 +20,7 @@ Bugfixes: * Commandline Interface: It is no longer possible to specify both ``--optimize-yul`` and ``--no-optimize-yul`` at the same time. * SMTChecker: Fix encoding of side-effects inside ``if`` and ``ternary conditional``statements in the BMC engine. * SMTChecker: Fix false negative when a verification target can be violated only by trusted external call from another public function. + * SMTChecker: Fix internal error caused by using external identifier to encode member access to functions that take an internal function as a parameter. * Standard JSON Interface: Fix an incomplete AST being returned when analysis is interrupted by certain kinds of fatal errors. * Yul Optimizer: Ensure that the assignment of memory slots for variables moved to memory does not depend on AST IDs that may depend on whether additional files are included during compilation. * Yul Optimizer: Fix optimized IR being unnecessarily passed through the Yul optimizer again before bytecode generation. diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 818efac5c..a328a7781 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -33,6 +33,7 @@ #include #include +#include #include @@ -1358,7 +1359,10 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess) { auto const* functionType = dynamic_cast(_memberAccess.annotation().type); if (functionType && functionType->hasDeclaration()) - defineExpr(_memberAccess, functionType->externalIdentifier()); + defineExpr( + _memberAccess, + util::selectorFromSignatureU32(functionType->richIdentifier()) + ); return true; } diff --git a/test/libsolidity/smtCheckerTests/functions/functions_library_internal.sol b/test/libsolidity/smtCheckerTests/functions/functions_library_internal.sol new file mode 100644 index 000000000..405c3f715 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_library_internal.sol @@ -0,0 +1,14 @@ +library L { + function value(function()internal a, uint256 b) internal {} +} +contract C { + using L for function()internal; + + function f() public { + function()internal x; + x.value(42); + } +} +// ==== +// SMTEngine: all +// ----