Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 12 additions & 0 deletions artifacts/verified-codegen-roadmap.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down
4 changes: 4 additions & 0 deletions crates/synth-backend-riscv/src/backend.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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(),
})
}

Expand Down Expand Up @@ -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(),
Expand Down
68 changes: 64 additions & 4 deletions crates/synth-backend/src/arm_backend.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -105,14 +105,15 @@ impl Backend for ArmBackend {
ops: &[WasmOp],
config: &CompileConfig,
) -> Result<CompiledFunction, BackendError> {
let (code, relocations) =
let (code, relocations, line_map) =
compile_wasm_to_arm(ops, config).map_err(BackendError::CompilationFailed)?;

Ok(CompiledFunction {
name: name.to_string(),
code,
wasm_ops: ops.to_vec(),
relocations,
line_map,
})
}

Expand Down Expand Up @@ -154,7 +155,7 @@ fn count_params(wasm_ops: &[WasmOp]) -> u32 {
fn compile_wasm_to_arm(
wasm_ops: &[WasmOp],
config: &CompileConfig,
) -> Result<(Vec<u8>, Vec<CodeRelocation>), String> {
) -> Result<(Vec<u8>, Vec<CodeRelocation>, LineMap), String> {
let num_params = count_params(wasm_ops);

let bounds_config = match config.effective_safety_bounds() {
Expand Down Expand Up @@ -458,6 +459,14 @@ fn compile_wasm_to_arm(
}
let mut pending_literals: Vec<PendingLiteral> = 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
Expand Down Expand Up @@ -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))?;
Expand Down Expand Up @@ -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).
Expand Down Expand Up @@ -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];
Expand Down
16 changes: 16 additions & 0 deletions crates/synth-core/src/backend.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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<usize>)>;

/// A single compiled function
#[derive(Debug, Clone)]
pub struct CompiledFunction {
Expand All @@ -237,6 +244,15 @@ pub struct CompiledFunction {
pub wasm_ops: Vec<WasmOp>,
/// Relocations for external symbol references (BL to bridge functions)
pub relocations: Vec<CodeRelocation>,
/// 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
Expand Down
Loading