halmos
halmos copied to clipboard
Code fastpath scanning for valid jump destinations
jumpi_id()
keeps showing up when I profile tests, because it causes us to eagerly compute valid_jump_destinations()
Fundamentally, valid_jump_destinations()
does a linear scan of the whole code for a contract. Even though ByteVec avoids z3 operations for this, it's still not ideal to do 10k+ individual byte lookups in a bytevec for almost contiguous data.
The insight here is that it is quite common to process contracts that have a large concrete prefix, sometimes followed by some symbolic data. In this case, we extract the concrete prefix in _fastcode
and scan that first for valid jump destinations.
With this change, the regression tests run about 15% faster for me (44s to 37s)