Allow dealing with abi.encodeWithSelector

[msooseth]

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]

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

[msooseth]

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

[blishko]

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]

Yes! :)

…

On Mon 6. Jan 2025 at 15:45, Martin Blicha ***@***.***> wrote: ***@***.**** commented on this pull request. ------------------------------ In src/EVM/Expr.hs <#625 (comment)>: > +indexWord (Lit a) (Or funSel (And (Lit 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffff) _)) | a < 4 = + indexWord (Lit a) funSel Do I understand it correctly that this simplification is correct because the four most significant bytes of (And (Lit 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffff) _) will always be zero? — Reply to this email directly, view it on GitHub <#625 (review)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AXYLY5GV2F7AG2LNPTSDS2T2JKJHTAVCNFSM6AAAAABUQFWJU6VHI2DSMVQWIX3LMV43YUDVNRWFEZLROVSXG5CSMV3GSZLXHMZDKMZSGI4TINJRGA> . You are receiving this because you authored the thread.Message ID: ***@***.***>

[blishko]

LGTM!