feat(dwarf): emit DWARF debug sections behind --debug-line (VCR-DBG-001, #242, #394)#429
Merged
Conversation
…01, #242, #394) PR B of v0.12.0: with `--debug-line`, synth emits a full DWARF unit (`.debug_info`/`.debug_abbrev`/`.debug_str`/`.debug_line`) into the relocatable ELF, mapping ARM `.text` addresses back to the input wasm's source lines via PR A's per-instruction line_map. Pipeline: read the input wasm's `.debug_line` (gimli, now a production dep of synth-core — auto-resolved by Bazel via from_cargo), compose `func_offset + machine_offset → op_offsets[op_idx] → op_offsets_to_source → source line`, emit a real `DW_TAG_compile_unit` whose `DW_AT_stmt_list` points at `.debug_line`, and add the sections as NON-ALLOC trailing PROGBITS (after `.text`/`.data`/`.bss`, so the hardcoded `with_section(4/5/6)` symbol indices are undisturbed). Frozen-safe: the entire emit is behind `if debug_line` (default off), so the default build is byte-identical. Oracles (dwarf_debug_line_emit_394.rs): - additivity: on a DWARF input (msgq) `.text`/`.data`/`.bss` are byte-identical with/without the flag and the `.debug_*` sections appear only under it; on a no-DWARF input (gust_kernel) the whole `.o` is byte-identical. - reachability: the emitted DWARF is walked via the NORMAL gimli `dwarf.units()` → CU `DW_AT_stmt_list` line-program path (the path a debugger uses), resolving 110 in-range `.text` addresses to non-zero source lines. EXPERIMENTAL scope: addresses are object-relative (`.text` base 0) with no `.rela.debug_*` yet, so they are correct for the unlinked object but shift by the load base once linked. PR C (VCR-DBG-002) generalizes the elf_builder's `.rel.text`-only relocation machinery to emit `.rela.debug_*` against the `.text` symbol — required before v0.12.0 is tagged. ARM only; RISC-V is a follow-up. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The hand-written rust_library `deps` in crates/BUILD.bazel are not generated from Cargo.toml, so moving gimli to a production dependency of synth-core (which cargo honours) left the Bazel target compiling synth-core without it → `error[E0433]: unresolved crate gimli` in "Bazel Build & Proofs". from_cargo makes the `@crates//:gimli` alias available; the manual target must still list it. Verified `bazel build //crates:synth` green.
Codecov Report❌ Patch coverage is
📢 Thoughts on this report? Let us know! |
This was referenced Jun 22, 2026
avrabe
added a commit
that referenced
this pull request
Jun 22, 2026
, #394) (#440) First release of the north-star verified-codegen campaign. Pin sweep 0.11.51 -> 0.12.0 (workspace + all path-dep versions + MODULE.bazel + Cargo.lock), CHANGELOG, and VCR-DBG-001 roadmap status -> implemented. Ships: - VCR-DBG-001 `--debug-line` DWARF emission (PR A #427 / B #429 / C #430): debugger-readable .debug_* mapping ARM .text -> wasm source lines, with .rel.debug_* relocations verified end-to-end against arm-none-eabi-ld. Purely additive; default build bit-identical. - VCR-MEM-001 layer-2 frozen-safe budget decision logic + oracles (#421-#425). - gimli 0.33 adaptation (#439) + wast 252 (#438). Minor bump: new user-facing `--debug-line` feature (semver-correct). 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.
What — PR B of v0.12.0 (DWARF)
With
--debug-line, synth emits a full DWARF unit (.debug_info/.debug_abbrev/.debug_str/.debug_line) into the relocatable ELF, mapping ARM.textaddresses back to the input wasm's source lines via PR A's per-instructionline_map(#427).Pipeline: read the input wasm's
.debug_line(gimli, now a production dep of synth-core — auto-resolved by Bazel via from_cargo #422) → composefunc_offset + machine_offset → op_offsets[op_idx] → op_offsets_to_source → source line→ emit a realDW_TAG_compile_unitwhoseDW_AT_stmt_listpoints at.debug_line→ add the sections as non-ALLOC trailing PROGBITS (after.text/.data/.bss, so the hardcodedwith_section(4/5/6)symbol indices are undisturbed).Frozen-safe
The entire emit is behind
if debug_line(default off) → default build byte-identical. Two oracles (dwarf_debug_line_emit_394.rs), independently re-run:.text/.data/.bssbyte-identical with/without the flag,.debug_*present only under it; no-DWARF input (gust_kernel) → whole.obyte-identical.gimli::Dwarf::units()→ CUDW_AT_stmt_list→ line-program path (the path a debugger uses), resolving 110 in-range.textaddresses to non-zero source lines (e.g..text+0x023c → line 175).Experimental scope (honest boundary — gates the v0.12.0 tag, not this merge)
Addresses are object-relative (
.textbase 0) with no.rela.debug_*relocations yet — correct for the unlinked object, but they shift by the load base once linked against the TCB. The flag's help text says so. PR C (VCR-DBG-002) generalizes the elf_builder's.rel.text-only relocation machinery to emit.rela.debug_*against the.textsymbol — required before v0.12.0 is tagged, so the flag is never released in the object-relative-only state.ARM only; RISC-V carries an empty
line_map(follow-up).Verification
cargo test --workspace --exclude synth-verifygreen; the 3 oracles pass (independently re-run)cargo fmt --checkclean;cargo clippy --workspace --exclude synth-verify --all-targets -- -D warningscleanRefs #242, #394. Builds on #427 (PR A).
🤖 Generated with Claude Code