-
Notifications
You must be signed in to change notification settings - Fork 71
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
Conversation
There was a problem hiding this 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
Outdated
account_addr = self.resolve_address_alias(ex, uint160(ex.st.pop())) | ||
account_code: Contract = ( | ||
ex.code.get(account_addr, None) or ByteVec() | ||
) |
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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?
There was a problem hiding this comment.
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:
-
print a warning that the address is assumed to be new, having no code in it
-
raise a halmos exception
neither is good, but not sure which is worse :(
There was a problem hiding this comment.
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
There was a problem hiding this comment.
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?
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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?
There was a problem hiding this comment.
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.
warning added in 30f5b6a |
Should address #324