feat: functional implementation of EXTCODEHASH and EXTCODECOPY #328
Conversation
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.
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.
I see, how should we handle that?
There was a problem hiding this comment.
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.
let's print a warning and hope it only happens rarely
There was a problem hiding this comment.
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.
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.
yeah, let's try printing a warning and reevaluate it later.
There was a problem hiding this comment.
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.
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