halmos icon indicating copy to clipboard operation
halmos copied to clipboard

Code fastpath scanning for valid jump destinations

Open 0xkarmacoma opened this issue 6 months ago • 1 comments

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)

0xkarmacoma avatar Aug 16 '24 00:08 0xkarmacoma