Repository navigation
End symbolic jump targets above two bytes in an invalid-jump error - #1203
Merged
Merged
Conversation
msooseth
changed the title
Solutions for a symbolic jump target cover its low two bytes only, and each path then fixed the whole target to one of them, so targets with higher bytes set, all past the end of the code, were on no path. JUMP and JUMPI now first branch on the target being below 2^16; above it, the path ends in a BadJumpDestination error. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Each CexReplay was a thunk over both final VMs, whose traces held the stubs' return and revert data, so replaying many counterexamples with 16MB returndata exhausted memory. eq-fuzz writes the programs it checks to HEVM_FUZZ_CASE_FILE, to find such cases. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
msooseth
force-pushed
the
symbolic-jump-high-bytes
branch
from
October 19, 2026 17:54
07de533 to
ffebbf4
Compare
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Description
For a symbolic
JUMP/JUMPItarget, hevm asks the solver only for the values of its low two bytes. Each resulting path then constrained the whole target to equal one of them, so targets with any higher byte set were on no path. The symbolic-execution fuzzer found this: a concrete input reached none of the leaves.JUMPandJUMPInow first branch on the target being below 2^16. Below that, the two-byte enumeration is exact. Above it, the path ends in aBadJumpDestinationerror; forJUMPI, only if the jump is taken.Such a target is invalid because a jump destination has to be inside the code, and code is at most 49,152 bytes (EIP-3860 for initcode; EIP-170 caps deployed code at 24,576). hevm doesn't enforce these limits when it is given raw bytecode. Code longer than 64KB could have a valid destination at or above 2^16, which this treats as invalid; before, it was missed.
This PR also fixes eq-fuzz running out of memory. Each counterexample replay result was a thunk over both final VMs. Their traces held the stubs' return and revert data, up to 16MB per call, so the VMs of all replays were kept alive until the results were shown. eq-fuzz now also writes the programs it checks to
HEVM_FUZZ_CASE_FILE, to find such cases.Checklist