-
Notifications
You must be signed in to change notification settings - Fork 67
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Support vyper jumptables #253
Comments
Here is an annotated example of a jump table dispatcher, looks like an example with 27 functions. And the input is the usual first 4 bytes of calldata (
|
Not perfect, but here is a potential idea for how to solve this in CODECOPY: elif opcode == EVM.CODECOPY:
loc: int = ex.st.mloc()
offset = ex.st.pop()
if is_concrete(offset):
concrete_offset = int_of(offset)
print(green(f"XXX CONCRETE CODECOPY {hexify(ex.this)}@{ex.pc} XXX"))
size: int = int_of(ex.st.pop(), "symbolic CODECOPY size")
wextend(ex.st.memory, loc, size)
codeslice = ex.pgm[concrete_offset : concrete_offset + size]
actual_size = byte_length(codeslice)
if actual_size != size:
raise HalmosException(
f"CODECOPY: expected {size} bytes but got {actual_size}"
)
ex.st.memory[loc : loc + size] = iter_bytes(codeslice)
else:
offsetSolver = SolverFor("QF_BV")
codesize = con(len(ex.pgm))
# TODO: we might want to also add a solution check for offset > codesize
offsetSolver.add(ULE(offset, codesize))
offsets = set([])
result = offsetSolver.check()
while result == sat:
value = offsetSolver.model().evaluate(offset).as_long()
offsetSolver.add(offset != value)
offsets.add(value)
result = offsetSolver.check()
if self.options.get("debug"):
print(f"Splitting execution for CODECOPY with possible offsets {offsets}")
# say we found 2 possible offset values a and b, we need to
# to create 2 new executions where we're going to reexecute
# this CODECOPY instruction (same pc), but one for each offset
for offset_value in offsets:
new_ex = self.create_branch(ex, offset == offset_value, ex.pc)
# replace the items we have consumed on the stack
new_ex.st.push(con(offset_value))
new_ex.st.push(con(loc))
stack.append((new_ex, step_id))
# we're done with this execution
continue note the use of a separate offsetSolver to enumerate possible values some problems with this:
Potentially, we could also fallback to another mechanism. Specifically, we could do pattern matching on the symbolic expression and see that it corresponds to something like |
btw the layout of the dispatcher is in the initcode cbor metadata. using this you should be able to reliably tell what kind (
and with
(you can ignore the tuple vs list distinction; they are equivalent in cbor). the codesize optimized bytecode has 2 data sections; the gas-optimized has 1. |
Is your feature request related to a problem? Please describe.
Newer versions of vyper use jumptable-based dispatchers. We don't currently handle them very gracefully because of the mod operation.
For instance say a vyper contract implements 3 functions, the dispatcher will do something like this:
Because of the mod operation, halmos will fail with
NotConcreteError(f"symbolic JUMP target: {dst}")
or a symbolic CODECOPY errorDoing this from memory, so I'm not sure exactly what input is used, but if it is concrete then we should be able to resolve it. If it is symbolic, we may have to run a solver query to know which are the possible values, or identify the pattern and loop over the jumptable values
cc @zobront @charles-cooper
The text was updated successfully, but these errors were encountered: