The gap
synth lowers WASM → bare-metal ELF but emits zero DWARF (confirmed: no .debug_* sections in any output). So a synth-compiled firmware image cannot be source-debugged in gdb/lldb — no source line at a PC, no variable locations, no backtraces with names. For a real embedded toolchain this is table-stakes.
Meanwhile the input carries it and the upstream preserves it:
- Real Rust/clang → wasm modules carry DWARF in custom sections (e.g. our
msgq_put_359.wasm has .debug_* across 8 custom sections).
- meld already remaps that WASM DWARF through its fusion transforms (
meld-core/src/dwarf.rs, dwarf_remap_witness/dwarf_passthrough tests) — so the wasm synth receives has valid, fusion-adjusted DWARF (wasm-code-offset → source file/line/variable).
synth is the only stage that drops it. Like meld adjusts WASM-DWARF through its transform, synth must emit ARM/RISC-V-ELF DWARF through its WASM→machine lowering.
Why this is tractable — synth already has the spine
Every ArmInstruction carries source_line: Option<usize> — the WASM op index it came from (≈220 threading sites already). That is the (machine-address → wasm-offset) half of the map. Composing it with the input wasm's DWARF (wasm-offset → source) yields (machine-address → source) — the .debug_line program.
Scope, two tiers
Tier 1 — .debug_line (near-term; raw material ready). Read the input wasm's .debug_line, compose with synth's source_line threading, emit an ELF .debug_line so breakpoints + single-stepping land on source lines, and backtraces show file:line. Independent of regalloc. The achievable first win.
Tier 2 — .debug_info variable locations (downstream of regalloc). Map source variables → their ARM register / stack-slot location ranges (DWARF location lists). This needs the value → physical-location mapping the register allocator produces — i.e. it is gated on the VCR-RA allocator wiring (and is the same (pc, local) → ARM-vreg mapping surfaced in the scry/VCR-RA-010 discussion). Until then, Tier 1 already gives line-level debugging.
Coordination
- meld owns wasm-DWARF remap (done); synth owns the wasm→ELF DWARF emit (this issue). Worth a shared note so the line/var encodings compose cleanly end-to-end (source → meld → synth → on-target debugger).
- Pairs with the
--native-pointer-abi path (where addresses are host-pointer-relative) and the relocatable-ELF builder (the DWARF sections must survive the host link).
Acceptance (Tier 1)
A synth-compiled ELF from a DWARF-carrying wasm, loaded in gdb/lldb against the target (or Renode), stops at the correct source line on a PC breakpoint and shows a file:line backtrace; the differential/frozen fixtures stay bit-identical in .text (DWARF is additive, non-loadable sections).
Filed from the codegen-debuggability discussion; tracked in rivet alongside VCR-RA (Tier 2 dependency).
The gap
synth lowers WASM → bare-metal ELF but emits zero DWARF (confirmed: no
.debug_*sections in any output). So a synth-compiled firmware image cannot be source-debugged in gdb/lldb — no source line at a PC, no variable locations, no backtraces with names. For a real embedded toolchain this is table-stakes.Meanwhile the input carries it and the upstream preserves it:
msgq_put_359.wasmhas.debug_*across 8 custom sections).meld-core/src/dwarf.rs,dwarf_remap_witness/dwarf_passthroughtests) — so the wasm synth receives has valid, fusion-adjusted DWARF (wasm-code-offset → source file/line/variable).synth is the only stage that drops it. Like meld adjusts WASM-DWARF through its transform, synth must emit ARM/RISC-V-ELF DWARF through its WASM→machine lowering.
Why this is tractable — synth already has the spine
Every
ArmInstructioncarriessource_line: Option<usize>— the WASM op index it came from (≈220 threading sites already). That is the (machine-address → wasm-offset) half of the map. Composing it with the input wasm's DWARF (wasm-offset → source) yields (machine-address → source) — the.debug_lineprogram.Scope, two tiers
Tier 1 —
.debug_line(near-term; raw material ready). Read the input wasm's.debug_line, compose with synth'ssource_linethreading, emit an ELF.debug_lineso breakpoints + single-stepping land on source lines, and backtraces show file:line. Independent of regalloc. The achievable first win.Tier 2 —
.debug_infovariable locations (downstream of regalloc). Map source variables → their ARM register / stack-slot location ranges (DWARF location lists). This needs the value → physical-location mapping the register allocator produces — i.e. it is gated on the VCR-RA allocator wiring (and is the same (pc, local) → ARM-vreg mapping surfaced in the scry/VCR-RA-010 discussion). Until then, Tier 1 already gives line-level debugging.Coordination
--native-pointer-abipath (where addresses are host-pointer-relative) and the relocatable-ELF builder (the DWARF sections must survive the host link).Acceptance (Tier 1)
A synth-compiled ELF from a DWARF-carrying wasm, loaded in gdb/lldb against the target (or Renode), stops at the correct source line on a PC breakpoint and shows a file:line backtrace; the differential/frozen fixtures stay bit-identical in
.text(DWARF is additive, non-loadable sections).Filed from the codegen-debuggability discussion; tracked in rivet alongside VCR-RA (Tier 2 dependency).