fix failed() cheatcode error #359
Conversation
|
ah I see it does address the specific issue in #358, but we still have a more general problem: should
|
src/halmos/cheatcodes.py
Outdated
| # vm.load(HEVM_ADDRESS, "failed") is handled separately | ||
| if arg == hevm_cheat_code.failed_payload: | ||
| # since fail(), which triggers vm.store(HEVM_ADDRESS, "failed", 1), halts immediately, (see vm.store() above) | ||
| # the "failed" slot is never assigned, thus vm.load(HEVM_ADDRESS, "failed") always return zero at this point | ||
| return ByteVec(con(0)) |
There was a problem hiding this comment.
would it be bad to return 0 if load_account_alias is None?
There was a problem hiding this comment.
ideally we wouldn't handle hevm as an edge case
There was a problem hiding this comment.
good idea! how should we do for vm.store() with nonexistent account?
There was a problem hiding this comment.
done for vm.load().
for vm.store(), currently an exception is raised if the given account doesn't exist.
There was a problem hiding this comment.
for vm.store(), currently an exception is raised if the given account doesn't exist
ok, so the idea is that we need to first deploy code at an address and then we can vm.store to it? is that because deploying resets the storage?
There was a problem hiding this comment.
so far, we have the invariant that for any address x, x in ex.code iff x in ex.storage. now, if we allow vm.store() for nonexistent addresses, the invariant would no longer hold, which leads to some logic changes in the codebase.
another invariant we have is that all addresses in ex.code/ex.storage are concrete. if the given address is symbolic, this invariant would be broken. note that calls to symbolic addresses don't break this, because of branching over concrete aliases, and calls to nonexistent address are essentially no-op.
while these invariants are convenient for various reasons, they aren't absolutely necessary. so we can break them and adjust our logic, if needed, although this would increase code complexity.
i'd suggest we wait until we see concrete use cases where vm.store() is used with nonexistent or symbolic addresses, before deciding how to redesign this logic.
yes, it returns None when the given address doesn't exist, or is assumed to not exist. so it's the caller's responsibility to check the result. |
done |
fix #358