fix(symbolic): make the symbolic CLI suite run and pass with z3 - #16634
Merged
Conversation
#15564 deferred the gasleft guards to SMT emission, but the local witness fallbacks resolve single-variable gas constraints before any SMT is emitted, so a property such as `assert(gasleft() > 2 ** 200)` produced a counterexample built from a fabricated gas value. The same change dropped the call-input guard, so `gas()` copied into a callee's calldata was silently accepted. Refuse gasleft constraints in `model()` while keeping the `is_sat` witnesses, and reject call input that depends on gasleft again, as the README's fail-closed contract describes.
A solver model that does not replay was rendered as `[FAIL: symbolic counterexample did not replay; counterexample: ...]`, exposing the unconfirmed model as a user-facing counterexample even though the JSON result already classifies the run as incomplete. Render it as `incomplete symbolic execution (Error): ...` without a counterexample, matching the invariant path.
Single-call counterexamples render the sender and target since #15217 and #15814, and invariant sequences report the assertion message, mask labeled targets under `[SENDER]`, and print the seed line since #15591. The minimization tests asserted a longer original sequence, which stopped holding once the engine reports the shortest failing prefix; check the invariant only at the terminal depth so there is a sequence to shrink, and bound the symbolic depth where end-only checking would exceed `max_paths`.
`--fuzz-runs 0` never affected `invariant.runs` in `forge test` and is rejected since #16303, so the symbolic invariant tests set `invariant.runs = 0` in the project config instead. The reverted handler test depends on the concrete campaign it nominally disabled, so it keeps the campaign.
Every `forge test --symbolic` CLI test starts with `skip_unless_z3!`, so the suite was silently skipped in CI. Install the pinned `z3-solver==5.1.0` wheel, which ships the `z3` executable, on the Linux runners.
Contributor
✅ Changelog foundThe deterministic check will validate the changed entry. |
DaniPopes
marked this pull request as ready for review
September 4, 2026 16:39
DaniPopes
requested review from
0xrusowsky,
figtracer,
grandizzy,
mablr,
mattsse and
stevencartavia
as code owners
September 4, 2026 16:39
mablr
reviewed
Sep 4, 2026
The call-input gasleft guard checked whole backing values, so a word whose low byte depends on `gasleft()` reported the run incomplete even when only its provably gas-independent bytes were sliced into CALL input, and `Sized` inputs considered bytes beyond `max_size` that can never reach the callee. Inspect only the represented byte range, while a gas-dependent slice offset or dynamic size still fails closed.
Member
|
makes sense completely forgot to do this while running locally .... |
figtracer
previously approved these changes
Sep 4, 2026
Refusing gasleft constraints in `model()` also aborted the seed materialization that runs on successful paths when fuzz corpus seeding is enabled, downgrading a proved-safe run to incomplete. Skip the seed for such a path instead, count model queries only after the guard, keep the Echidna flags test on the default check interval so shortest-prefix minimization stays covered, move the `SymBytes` test next to the type, narrow the README gas row to what the engine actually does, and pin the exact z3 wheel version.
…ani/symbolic-cli-tests # Conflicts: # crates/forge/src/runner.rs
DaniPopes
enabled auto-merge (squash)
September 4, 2026 22:18
DaniPopes
marked this pull request as draft
September 4, 2026 22:43
auto-merge was automatically disabled
September 4, 2026 22:43
Pull request was converted to draft
DaniPopes
marked this pull request as ready for review
September 4, 2026 22:45
DaniPopes
enabled auto-merge (squash)
September 4, 2026 22:45
figtracer
approved these changes
Sep 4, 2026
This was referenced Sep 5, 2026
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
4 participants
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.
The
forge test --symbolicCLI snapshot tests all start withskip_unless_z3!, and CI has never installed z3, so the suite has been silently skipped since it landed. With az3binary on PATH, 33 of them fail on master. This PR goes through each failure, decides whether the fixture went stale or the code regressed, fixes the code where it regressed, and installs a pinned z3 in CI so the suite actually runs from now on.Three regressions were fixed. First, the symbolic engine no longer failed closed on
gasleft(): #15564 deferred the gas guards to SMT emission, but the local witness fallbacks resolve single-variable gas constraints before any SMT is emitted, soassert(gasleft() > 2 ** 200)produced a concrete counterexample from a fabricated gas value; separately, #15395 stopped scanning byte buffers forgasleft(), sogas()copied into a callee's calldata went unnoticed. The solver'smodel()now refuses constraints that containgasleft()while theis_satfeasibility witnesses are kept, matching the intent of #15564, and successful paths whose constraints depend on gas are simply not materialized into fuzz corpus seeds instead of failing the run. The call path rejects call input that depends ongasleft()again, inspecting only the bytes that actually reach the callee so a provably gas-independent slice of a gas-tainted word stays supported. The README's gas row now states what the engine actually does: gas branches may be explored through local witnesses, but nothing derived from gas ever becomes a counterexample. Second, the single-call runner rendered a solver model that failed to replay as[FAIL: symbolic counterexample did not replay; counterexample: ...], which is exactly the user-facing counterexample the JSON result already classifies as incomplete; it now reports[FAIL: incomplete symbolic execution (Error): symbolic counterexample did not replay]with no user-facing counterexample, the same wording the invariant path uses. The unconfirmed model is still recorded under the JSONsymbolic.counterexamplefield, as before, for debugging. Third, sixteen invariant tests passed--fuzz-runs 0, evidently to skip the fuzz campaign; that flag never affectedinvariant.runsinforge test, and #16303 now rejectsfuzz.runs = 0outright, so the command failed before producing any output. Fifteen of those tests only care about the symbolic phase and now setinvariant.runs = 0in the project config, which is the supported way to skip the campaign. The remaining one,symbolic_reverted_handler_effect_is_not_reported_safe, turned out to depend on the campaign it was nominally disabling: the symbolic run is incomplete and the concrete fuzz campaign is what observes the mock surviving the reverted handler call, so that test simply drops the flag and keeps the campaign.The remaining fixtures were stale. Single-call counterexamples have rendered the sender and target since the artifact work in #15217 and the display change in #15814, and the newer fixtures already expect
[SENDER] [SENDER] [CALLDATA] [ARGS], so the seven older ones and the Medusa literal were updated to match. The invariant sequence fixtures predate #15591, which reports the actual assertion message instead of the genericsymbolic invariant counterexample, masks labeled target addresses under[SENDER], and prints the seed line; those were updated too. The two Echidna minimization tests asserted that the engine's original sequence was longer than the minimized one, which stopped being true once the engine reports the shortest failing prefix under the default per-call invariant check. The flags test keeps the default interval and now asserts that the two-call witness is already minimal, so the default configuration stays covered, while the revert test usescheck_interval = 0so the engine reports a full-depth sequence that the shrinker actually has to reduce to one call. The JSON minimization test already usedcheck_interval = 0and expected the engine to find the two-call sequence; with end-only checking at the default symbolic depth of ten it now exceedsmax_paths, so it boundssymbolic.invariant_depthto two.CI now installs the
z3-solver==5.1.0.0wheel from PyPI on the Linux runners, alongside the existing Vyper install; the wheel ships thez3executable on PATH. It is Linux-only for now to keep the blast radius small on the push-only macOS and Windows jobs, andskip_unless_z3is unchanged for local runs. Fixture noise from solver-chosen values is already masked by the existing redactions. On the first push of this branch the Linuxtest alljob ran the previously skipped symbolic tests and finished in about 7 minutes, versus about 9 minutes for the same job on master.AI assistance (Claude) was used in preparing this change.