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

feat: functional implementation of EXTCODEHASH and EXTCODECOPY #328

Merged
merged 7 commits into from
Jul 26, 2024

Conversation

karmacoma-eth
Copy link
Collaborator

Should address #324

@karmacoma-eth karmacoma-eth requested a review from daejunpark July 23, 2024 00:55
Copy link
Collaborator

@daejunpark daejunpark left a comment

Choose a reason for hiding this comment

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

thanks for this! i have a concern with EXTCODECOPY, but EXTCODEHASH looks great to me!

src/halmos/sevm.py Show resolved Hide resolved
account_addr = self.resolve_address_alias(ex, uint160(ex.st.pop()))
account_code: Contract = (
ex.code.get(account_addr, None) or ByteVec()
)
Copy link
Collaborator

Choose a reason for hiding this comment

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

this may be unsound. when resolve_address_alias return None, it may be the case that the given address is too complex to solve, but it might be still aliased with an existing address. in that case, returning an empty byte here would be problematic.

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 see, how should we handle that?

Copy link
Collaborator

@daejunpark daejunpark Jul 23, 2024

Choose a reason for hiding this comment

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

i don't have a good idea, but for now, we could either:

  1. print a warning that the address is assumed to be new, having no code in it

  2. raise a halmos exception

neither is good, but not sure which is worse :(

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

let's print a warning and hope it only happens rarely

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

do you have a sense for the kind of pattern that would cause the solver in resolve_address_alias to time out?

Copy link
Collaborator

Choose a reason for hiding this comment

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

You can try running the farcaster test after reducing the timeout for the address resolving, and will see the complex term. If i remember correctly, it’s involved with several bit manipulations. It's not very complicated per se, but the timeout for resolution is just 1 second. Increasing it may hurt performance, when there are frequent calls or sends to symbolic addresses.

Copy link
Collaborator

Choose a reason for hiding this comment

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

yeah, let's try printing a warning and reevaluate it later.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

also it seems like this could be unsound if there are multiple addresses that it may alias: we would return an empty bytevec, but it seems like we should instead instantiate new paths

e.g. imagine account may alias A and B, in this PR we would have:
path 1 => extcodecopy(account) is empty

I think instead we should do this:

path 1, condition account == A, extcodecopy(account) returns code[A]
path 2, condition account == B, extcodecopy(account) returns code[B]
path 3, condition account != A and account != B, extcodecopy(account) is empty

wdyt?

Copy link
Collaborator

Choose a reason for hiding this comment

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

yes, a sound approach in general is to check account == x for every existing address x, and then branch a new path for each of them, unless the check result is not unsat. this captures what you described.

my concern was this may lead to path explosion. in the worse case, N paths are newly created for each opcode that requires address alias resolution, where N is the number of known addresses. that's why we don't support multiple aliases for now.

but perhaps it's time to experiment the more general approach, at least to see how bad the path explosion would be in practice.

tests/regression/test/Extcodehash.t.sol Show resolved Hide resolved
@karmacoma-eth
Copy link
Collaborator Author

warning added in 30f5b6a

@karmacoma-eth karmacoma-eth requested a review from daejunpark July 24, 2024 22:15
@karmacoma-eth karmacoma-eth merged commit c969bcd into main Jul 26, 2024
57 checks passed
@karmacoma-eth karmacoma-eth deleted the feat-extcodehash branch July 26, 2024 00:45
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