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
39 changes: 36 additions & 3 deletions artifacts/verified-codegen-roadmap.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -1455,9 +1455,42 @@ artifacts:
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.
only; RISC-V carries an empty map (follow-up).
- step (5b) EMIT landed (PR B #429, a89ef28, v0.12.0 in progress):
gimli is now a PRODUCTION dep of synth-core (Cargo.toml + the
hand-written `crates/BUILD.bazel` synth-core `deps` — from_cargo makes
`@crates//:gimli` available but the manual rust_library must list it;
cargo passed locally while Bazel reddened E0433 until fix 63c510f).
`--debug-line` (clap flag, EXPERIMENTAL caveat) gates emission: when set
AND the input wasm carries `.debug_line`, synth reads the input rows
(`read_input_dwarf_line`), composes addr→source via the captured
`line_map`, and emits a FULL DWARF unit (DW_TAG_compile_unit with
DW_AT_stmt_list → `.debug_line`, so a normal `dwarf.units()` walk reads
it — not just a bare `DebugLine` program). Three oracles
(dwarf_debug_line_emit_394.rs): additive-on-dwarf-input (byte-compares
.text/.data/.bss, asserts `.debug_*` flag-gated), no-op-on-nodwarf-input
(whole-.o identical), and resolves-arm-addr-to-source (walks the normal
unit path, 110 in-range rows → non-zero lines). Frozen fixtures
untouched. KNOWN GAP closed by step 5c: emitted `.debug_*` addresses are
`.text`-base-0 with NO relocations, so they are CORRECT in the object
but WRONG on a linked image — a `--debug-line` consumer (jess, actively
Renode/silicon-debugging gust, the plausible first consumer) would get
silently-wrong source lines after host-link. The v0.12.0 TAG is HELD for
step 5c (advisor-confirmed: PR B in main is default-off + frozen-safe, so
it banks the work at zero risk; the tag waits for relocations).
- step (5c) RELOCATIONS — PR C, REQUIRED before the v0.12.0 tag:
C1 = generalize elf_builder's `.rel.text`-ONLY relocation machinery to
PER-SECTION relocations, **REL form (not RELA)** — synth/ARM32 uses REL
with the addend stored in-place (`.rel.debug_*`, matching the existing
`.rel.text` convention); frozen-safe, gated on the existing `.rel.text`
fixtures (cabi_arena_realloc_linkability_418) staying byte-identical.
C2 = emit DWARF addresses via gimli `Address::Symbol{text_sym, addend}`,
extract the relocations, emit `.rel.debug_line` / `.rel.debug_info`
against the `.text` symbol. The C2 ORACLE must APPLY the relocations at a
NONZERO `.text` base and verify the address resolves to the CORRECT
source line (not merely that a reloc record exists). Advisor caution:
"do NOT rush the addend math into a debug-info path — careful (even next
session) beats fast."
status: approved
tags: [toolchain, dwarf, debuggability, elf, meld-coordination, feature-loop, release-v0.12.0, synth-394]
links:
Expand Down
129 changes: 119 additions & 10 deletions crates/synth-backend/src/elf_builder.rs
Original file line number Diff line number Diff line change
Expand Up @@ -338,6 +338,16 @@ pub enum ArmRelocationType {
MovtAbs = 44,
}

/// A built `.rel.<name>` section: its name offset in `.shstrtab`, the target
/// section index it relocates (`sh_info`), its file offset, and the encoded
/// REL entries. Internal to [`ElfBuilder::build`].
struct ExtraRelSection {
name_offset: usize,
target_idx: u32,
offset: usize,
data: Vec<u8>,
}

