diff --git a/artifacts/verified-codegen-roadmap.yaml b/artifacts/verified-codegen-roadmap.yaml index e283d2ec..9f6f1909 100644 --- a/artifacts/verified-codegen-roadmap.yaml +++ b/artifacts/verified-codegen-roadmap.yaml @@ -1446,6 +1446,18 @@ artifacts: and host-link survival — the deliberate v0.12.0 release step (step 5 oracle then asserts .text byte-identical to the no-DWARF build). NOT an idle-tick increment. + - step (5a) MACHINE-OFFSET CAPTURE landed (PR A, v0.12.0 in progress): + the encoder gap is closed — `compile_wasm_to_arm` now captures a + `LineMap = Vec<(machine_offset, wasm_op_index)>` (synth-core backend.rs) + during the encode loop (`code.len()` immediately before each `encode()`; + the trailing literal pool and in-place LDR patch don't shift earlier + offsets), carried on `CompiledFunction.line_map`. Purely additive: the + map is never serialized, so `.text` is byte-identical (the existing + differential fixtures + `test_line_map_is_wellformed_dbg001` assert + monotonic in-bounds offsets and deterministic, unperturbed code). ARM + only; RISC-V carries an empty map (follow-up). step (5b) = gimli prod-dep + + input `.debug_line` read + emit behind `--debug-line` + the additivity + byte-diff oracle. status: approved tags: [toolchain, dwarf, debuggability, elf, meld-coordination, feature-loop, release-v0.12.0, synth-394] links: diff --git a/crates/synth-backend-riscv/src/backend.rs b/crates/synth-backend-riscv/src/backend.rs index 16c08f2d..9d1b6365 100644 --- a/crates/synth-backend-riscv/src/backend.rs +++ b/crates/synth-backend-riscv/src/backend.rs @@ -177,6 +177,9 @@ fn compile_function_with_opts( code: bytes, wasm_ops: ops.to_vec(), relocations: Vec::new(), + // RISC-V DWARF `.debug_line` emission is a VCR-DBG-001 follow-up; no + // source map produced yet (empty ⇒ the emitter skips this backend). + line_map: Vec::new(), }) } @@ -381,6 +384,7 @@ mod tests { code: Vec::new(), wasm_ops: ops.clone(), relocations: Vec::new(), + line_map: Vec::new(), }; let cfg = CompileConfig { target: TargetSpec::riscv32imac(), diff --git a/crates/synth-backend/src/arm_backend.rs b/crates/synth-backend/src/arm_backend.rs index 0d2ac75c..0071aab1 100644 --- a/crates/synth-backend/src/arm_backend.rs +++ b/crates/synth-backend/src/arm_backend.rs @@ -6,7 +6,7 @@ use crate::ArmEncoder; use synth_core::backend::{ Backend, BackendCapabilities, BackendError, CodeRelocation, CompilationResult, CompileConfig, - CompiledFunction, SafetyBounds, + CompiledFunction, LineMap, SafetyBounds, }; use synth_core::target::{IsaVariant, TargetSpec}; use synth_core::wasm_decoder::DecodedModule; @@ -105,7 +105,7 @@ impl Backend for ArmBackend { ops: &[WasmOp], config: &CompileConfig, ) -> Result { - let (code, relocations) = + let (code, relocations, line_map) = compile_wasm_to_arm(ops, config).map_err(BackendError::CompilationFailed)?; Ok(CompiledFunction { @@ -113,6 +113,7 @@ impl Backend for ArmBackend { code, wasm_ops: ops.to_vec(), relocations, + line_map, }) } @@ -154,7 +155,7 @@ fn count_params(wasm_ops: &[WasmOp]) -> u32 { fn compile_wasm_to_arm( wasm_ops: &[WasmOp], config: &CompileConfig, -) -> Result<(Vec, Vec), String> { +) -> Result<(Vec, Vec, LineMap), String> { let num_params = count_params(wasm_ops); let bounds_config = match config.effective_safety_bounds() { @@ -458,6 +459,14 @@ fn compile_wasm_to_arm( } let mut pending_literals: Vec = Vec::new(); + // VCR-DBG-001: per-instruction source map for DWARF `.debug_line`. Captured + // here because `code.len()` immediately before `encode()` is the final + // machine offset of the instruction within this function's `.text` — nothing + // after the loop shifts earlier instructions (the literal pool is appended at + // the end; the LDR patch below is in-place/length-preserving). Purely + // additive: it does not touch `code`, so `.text` is byte-identical. + let mut line_map: LineMap = Vec::new(); + for instr in &arm_instrs { // Record a relocation for every BL: the encoder emits `bl #0` and // relies on a relocation to patch the target. This covers BOTH import @@ -499,6 +508,10 @@ fn compile_wasm_to_arm( }); } + // The machine offset of this instruction is the current code length, + // captured before the bytes are appended. + line_map.push((code.len() as u32, instr.source_line)); + let encoded = encoder .encode(&instr.op) .map_err(|e| format!("ARM encoding failed: {}", e))?; @@ -557,7 +570,7 @@ fn compile_wasm_to_arm( } } - Ok((code, relocations)) + Ok((code, relocations, line_map)) } /// Resolve local label branches to byte-accurate offsets (#202). @@ -692,6 +705,53 @@ mod tests { assert_eq!(func.wasm_ops, ops); } + /// VCR-DBG-001: the per-instruction source map must cover the function with + /// monotonic, in-bounds machine offsets, and must not perturb the emitted + /// code (it is captured at encode time, never serialized here). + #[test] + fn test_line_map_is_wellformed_dbg001() { + let backend = ArmBackend::new(); + let ops = vec![ + WasmOp::LocalGet(0), + WasmOp::LocalGet(1), + WasmOp::I32Add, + WasmOp::End, + ]; + let config = CompileConfig::default(); + let func = backend.compile_function("add", &ops, &config).unwrap(); + + // Non-empty, and the first instruction starts at machine offset 0. + assert!( + !func.line_map.is_empty(), + "a non-trivial function captures a source map" + ); + assert_eq!(func.line_map[0].0, 0, "first instruction at offset 0"); + + // Offsets strictly increase by at least one ARM/Thumb instruction (>= 2 + // bytes) and every mapped offset lies inside the emitted `.text`. + for w in func.line_map.windows(2) { + assert!(w[1].0 > w[0].0, "instruction offsets strictly increase"); + assert!( + w[1].0 - w[0].0 >= 2, + "each ARM/Thumb instruction is >= 2 bytes" + ); + } + let last = func.line_map.last().unwrap().0 as usize; + assert!( + last < func.code.len(), + "every mapped offset lies inside .text" + ); + + // The side-table is additive: recompiling is deterministic and the map is + // consistent with that exact code (capturing it does not alter output). + let again = backend.compile_function("add", &ops, &config).unwrap(); + assert_eq!( + again.code, func.code, + "compilation deterministic; map is additive" + ); + assert_eq!(again.line_map, func.line_map); + } + #[test] fn test_count_params() { let ops = vec![WasmOp::LocalGet(0), WasmOp::LocalGet(1), WasmOp::I32Add]; diff --git a/crates/synth-core/src/backend.rs b/crates/synth-core/src/backend.rs index 80cf03ea..a9d96fcf 100644 --- a/crates/synth-core/src/backend.rs +++ b/crates/synth-core/src/backend.rs @@ -226,6 +226,13 @@ pub struct CodeRelocation { pub kind: RelocKind, } +/// VCR-DBG-001: a per-instruction source map — `(machine_offset_within_code, +/// wasm_op_index)` pairs, one per emitted machine instruction. A `None` op-index +/// marks an instruction with no originating wasm op (prologue/epilogue, literal +/// pool). Consumed by the DWARF `.debug_line` emitter; empty when no source map +/// was produced. +pub type LineMap = Vec<(u32, Option)>; + /// A single compiled function #[derive(Debug, Clone)] pub struct CompiledFunction { @@ -237,6 +244,15 @@ pub struct CompiledFunction { pub wasm_ops: Vec, /// Relocations for external symbol references (BL to bridge functions) pub relocations: Vec, + /// VCR-DBG-001: per-instruction source map for DWARF `.debug_line` emission — + /// `(machine_offset_within_code, wasm_op_index)` captured at encode time, one + /// entry per emitted machine instruction. A `None` op-index marks an + /// instruction with no originating wasm op (prologue/epilogue, literal-pool + /// word). This is purely additive metadata: it is never serialized unless + /// `.debug_line` emission is requested, so the emitted `.text` is + /// byte-identical with or without it. Empty for backends/paths that do not + /// yet produce a source map (RISC-V, the optimized ARM path). + pub line_map: LineMap, } /// Result of compiling a full module