halmos icon indicating copy to clipboard operation
halmos copied to clipboard

find a better way to handle empty bytes

Open 0xkarmacoma opened this issue 11 months ago • 0 comments

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)

0xkarmacoma avatar Mar 26 '24 17:03 0xkarmacoma