Repository navigation
v0.44.0 Lane D: #390 redundant-store elimination in forward_stack_reloads (gust_poll 724→716 B) - #765
Merged
Merged
Conversation
…st_poll 724→716 B VCR-PERF-001 Lane D (v0.44): extend the forward_stack_reloads holder lattice with redundant-store elimination. A `str rd,[sp,#N]` whose slot #N the lattice PROVES already holds rd's value (a caller-save value re-spilled unchanged between two calls) writes bytes the slot already has — a no-op. Delete it. gust_poll: one redundant `str.w r0,[sp,#40]` removed between the func_0 reload and the func_1 call (r0 unchanged since the reload, slot #40 still holding it from the pre-func_0 spill). 722→716 B machine code (−6, one str.w + 2 B realignment); 724→716 B by the size oracle's symbol-delta method (−8). Only gust_poll's bytes change — func_0/func_1/gust_mix byte-identical. SOUNDNESS: - Same #606 frozen-span guard as reload-deletion: a deletion inside a resolved branch→target span would shift the pre-resolved displacement, so a frozen candidate is kept (re-writes the same value; state below identical). - On deletion the holder set is left UNCHANGED — the slot content is unaltered by removing a redundant write, so every co-holder register stays valid; collapsing to {rd} would only lose precision. - OVERWRITE-ONLY / sub-word-hole invariants untouched: this deletes a full-word store the lattice already tracks; sub-word sp accesses still clear holders. Correctness evidence on the new bytes BEFORE re-pinning the size oracle: - gust_spill_fwd_390_differential.py PASS — gust_poll return value AND post-call state struct match wasmtime in all three configs (default, SYNTH_NO_STACK_FWD, SYNTH_SPILL_REALLOC=0). - full scripts/repro/*_differential.py sweep: 90 PASS; the 6 failures fail IDENTICALLY on the pristine origin/main binary (5 fact_spec_* need --features verify; 1 u64_unpack_riscv a pre-existing RISC-V unicorn harness issue) — none are regressions. - full synth-cli + synth-synthesis test suites green (frozen anchors unchanged). Also fixes gust_spill_fwd_390_differential.py: post-#758 (v0.43.1) the self-contained image carries the ~1 MB data ROM image inside `.text`, so `text.data()` overflowed the 64 KB unicorn code window (UC_ERR_WRITE_UNMAPPED) on ANY binary. Write only the code prefix that fits — every reachable instruction lives in the first few KB. Size oracle re-pinned 724→716; artifacts/size_attribution_390.md regenerated (gust_poll 3.55x→3.44x vs cited LLVM). Two new unit tests cover the delete and the reg-reloaded-between keep. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
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.
VCR-PERF-001 Lane D. Extends the
forward_stack_reloadsholder lattice with redundant-store elimination: a full-wordstr rd,[sp,#N]whose slot the lattice PROVES already holdsrd's value writes bytes the slot already has — a no-op — so it's deleted.gust_poll 724→716 B (−8 by the size-oracle symbol-delta method): one redundant
str.w r0,[sp,#40]removed between the func_0 reload and the func_1 call (r0 unchanged since the reload, slot #40 still holding it). Only gust_poll's bytes change; func_0/func_1/gust_mix byte-identical.Soundness (reuses the shipped reload-forwarding lattice)
holders[slot]provably containsrd— the SAME conservative fact that powers shipped reload-forwarding.holdersleft UNCHANGED (slot content unaltered by removing a redundant write ⇒ all co-holders stay valid).Verification (coordinator re-ran ALL of this — original agent died on an API stall before pushing)
forward_redundant_store_of_resident_value_deleted+ keep-when-clobbered — 10/10 green.gust_spill_fwd_390_differential.pyPASS (return value + post-call state struct vs wasmtime, all 3 configs).size_attribution_390.mdregenerated (gust_poll 3.55×→3.44× vs cited LLVM).gust_spill_fwd_390_differential.py: post-default --cortex-m self-contained image silently DROPS active (data) segments: .linear_memory is NoBits, initializer bytes absent -> every load from an initialized region reads 0 (silent miscompile) #758 the self-contained image carries the ~1 MB data ROM inside.text, overflowing the 64 KB unicorn code window — now writes only the reachable code prefix.🤖 Generated with Claude Code