Repository navigation
Conversation
msooseth
force-pushed
the
stack/4-merge
branch
from
November 13, 2026 14:24
dab0844 to
34f1817
Compare
msooseth
force-pushed
the
stack/4-merge
branch
from
November 13, 2026 14:34
34f1817 to
1bc9212
Compare
The two sides of a JUMPI may meet after the jump target, as in if/else and ternaries. Inside a merged side, a branch its own condition decides is followed. A JUMPI reached again from the same call site is in a loop and forks, so the loop bound applies even when the loop condition is concrete. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
A merged ternary leaves a two-valued term, e.g. LT 0 x for `b ? 1 : 0`. Used as an array length, it made the free memory pointer and every later memory access symbolic. Memory instructions now fork on such a term in an offset or size, and run again with each value. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
splitMergedMemArg forked on a merged memory offset before the op ran, even when the stack held fewer items than the op takes: a RETURN with a single symbolic item forked instead of halting with StackUnderrun, and symbolic-lockstep found the symbolic run going on where the concrete one had halted. The split now requires the op's full arity on the stack. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
When a memory offset or size is not a literal or a merged ITE, but becomes one for each value of a subterm with at most --max-mem-arg-split values (default 8), e.g. the symbolic length of a short array argument, the path forks on those values and substitutes each one into the stacks, memory, buffers and contract storage and balances. The pushed equality keeps it sound wherever the substitution does not reach. Memory then stays concrete, e.g. for a CREATE after allocating such an array. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The atom enumerateViaSmallSubterm returns is a subterm of the argument simplified, which the stack may not hold as is: substituting it changed nothing, the op ran into the same split again, and a CALL with an input size of mod(x, 8) forked forever (eq-all-yul-optimization-tests timed out). Each branch now also sets the argument to its value. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Memory staying concrete is of no use to an op that ends the frame, and forking there made the lockstep fuzzers find the symbolic run going on where the concrete one had halted, e.g. RETURN at an offset calldataload(0x24) & 1. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
msooseth
force-pushed
the
stack/4-merge
branch
from
November 13, 2026 14:36
1bc9212 to
a0b38ca
Compare
This branch has not been deployed
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
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
State merging also merges if/else branches and ternaries, and follows branches inside a merged side that its condition decides. A memory offset or size that depends on a merged condition or a small-range subterm forks on its values (
--max-mem-arg-split), so memory stays concrete.Part 4 of 7 of splitting #1248.
Checklist