fix: we do support empty bytes now #462
Conversation
|
the ci failure is orthogonal to the change in the test. but the change somehow triggers solc optimization, which replaces this temporary workaround ae0cacb fixes the ci failure, but it needs to be properly implemented. do not merge. |
ae0cacb to
ca7c6e3
Compare
|
it turns out that the empty keccak value is read from memory (probably because it was previously stored into memory using codecopy). ca7c6e3 moves the special value handling logic to the point where a value is pushed to the stack to cover various cases. |
src/halmos/cheatcodes.py
Outdated
| name = name_of(extract_string_argument(arg, 1)) | ||
| symbolic_bytes = create_generic(ex, byte_size * 8, name, "bytes") | ||
| symbolic_bytes = create_any(ex, bits, name, "bytes") if bits else ByteVec() |
There was a problem hiding this comment.
an alternative approach is to add the empty byte logic inside create_any() rather than here. though, it's unclear to me which is necessarily better.
if we decide to keep it here, then we also need to add it to create_string() below, which is basically the same as create_bytes() except for the error message. indeed, it would be better to factor out the common logic to avoid code duplication.
5593859 to
518857e
Compare
|
applied the special handling only to push and mload operations, instead of to all stack pushes, for performance consideration: 518857e it would be more robust to apply to all pushes, if it doesn't hurt performance too much, though. wdyt? |
|
seems related to #393, but does not fix it |
|
trying to wrap my head around this. It does feel like we're playing whack-a-mole since there could be other sources of concrete hashes (returndata, calldata, codecopy, ...). So we may end up with values on the stack that are either a concrete hash value, or its hash expression. In that sense, it would indeed be more consistent to eagerly lookup every value that goes on the stack in sha_inv and try to make it an expr, but at a cost. OTOH, I'm not completely sure I understand what issues we solve by eagerly converting everything to an expr. Some things that come to mind:
Maybe an alternative would be that we don't need to eagerly do anything, and instead try to convert lazily to an expr at the point of use -- that could be both robust and cheap? I say let's merge this PR as-is and do a more intentional keccak refactor in a follow-up |
No description provided.