Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

createCalldata does not display function selector #374

Open
aviggiano opened this issue Sep 25, 2024 · 1 comment
Open

createCalldata does not display function selector #374

aviggiano opened this issue Sep 25, 2024 · 1 comment
Labels
bug Something isn't working

Comments

@aviggiano
Copy link
Contributor

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:

  • OS: macOS
  • Python version: Python 3.11.7
  • Halmos and other dependency versions: halmos 0.2.0

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

@aviggiano aviggiano added the bug Something isn't working label Sep 25, 2024
@daejunpark
Copy link
Collaborator

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working
Projects
None yet
Development

No branches or pull requests

2 participants