Skip to content

Conversation

@msooseth
Copy link
Collaborator

@msooseth msooseth commented Jan 2, 2025

Description

This helps to deal with abi.encodeWithSelector. Adds a corresponding simplification rules.

Fixes the test case added:

contract C {
function prove_warp_symbolic(uint128 jump) public {
        uint pre = block.timestamp;
        address hevm = 0x7109709ECfa91a80626fF3989D68f67F5b1DD12D;
        (bool success, ) = hevm.call(abi.encodeWithSelector(bytes4(keccak256("warp(uint256)")), block.timestamp+jump));
        require(success, "Call to hevm.warp failed");
        assert(block.timestamp == pre + jump);
    }
}

Meant to be used together with #619 and works only on top of #619

Checklist

  • tested locally
  • added automated tests
  • updated the docs
  • updated the changelog

@msooseth msooseth marked this pull request as ready for review January 2, 2025 15:48
JumpIntoSymbolicCode pc idx -> "Encountered a jump into a potentially symbolic code region while executing initcode. pc: " <> pack (show pc) <> " jump dst: " <> pack (show idx)

formatSomeExpr :: SomeExpr -> Text
formatSomeExpr (SomeExpr e) = formatExpr e
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I added this change, because it's waaay nicer for the user, and we should be getting cleaner issues, too.

@msooseth
Copy link
Collaborator Author

msooseth commented Jan 2, 2025

NOTE: This is failing currently only because #619 is not yet merged :)

Comment on lines +1438 to +1439
indexWord (Lit a) (Or funSel (And (Lit 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffff) _)) | a < 4 =
indexWord (Lit a) funSel
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do I understand it correctly that this simplification is correct because the four most significant bytes of (And (Lit 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffff) _) will always be zero?

@msooseth
Copy link
Collaborator Author

msooseth commented Jan 6, 2025 via email

Copy link
Collaborator

@blishko blishko left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM!

@msooseth msooseth merged commit 0804e54 into main Jan 7, 2025
8 of 9 checks passed
@blishko blishko deleted the func-selector-fix branch July 29, 2025 19:10
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants