Last active
August 26, 2021 17:46
Star
You must be signed in to star a gist
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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! | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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!).