a16z / halmos

A symbolic testing tool for EVM smart contracts
GNU Affero General Public License v3.0
802 stars 65 forks source link

`createCalldata` does not display function selector #374

Open aviggiano opened 1 week ago

aviggiano commented 1 week ago

Describe the bug

When using createCalldata, only the function arguments are shown

To Reproduce

git clone https://github.com/aviggiano/halmos-differential-erc20
git checkout 17c99b890779512b688dff5677afe48516c8ccf9
halmos

Environment:

Additional context

Logs:

Counterexample:
    p_amount_uint256_21 = 0x0000000000000000000000000000000000000000000000000000000000000000 (0)
    p_amount_uint256_42 = 0x0000000000000000000000000000000000000000000000000000000000000000 (0)
    p_from_address_19 = 0x0000000000000000008000000000000000000000
    p_from_address_40 = 0x0000000000000000000000000000000000000000
    p_n_staticcalls_uint256_00 = 0x0000000000000000000000000000000000000000000000000000000000000000 (0)
    p_senders[0]_address_00 = 0xffffffff7fffbfcdbe7ffffffff7fffffdfeffff
    p_senders[1]_address_00 = 0x0000000000000000000000000000000000000000
    p_senders_length_00 = 0x0000000000000000000000000000000000000000000000000000000000000002
    p_to_address_20 = 0x0000000000000000008000000000000000000000
    p_to_address_41 = 0x0000000000000000000000000000000000000000

Note: this is a minor issue, since console.log helps with debugging

daejunpark commented 5 days ago

thanks for reporting. in the meantime while we're improving this, you can use the following trick:

function check_...(..., bytes4 selector, ...) {
  data = svm.createCalldata(...);
  vm.assume(selector == bytes4(data));
  ...
}

this way, you'll see the selector in counterexamples.