Fix error in SMTChecker: Use rich indentifier instead of external identifier to encode member access to functions #14344
Conversation
|
Thank you for your contribution to the Solidity compiler! A team member will follow up shortly. If you haven't read our contributing guidelines and our review checklist before, please do it now, this makes the reviewing process and accepting your contribution smoother. If you have any questions or need our help, feel free to post them in the PR or talk to us directly on the #solidity-dev channel on Matrix. |
|
|
||
| function f() public { | ||
| function()internal x; | ||
| x.value(42); |
There was a problem hiding this comment.
What exactly was triggering the assertion before, was it x.value?
There was a problem hiding this comment.
I think I still don't fully understand the bug. The MemberAccess in the C++ code has function type, right? But it's not the function type of the variable x, it's the function type of x.value?
There was a problem hiding this comment.
Right. MemberAccess is about the value function. It's the function type of value or x.value function from library.
There was a problem hiding this comment.
@leonardoalt I was wrong about that. I updated PR description with hopefully true cause.
pgebal
force-pushed
the
pgebal/fix-ice-internal-type
branch
from
fa5a788
to
520e666
Compare
Changelog.md
Outdated
| @@ -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 when verifying code with internal functions. | |||
There was a problem hiding this comment.
@pgebal can you also update the bugfix message here with something more precise?
…ntifier to ecnode member access to functions
pgebal
force-pushed
the
pgebal/fix-ice-internal-type
branch
from
520e666
to
826fd90
Compare
pgebal
changed the title
Closes #14181
Cause:
FunctionType::externalIdentifierinSMTEncoderto encode functions,externalIdentifierrequires all parameters to have external type. Error happens when function parameter is an internal functionSolution:
SMTEncoder