Code fastpath scanning for valid jump destinations

[karmacoma-eth]

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)

[karmacoma-eth]

main baseline for my maze benchmark: 62.89s
new time: 52.56s (-16.4%) 50.10s (-21%)

[daejunpark]

this is fine if the result of unbox_int is immediately pushed to the stack. but, there are cases where a simplified result is needed, e.g.,:

• halmos/src/halmos/__main__.py

  Line 760 in c3f45dd

  and unbox_int(ex.context.output.data) == ASSERT_FAIL

  the structural equality test may fail against unsimplified results, while it would pass with simplified ones.

• halmos/src/halmos/bytevec.py

  Line 704 in c3f45dd

  return unbox_int(data)

  the result of get_word() is better to be simplified, as it is used in many cheatcodes, and passed through further logic.

simplifying symbolic terms into their normalized form is leveraged by several other routines, so passing around unsimplified terms may cause unexpected issues, which may be difficult to debug later. this also increases code maintenance cost, while we still need further large iterations.

[karmacoma-eth]

I think it's weird for unbox_int to try to convert to an int, but also simplify if it's not.

I think simplify should happen at well defined boundaries, like:

• in and out of the stack
• in and out of memory
• not in an intermediate place like unbox_int

unbox_int(ex.context.output.data) == ASSERT_FAIL

☝️ this is not a great use of unbox_int, if the result is a bv we produce a new cond rather than evaluating a bool. In this case we probably want to call simplify first, then try to unbox, and skip if the unboxed output is still a bv

[karmacoma-eth]

the result of get_word() is better to be simplified, as it is used in many cheatcodes, and passed through further logic

I agree, that's why the output of unwrap is simplified

[daejunpark]

In this case we probably want to call simplify first, then try to unbox, and skip if the unboxed output is still a bv

i agree. could you please fix that as you suggested? btw, for the long term, we'd need to generalize this condition to cover arbitrary Panic(k) where k is given by users.

I agree, that's why the output of unwrap is simplified

thanks for clarification, now i see that it's already simplified before being passed into unbox_int

--

i agree that it would make more sense to not simplify inside unbox_int. then, let me double-check other places to make sure:

• halmos/src/halmos/sevm.py

  Lines 727 to 728 in c3f45dd

  	def current_opcode(self) -> UnionType[int, BitVecRef]:
  	return unbox_int(self.pgm[self.pc])

  this is fine because self.pgm[self.pc] is already simplified, right?

• halmos/src/halmos/utils.py

  Lines 265 to 269 in c3f45dd

  	def extract_funsig(calldata: Bytes) -> Any:
  	"""Extracts the function signature (first 4 bytes) from calldata"""
  	if hasattr(calldata, "__getitem__"):
  	return unbox_int(calldata[:4])
  	return extract_bytes(calldata, 0, 4)

  if i understand correctly, calldata[:4] may not be simplified, right? for now, it's fine because the extract_funsig() result is immediately passed to int_of, which would revert anyway if it's a bv. (there is another use of extract_funsig(), but it will be removed anyway in feat: branching over symbolic call addresses #349, so it doesn't matter.) however, for the longer term, should we simplify calldata[:4] here? wdty?

[karmacoma-eth]

could you please fix that as you suggested?

yea 👍

self.pgm[self.pc] is already simplified, right?

it defers to ByteVec.get_byte(), which calls chunk.get_byte()

• for a concrete chunk, we get an int
• for a symbolic chunk, it relies on extract_bytes, which does return simplified bitvecs

so rn yes, but it's not strongly part of the contract (it just so happens that extract_bytes does simplify)

should we simplify calldata[:4] here?

yes, instead of "trying" to unbox it, returning calldata[:4].unwrap() would do it (return either a concrete value or a simplified bv)

[karmacoma-eth]

could you please fix that as you suggested?

more robust version in af3df48 and test in afd5c11. I confirmed that unbox_int(...) == ASSERT_FAIL does produce a BoolRef of the form Concat(1313373041, p_x_uint256) == 152078208365357342262005707660225848957176981554335715805457651098985835139029979365377, which for some reason evaluates to False in the condition (instead of generating an exception as I was expecting).

[daejunpark]

should we simplify calldata[:4] here?

yes, instead of "trying" to unbox it, returning calldata[:4].unwrap() would do it (return either a concrete value or a simplified bv)

great, let's do it! actually, i realized that unbox_int() calls unwrap() inside, so it's already simplified there. also, if i understand correctly, unwrap() may return a bv_value, so calldata[:4].unwrap() may not be fully equivalent to unbox_int(calldata[:4]). while it might be fine for extract_funsig() to return a bv_value, i'd like to just leave it as is.

[daejunpark]

nice! but why do we need to compare only the prefix of data, not the full data?

[karmacoma-eth]

equality check fails if length is different, do you think that's closer to what we want?