/// ELF relocation entry (REL format, no addend)
#[derive(Debug, Clone)]
pub struct Relocation {
Expand Down Expand Up @@ -378,6 +388,12 @@ pub struct ElfBuilder {
program_headers: Vec<ProgramHeader>,
/// Relocations for .text section
relocations: Vec<Relocation>,
/// Extra per-section relocation tables, keyed by the target section's name
/// (e.g. `.debug_line`). Each produces a `.rel.<name>` section. Kept separate
/// from `relocations` (the `.text` set) so the existing `.rel.text` byte
/// layout is untouched: when this is empty the build is byte-identical to the
/// pre-generalization output (VCR-DBG-001 PR C, #394).
extra_relocations: Vec<(String, Vec<Relocation>)>,
}

impl ElfBuilder {
Expand All @@ -394,6 +410,7 @@ impl ElfBuilder {
symbols: Vec::new(),
program_headers: Vec::new(),
relocations: Vec::new(),
extra_relocations: Vec::new(),
}
}

Expand Down Expand Up @@ -431,6 +448,16 @@ impl ElfBuilder {
self.symbols.push(symbol);
}

/// Add a symbol and return its 1-based index in `.symtab` (index 0 is the
/// reserved null symbol). Use when a later relocation must reference this
/// symbol — e.g. the `.text` base symbol the DWARF `.rel.debug_*` records
/// resolve against (VCR-DBG-001).
pub fn add_symbol_indexed(&mut self, symbol: Symbol) -> u32 {
let index = self.symbols.len() as u32 + 1;
self.symbols.push(symbol);
index
}

/// Add a program header (segment)
pub fn add_program_header(&mut self, ph: ProgramHeader) {
self.program_headers.push(ph);
Expand All @@ -441,6 +468,20 @@ impl ElfBuilder {
self.relocations.push(reloc);
}

/// Add a relocation table targeting a non-`.text` section by name (e.g.
/// `.debug_line`). Produces a separate `.rel.<name>` section whose `sh_info`
/// points at the named section. The section must already have been added via
/// [`add_section`]; if no matching section exists at build time the table is
/// silently dropped. Used by VCR-DBG-001 to relocate the DWARF `.text`
/// references so a host linker fixes them up alongside `.text`.
pub fn add_section_relocations(&mut self, target_section: &str, relocs: Vec<Relocation>) {
if relocs.is_empty() {
return;
}
self.extra_relocations
.push((target_section.to_string(), relocs));
}

/// Add an undefined external symbol (e.g., __meld_dispatch_import)
/// Returns the symbol index (1-based, accounting for null symbol)
pub fn add_undefined_symbol(&mut self, name: &str) -> u32 {
Expand Down Expand Up @@ -471,7 +512,8 @@ impl ElfBuilder {
output.resize(header_size + ph_table_size, 0);

// Build string table for section names
let (shstrtab_data, section_name_offsets) = self.build_section_string_table();
let (shstrtab_data, section_name_offsets, extra_rel_name_offsets) =
self.build_section_string_table();

// Build symbol string table
let (strtab_data, symbol_name_offsets) = self.build_symbol_string_table();
Expand Down Expand Up @@ -504,6 +546,26 @@ impl ElfBuilder {
let rel_offset = current_offset;
current_offset += rel_data.len();

// Extra per-section relocation tables (.rel.<name>), laid out after
// .rel.text. Each entry resolves its target section index by name; a
// table whose target section is absent is dropped. Empty when no
// --debug-line ⇒ byte-identical to the pre-generalization layout.
let mut extra_rel: Vec<ExtraRelSection> = Vec::new();
for (i, (target, relocs)) in self.extra_relocations.iter().enumerate() {
let Some(target_idx) = self.section_index_by_name(target) else {
continue;
};
let data = Self::encode_rel_entries(relocs);
let name_offset = extra_rel_name_offsets.get(i).copied().unwrap_or(0);
extra_rel.push(ExtraRelSection {
name_offset,
target_idx,
offset: current_offset,
data,
});
current_offset += extra_rel.last().unwrap().data.len();
}

// Section header table comes at the end
let sh_offset = current_offset;

Expand All @@ -517,6 +579,9 @@ impl ElfBuilder {

output.extend_from_slice(&symtab_data);
output.extend_from_slice(&rel_data);
for er in &extra_rel {
output.extend_from_slice(&er.data);
}

// Write section headers
let section_headers = self.build_section_headers_with_rel(
Expand All @@ -530,6 +595,7 @@ impl ElfBuilder {
&section_offsets,
rel_offset,
&rel_data,
&extra_rel,
);
output.extend_from_slice(&section_headers);

Expand All @@ -555,7 +621,7 @@ impl ElfBuilder {

// Now write the actual ELF header at the beginning
let has_rel = !self.relocations.is_empty();
let num_sections = 4 + self.sections.len() + if has_rel { 1 } else { 0 };
let num_sections = 4 + self.sections.len() + if has_rel { 1 } else { 0 } + extra_rel.len();
let ph_offset = if ph_count > 0 { header_size as u32 } else { 0 };
self.write_elf_header_with_phdrs(
&mut output[0..header_size],
Expand Down Expand Up @@ -700,8 +766,12 @@ impl ElfBuilder {
Ok(())
}

/// Build section name string table
fn build_section_string_table(&self) -> (Vec<u8>, Vec<usize>) {
/// Build section name string table. Returns the bytes, the per-user-section
/// name offsets, and the per-extra-relocation `.rel.<name>` name offsets
/// (parallel to `self.extra_relocations`). The extra-rel names are appended
/// AFTER `.rel.text`, so when `extra_relocations` is empty the table is
/// byte-identical to the pre-generalization layout.
fn build_section_string_table(&self) -> (Vec<u8>, Vec<usize>, Vec<usize>) {
let mut strtab = vec![0]; // null string at offset 0
let mut offsets = Vec::new();

Expand All @@ -723,7 +793,15 @@ impl ElfBuilder {
strtab.extend_from_slice(b".rel.text\0");
}

(strtab, offsets)
// .rel.<name> for each extra per-section relocation table.
let mut extra_rel_offsets = Vec::new();
for (target, _) in &self.extra_relocations {
let offset = strtab.len();
extra_rel_offsets.push(offset);
strtab.extend_from_slice(format!(".rel{target}\0").as_bytes());
}

(strtab, offsets, extra_rel_offsets)
}

/// Build symbol name string table
Expand All @@ -743,12 +821,14 @@ impl ElfBuilder {

/// Build relocation table (ELF32 REL entries: 8 bytes each)
fn build_relocation_table(&self) -> Vec<u8> {
if self.relocations.is_empty() {
return Vec::new();
}
Self::encode_rel_entries(&self.relocations)
}

/// Encode a slice of relocations as ELF32 REL entries (8 bytes each). Shared
/// by `.rel.text` and the per-section `.rel.<name>` tables.
fn encode_rel_entries(relocs: &[Relocation]) -> Vec<u8> {
let mut rel_data = Vec::new();
for reloc in &self.relocations {
for reloc in relocs {
// r_offset (4 bytes)
rel_data.extend_from_slice(&reloc.offset.to_le_bytes());
// r_info (4 bytes) = (sym_index << 8) | type
Expand All @@ -758,6 +838,16 @@ impl ElfBuilder {
rel_data
}

/// Resolve a target section name to its ELF section index. User sections
/// begin at index 4 (null=0, shstrtab=1, strtab=2, symtab=3). Returns `None`
/// if no user section has that name.
fn section_index_by_name(&self, name: &str) -> Option<u32> {
self.sections
.iter()
.position(|s| s.name == name)
.map(|pos| 4 + pos as u32)
}

/// Build symbol table
fn build_symbol_table(&self, name_offsets: &[usize]) -> Vec<u8> {
let mut symtab = Vec::new();
Expand Down Expand Up @@ -817,6 +907,7 @@ impl ElfBuilder {
section_offsets: &[usize],
rel_offset: usize,
rel_data: &[u8],
extra_rel: &[ExtraRelSection],
) -> Vec<u8> {
let mut headers = Vec::new();

Expand Down Expand Up @@ -920,6 +1011,24 @@ impl ElfBuilder {
);
}

// Extra .rel.<name> sections (e.g. .rel.debug_line). Same shape as
// .rel.text but sh_info points at the named target section.
for er in extra_rel {
self.write_section_header(
&mut headers,
er.name_offset as u32,
SectionType::Rel as u32,
0,
0,
er.offset as u32,
er.data.len() as u32,
3, // sh_link = .symtab section index
er.target_idx, // sh_info = relocated section
4,
8, // Each REL entry is 8 bytes
);
}

headers
}

Expand Down Expand Up @@ -1233,7 +1342,7 @@ mod tests {
builder.add_section(Section::new(".text", SectionType::ProgBits));
builder.add_section(Section::new(".data", SectionType::ProgBits));

let (strtab, offsets) = builder.build_section_string_table();
let (strtab, offsets, _extra_rel_offsets) = builder.build_section_string_table();

// Should have null byte at start
assert_eq!(strtab[0], 0);
Expand Down
Loading
Loading