Fix Internal Function Summary Support (#20)#21
Open
tarasbob wants to merge 1 commit intoCertora:masterfrom
Open
Fix Internal Function Summary Support (#20)#21tarasbob wants to merge 1 commit intoCertora:masterfrom
tarasbob wants to merge 1 commit intoCertora:masterfrom
Conversation
Internal functions parsed from bytecode often lack return type information (empty 'res' field), while CVL summaries specify return types. This caused "Bad internal method returns: Different arities" errors when trying to merge signatures. This fix adds special handling in two places: 1. CVLASTBuilder: Trust CVL-specified return types when bytecode has none 2. QualifiedFunctionName.mergeReturns: Handle asymmetric return types This enables summarization of internal functions like OpenZeppelin's Context._msgSender() which are commonly used for access control. Added test case in Public/TestEVM/Summarization/InternalFunctionReturns/ demonstrating the fix with a minimal Context pattern implementation.
Contributor
|
See the comment in #20 - I believe there's nothing to fix here. Waiting for your confirmation there before closing this PR though. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Problem
Internal functions parsed from bytecode often lack return type information, causing "Bad internal method returns: Different arities" errors when users try to provide CVL summaries with return types.
Solution
Added special handling in signature merging to trust CVL-specified return types when bytecode provides no return type information.
Impact
Enables verification of contracts using OpenZeppelin's Context and similar patterns where internal functions like
_msgSender()are used for access control.I haven't tested it very thoroughly. Please make sure this doesn't break anything.
Fixes #20