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

fix: concretize calldatacopy #364

Merged
merged 12 commits into from
Sep 18, 2024
Merged

fix: concretize calldatacopy #364

merged 12 commits into from
Sep 18, 2024

Conversation

daejunpark
Copy link
Collaborator

@daejunpark daejunpark commented Sep 17, 2024

there are two instructions that read calldata, and their concretization logic works as follows:

  • calldataload: concretizes symbols if they exist in either the substitution or candidates mapping. it may cause the current path to branch.
  • calldatacopy: concretizes symbols only if they exist in the substitution mapping. no path branching.

this behavior is based on typical calldata decoding logic, where the length of dynamic arguments is first read using calldataload, and their data is then read using either calldataload or calldatacopy. for example, see the test provided in #371.

@daejunpark daejunpark mentioned this pull request Sep 17, 2024
15 tasks
Co-authored-by: karmacoma <karma@coma.lol>
src/halmos/sevm.py Show resolved Hide resolved
src/halmos/bytevec.py Outdated Show resolved Hide resolved
src/halmos/config.py Outdated Show resolved Hide resolved
src/halmos/bytevec.py Outdated Show resolved Hide resolved

data = self.data
# TODO: call substitute() only when the data contains variables to be substituted
new_data = substitute(data, *substitution.items())
Copy link
Collaborator

Choose a reason for hiding this comment

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

I am slightly worried about the perf impact of substitute always constructing a new object, but I guess we'll see how it looks like when I profile (not a blocker)

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

yeah, proper profiling would be greatly helpful. based on my performance tests, it gets slower if data is a complex term, e.g., LibUint1024Test:testProveSubAdd().

i'm thinking applying this substitution to selected int_of() only, rather than blindly applying to all calldatacopy. would be a separate pr though.

src/halmos/config.py Outdated Show resolved Hide resolved
daejunpark and others added 2 commits September 18, 2024 16:18
Co-authored-by: karmacoma <karma@coma.lol>
@daejunpark daejunpark merged commit e4a4ef7 into main Sep 18, 2024
53 checks passed
@daejunpark daejunpark deleted the fix/concretize-calldatacopy branch September 18, 2024 23:40
pcaversaccio added a commit to pcaversaccio/snekmate that referenced this pull request Sep 19, 2024
### 🕓 Changelog

[`halmos`](https://github.com/a16z/halmos) has released support for the
following new cheat codes via PRs
[#360](a16z/halmos#360) and (small patch)
[#364](a16z/halmos#364):

```solidity
createCalldata(string contractName);
createCalldata(string contractName, bool includeViewFunctions);
createCalldata(string filename, string contractName);
createCalldata(string filename, string contractName, bool includeViewFunctions);
```

> Please note that `includeViewFunctions` defaults to `false`, if not
provided.

This PR refactors the `halmos`-based tests to capitalise on these new
cheat codes. To verify the correct behaviour of the Vyper compiler for
`view` and `pure` functions, we include read-only functions in the
calldata creation.

---------

Signed-off-by: Pascal Marco Caversaccio <pascal.caversaccio@hotmail.ch>
daejunpark added a commit that referenced this pull request Sep 24, 2024
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.

2 participants