investigate(#757): 7 faithful RawVec-grow+memmove reconstructions — all GREEN (bug needs gale's module; NO FIX) - #772
Merged
Conversation
Reproduction lane for the #757 multi-chunk static-copy source-offset miscompile (gale gust:os v0.4.0, RawVec-grow + memmove of a >=9B static above wasm_data_base under --relocatable --native-pointer-abi). Five faithful shapes built from gale's mechanism-neutral facts (string at .data offset 0x20 with low consts at 0x00-0x1f; garbage = the low const region): - mem757_low_const_copy: i64-head + 3xi8-tail, single segment, low consts - mem757_memcopy_static_src: memory.copy from a const static pointer - mem757_ptr_base_copy: pointer-base + small memarg offset - mem757_memmove_param: separate memmove(dst,src,len) fn, overlapping head-i64 + tail-i32, +0x20 applied by caller - mem757_inlined_memmove: inlined #746 large-memarg head + overlapping tail All FIVE compile CORRECTLY on current main (v0.44.0) — every emitted __synth_wasm_seg_0 addend is +0x20 exactly, execution matches wasmtime byte-for-byte. The const/base-CSE aliasing hypotheses are ruled out: const_materialization ignores relocated-symbol loads (opaque to const-CSE), and base-CSE is optimized-path-only (never reaches --relocatable). Investigation continues into the select_with_stack head/tail source-base derivation. Harnesses resolve BOTH R_ARM_ABS32 and R_ARM_THM_CALL (an unresolved bl self-corrupts = vacuous gate). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…ll/reload Move onto the RUNTIME-OFFSET axis (not the relocation-addend axis the five prior fixtures verified). mem757_rawvec_memcopy holds the &STATIC[0] source pointer (data_base+0x20) in a local ACROSS the RawVec-grow call, forcing spill/reload, then uses it as the memory.copy source — gale's exact run->grow->memmove call graph. GREEN: disasm confirms the +0x20 is computed at runtime (ldr =seg_0; add r3,r1,#0x20), spilled to [sp], reloaded intact after the call, and the copy loop sources correctly. The source pointer value survives the call byte-perfect. Six faithful shapes now green across BOTH axes (link-time addend AND runtime value). No copy-lowering change since v0.43.1 (git log confirms). The reducible shapes provably relocate AND run correctly. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
… guard 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 16, 2026
… WasmCert anchor + VCR-ISA 41→50, A64 7→50, 12× beat-LLVM, MC/DC provenance) (#775) Five oracle-gated lanes across semantics/capability/perf/assurance: - VCR-WASM-001 (#771): WasmCert-Coq source anchor (i32.add refinement, 474→476) - VCR-ISA-001 (#773): generate-not-mirror 41→50 ops (476→485 Qed) - #538 (#769): AArch64 milestone 2 — 7→50 integer ops, honest div/rem decline - #494 (#770): proof-carrying rem_u elision — 12× beat over clang -Os - #396 (#774): synth-provenance-v1 MC/DC source-to-object map (VCR-DEC-003) #757 stays OPEN (accepted residual — 7 reconstructions all green, needs reporter module; #772 lands them as regression guards). i64.trunc_f64 + #761 residuals noted. Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
avrabe
added a commit
that referenced
this pull request
Jul 16, 2026
…ST-declared owner (#779) gale's fused os-tl node (loom.wasm) declares THREE active data segments ALL at wasm linear-memory offset 0x100000. In WASM, active segments apply in declaration order, so a LATER segment OVERWRITES an earlier one — seg_2 (last, 24 B) owns those bytes at runtime and holds "gust:os up\n" at linmem 0x100008. The #354 mixed-split reloc retargeting (main.rs) mapped each `__synth_wasm_data + C` static access to a per-segment `__synth_wasm_seg_K` symbol by finding the segment whose wasm-offset range contains C — via `.position()`, the FIRST match. With overlapping segments that binds an address to the earliest segment, not the one that owns it at runtime: the string source at 0x100008 bound to `__synth_wasm_seg_0 + 8` (seg_0's stale const 0x02) instead of `__synth_wasm_seg_2 + 8` (the string). Runtime: got=[2,0,0,0,1,0,0,32,...] instead of "gust:os up\n" — a silent miscompile, byte-identical across 0.43.0/0.43.1/0.44.0/ 0.45.0 and NOT reproducible by synthetic reconstructions (PR #772: 7 shapes green). Fix: `.position()` -> `.rposition()` — resolve overlapping addresses to the LAST-declared containing segment, matching WASM overwrite semantics. For non-overlapping segments every address is in exactly one, so first==last match and the emitted bytes are byte-identical (frozen anchors 10/10, all existing static-data differentials green — #739/#746/#758/#406 unaffected). Oracle: scripts/repro/mem757_gale_differential.py pins gale's exact loom.wasm as a permanent CI regression fixture. It reconstructs runtime linmem (segments applied in order, later-wins) and asserts every static-data reloc reads the runtime-correct byte — RED on pre-fix (seg_0+8 reads 0x02, runtime owns 'g'=0x67), GREEN on fix. Non-vacuous by construction; the real module lives in CI because the synthetic shapes provably don't cover it. Follow-up North Star lane filed: VCR-VER-003 (#777) — per-compilation translation validation of static-data addressing, so this whole #739/#746/#757/#758 cluster becomes unrepresentable. Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L 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
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.
v0.45 Lane 1 — attempted to reproduce + fix #757 from gale's mechanism-neutral characterization. Result: NO FIX — the miscompile does not reproduce on any synthetic reconstruction. #757 stays OPEN, blocked on gale's exact
loom.wasm/os-tl-cm3.o.What was tried
gale's 0.43.1 re-test characterized #757 as: garbage output bytes are the low-offset
.dataconst region (0x00–0x1f), not string-adjacent → a multi-chunk memmove readsdata_base + smallinstead ofdata_base + 0x20, in the RawVec-grow + memmove copying a ≥9-byte static abovewasm_data_baseshape (reached via a grow-call spill/reload). The direct-i64.loadtoy does NOT trigger it.Built 7 faithful reconstructions of that shape (
scripts/repro/mem757_*): inlined memmove, low-const-copy, memcopy static-src, memmove-param, ptr-base-copy, rawvec-memcopy (the closest to gale's grow-call shape), pressure-chunks. All 7 compile byte-correct vs wasmtime —src+0x20survives the grow-call spill/reload in every case; the source offset is correct.Conclusion
Consistent with the v0.43.1 disproof (7 direct-load shapes also green): the exact ARM instruction shape that triggers the miscompile is not reconstructable from the description. It needs gale's exact reduced object. Re-requested
loom.wasm/os-tl-cm3.oon #757.What lands here (investigation value, not a fix)
mem757_rawvec_memcopy_differential.py) CI-wired as a regression guard that the RawVec-grow copy path stays correct.#757 remains OPEN. No source changed (scripts/repro + ci.yml only).
🤖 Generated with Claude Code