halmos
halmos copied to clipboard
find a better way to handle empty bytes
we don't have a very nice way to deal with empty byte sequences in general (for things like calldata, returndata, code). They get sometimes represented as bytes()
, sometimes as []
, sometimes as None
.
this leads to a proliferation of checks like:
def extract_bytes(
data: Optional[BitVecRef], byte_offset: int, size_bytes: int
) -> BitVecRef:
"""Extract bytes from calldata. Zero-pad if out of bounds."""
if data is None:
return BitVecVal(0, size_bytes * 8)