Skip to content

Instantly share code, notes, and snippets.

@pschanely
Last active August 26, 2021 17:46
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
Star You must be signed in to star a gist
Save pschanely/6b57c2fe867a9af087b728c35a9e191b to your computer and use it in GitHub Desktop.
buf = bytearray(buf) # <== Materializes the symbolic `buf`. (the returned byte array is native, and so must force the symbolic into concrete values)
self.__bytes_drawn += n_bytes
assert len(buf) == n_bytes
# If we have a number of bits that is not a multiple of 8
# we have to mask off the high bits.
buf[0] &= BYTE_MASKS[n % 8] # <== bitwise operators also materialize symbolics. I think this is special-case-able, as this mask is essentially the same as a mod operation.
buf = bytes(buf)
result = int_from_bytes(buf) # <== also materializes symbolics! I think materialization could be avoided here by patching int.from_bytes().
self.observer.draw_bits(n, forced is not None, result)
self.__example_record.draw_bits(n, forced)
initial = self.index
self.buffer.extend(buf) # <== also materializes symbolics! I don't think this is resolvable.
self.index = len(self.buffer)
if forced is not None:
self.forced_indices.update(range(initial, self.index))
self.blocks.add_endpoint(self.index)
assert bit_length(result) <= n # <== my symbolic ints don't implement bit_length. Time to file a bug!
@pschanely
Copy link
Author

All of the blockers in the comment lines above have now been resolved!

CrossHair can now get through this code maintaining at least symbolic state (though that's not to say it's doing this efficiently!).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment