Repository navigation
fix(bridge): every return path deallocates the spill frame — close #499 - #593
Merged
Merged
Conversation
The optimized path's ir_to_arm allocates a spill frame (sub sp,#N) but only inserted the add sp,#N teardown before returns that ALREADY existed in the body. A return APPENDED for a function that falls off its end (the common wasm shape) only got the teardown under SYNTH_SPILL_ON_EXHAUST — gated on the false belief that a flag-off spill implied scratch-pool exhaustion (which declines the function). The flag-off Opcode::Const allocator has its own oldest-vreg eviction spill on R4-R11/R3 pool exhaustion that never sets r12_exhausted, so such functions shipped with SP off by the frame size; post-#490 the pop {…,pc} epilogue reads PC from a spill slot → crash. Reachable straight-line (#592 flip-lane reproducer, init_fields) AND under control flow (the original #499 nested shape). Fix: the appended return deallocates the frame unconditionally, plus a defensive post-condition (internal-bug panic pattern) — with a frame allocated, every `bx lr` must be immediately preceded by the exact `add sp,#frame_size`. Gate: scripts/repro/spill_frame_499_differential.py (minimal straight-line + init_fields + nested both branch directions, unicorn vs wasmtime, SP-balance + memory equality + spill-frame non-vacuity tripwire; SYNTH_BASE_CSE=0 pins the exposure post-#592) — red on main (4/4 execution faults), green with the fix. CI job added. Correctness re-pin: the base_cse_flip_468 OPT-OUT golden for redundant_base_materialization pinned the miscompiled bytes (342 B). Fixed bytes are 326 B: +4 (add sp) −20 (frame-slot DCE now removes the dead spill stores the mis-paired pop previously appeared to read). Execution-validated before re-pinning; base_cse_differential.py's "known #499" tolerance arm now passes clean. Frozen --relocatable/direct and RV32 anchors bit-identical. Closes #499 Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
avrabe
added a commit
that referenced
this pull request
Jul 3, 2026
…+ ordeal solver (#600) base-CSE flip (#592, -180B corpus), spill-frame dealloc fix (#499/#593), A32 call_indirect real call (#594/#596), synth-verify on ordeal 0.4 with Z3 as differential oracle (#553/#595, first C++-free build). Known issues #597/#599 tracked for v0.27.1. Pin sweep + lock + CHANGELOG. Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
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.
The bug (shipped miscompile)
The optimized (non-
--relocatable) ARM path allocates a spill frame (sub sp,#N) under register pressure, but theadd sp,#Nteardown was only inserted before returns that already existed in the body. A return appended for a function that falls off its end — the common wasm shape — only got the teardown underSYNTH_SPILL_ON_EXHAUST.The named accounting defect: the appended-return dealloc was gated on
spill_on_exhaustunder the belief that any flag-off spill implied scratch-pool exhaustion (which declines the function to the direct selector). That belief is false: the flag-offOpcode::Constallocator has its own oldest-vreg eviction spill on R4-R11/R3 pool exhaustion (optimizer_bridge.rs~3649) that never setsr12_exhausted— so the function compiled, spilled, and returned with SP off by the frame size. Post-#490 the epilogue ispop {…,pc}, which reads PC through SP → PC popped from a spill slot → crash.Reachable straight-line (the #592 flip-lane reproducer,
redundant_base_materialization.wat::init_fieldswithSYNTH_BASE_CSE=0) and under the original #499 control-flow shape (nested, block/br_if/br — its return is also the appended fall-off-the-end return, same single root cause).Broken → fixed epilogue (
init_fields,SYNTH_BASE_CSE=0)Broken (main):
Fixed:
(unicorn on main:
UC_ERR_INSN_INVALID/UC_ERR_FETCH_UNMAPPED, PC popped from a spill slot)Fix
ir_to_arm: the appended return deallocates the frame unconditionally (next_spill_offset > 4, no flag gate).bx lrmust be immediately preceded by the exactadd sp,#frame_size— any violation is an epilogue bug and panics instead of shipping an SP-imbalanced function.Gate — red → green
New
scripts/repro/spill_frame_499_differential.py(+ CI job): compilesmin_fields(minimal straight-line spill),nested(original #499 CF shape, both branch directions), andinit_fieldswithSYNTH_BASE_CSE=0(the #592 default relieves the pressure — pinned so the teardown path stays covered, with a loud non-vacuity tripwire if a fixture stops spilling); runs under unicorn and asserts return reached + SP balanced + memory bit-identical to wasmtime.base_cse_differential.py's "known #499" tolerance arm now passes clean (off=ok), as its comment predicted.Correctness re-pin (real finding, as anticipated)
base_cse_flip_468.rs's opt-out golden forredundant_base_materialization.wathad pinned the miscompiled bytes (342 B). Fixed opt-out bytes are 326 B: +4 (add sp) − 20 (frame-slot DCE now removes the five dead spill stores that the mis-pairedpoppreviously appeared to read, which forced a conservative keep). Re-pinned only after execution validation (both differentials green). The shipped-default golden (224 B) is untouched.All other anchors bit-identical:
frozen_codegen_bytes(--relocatable/direct ARM + RV32, escape hatches) green unchanged.Verification
spill_frame_499_differential.py: red on main → green herebase_cse_differential.py: PASS, Optimized path: spill frame not deallocated before return (missing 'add sp') on a function with control flow #499 warning gonecargo test -p synth-synthesis -p synth-cli: greencargo clippy -p synth-synthesis -p synth-cli --all-targets -- -D warnings,cargo fmt --check: cleanCloses #499
🤖 Generated with Claude Code