From 0ca504244b3a69e9e849463fca95525ae4034ecd Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 30 Jul 2026 14:35:45 +0200 Subject: [PATCH 1/9] aarch64: encoder primitives for call_indirect + globals (#851) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds the five A64 primitives lane L3 needs, each pinned to `clang -c -target aarch64-linux-gnu` ground truth in a unit test: blr xn — the indirect-call branch (call_indirect dispatch) adrp xd, — PC-relative page address (the data-region reach) cmp wn/xn, #imm12 — flags-only immediate compare (no scratch register) add xd,xn,wm,uxtw#s — scaled zero-extended index add (table slot address) `adrp`'s 21-bit page delta splits across TWO disjoint fields (immlo[30:29] + immhi[23:5]); a contiguous placement is silently wrong for every delta >= 1, so the split is pinned by a second test against capstone decodes of the literal words (0xF0000000 = adrp x0,#0x3000; 0x90000020 = #0x4000; 0xF0FFFFE0 = #-0x1000). Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- crates/synth-backend-aarch64/src/encoder.rs | 87 +++++++++++++++++++++ 1 file changed, 87 insertions(+) diff --git a/crates/synth-backend-aarch64/src/encoder.rs b/crates/synth-backend-aarch64/src/encoder.rs index 12fdc597..64ccdb4c 100644 --- a/crates/synth-backend-aarch64/src/encoder.rs +++ b/crates/synth-backend-aarch64/src/encoder.rs @@ -440,6 +440,51 @@ pub fn b_uncond(imm26: i32) -> u32 { 0x1400_0000 | ((imm26 as u32) & 0x03FF_FFFF) } +/// `blr xn` — branch-with-link to the address in `xn`, sets `x30`/LR. The +/// indirect-call primitive: `call_indirect` funnels its verified slot address +/// through this (#851). Clang ground truth: `blr x16` = 0xD63F_0200. +pub fn blr(rn: Reg) -> u32 { + 0xD63F_0000 | ((rn as u32) << 5) +} + +/// `adrp xd, ` — form the PC-relative address of the 4 KiB PAGE containing +/// `sym` (the low 12 bits come from a following `add xd, xd, :lo12:sym`). The +/// 21-bit page delta lives in `immlo` [30:29] + `immhi` [23:5]; emitting `adrp +/// xd, #0` and recording an `R_AARCH64_ADR_PREL_PG_HI21` relocation lets the +/// linker (or the differential harness's own resolver) fill it in. +/// +/// This is the aarch64 answer to "how does the code reach a synth-EMITTED data +/// region": PC-relative + a link-time relocation, with NO dedicated base +/// register — so neither globals nor the funcref table adds a precondition +/// alongside `x28` (see `selector::LINMEM_BASE`). Clang: `adrp x16, sym` = +/// 0x9000_0010. +pub fn adrp(rd: Reg, imm21_pages: i32) -> u32 { + let v = (imm21_pages as u32) & 0x1F_FFFF; + 0x9000_0000 | ((v & 0x3) << 29) | (((v >> 2) & 0x7_FFFF) << 5) | (rd as u32) +} + +/// `cmp wn, #imm12` — `subs wzr, wn, #imm12` (flags only). Compares against an +/// unsigned 12-bit immediate without burning a scratch register. Clang ground +/// truth: `cmp w17, #7` = 0x7100_1E3F. +pub fn cmp_imm(rn: Reg, imm12: u32) -> u32 { + debug_assert!(imm12 < 0x1000, "cmp imm12 out of range"); + 0x7100_0000 | (imm12 << 10) | ((rn as u32) << 5) | (WZR as u32) +} + +/// `cmp xn, #imm12` — 64-bit form. Clang: `cmp x17, #7` = 0xF100_1E3F. +pub fn cmp_imm64(rn: Reg, imm12: u32) -> u32 { + cmp_imm(rn, imm12) | SF64 +} + +/// `add xd, xn, wm, uxtw #shift` — [`add_ext_uxtw`] with a left-shift applied to +/// the zero-extended operand (extend-shift field [12:10], 0..=4). Used to scale a +/// zero-extended i32 table index by the slot size. Clang ground truth: +/// `add x16, x16, w9, uxtw #3` = 0x8B29_4E10. +pub fn add_ext_uxtw_sh(rd: Reg, rn: Reg, rm: Reg, shift: u32) -> u32 { + debug_assert!(shift <= 4, "uxtw extend-shift out of range"); + add_ext_uxtw(rd, rn, rm) | (shift << 10) +} + /// `bl #(imm26*4)` — branch-with-link, PC-relative in words (signed 26-bit), /// sets `x30`/LR to the return address. WASM direct `call` lowers to `bl func_N` /// (#851). When the callee's `.text` offset is not known at selection time (the @@ -902,6 +947,48 @@ mod tests { assert_eq!(ret(), 0xD65F_03C0); } + /// #851 lane L3 — the `call_indirect` + globals addressing primitives. + /// Ground truth from `clang -c -target aarch64-linux-gnu` on: + /// ```text + /// adrp x16, sym -> 90000010 + /// add x16, x16, #0 -> 91000210 + /// add x16, x16, w9, uxtw #3 -> 8b294e10 + /// ldr w17, [x16] -> b9400211 + /// cmp w17, #7 -> 71001e3f + /// cmp x17, #7 -> f1001e3f + /// blr x16 -> d63f0200 + /// adrp x0, sym -> 90000000 + /// ``` + #[test] + fn indirect_and_globals_encodings_match_clang() { + assert_eq!(adrp(16, 0), 0x9000_0010); + assert_eq!(adrp(0, 0), 0x9000_0000); + assert_eq!(add_imm64(16, 16, 0), 0x9100_0210); + assert_eq!(add_ext_uxtw_sh(16, 16, 9, 3), 0x8B29_4E10); + assert_eq!(ldr_w(17, 16, 0), 0xB940_0211); + assert_eq!(cmp_imm(17, 7), 0x7100_1E3F); + assert_eq!(cmp_imm64(17, 7), 0xF100_1E3F); + assert_eq!(blr(16), 0xD63F_0200); + } + + /// The `adrp` page-delta immediate splits ACROSS two disjoint fields — + /// `immlo`[30:29] and `immhi`[23:5] — so a naive contiguous placement is + /// silently wrong for every delta ≥ 1. A relocation normally supplies the + /// delta, but the harness/linker patches these same fields, so the split + /// must be pinned. Ground truth (capstone `CS_ARCH_ARM64` decode of the + /// literal word): + /// ```text + /// 0xF0000000 -> adrp x0, #0x3000 (3 pages: immlo=3, immhi=0) + /// 0x90000020 -> adrp x0, #0x4000 (4 pages: immlo=0, immhi=1) + /// 0xF0FFFFE0 -> adrp x0, #-0x1000 (-1 page: all field bits set) + /// ``` + #[test] + fn adrp_page_delta_splits_immlo_immhi() { + assert_eq!(adrp(0, 3), 0xF000_0000); + assert_eq!(adrp(0, 4), 0x9000_0020); + assert_eq!(adrp(0, -1), 0xF0FF_FFE0); + } + // #851 — divide / multiply-subtract / SIMD popcount building blocks. // Ground truth from `llvm-mc -triple=aarch64 -show-encoding`. #[test] From e42ae16d61f9e8e6fd8cd6ce55ab74a45bf70e8b Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 30 Jul 2026 14:43:48 +0200 Subject: [PATCH 2/9] aarch64 ELF: .data section + the four AArch64 relocation kinds (#851) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The substrate both lane-L3 features need, with NO new precondition. `DataBlob` — a synth-EMITTED `.data` (PROGBITS, ALLOC|WRITE, align 8) plus `STT_OBJECT` symbols into it. This is the honest answer to "where do WASM globals live on a backend that emits no startup and no linker script": the bytes ARE the initial values, shipped in the object; the linker places the section; code reaches it with `adrp`+`add :lo12:`. Contrast `x28` (the linear-memory base), which IS an embedder precondition — globals add no second one. RelocKind gains the three AArch64 kinds beyond CALL26: JUMP26 (282, the funcref-table `b func_N` trampolines), ADR_PREL_PG_HI21 (275) and ADD_ABS_LO12_NC (277) (the symbol-address pair). The builder's kind→type mapping has NO wildcard, and an unplaceable symbol now PANICS instead of silently dropping the relocation — an unrelocated `adrp #0` would address the wrong page (silent miscompile), where the old `continue` merely assumed it could not happen. `ElfFunction::is_object` types the `.text`-resident funcref table as OBJECT, not FUNC: it is branched INTO at slot+4, never called at slot+0. Byte-identity: an empty `DataBlob` reproduces the previous 5-section layout exactly (asserted by `empty_data_blob_is_byte_identical_to_the_data_free_builder`), so every globals-free module is unchanged. Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- crates/synth-backend-aarch64/src/backend.rs | 10 +- crates/synth-backend-aarch64/src/elf.rs | 411 +++++++++++++++++--- crates/synth-cli/src/main.rs | 37 +- crates/synth-core/src/backend.rs | 21 + 4 files changed, 398 insertions(+), 81 deletions(-) diff --git a/crates/synth-backend-aarch64/src/backend.rs b/crates/synth-backend-aarch64/src/backend.rs index 2b580526..67a1cb51 100644 --- a/crates/synth-backend-aarch64/src/backend.rs +++ b/crates/synth-backend-aarch64/src/backend.rs @@ -295,11 +295,11 @@ impl Backend for AArch64Backend { { aliases.push(exp.clone()); } - elf_funcs.push(ElfFunction { - symbols: aliases, - code: compiled.code.clone(), - relocations: compiled.relocations.clone(), - }); + elf_funcs.push(ElfFunction::code( + aliases, + compiled.code.clone(), + compiled.relocations.clone(), + )); functions.push(compiled); } diff --git a/crates/synth-backend-aarch64/src/elf.rs b/crates/synth-backend-aarch64/src/elf.rs index 18a0cf9c..1fc855aa 100644 --- a/crates/synth-backend-aarch64/src/elf.rs +++ b/crates/synth-backend-aarch64/src/elf.rs @@ -12,20 +12,63 @@ use synth_core::backend::{CodeRelocation, RelocKind}; -/// R_AARCH64_CALL26 — the ELF relocation type for a `bl`/`b` 26-bit call site. +/// R_AARCH64_CALL26 — the ELF relocation type for a `bl` 26-bit call site. const R_AARCH64_CALL26: u32 = 283; +/// R_AARCH64_JUMP26 — the same 26-bit field on a plain `b` (no link). Used by +/// the `call_indirect` funcref-table trampolines (#851 lane L3). +const R_AARCH64_JUMP26: u32 = 282; +/// R_AARCH64_ADR_PREL_PG_HI21 — the `adrp` half of a PC-relative symbol address. +const R_AARCH64_ADR_PREL_PG_HI21: u32 = 275; +/// R_AARCH64_ADD_ABS_LO12_NC — the `add …, :lo12:sym` half of the same pair. +const R_AARCH64_ADD_ABS_LO12_NC: u32 = 277; /// A compiled function to place in `.text`. pub struct ElfFunction { /// Symbol name aliases for this function's `.text` offset. The first is the /// canonical `func_N`; a distinct export name (if any) follows. All are - /// emitted as GLOBAL `STT_FUNC` symbols pointing at the same body. + /// emitted as GLOBAL symbols pointing at the same body. pub symbols: Vec, /// Function body machine code. pub code: Vec, /// Call relocations within this function's code (offsets are function-local; /// the builder rebases them to the `.text` offset). Empty for leaf functions. pub relocations: Vec, + /// #851 lane L3: this entry is DATA that happens to live in `.text` (the + /// `call_indirect` funcref table: `[u32 class-id][b func_N]` slot records). + /// Its symbols are emitted `STT_OBJECT` rather than `STT_FUNC` — the table + /// is branched INTO at slot+4, never called at slot+0, and typing it as a + /// function would misdescribe the object to any consumer. + pub is_object: bool, +} + +impl ElfFunction { + /// A normal code function (`STT_FUNC` symbols). + pub fn code(symbols: Vec, code: Vec, relocations: Vec) -> Self { + Self { + symbols, + code, + relocations, + is_object: false, + } + } +} + +/// #851 lane L3 — the synth-EMITTED `.data` image (the WASM globals region). +/// +/// PRECONDITION STATUS, stated plainly: there is NONE. Unlike the `x28` +/// linear-memory base (an ambient input the embedder supplies — see +/// `selector::LINMEM_BASE`), the globals region is emitted BY synth into this +/// section, carrying each global's decoded constant initializer, and reached +/// from code by an `adrp`+`add :lo12:` pair against [`Self::symbols`]. The +/// linker places it; no register convention, no startup, no linker script and +/// no second ambient input is required. +#[derive(Debug, Default, Clone)] +pub struct DataBlob { + /// The `.data` bytes (little-endian, already laid out). + pub bytes: Vec, + /// `(symbol name, byte offset within `.data`)` — e.g. + /// `("__synth_globals", 0)`. Emitted as GLOBAL `STT_OBJECT`. + pub symbols: Vec<(String, u64)>, } const EHDR_SIZE: usize = 64; @@ -45,7 +88,21 @@ fn push_u64(v: &mut Vec, x: u64) { /// Build an `EM_AARCH64` `ET_REL` object exposing each function's symbols as /// GLOBAL `STT_FUNC` in `.text`, plus a `.rela.text` for any call relocations. +/// Data-free shorthand for [`build_relocatable_object_with_data`] — a module +/// with no globals emits byte-identical output to the pre-lane-L3 builder. pub fn build_relocatable_object(functions: &[ElfFunction]) -> Vec { + build_relocatable_object_with_data(functions, &DataBlob::default()) +} + +/// Build an `EM_AARCH64` `ET_REL` object with an optional synth-emitted `.data` +/// section (#851 lane L3 — the WASM globals region, see [`DataBlob`]). +/// +/// Section indices: `[0]=NULL [1]=.text [2]=.symtab [3]=.strtab [4]=.shstrtab`, +/// then `.data` (when non-empty) and `.rela.text` (when non-empty) appended in +/// that order. An EMPTY `DataBlob` reproduces the previous layout exactly, so +/// every module without globals stays byte-identical (the frozen-anchor +/// contract). +pub fn build_relocatable_object_with_data(functions: &[ElfFunction], data: &DataBlob) -> Vec { // --- .text: concatenated bodies; record each function's .text offset. --- let mut text: Vec = Vec::new(); let mut func_off: Vec = Vec::new(); @@ -55,49 +112,89 @@ pub fn build_relocatable_object(functions: &[ElfFunction]) -> Vec { text.extend_from_slice(&f.code); } - // --- .strtab + .symtab: one GLOBAL STT_FUNC per (function, symbol-alias). --- - // st_info = (bind << 4) | type; GLOBAL=1, FUNC=2 → 0x12. shndx = 1 (.text). + let have_data = !data.bytes.is_empty(); + // Section indices. [0]=NULL [1]=.text [2]=.symtab [3]=.strtab [4]=.shstrtab; + // `.data` (when present) is 5 and `.rela.text` follows. Fixing `.data` BEFORE + // `.rela.text` keeps the data symbols' `st_shndx` independent of whether the + // module has relocations. + let idx_data: u16 = 5; + + // --- .strtab + .symtab: one GLOBAL symbol per (function, symbol-alias). --- + // st_info = (bind << 4) | type; GLOBAL=1, so FUNC(2) → 0x12 and OBJECT(1) → + // 0x11. shndx = 1 (.text) for code, `idx_data` for the `.data` symbols. // Also build a name → symbol-index map so relocations resolve by symbol name. let mut strtab: Vec = vec![0]; let mut symtab: Vec = Vec::new(); symtab.extend_from_slice(&[0u8; SYM_SIZE]); // null symbol at index 0 let mut sym_index: std::collections::HashMap = std::collections::HashMap::new(); let mut next_sym_idx: u32 = 1; - for (i, f) in functions.iter().enumerate() { - let off = func_off[i]; - let size = f.code.len() as u64; - for sym in &f.symbols { + let mut push_sym = + |name: &str, info: u8, shndx: u16, value: u64, size: u64, strtab: &mut Vec| { let name_off = strtab.len() as u32; - strtab.extend_from_slice(sym.as_bytes()); + strtab.extend_from_slice(name.as_bytes()); strtab.push(0); push_u32(&mut symtab, name_off); // st_name - symtab.push(0x12); // st_info: GLOBAL FUNC + symtab.push(info); // st_info symtab.push(0); // st_other - push_u16(&mut symtab, 1); // st_shndx = .text (section 1) - push_u64(&mut symtab, off); // st_value + push_u16(&mut symtab, shndx); // st_shndx + push_u64(&mut symtab, value); // st_value push_u64(&mut symtab, size); // st_size - sym_index.entry(sym.clone()).or_insert(next_sym_idx); + sym_index.entry(name.to_string()).or_insert(next_sym_idx); next_sym_idx += 1; + }; + for (i, f) in functions.iter().enumerate() { + let off = func_off[i]; + let size = f.code.len() as u64; + // #851 lane L3: the funcref table is DATA in `.text` — type it OBJECT so + // the object does not claim a branch-table blob is a callable function. + let info = if f.is_object { 0x11 } else { 0x12 }; + for sym in &f.symbols { + push_sym(sym, info, 1, off, size, &mut strtab); + } + } + // #851 lane L3: synth-emitted `.data` symbols (the globals region base). + if have_data { + for (name, off) in &data.symbols { + let size = data.bytes.len() as u64 - off.min(&(data.bytes.len() as u64)); + push_sym(name, 0x11, idx_data, *off, size, &mut strtab); } } - // --- .rela.text: one entry per call relocation (rebased to .text). --- + // --- .rela.text: one entry per code relocation (rebased to .text). --- // ELF64 packs r_info = (sym_index << 32) | type (sym in the HIGH word). let mut rela: Vec = Vec::new(); for (i, f) in functions.iter().enumerate() { for r in &f.relocations { - debug_assert!( - matches!(r.kind, RelocKind::AArch64Call26), - "aarch64 ELF builder only emits R_AARCH64_CALL26 relocations (#851)" - ); - let Some(&sidx) = sym_index.get(&r.symbol) else { - // A call to a symbol we did not place: leave it unrelocated. The - // selector only records calls to LOCAL functions (all placed), so - // this is defensive — a missing symbol would fail at link time. - continue; + // NO wildcard: a relocation kind this backend cannot express must + // fail loudly here rather than be silently dropped (which would ship + // an unrelocated `bl #0` / `adrp #0` — a branch-to-self or a wrong + // address, the silent-miscompile class). + let r_type = match r.kind { + RelocKind::AArch64Call26 => R_AARCH64_CALL26, + RelocKind::AArch64Jump26 => R_AARCH64_JUMP26, + RelocKind::AArch64AdrPrelPgHi21 => R_AARCH64_ADR_PREL_PG_HI21, + RelocKind::AArch64AddAbsLo12Nc => R_AARCH64_ADD_ABS_LO12_NC, + other => panic!( + "aarch64 ELF builder cannot emit relocation kind {other:?} \ + (#851): only the four AArch64 kinds are expressible" + ), }; + // A relocation against a symbol this object does not place is an + // INTERNAL BUG, and silently dropping it ships the unrelocated + // placeholder: `bl #0` branches to itself, `adrp #0` addresses the + // WRONG page (a silent miscompile, not a link error). Panic — the + // defensive-panic convention for backend invariants. + let sidx = *sym_index.get(&r.symbol).unwrap_or_else(|| { + panic!( + "aarch64 ELF builder: relocation at .text+{} targets symbol \ + '{}', which this object does not place — refusing to ship an \ + unrelocated placeholder (#851)", + func_off[i] + r.offset as u64, + r.symbol + ) + }); let r_offset = func_off[i] + r.offset as u64; - let r_info = ((sidx as u64) << 32) | (R_AARCH64_CALL26 as u64); + let r_info = ((sidx as u64) << 32) | (r_type as u64); push_u64(&mut rela, r_offset); push_u64(&mut rela, r_info); push_u64(&mut rela, 0); // r_addend = 0 @@ -124,38 +221,54 @@ pub fn build_relocatable_object(functions: &[ElfFunction]) -> Vec { let n_symtab = add_shstr(&mut shstrtab, ".symtab"); let n_strtab = add_shstr(&mut shstrtab, ".strtab"); let n_shstrtab = add_shstr(&mut shstrtab, ".shstrtab"); + let n_data = if have_data { + add_shstr(&mut shstrtab, ".data") + } else { + 0 + }; // --- Section indices. --- - // [0]=NULL [1]=.text [2]=.symtab [3]=.strtab [4]=.shstrtab, and when present - // .rela.text is appended as the LAST content section (index 5). Keeping + // [0]=NULL [1]=.text [2]=.symtab [3]=.strtab [4]=.shstrtab, then (when + // present) .data at 5 and .rela.text last. Keeping // .text=1/.symtab=2/.strtab=3/.shstrtab=4 stable preserves the milestone-1b - // layout for call-free modules (byte-identical) — the symtab st_shndx=1 and - // e_shstrndx=4 are unchanged. - // .symtab is section 2 (the .rela.text `sh_link`). .rela.text, when present, - // is section 5 (the last content section) — but the ELF section-header table - // is position-indexed, so we never need to name that index explicitly. + // layout for call-free, globals-free modules (byte-identical) — the symtab + // st_shndx=1 and e_shstrndx=4 are unchanged. + // .symtab is section 2 (the .rela.text `sh_link`). let idx_symtab = 2u32; - // --- Layout: ehdr | .text | .symtab | .strtab | .shstrtab | [.rela] | shdrs. --- + // --- Layout: ehdr | .text | .symtab | .strtab | .shstrtab | [.data] | + // [.rela] | shdrs. --- let text_off = EHDR_SIZE; let symtab_off = text_off + text.len(); let strtab_off = symtab_off + symtab.len(); let shstrtab_off = strtab_off + strtab.len(); - // 8-align .rela.text (SHT_RELA entries are 8-aligned). - let rela_off = { + // 8-align .data (an i64 global slot must land naturally aligned). + let data_off = { let base = shstrtab_off + shstrtab.len(); base.div_ceil(8) * 8 }; - let rela_pad = rela_off - (shstrtab_off + shstrtab.len()); + let data_pad = if have_data { + data_off - (shstrtab_off + shstrtab.len()) + } else { + 0 + }; + let after_data = if have_data { + data_off + data.bytes.len() + } else { + shstrtab_off + shstrtab.len() + }; + // 8-align .rela.text (SHT_RELA entries are 8-aligned). + let rela_off = after_data.div_ceil(8) * 8; + let rela_pad = rela_off - after_data; let after_content = if have_rela { rela_off + rela.len() } else { - shstrtab_off + shstrtab.len() + after_data }; // 8-align the section-header table. let shdr_off = after_content.div_ceil(8) * 8; let shdr_pad = shdr_off - after_content; - let num_sections: u16 = if have_rela { 6 } else { 5 }; + let num_sections: u16 = 5 + u16::from(have_data) + u16::from(have_rela); let mut out: Vec = Vec::new(); @@ -186,6 +299,10 @@ pub fn build_relocatable_object(functions: &[ElfFunction]) -> Vec { out.extend_from_slice(&symtab); out.extend_from_slice(&strtab); out.extend_from_slice(&shstrtab); + if have_data { + out.extend_from_slice(&vec![0u8; data_pad]); + out.extend_from_slice(&data.bytes); + } if have_rela { out.extend_from_slice(&vec![0u8; rela_pad]); out.extend_from_slice(&rela); @@ -227,7 +344,13 @@ pub fn build_relocatable_object(functions: &[ElfFunction]) -> Vec { shdr(n_strtab, 3, 0, strtab_off, strtab.len(), 0, 0, 1, 0); // [4] .shstrtab — STRTAB(3) shdr(n_shstrtab, 3, 0, shstrtab_off, shstrtab.len(), 0, 0, 1, 0); - // [5] .rela.text — RELA(4), link=.symtab(2), info=.text(1), align 8. Only + // [5] .data — PROGBITS(1), ALLOC|WRITE (0x2|0x1), align 8. The synth-emitted + // globals region (#851 lane L3): its bytes ARE the initial values, so no + // startup, no linker script and no base-register precondition is needed. + if have_data { + shdr(n_data, 1, 0x3, data_off, data.bytes.len(), 0, 0, 8, 0); + } + // [5|6] .rela.text — RELA(4), link=.symtab(2), info=.text(1), align 8. Only // emitted when there is at least one relocation. if have_rela { shdr( @@ -253,16 +376,16 @@ mod tests { #[test] fn well_formed_header_and_symbols() { let obj = build_relocatable_object(&[ - ElfFunction { - symbols: vec!["func_0".into(), "add".into()], - code: vec![0, 0, 1, 0x0B, 0xE0, 0x03, 9, 0x2A, 0xC0, 0x03, 0x5F, 0xD6], - relocations: vec![], - }, - ElfFunction { - symbols: vec!["func_1".into(), "sub".into()], - code: vec![0x62, 0, 4, 0x4B, 0xC0, 0x03, 0x5F, 0xD6], - relocations: vec![], - }, + ElfFunction::code( + vec!["func_0".into(), "add".into()], + vec![0, 0, 1, 0x0B, 0xE0, 0x03, 9, 0x2A, 0xC0, 0x03, 0x5F, 0xD6], + vec![], + ), + ElfFunction::code( + vec!["func_1".into(), "sub".into()], + vec![0x62, 0, 4, 0x4B, 0xC0, 0x03, 0x5F, 0xD6], + vec![], + ), ]); // ELF magic + class64 + LSB. assert_eq!(&obj[0..4], &[0x7F, b'E', b'L', b'F']); @@ -283,20 +406,16 @@ mod tests { fn call_reloc_produces_rela_text() { // A caller (func_1) with a `bl func_0` at byte offset 0. let obj = build_relocatable_object(&[ - ElfFunction { - symbols: vec!["func_0".into()], - code: vec![0xC0, 0x03, 0x5F, 0xD6], // ret - relocations: vec![], - }, - ElfFunction { - symbols: vec!["func_1".into(), "run".into()], - code: vec![0x00, 0x00, 0x00, 0x94, 0xC0, 0x03, 0x5F, 0xD6], // bl #0 ; ret - relocations: vec![CodeRelocation { + ElfFunction::code(vec!["func_0".into()], vec![0xC0, 0x03, 0x5F, 0xD6], vec![]), + ElfFunction::code( + vec!["func_1".into(), "run".into()], + vec![0x00, 0x00, 0x00, 0x94, 0xC0, 0x03, 0x5F, 0xD6], // bl #0 ; ret + vec![CodeRelocation { offset: 0, symbol: "func_0".into(), kind: RelocKind::AArch64Call26, }], - }, + ), ]); // e_shnum = 6 (adds .rela.text). assert_eq!(u16::from_le_bytes([obj[60], obj[61]]), 6); @@ -310,4 +429,180 @@ mod tests { // differential harness links + runs, the ultimate check). assert_eq!(R_AARCH64_CALL26, 283); } + + /// Minimal ELF64 section walk: `(name, sh_type, sh_flags, offset, size)`. + fn sections(obj: &[u8]) -> Vec<(String, u32, u64, usize, usize)> { + let rd_u16 = |o: usize| u16::from_le_bytes([obj[o], obj[o + 1]]) as usize; + let rd_u64 = |o: usize| u64::from_le_bytes(obj[o..o + 8].try_into().unwrap()); + let shoff = rd_u64(40) as usize; + let shnum = rd_u16(60); + let shstrndx = rd_u16(62); + let hdr = |i: usize| shoff + i * SHDR_SIZE; + let strtab_off = rd_u64(hdr(shstrndx) + 24) as usize; + (0..shnum) + .map(|i| { + let b = hdr(i); + let name_off = + strtab_off + u32::from_le_bytes(obj[b..b + 4].try_into().unwrap()) as usize; + let end = obj[name_off..].iter().position(|c| *c == 0).unwrap() + name_off; + ( + String::from_utf8_lossy(&obj[name_off..end]).into_owned(), + u32::from_le_bytes(obj[b + 4..b + 8].try_into().unwrap()), + rd_u64(b + 8), + rd_u64(b + 24) as usize, + rd_u64(b + 32) as usize, + ) + }) + .collect() + } + + /// #851 lane L3: a `DataBlob` produces a real ALLOC|WRITE `.data` section + /// holding EXACTLY the supplied bytes, plus a `STT_OBJECT` symbol pointing + /// into it. This is the substrate that makes globals precondition-free — + /// the initial values ship in the object. + #[test] + fn data_blob_emits_alloc_write_data_section_and_object_symbol() { + let blob = DataBlob { + bytes: vec![7, 0, 0, 0, 0, 0, 0, 0, 0xFF, 0xFF, 0, 0, 0, 0, 0, 0], + symbols: vec![("__synth_globals".into(), 0)], + }; + let obj = build_relocatable_object_with_data( + &[ElfFunction::code( + vec!["func_0".into(), "run".into()], + vec![0xC0, 0x03, 0x5F, 0xD6], + vec![], + )], + &blob, + ); + let secs = sections(&obj); + let data = secs + .iter() + .find(|s| s.0 == ".data") + .expect(".data section missing"); + assert_eq!(data.1, 1, ".data must be SHT_PROGBITS"); + assert_eq!(data.2, 0x3, ".data must be SHF_ALLOC|SHF_WRITE"); + assert_eq!(&obj[data.3..data.3 + data.4], &blob.bytes[..]); + // The `__synth_globals` symbol must be STT_OBJECT (0x11) in .data. + let symtab = secs.iter().find(|s| s.0 == ".symtab").unwrap(); + let strtab = secs.iter().find(|s| s.0 == ".strtab").unwrap(); + let data_idx = secs.iter().position(|s| s.0 == ".data").unwrap() as u16; + let mut found = false; + for i in 0..symtab.4 / SYM_SIZE { + let b = symtab.3 + i * SYM_SIZE; + let no = strtab.3 + u32::from_le_bytes(obj[b..b + 4].try_into().unwrap()) as usize; + let end = obj[no..].iter().position(|c| *c == 0).unwrap() + no; + if &obj[no..end] == b"__synth_globals" { + assert_eq!(obj[b + 4], 0x11, "globals symbol must be GLOBAL OBJECT"); + assert_eq!(u16::from_le_bytes([obj[b + 6], obj[b + 7]]), data_idx); + found = true; + } + } + assert!(found, "__synth_globals symbol not emitted"); + } + + /// A globals-free, call-free module must be BYTE-IDENTICAL to the + /// pre-lane-L3 builder — the frozen-anchor contract (an empty `DataBlob` + /// adds no section, no symbol, no padding). + #[test] + fn empty_data_blob_is_byte_identical_to_the_data_free_builder() { + let f = || { + vec![ElfFunction::code( + vec!["func_0".into(), "run".into()], + vec![0xC0, 0x03, 0x5F, 0xD6], + vec![], + )] + }; + assert_eq!( + build_relocatable_object(&f()), + build_relocatable_object_with_data(&f(), &DataBlob::default()) + ); + assert_eq!( + u16::from_le_bytes([ + build_relocatable_object(&f())[60], + build_relocatable_object(&f())[61] + ]), + 5, + "no .data / no .rela.text → the original 5-section layout" + ); + } + + /// #851 lane L3: the funcref-table trampoline blob is DATA in `.text` — + /// its symbol must be `STT_OBJECT`, and a `JUMP26` relocation must map to + /// ELF type 282 (not the 283 a `bl` uses). + #[test] + fn func_table_object_symbol_and_jump26_reloc_type() { + let obj = build_relocatable_object(&[ + ElfFunction::code(vec!["func_0".into()], vec![0xC0, 0x03, 0x5F, 0xD6], vec![]), + ElfFunction { + symbols: vec!["__synth_func_table".into()], + // slot 0: [class id 1][b func_0] + code: vec![1, 0, 0, 0, 0x00, 0x00, 0x00, 0x14], + relocations: vec![CodeRelocation { + offset: 4, + symbol: "func_0".into(), + kind: RelocKind::AArch64Jump26, + }], + is_object: true, + }, + ]); + let secs = sections(&obj); + let rela = secs.iter().find(|s| s.0 == ".rela.text").unwrap(); + let r_info = u64::from_le_bytes(obj[rela.3 + 8..rela.3 + 16].try_into().unwrap()); + assert_eq!( + (r_info & 0xFFFF_FFFF) as u32, + R_AARCH64_JUMP26, + "a trampoline `b func_N` must relocate as JUMP26 (282), not CALL26" + ); + let symtab = secs.iter().find(|s| s.0 == ".symtab").unwrap(); + let strtab = secs.iter().find(|s| s.0 == ".strtab").unwrap(); + let mut found = false; + for i in 0..symtab.4 / SYM_SIZE { + let b = symtab.3 + i * SYM_SIZE; + let no = strtab.3 + u32::from_le_bytes(obj[b..b + 4].try_into().unwrap()) as usize; + let end = obj[no..].iter().position(|c| *c == 0).unwrap() + no; + if &obj[no..end] == b"__synth_func_table" { + assert_eq!(obj[b + 4], 0x11, "table symbol must be GLOBAL OBJECT"); + found = true; + } + } + assert!(found, "__synth_func_table symbol not emitted"); + } + + /// The ADRP/ADD symbol-address pair maps to ELF types 275 / 277. + #[test] + fn adrp_add_pair_reloc_types() { + let obj = build_relocatable_object_with_data( + &[ElfFunction::code( + vec!["run".into()], + vec![0; 8], + vec![ + CodeRelocation { + offset: 0, + symbol: "__synth_globals".into(), + kind: RelocKind::AArch64AdrPrelPgHi21, + }, + CodeRelocation { + offset: 4, + symbol: "__synth_globals".into(), + kind: RelocKind::AArch64AddAbsLo12Nc, + }, + ], + )], + &DataBlob { + bytes: vec![0; 8], + symbols: vec![("__synth_globals".into(), 0)], + }, + ); + let secs = sections(&obj); + let rela = secs.iter().find(|s| s.0 == ".rela.text").unwrap(); + let ty = |i: usize| { + (u64::from_le_bytes( + obj[rela.3 + i * RELA_SIZE + 8..rela.3 + i * RELA_SIZE + 16] + .try_into() + .unwrap(), + ) & 0xFFFF_FFFF) as u32 + }; + assert_eq!(ty(0), R_AARCH64_ADR_PREL_PG_HI21); + assert_eq!(ty(1), R_AARCH64_ADD_ABS_LO12_NC); + } } diff --git a/crates/synth-cli/src/main.rs b/crates/synth-cli/src/main.rs index cd4f0416..b962ebd4 100644 --- a/crates/synth-cli/src/main.rs +++ b/crates/synth-cli/src/main.rs @@ -5259,13 +5259,18 @@ fn build_relocatable_elf( ); ArmRelocationType::Abs32 } - // #851: R_AARCH64_CALL26 is emitted only by the EM_AARCH64 backend - // (its own `.rela.text` builder). It can never reach this ARM ELF - // relocation path; bail loudly if it somehow does. - synth_core::backend::RelocKind::AArch64Call26 => { + // #851: the AArch64 relocations (CALL26 / JUMP26 / the + // ADRP+ADD symbol-address pair) are emitted only by the + // EM_AARCH64 backend (its own `.rela.text` builder). None can + // reach this ARM ELF relocation path; bail loudly if one does. + synth_core::backend::RelocKind::AArch64Call26 + | synth_core::backend::RelocKind::AArch64Jump26 + | synth_core::backend::RelocKind::AArch64AdrPrelPgHi21 + | synth_core::backend::RelocKind::AArch64AddAbsLo12Nc => { anyhow::bail!( - "internal error: AArch64 CALL26 relocation reached the ARM \ - ELF emitter — the aarch64 backend emits its own .rela.text (#851)" + "internal error: an AArch64 relocation ({:?}) reached the ARM \ + ELF emitter — the aarch64 backend emits its own .rela.text (#851)", + reloc.kind ) } // #871: R_RISCV_CALL_PLT is emitted only by the EM_RISCV backend @@ -6788,11 +6793,11 @@ fn build_multi_func_riscv_elf( /// (EM_ARM/ELF32) container. Mirrors `build_riscv_elf` — the per-backend ELF path. fn build_aarch64_elf(code: &[u8], func_name: &str) -> Result> { use synth_backend_aarch64::elf::{ElfFunction as A64ElfFunction, build_relocatable_object}; - Ok(build_relocatable_object(&[A64ElfFunction { - symbols: vec![func_name.to_string()], - code: code.to_vec(), - relocations: Vec::new(), - }])) + Ok(build_relocatable_object(&[A64ElfFunction::code( + vec![func_name.to_string()], + code.to_vec(), + Vec::new(), + )])) } /// #546: emit a multi-function `EM_AARCH64` ELF64 (`ET_REL`) object exposing one @@ -6811,13 +6816,9 @@ fn build_multi_func_aarch64_elf(funcs: &[ElfFunction]) -> Result> { if f.name != func_sym { symbols.push(f.name.clone()); } - A64ElfFunction { - symbols, - code: f.code.clone(), - // #851: forward the call relocations so `bl func_N` sites resolve - // via `.rela.text` (these were dropped pre-#851). - relocations: f.relocations.clone(), - } + // #851: forward the call relocations so `bl func_N` sites resolve + // via `.rela.text` (these were dropped pre-#851). + A64ElfFunction::code(symbols, f.code.clone(), f.relocations.clone()) }) .collect(); Ok(build_relocatable_object(&a64_funcs)) diff --git a/crates/synth-core/src/backend.rs b/crates/synth-core/src/backend.rs index 8aca149d..a477719b 100644 --- a/crates/synth-core/src/backend.rs +++ b/crates/synth-core/src/backend.rs @@ -540,6 +540,27 @@ pub enum RelocKind { /// word-offset immediate of the `bl` at `offset` to reach the target symbol. /// Emitted only by the `EM_AARCH64` backend's `.rela.text`. AArch64Call26, + /// R_AARCH64_JUMP26 (ELF type 282) — an AArch64 `B` (tail-branch) site + /// (#851 lane L3). Same 26-bit word-offset immediate as + /// [`RelocKind::AArch64Call26`], but for a branch that does NOT set `x30`: + /// the aarch64 `call_indirect` funcref table is a `.text`-resident array of + /// `b func_N` trampolines, so the dispatch's `blr` sets the return address + /// and the trampoline tail-branches into the callee (which returns straight + /// to the dispatcher). + AArch64Jump26, + /// R_AARCH64_ADR_PREL_PG_HI21 (ELF type 275) — the `adrp` half of a + /// PC-relative symbol address (#851 lane L3). Patches the 21-bit page delta + /// (`immlo`[30:29] + `immhi`[23:5]) so `adrp xd, sym` reaches the 4 KiB page + /// containing `sym`. Always paired with an + /// [`RelocKind::AArch64AddAbsLo12Nc`] on the next instruction. This pair is + /// how aarch64 reaches a synth-EMITTED region (the globals `.data` image, + /// the funcref table) with NO dedicated base register — so neither feature + /// adds an embedder precondition alongside `x28`. + AArch64AdrPrelPgHi21, + /// R_AARCH64_ADD_ABS_LO12_NC (ELF type 277) — the `add xd, xd, :lo12:sym` + /// half of a PC-relative symbol address (#851 lane L3). Patches the 12-bit + /// immediate field [21:10] with `(S + A) & 0xFFF`. + AArch64AddAbsLo12Nc, /// R_RISCV_CALL_PLT (ELF type 19) — a RISC-V `auipc`+`jalr` call pair /// (#871). The RV32 analogue of [`RelocKind::ThmCall`]: `offset` points at /// the `auipc` of an 8-byte `auipc ra, 0 ; jalr ra, 0(ra)` placeholder and From a7caca0f94fb4ed317057dc9938a6cefdc165f89 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 30 Jul 2026 14:54:46 +0200 Subject: [PATCH 3/9] core: structural type-class ids + per-type result counts for aarch64 dispatch (#851) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Three additions the aarch64 `call_indirect` + globals lowerings consume: * `DecodedModule::structural_type_class_ids()` — factored out of `call_indirect_guards`, which exposed the ids ONLY when its heterogeneous- table sidecar existed. The aarch64 dispatch type-checks UNCONDITIONALLY, so it needs them always. These are STRUCTURAL classes, not raw type indices: WASM type equality is structural, so `call_indirect (type 1)` must reach a function declared with a duplicate `type 0` (SS4.4.8) — comparing indices would trap where wasmtime calls. * `DecodedModule::funcref_region_class_ids()` — per-slot class id in the same contiguous order as `funcref_region_slots()`, 0 for null/unclassifiable. Storing this beside each slot makes ONE compare serve as both the SS4.4.8 type check and the null check (0 never equals a real class, which is >= 1). * `type_result_counts` on `DecodedModule` + `CompileConfig` — an indirect callee is known only by its static type, and `type_ret_i64/f32/f64` conflate void with i32, so the 0-vs-1 "is a value pushed back" distinction needs its own table. Plus `CompileConfig::a64_substrate_emitted`, FAIL-SAFE at `false`: the aarch64 selector will loud-decline globals and `call_indirect` unless the driver has actually emitted the `.data` globals image and the `.text` funcref table, so a driver that compiles bodies without emitting the regions cannot ship code addressing a symbol that is not there. Behavior unchanged: `call_indirect_guards` output is identical (pure refactor), and no consumer reads the new fields yet. Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- crates/synth-core/src/backend.rs | 19 +++++++ crates/synth-core/src/wasm_decoder.rs | 73 +++++++++++++++++++++++---- 2 files changed, 81 insertions(+), 11 deletions(-) diff --git a/crates/synth-core/src/backend.rs b/crates/synth-core/src/backend.rs index a477719b..33b7122b 100644 --- a/crates/synth-core/src/backend.rs +++ b/crates/synth-core/src/backend.rs @@ -396,6 +396,23 @@ pub struct CompileConfig { /// DECLINES every `call_indirect` lowering: an unchecked indirect branch /// is never emitted (WASM Core §4.4.8 requires OOB/type-mismatch traps). pub call_indirect_guards: crate::wasm_decoder::CallIndirectGuards, + /// #851 lane L3: result count per FUNCTION TYPE (see + /// [`crate::wasm_decoder::DecodedModule::type_result_counts`]). The aarch64 + /// `call_indirect` lowering needs the 0-vs-1 result distinction for a callee + /// it knows only by its static type. + pub type_result_counts: Vec, + /// #851 lane L3, aarch64 only — the driver has EMITTED the module-level + /// substrate the globals and `call_indirect` lowerings address: the `.data` + /// globals image (`__synth_globals`) and the `.text` funcref table + /// (`__synth_func_table`), both produced by + /// `synth_backend_aarch64::substrate::plan`. + /// + /// FAIL-SAFE BY DEFAULT (`false`): the aarch64 selector LOUD-DECLINES + /// `global.get`/`global.set`/`call_indirect` unless this is set, so a driver + /// that compiles function bodies but never emits the regions cannot ship + /// code addressing a symbol that does not exist. Set only on the two paths + /// that call `plan()` and place its output in the object. + pub a64_substrate_emitted: bool, } /// #543 — an integrator-marked volatile linear-memory segment (the DMA transfer @@ -495,6 +512,8 @@ impl Default for CompileConfig { // loudly (never an unchecked indirect branch). Driver loops fill // this from the decoded module. call_indirect_guards: crate::wasm_decoder::CallIndirectGuards::default(), + type_result_counts: Vec::new(), + a64_substrate_emitted: false, // #778 phase 2: no --wcet-hints file ⇒ no hints. Consulted ONLY by // the WCET sidecar computation — never by codegen (the emitted // bytes are byte-identical with or without hints). diff --git a/crates/synth-core/src/wasm_decoder.rs b/crates/synth-core/src/wasm_decoder.rs index 2de42b4b..8adfe356 100644 --- a/crates/synth-core/src/wasm_decoder.rs +++ b/crates/synth-core/src/wasm_decoder.rs @@ -406,6 +406,13 @@ pub struct DecodedModule { /// check, which must compare SIGNATURES, not raw type indices (a module /// may carry structurally-identical duplicate types). pub type_signatures: Vec, + /// #851 lane L3: result (return-value) count per FUNCTION TYPE, indexed by + /// type index — the `call_indirect` analogue of [`Self::func_result_counts`]. + /// An indirect call's callee is known only by its static type, so the + /// 0-vs-1 result distinction (does a value get pushed back?) has to come + /// from here; `type_ret_i64/f32/f64` carry the result TYPE but conflate + /// void with i32 (both all-false). + pub type_result_counts: Vec, /// VCR-PERF-002 Phase 1 (#494): proven invariants from loom's `wsc.facts` /// custom section, keyed by `(function index, value id)` — see /// `docs/design/wsc-facts-encoding.md` (schema v1) and @@ -418,6 +425,56 @@ pub struct DecodedModule { } impl DecodedModule { + /// #676/#851: the STRUCTURAL signature class of every function type — + /// structurally-equal types share one dense 1-based id (first-occurrence + /// order over the type section); id 0 is reserved for "null slot / not + /// statically classifiable" and therefore never equals a real class. + /// + /// This is the id a `call_indirect` type check must compare, NOT the raw + /// type index: WASM type equality is STRUCTURAL, so a module carrying two + /// identical `(param i32) (result i32)` entries must let `call_indirect + /// (type 1)` reach a function declared with type 0 (§4.4.8). Comparing + /// indices would trap where wasmtime calls. + /// + /// [`CallIndirectGuards::type_class_ids`] exposes this only when the ARM + /// heterogeneous-table sidecar exists; the aarch64 dispatch type-checks + /// UNCONDITIONALLY, so it reads the ids from here. + pub fn structural_type_class_ids(&self) -> Vec { + let mut class_of_sig: std::collections::HashMap<&str, u32> = + std::collections::HashMap::new(); + let mut ids: Vec = Vec::with_capacity(self.type_signatures.len()); + for sig in &self.type_signatures { + let next = class_of_sig.len() as u32 + 1; + ids.push(*class_of_sig.entry(sig.as_str()).or_insert(next)); + } + ids + } + + /// #851 lane L3: the structural class id of every funcref-region slot, in + /// the SAME contiguous order as [`Self::funcref_region_slots`] — 0 for a + /// null slot, for a slot whose function has no known type, and for a table + /// whose image is not statically verifiable (all of which + /// `funcref_region_slots` already reports as `None`). + /// + /// The aarch64 funcref table stores this id beside each slot's branch + /// trampoline, so the dispatch's `cmp` against the expected class id is + /// simultaneously the §4.4.8 TYPE check and the NULL check (id 0 matches + /// no expected class, which is >= 1). + pub fn funcref_region_class_ids(&self) -> Vec { + let class = self.structural_type_class_ids(); + self.funcref_region_slots() + .iter() + .map(|slot| match slot { + None => 0, + Some(f) => self + .func_type_indices + .get(*f as usize) + .and_then(|&t| class.get(t as usize).copied()) + .unwrap_or(0), + }) + .collect() + } + /// #642/#650: compute the `call_indirect` guard inputs — per table, the /// compile-time size for the runtime bounds check, the base byte offset /// within the contiguous R11 region, and the per-expected-type @@ -442,17 +499,10 @@ impl DecodedModule { entry)", ); - // #676: structural signature classes — structurally-equal types share - // one dense 1-based id (first-occurrence order over the type section); - // id 0 is reserved for null slots. These feed the type-id sidecar and - // the expected-type compare immediate of the runtime type check. - let mut class_of_sig: std::collections::HashMap<&str, u32> = - std::collections::HashMap::new(); - let mut type_class_ids: Vec = Vec::with_capacity(n_types); - for sig in &self.type_signatures { - let next = class_of_sig.len() as u32 + 1; - type_class_ids.push(*class_of_sig.entry(sig.as_str()).or_insert(next)); - } + // #676: structural signature classes — see + // [`Self::structural_type_class_ids`]. These feed the type-id sidecar + // and the expected-type compare immediate of the runtime type check. + let type_class_ids = self.structural_type_class_ids(); let mut tables = Vec::with_capacity(self.table_sizes.len()); // #676: per table, the slot class ids (None = image not statically @@ -1350,6 +1400,7 @@ pub fn decode_wasm_module(wasm_bytes: &[u8]) -> Result { }) .collect(), func_type_indices, + type_result_counts: type_block_arity.iter().map(|&(_p, r)| r as u32).collect(), type_signatures, wsc_facts: wsc_facts.unwrap_or_default(), }) From eea007bf5215185488b289773f2c9b4b85c4013c Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 30 Jul 2026 14:57:30 +0200 Subject: [PATCH 4/9] =?UTF-8?q?aarch64:=20substrate=20planner=20=E2=80=94?= =?UTF-8?q?=20the=20one=20source=20of=20both=20emitted=20regions=20(#851)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `substrate::plan` materializes the globals `.data` image and the `.text` funcref table from decoded module state, and is called by BOTH aarch64 ELF drivers, so the regions the code addresses and the regions the object ships cannot disagree. PRECONDITION STATUS, stated plainly: neither region is one. Both are EMITTED BY SYNTH and reached with `adrp` + `add :lo12:` against a symbol the same object defines. That is deliberately unlike `x28` (the linear-memory base), which IS an embedder precondition — v0.53 made that explicit so the next feature would not quietly add a second, and this one does not. Using PC-relative addressing instead of a dedicated base register also sidesteps the #275/#717 collision class outright: there is no base register to collide with. Layouts. Globals: ONE 8-BYTE SLOT PER GLOBAL at `k*8` (NOT the ARM/#643 dense width-summed layout) — uniform slots stay naturally aligned for `ldr x`, where a dense layout puts an i64 at offset 4, and the offset stays a foldable constant. Funcref table: 8 bytes per slot, `[u32 structural class id][b func_N]`, null slots `[0][brk #0]`. Every unrepresentable shape LOUD-DECLINES with a machine reason rather than guessing (9 unit tests, decline text asserted): imported globals (value arrives at instantiation), a global with no decoded const initializer (float/v128/non-const expr), >2048 globals or a v128 slot, an unsized (growable imported) table, >4095 slots or class ids past the 12-bit guard immediates, and a table slot holding an imported function. The load-bearing one: an UNVERIFIABLE element segment declines instead of shipping a table. `funcref_region_slots` degrades such a table to all-null, which traps on every dispatch — that LOOKS conservative but is wrong in the other direction, trapping where wasmtime calls successfully. Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- crates/synth-backend-aarch64/src/elf.rs | 1 + crates/synth-backend-aarch64/src/lib.rs | 1 + crates/synth-backend-aarch64/src/substrate.rs | 593 ++++++++++++++++++ 3 files changed, 595 insertions(+) create mode 100644 crates/synth-backend-aarch64/src/substrate.rs diff --git a/crates/synth-backend-aarch64/src/elf.rs b/crates/synth-backend-aarch64/src/elf.rs index 1fc855aa..ec991a63 100644 --- a/crates/synth-backend-aarch64/src/elf.rs +++ b/crates/synth-backend-aarch64/src/elf.rs @@ -23,6 +23,7 @@ const R_AARCH64_ADR_PREL_PG_HI21: u32 = 275; const R_AARCH64_ADD_ABS_LO12_NC: u32 = 277; /// A compiled function to place in `.text`. +#[derive(Debug, Clone)] pub struct ElfFunction { /// Symbol name aliases for this function's `.text` offset. The first is the /// canonical `func_N`; a distinct export name (if any) follows. All are diff --git a/crates/synth-backend-aarch64/src/lib.rs b/crates/synth-backend-aarch64/src/lib.rs index 6e14e33f..013e7bc9 100644 --- a/crates/synth-backend-aarch64/src/lib.rs +++ b/crates/synth-backend-aarch64/src/lib.rs @@ -46,6 +46,7 @@ pub mod backend; pub mod elf; pub mod encoder; pub mod selector; +pub mod substrate; pub use backend::AArch64Backend; pub use selector::{SelectError, select}; diff --git a/crates/synth-backend-aarch64/src/substrate.rs b/crates/synth-backend-aarch64/src/substrate.rs new file mode 100644 index 00000000..094cd943 --- /dev/null +++ b/crates/synth-backend-aarch64/src/substrate.rs @@ -0,0 +1,593 @@ +//! #851 lane L3 — the aarch64 MODULE-LEVEL substrate: the WASM globals region +//! and the `call_indirect` funcref table. +//! +//! # Precondition status (stated plainly) +//! +//! Neither region is a precondition. Both are EMITTED BY SYNTH into the object +//! and reached with an `adrp` + `add :lo12:` pair against a symbol the same +//! object defines, so the linker places them and no register convention, no +//! startup, no linker script and no ambient input is required. +//! +//! This is deliberately DIFFERENT from `x28` (the linear-memory base, see +//! [`crate::selector`]'s `LINMEM_BASE`), which IS a precondition the embedder +//! supplies: synth emits nothing that establishes it. Lane L3 adds NO second +//! precondition — v0.53 made the `x28` one explicit precisely so that the next +//! feature would not quietly add another. +//! +//! # Why PC-relative and not a base register +//! +//! The ARM backend reaches its globals through R9 and its funcref table through +//! a literal-pool word, because a Cortex-M image has no linker to consult. The +//! aarch64 backend emits `ET_REL` and is always host-linked, so `adrp`+`add` +//! costs the same two instructions and needs no ambient register — which also +//! sidesteps the #275/#717 class outright: there is no base register to collide +//! with the linear-memory base. +//! +//! # Layouts +//! +//! **Globals (`__synth_globals`, in `.data`)** — ONE 8-BYTE SLOT PER GLOBAL, +//! `global k` at byte offset `k * 8`, regardless of declared width. An i32/f32 +//! global occupies the low 4 bytes (read back through the `w` view) and an +//! i64/f64 global the full 8. This is NOT the ARM/#643 dense width-summed +//! layout: uniform 8-byte slots keep every slot naturally aligned for `ldr x` +//! (a dense layout puts an i64 at offset 4) and make the slot offset a constant +//! `k * 8` the selector can fold into the load/store immediate. Nothing outside +//! this backend reads the region, so the layouts need not agree. +//! +//! **Funcref table (`__synth_func_table`, in `.text`)** — ONE 8-BYTE SLOT PER +//! TABLE ENTRY across all tables in declaration order (the same contiguous +//! region order `DecodedModule::funcref_region_slots` describes), each: +//! +//! ```text +//! +0 u32 structural class id of the slot's function (0 = null slot) +//! +4 insn `b func_N` (an R_AARCH64_JUMP26 site) — or `brk #0` when null +//! ``` +//! +//! The class-id word is DATA that lives in `.text`; it is never executed +//! (the dispatch branches to slot+4, never slot+0). A slot's trampoline is a +//! TAIL branch, so the dispatcher's `blr` sets `x30` and the callee returns +//! straight to the dispatcher. + +use synth_core::backend::{CodeRelocation, FUNC_TABLE_SYMBOL, RelocKind}; +use synth_core::wasm_decoder::{DecodedModule, GlobalInit, WasmGlobal}; + +use crate::elf::{DataBlob, ElfFunction}; +use crate::encoder as enc; + +/// The `.data` symbol naming the base of the emitted globals region. +pub const GLOBALS_SYMBOL: &str = "__synth_globals"; + +/// Bytes per emitted global slot — see the module docs (uniform, not dense). +pub const GLOBAL_SLOT_BYTES: u32 = 8; + +/// Bytes per emitted funcref-table slot: `[u32 class id][b func_N]`. +pub const TABLE_SLOT_BYTES: u32 = 8; + +/// The largest global index this lowering can address. `global.get` of an i32 +/// global emits `ldr w, [xT, #k*8]`, whose SCALED 12-bit immediate is `k*2`, so +/// `k*2` must stay below 4096. +pub const MAX_GLOBALS: usize = 2048; + +/// The largest table this lowering can bounds-check: the out-of-range guard is +/// `cmp w_idx, #size`, an unsigned 12-bit immediate. +pub const MAX_TABLE_SLOTS: usize = 4095; + +/// The largest structural class id the type check can compare: `cmp w, #id`. +pub const MAX_CLASS_ID: u32 = 4095; + +/// What the two aarch64 drivers must place in the object for the globals and +/// `call_indirect` lowerings to be sound. +#[derive(Debug, Default, Clone)] +pub struct Substrate { + /// The `.data` image — empty when the module uses no globals. + pub globals: DataBlob, + /// The `.text`-resident funcref table (an `is_object` [`ElfFunction`] to be + /// appended LAST, so real functions keep their `.text` offsets) — `None` + /// when the module performs no `call_indirect`. + pub table: Option, + /// True when at least one region was emitted, i.e. when the selector may be + /// told `a64_substrate_emitted`. A module using neither feature plans an + /// EMPTY substrate and stays byte-identical. + pub emitted: bool, +} + +/// Everything [`plan`] needs, so both drivers (the `Backend::compile_module` +/// path and the CLI's own multi-function ELF path) can call it from whatever +/// module state they hold. +#[derive(Debug, Clone, Copy)] +pub struct PlanInputs<'a> { + /// Defined globals with their decoded constant initializers. + pub globals: &'a [WasmGlobal], + /// How many globals the module IMPORTS (their values arrive at + /// instantiation, which this backend cannot perform). + pub imported_globals: u32, + /// Does any compiled function execute `global.get`/`global.set`? + pub uses_globals: bool, + /// The contiguous funcref-region image (`DecodedModule::funcref_region_slots`). + pub funcref_slots: &'a [Option], + /// The matching per-slot structural class ids + /// (`DecodedModule::funcref_region_class_ids`). + pub funcref_class_ids: &'a [u32], + /// Per-table compile-time sizes (`DecodedModule::table_sizes`). + pub table_sizes: &'a [Option], + /// Element segments, for the statically-verifiable-image check. + pub elem_segments: &'a [synth_core::wasm_decoder::ElemSegmentInfo], + /// Number of imported functions — a table slot pointing at one has no + /// `func_N` body in this object. + pub num_imported_funcs: u32, + /// Does any compiled function execute `call_indirect`? + pub uses_call_indirect: bool, +} + +impl<'a> PlanInputs<'a> { + /// Derive the inputs from a whole decoded module plus the two usage flags + /// (which the driver computes from the op streams it is about to compile). + pub fn from_module( + module: &'a DecodedModule, + slots: &'a [Option], + class_ids: &'a [u32], + uses_globals: bool, + uses_call_indirect: bool, + ) -> Self { + Self { + globals: &module.globals, + imported_globals: module + .imports + .iter() + .filter(|i| matches!(i.kind, synth_core::ImportKind::Global)) + .count() as u32, + uses_globals, + funcref_slots: slots, + funcref_class_ids: class_ids, + table_sizes: &module.table_sizes, + elem_segments: &module.elem_segments, + num_imported_funcs: module.num_imported_funcs, + uses_call_indirect, + } + } +} + +/// Plan (and materialize) the module-level substrate. +/// +/// Every `Err` is a LOUD DECLINE with a machine-readable reason — the compile +/// fails rather than shipping a region whose contents synth cannot vouch for. +/// The two features are planned INDEPENDENTLY: a module that uses only globals +/// never touches the table checks and vice versa. +pub fn plan(input: PlanInputs<'_>) -> Result { + let globals = if input.uses_globals { + plan_globals(&input)? + } else { + DataBlob::default() + }; + let table = if input.uses_call_indirect { + Some(plan_table(&input)?) + } else { + None + }; + Ok(Substrate { + emitted: !globals.bytes.is_empty() || table.is_some(), + globals, + table, + }) +} + +/// Build the `.data` globals image, or decline. +fn plan_globals(input: &PlanInputs<'_>) -> Result { + // An IMPORTED global's value is supplied by the host at instantiation. + // This backend emits no instantiation step, so its slot would ship whatever + // synth guessed — the silent-wrong-initial-value class. Decline. + if input.imported_globals > 0 { + return Err(format!( + "module imports {} global(s), whose values are supplied at \ + instantiation — the aarch64 backend emits no instantiation step, so \ + the emitted region would ship a fabricated initial value; \ + loud-declining (#851)", + input.imported_globals + )); + } + if input.globals.is_empty() { + return Err( + "function executes global.get/global.set but the module declares no \ + globals — refusing to address an empty region (#851)" + .into(), + ); + } + if input.globals.len() > MAX_GLOBALS { + return Err(format!( + "module declares {} globals; the aarch64 lowering addresses at most \ + {MAX_GLOBALS} (a `ldr w, [base, #k*8]` scaled 12-bit immediate); \ + loud-declining (#851)", + input.globals.len() + )); + } + + let mut bytes = vec![0u8; input.globals.len() * GLOBAL_SLOT_BYTES as usize]; + for (k, g) in input.globals.iter().enumerate() { + // A global whose declared type is not i32/i64 (f32/f64/v128), or whose + // initializer is not a plain const, decodes to `init: None`. Shipping a + // zero there is exactly the #757/#798 "region reads the wrong bytes" + // class — decline instead. + let off = k * GLOBAL_SLOT_BYTES as usize; + match g.init { + Some(GlobalInit::I32(v)) => { + bytes[off..off + 4].copy_from_slice(&(v as u32).to_le_bytes()); + } + Some(GlobalInit::I64(v)) => { + bytes[off..off + 8].copy_from_slice(&(v as u64).to_le_bytes()); + } + None => { + return Err(format!( + "global {k} has no decoded constant initializer (a float, \ + v128, or non-const init expression) — the emitted region \ + would ship a WRONG initial value; loud-declining (#851)" + )); + } + } + if g.slot_bytes > GLOBAL_SLOT_BYTES { + return Err(format!( + "global {k} declares a {}-byte value type (v128); the aarch64 \ + globals region uses {GLOBAL_SLOT_BYTES}-byte slots; \ + loud-declining (#851)", + g.slot_bytes + )); + } + } + Ok(DataBlob { + bytes, + symbols: vec![(GLOBALS_SYMBOL.to_string(), 0)], + }) +} + +/// Build the `.text` funcref-table trampoline blob, or decline. +fn plan_table(input: &PlanInputs<'_>) -> Result { + // 1. Every table must have a compile-time size, or its slots have no + // constant base offset within the region (and no sound bounds check). + if input.table_sizes.is_empty() { + return Err( + "function executes call_indirect but the module declares no table — \ + loud-declining (#851)" + .into(), + ); + } + for (n, size) in input.table_sizes.iter().enumerate() { + if size.is_none() { + return Err(format!( + "table {n} has no compile-time size (an imported table whose \ + limits do not pin it); neither its bounds check nor any later \ + table's base offset is a constant — loud-declining (#851)" + )); + } + } + + // 2. The table IMAGE must be statically verifiable. `funcref_region_slots` + // reports an unverifiable table as all-null, which would make EVERY + // dispatch trap — sound-looking but WRONG in the other direction (it + // traps where wasmtime calls). Detect and decline instead of shipping a + // silently-always-trapping table. + for (i, seg) in input.elem_segments.iter().enumerate() { + let (Some(off), Some(funcs)) = (seg.offset, seg.funcs.as_ref()) else { + return Err(format!( + "element segment {i} is not statically verifiable (passive or \ + declared segment, non-constant offset, or a non-`ref.func` \ + entry) — the emitted table would trap on entries wasm calls \ + successfully; loud-declining (#851)" + )); + }; + let size = input + .table_sizes + .get(seg.table_index as usize) + .copied() + .flatten() + .ok_or_else(|| { + format!( + "element segment {i} targets table {} which the module does \ + not declare — loud-declining (#851)", + seg.table_index + ) + })?; + if off as u64 + funcs.len() as u64 > size as u64 { + return Err(format!( + "element segment {i} writes {} entries at offset {off} of table \ + {} (size {size}) — out of range; loud-declining (#851)", + funcs.len(), + seg.table_index + )); + } + } + + // 3. Size + class-id immediates must fit the guard encodings. + let slots = input.funcref_slots; + if slots.len() > MAX_TABLE_SLOTS { + return Err(format!( + "funcref region holds {} slots; the out-of-range guard compares \ + against an unsigned 12-bit immediate (at most {MAX_TABLE_SLOTS}) — \ + loud-declining (#851)", + slots.len() + )); + } + if slots.len() != input.funcref_class_ids.len() { + return Err(format!( + "internal: funcref slot/class-id lengths disagree ({} vs {}) — \ + loud-declining (#851)", + slots.len(), + input.funcref_class_ids.len() + )); + } + if let Some(bad) = input.funcref_class_ids.iter().find(|c| **c > MAX_CLASS_ID) { + return Err(format!( + "module carries structural type class id {bad}; the type check \ + compares against an unsigned 12-bit immediate (at most \ + {MAX_CLASS_ID}) — loud-declining (#851)" + )); + } + + // 4. Emit the trampolines. + let mut code: Vec = Vec::with_capacity(slots.len() * TABLE_SLOT_BYTES as usize); + let mut relocations: Vec = Vec::new(); + for (s, slot) in slots.iter().enumerate() { + let class = input.funcref_class_ids[s]; + code.extend_from_slice(&class.to_le_bytes()); + match slot { + Some(f) => { + // A slot pointing at an IMPORTED function has no `func_N` body + // in this object; import dispatch is declined on this backend, + // so a `b func_N` would relocate against a symbol we never + // place (and the ELF builder now panics rather than drop it). + if *f < input.num_imported_funcs { + return Err(format!( + "table slot {s} holds imported function {f}; import \ + dispatch is not supported on aarch64, so the table \ + cannot carry a trampoline to it — loud-declining (#851)" + )); + } + relocations.push(CodeRelocation { + offset: (s as u32 * TABLE_SLOT_BYTES) + 4, + symbol: format!("func_{f}"), + kind: RelocKind::AArch64Jump26, + }); + // `b #0` placeholder — the JUMP26 relocation supplies the imm26. + code.extend_from_slice(&enc::b_uncond(0).to_le_bytes()); + } + // A NULL slot: calling it must trap (WASM §4.4.8 "uninitialized + // element"). Its class id is 0, which never equals an expected + // class (>= 1), so the dispatch's type check traps FIRST; the `brk` + // is the belt-and-braces second line of defence. + None => code.extend_from_slice(&enc::brk(0).to_le_bytes()), + } + } + Ok(ElfFunction { + symbols: vec![FUNC_TABLE_SYMBOL.to_string()], + code, + relocations, + is_object: true, + }) +} + +#[cfg(test)] +mod tests { + use super::*; + use synth_core::wasm_decoder::ElemSegmentInfo; + + fn g(index: u32, init: Option, slot_bytes: u32) -> WasmGlobal { + WasmGlobal { + index, + init, + mutable: true, + slot_bytes, + } + } + + fn base<'a>() -> PlanInputs<'a> { + PlanInputs { + globals: &[], + imported_globals: 0, + uses_globals: false, + funcref_slots: &[], + funcref_class_ids: &[], + table_sizes: &[], + elem_segments: &[], + num_imported_funcs: 0, + uses_call_indirect: false, + } + } + + /// A module using neither feature plans an EMPTY substrate — no `.data`, no + /// table, `emitted == false` (so the selector keeps declining and every + /// existing module's bytes are untouched). + #[test] + fn unused_features_plan_an_empty_substrate() { + let s = plan(base()).unwrap(); + assert!(s.globals.bytes.is_empty()); + assert!(s.table.is_none()); + assert!(!s.emitted); + } + + /// The globals image carries the DECODED initial values at uniform 8-byte + /// slots — an i32 in the low word, an i64 across both. + #[test] + fn globals_image_holds_initial_values_at_eight_byte_slots() { + let gs = [ + g(0, Some(GlobalInit::I32(7)), 4), + g(1, Some(GlobalInit::I64(-2)), 8), + g(2, Some(GlobalInit::I32(-1)), 4), + ]; + let s = plan(PlanInputs { + globals: &gs, + uses_globals: true, + ..base() + }) + .unwrap(); + assert_eq!(s.globals.bytes.len(), 24); + assert_eq!(&s.globals.bytes[0..8], &7u64.to_le_bytes()); + assert_eq!(&s.globals.bytes[8..16], &(-2i64 as u64).to_le_bytes()); + // i32 -1 fills the LOW word only; the upper word stays zero. + assert_eq!( + &s.globals.bytes[16..24], + &[0xFF, 0xFF, 0xFF, 0xFF, 0, 0, 0, 0] + ); + assert_eq!(s.globals.symbols, vec![(GLOBALS_SYMBOL.to_string(), 0)]); + assert!(s.emitted); + } + + /// A global with no decoded constant initializer (float / non-const expr) + /// must DECLINE — shipping a zero there is the wrong-initial-value class. + #[test] + fn global_without_const_initializer_declines() { + let gs = [g(0, Some(GlobalInit::I32(1)), 4), g(1, None, 4)]; + let e = plan(PlanInputs { + globals: &gs, + uses_globals: true, + ..base() + }) + .unwrap_err(); + assert!(e.contains("global 1"), "{e}"); + assert!(e.contains("no decoded constant initializer"), "{e}"); + } + + /// An IMPORTED global declines: its value arrives at instantiation. + #[test] + fn imported_global_declines() { + let gs = [g(0, Some(GlobalInit::I32(1)), 4)]; + let e = plan(PlanInputs { + globals: &gs, + imported_globals: 1, + uses_globals: true, + ..base() + }) + .unwrap_err(); + assert!(e.contains("imports 1 global"), "{e}"); + } + + /// The table blob is `[u32 class][b func_N]` per slot, with a JUMP26 + /// relocation at slot+4 for every INITIALIZED slot and a `brk #0` (no + /// relocation) for every null one. + #[test] + fn table_blob_layout_and_null_slot_traps() { + let slots = [Some(0u32), None, Some(1u32)]; + let ids = [1u32, 0, 2]; + let sizes = [Some(3u32)]; + let segs = [ElemSegmentInfo { + table_index: 0, + offset: Some(0), + funcs: Some(vec![0, 9, 1]), + }]; + let s = plan(PlanInputs { + funcref_slots: &slots, + funcref_class_ids: &ids, + table_sizes: &sizes, + elem_segments: &segs, + uses_call_indirect: true, + ..base() + }) + .unwrap(); + let t = s.table.unwrap(); + assert!(t.is_object, "the table is DATA in .text, not a function"); + assert_eq!(t.symbols, vec![FUNC_TABLE_SYMBOL.to_string()]); + assert_eq!(t.code.len(), 24); + assert_eq!(&t.code[0..4], &1u32.to_le_bytes()); + assert_eq!(&t.code[4..8], &enc::b_uncond(0).to_le_bytes()); + // Null slot: class id 0 + an in-slot trap, and NO relocation. + assert_eq!(&t.code[8..12], &0u32.to_le_bytes()); + assert_eq!(&t.code[12..16], &enc::brk(0).to_le_bytes()); + assert_eq!(&t.code[16..20], &2u32.to_le_bytes()); + assert_eq!(t.relocations.len(), 2); + assert_eq!(t.relocations[0].offset, 4); + assert_eq!(t.relocations[0].symbol, "func_0"); + assert_eq!(t.relocations[1].offset, 20); + assert_eq!(t.relocations[1].symbol, "func_1"); + assert!( + t.relocations + .iter() + .all(|r| matches!(r.kind, RelocKind::AArch64Jump26)) + ); + } + + /// An UNVERIFIABLE element segment must DECLINE, not ship an all-null table. + /// `funcref_region_slots` degrades such a table to all-null, which would + /// trap on every dispatch — sound-LOOKING but wrong in the other direction + /// (wasmtime calls those entries successfully). + #[test] + fn unverifiable_element_segment_declines_rather_than_shipping_a_trap_table() { + let slots = [None, None]; + let ids = [0u32, 0]; + let sizes = [Some(2u32)]; + // A passive/non-const segment: offset is None. + let segs = [ElemSegmentInfo { + table_index: 0, + offset: None, + funcs: Some(vec![0, 1]), + }]; + let e = plan(PlanInputs { + funcref_slots: &slots, + funcref_class_ids: &ids, + table_sizes: &sizes, + elem_segments: &segs, + uses_call_indirect: true, + ..base() + }) + .unwrap_err(); + assert!(e.contains("not statically verifiable"), "{e}"); + assert!(e.contains("trap on entries wasm calls successfully"), "{e}"); + } + + /// A table of unknown compile-time size (a growable imported table) has no + /// sound bounds check and no constant base — decline. + #[test] + fn unsized_table_declines() { + let e = plan(PlanInputs { + table_sizes: &[None], + uses_call_indirect: true, + ..base() + }) + .unwrap_err(); + assert!(e.contains("no compile-time size"), "{e}"); + } + + /// A slot holding an IMPORTED function declines: this object places no + /// `func_N` body for it, so the trampoline could not be relocated. + #[test] + fn table_slot_holding_an_import_declines() { + let slots = [Some(0u32)]; + let ids = [1u32]; + let sizes = [Some(1u32)]; + let segs = [ElemSegmentInfo { + table_index: 0, + offset: Some(0), + funcs: Some(vec![0]), + }]; + let e = plan(PlanInputs { + funcref_slots: &slots, + funcref_class_ids: &ids, + table_sizes: &sizes, + elem_segments: &segs, + num_imported_funcs: 1, + uses_call_indirect: true, + ..base() + }) + .unwrap_err(); + assert!(e.contains("imported function 0"), "{e}"); + } + + /// A table larger than the 12-bit bounds-guard immediate declines. + #[test] + fn oversized_table_declines() { + let slots = vec![Some(0u32); MAX_TABLE_SLOTS + 1]; + let ids = vec![1u32; MAX_TABLE_SLOTS + 1]; + let sizes = [Some(slots.len() as u32)]; + let segs = [ElemSegmentInfo { + table_index: 0, + offset: Some(0), + funcs: Some(vec![0; slots.len()]), + }]; + let e = plan(PlanInputs { + funcref_slots: &slots, + funcref_class_ids: &ids, + table_sizes: &sizes, + elem_segments: &segs, + uses_call_indirect: true, + ..base() + }) + .unwrap_err(); + assert!(e.contains("unsigned 12-bit immediate"), "{e}"); + } +} From de9d1087fe49f0fae2fcbe7100e2ab68dcfb6382 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 30 Jul 2026 15:14:12 +0200 Subject: [PATCH 5/9] aarch64: globals + call_indirect LOWER, with param homing (#851) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Three parity-gate entries flip Err(reason) -> lowering in this commit, so no gap claim outlives its gap: `global.get`, `global.set` (ledger entries deleted) and `call_indirect` (`a64_extended_surface` -> `Ok(())`). GLOBALS. `global k` lives at `__synth_globals + k*8` in the `.data` image synth EMITS; the address is formed `adrp`+`add :lo12:`. i32/f32 use the low word of the slot, i64/f64 the whole slot, and the size-scaled load/store immediate folds the offset. PRECONDITION STATUS: none. Unlike `x28` (the linear-memory base, which IS an embedder precondition), synth ships the region and its initial values; the linker places it. No base register, so nothing can collide with the linear-memory base the way #275/#717 did on ARM. CALL_INDIRECT. All three §4.4.8 traps are emitted, none inherited from `blr`: cmp w_idx,#size / b.lo +2 / brk out-of-range index adrp+add / add x16,x16,w_idx,uxtw#3 slot address (no base register) ldr w17,[x16] / cmp w17,#expected signature mismatch — and, because a b.eq +2 / brk null slot's class id is 0 and every real class is >=1, the null check too add x16,x16,#4 / blr x16 the slot's tail-branch trampoline The compared id is STRUCTURAL, so duplicate-but-identical types stay interchangeable; comparing raw type indices would trap where wasmtime calls. x16/x17 are the AAPCS64 IP0/IP1 scratch registers — outside both the value- stack temp pool (x9..x15) and the argument registers, so no guard can alias a live value. PARAM HOMING was the blocker: a non-leaf function referencing a parameter loud-declined, and a table index almost always IS a parameter, so `call_indirect` would only have dispatched on constants. Non-leaf functions now give EVERY local (params included) an 8-byte stack slot and store the incoming argument registers there at the prologue, reusing the non-param-local machinery verbatim. That restores both properties the decline protected: a post-call read hits the slot (which the call cannot clobber), and every value-stack entry is a temp again, so argument marshalling stays hazard-free. LEAF functions are untouched and byte-identical, so writing a param still declines there and that ledger entry stays valid; a non-leaf FLOAT param also still declines (homing a v-register needs an FP store this encoder lacks). Verified end-to-end, not just in unit tests: both features compile, LINK with a real `ld.lld`, and disassemble correctly — the linker relaxes `adrp`+`add` to `adr`, resolves `__synth_globals` to the emitted `.data` (0x29 = 41, 0x11f71fb04cb = 1234567890123), and the table lays out as `[1][b func_0] [1][b func_1] [2][b func_2] [0][brk #0]`. Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- crates/synth-backend-aarch64/src/backend.rs | 94 +++- crates/synth-backend-aarch64/src/selector.rs | 477 ++++++++++++++++-- crates/synth-backend-aarch64/src/substrate.rs | 154 +++--- .../tests/cross_backend_op_parity.rs | 47 +- crates/synth-cli/src/main.rs | 77 ++- crates/synth-core/src/backend.rs | 8 + 6 files changed, 722 insertions(+), 135 deletions(-) diff --git a/crates/synth-backend-aarch64/src/backend.rs b/crates/synth-backend-aarch64/src/backend.rs index 67a1cb51..e71b91f9 100644 --- a/crates/synth-backend-aarch64/src/backend.rs +++ b/crates/synth-backend-aarch64/src/backend.rs @@ -82,7 +82,11 @@ impl AArch64Backend { ))); } }; - let (words, call_sites) = selector::select_typed_cf_calls( + // #851 lane L3: the module-level context for globals + call_indirect. + // Its `substrate_emitted` flag is FAIL-SAFE — false unless the driver + // has actually placed `__synth_globals` / `__synth_func_table`. + let ctx = module_ctx(config); + let (words, call_sites, sym_relocs) = selector::select_typed_cf_calls( ops, num_params, &config.current_func_params_f32, @@ -93,11 +97,14 @@ impl AArch64Backend { func_result_counts, func_ret_float, bounds, + &ctx, ) .map_err(|e| BackendError::CompilationFailed(e.to_string()))?; let code: Vec = words.iter().flat_map(|w| w.to_le_bytes()).collect(); // Each direct call site → an R_AARCH64_CALL26 against the callee's - // `func_N` symbol (emitted for every local function by compile_module). + // `func_N` symbol (emitted for every local function by compile_module); + // #851 lane L3 adds the `adrp`+`add :lo12:` pairs that reach the + // emitted globals region / funcref table. let relocations: Vec = call_sites .iter() .map(|cs| CodeRelocation { @@ -105,6 +112,7 @@ impl AArch64Backend { symbol: format!("func_{}", cs.callee), kind: RelocKind::AArch64Call26, }) + .chain(sym_relocs) .collect(); Ok(CompiledFunction { name: name.to_string(), @@ -122,6 +130,48 @@ impl AArch64Backend { } } +/// #851 lane L3 — build the selector's module context from the driver-supplied +/// [`CompileConfig`]. `substrate_emitted` is threaded verbatim: it is `false` +/// unless the driver ran [`crate::substrate::plan`] AND placed its output, so a +/// context built here can never authorize code that addresses a region the +/// object lacks. +fn module_ctx(config: &CompileConfig) -> selector::ModuleCtx { + let guards = &config.call_indirect_guards; + // Per table: (slot count, base SLOT index). `base_byte_offset` counts the + // 4-byte pointer slots of the ARM region contract, so /4 recovers the slot + // index — the aarch64 table uses the same SLOT ORDER with 8-byte records. + // Stop at the first table without a compile-time size/base: every later + // table's base is then not a constant, and an index past the end + // LOUD-DECLINES at the lowering (matching `funcref_region_slots`). + let mut tables: Vec<(u32, u32)> = Vec::new(); + for t in &guards.tables { + match (t.table_size, t.base_byte_offset) { + (Some(size), Some(base_bytes)) => tables.push((size, base_bytes / 4)), + _ => break, + } + } + let n_types = config + .type_arg_counts + .len() + .max(config.type_class_ids.len()) + .max(config.type_result_counts.len()); + selector::ModuleCtx { + substrate_emitted: config.a64_substrate_emitted, + // #643 slot widths: 8 ⇒ an i64/f64 global (the `x` view). + global_is64: config.global_widths.iter().map(|w| *w == 8).collect(), + tables, + type_class_ids: config.type_class_ids.clone(), + type_arg_counts: config.type_arg_counts.clone(), + type_result_counts: config.type_result_counts.clone(), + type_ret_float: (0..n_types) + .map(|i| { + config.type_ret_f32.get(i).copied().unwrap_or(false) + || config.type_ret_f64.get(i).copied().unwrap_or(false) + }) + .collect(), + } +} + /// Count register parameters from the op stream (a local index read before it is /// written is a parameter). Mirrors the ARM/RISC-V backends' heuristic. fn count_params(ops: &[WasmOp]) -> u32 { @@ -237,6 +287,28 @@ impl Backend for AArch64Backend { )); } + // #851 lane L3 — plan the MODULE-LEVEL substrate (globals `.data` image + // + `.text` funcref table) BEFORE compiling any body, so an + // unrepresentable shape declines the whole compile rather than being + // discovered after code that addresses it was emitted. `plan` is the + // single producer of both regions, so what the code addresses and what + // the object ships cannot disagree. + let uses_globals = locals.iter().any(|f| { + f.ops + .iter() + .any(|op| matches!(op, WasmOp::GlobalGet(_) | WasmOp::GlobalSet(_))) + }); + let uses_call_indirect = locals.iter().any(|f| { + f.ops + .iter() + .any(|op| matches!(op, WasmOp::CallIndirect { .. })) + }); + let substrate = crate::substrate::plan( + &crate::substrate::PlanInputs::from_module(module) + .with_usage(uses_globals, uses_call_indirect), + ) + .map_err(|e| BackendError::CompilationFailed(format!("aarch64: {e}")))?; + // #851: per-function "returns a float" mask (v0/d0 result) — a // float-returning callee is loud-declined by the call lowering. let nrf = module.func_ret_f32.len().max(module.func_ret_f64.len()); @@ -277,6 +349,17 @@ impl Backend for AArch64Backend { current_func_param_count: declared_params.or(config.current_func_param_count), num_imports: module.num_imported_funcs, func_arg_counts: module.func_arg_counts.clone(), + // #851 lane L3: the substrate metadata + the fail-safe gate. + // `emitted` is true only when `plan` produced a region that the + // ELF build below actually places. + a64_substrate_emitted: substrate.emitted, + call_indirect_guards: module.call_indirect_guards(), + type_class_ids: module.structural_type_class_ids(), + type_arg_counts: module.type_arg_counts.clone(), + type_result_counts: module.type_result_counts.clone(), + type_ret_f32: module.type_ret_f32.clone(), + type_ret_f64: module.type_ret_f64.clone(), + global_widths: module.globals.iter().map(|g| g.slot_bytes).collect(), ..config.clone() }; let compiled = self.compile_function_with_results( @@ -303,7 +386,12 @@ impl Backend for AArch64Backend { functions.push(compiled); } - let elf = elf::build_relocatable_object(&elf_funcs); + // #851 lane L3: the funcref table goes LAST in `.text`, so every real + // function keeps the offset it had before the table existed. + if let Some(table) = substrate.table { + elf_funcs.push(table); + } + let elf = elf::build_relocatable_object_with_data(&elf_funcs, &substrate.globals); Ok(CompilationResult { functions, elf: Some(elf), diff --git a/crates/synth-backend-aarch64/src/selector.rs b/crates/synth-backend-aarch64/src/selector.rs index ba44c444..45828fc1 100644 --- a/crates/synth-backend-aarch64/src/selector.rs +++ b/crates/synth-backend-aarch64/src/selector.rs @@ -96,6 +96,7 @@ use crate::encoder as enc; use crate::encoder::{Cond, FReg, Reg}; use synth_core::WasmOp; +use synth_core::backend::{CodeRelocation, FUNC_TABLE_SYMBOL, RelocKind}; /// The GP value-stack temp registers: caller-saved `w9/x9..w15/x15` (7 slots). /// `w0..w7` hold incoming integer params; results funnel back through `x0`. @@ -254,7 +255,10 @@ pub fn select_typed_cf( // No memory context either → bounds-unchecked, matching the pre-#865 // behavior of these compatibility wrappers (the real driver — the Backend // impl — threads the resolved `MemBounds` explicitly). - let (words, _sites) = select_typed_cf_calls( + // No module context either -> `ModuleCtx::default()` has + // `substrate_emitted == false`, so globals and `call_indirect` LOUD-DECLINE + // here (this wrapper's callers place no `.data` / funcref table). + let (words, _sites, _relocs) = select_typed_cf_calls( ops, num_params, params_f32, @@ -265,6 +269,7 @@ pub fn select_typed_cf( &[], &[], MemBounds::Unchecked, + &ModuleCtx::default(), )?; Ok(words) } @@ -301,6 +306,42 @@ pub struct CallSite { /// and every epilogue restores them (`ldp`) before `ret`. Leaf functions stay /// byte-identical to the pre-#851 output (the frame is gated on "body has a /// lowered call"). +/// #851 lane L3 — the MODULE-LEVEL context the `global.get`/`global.set` and +/// `call_indirect` lowerings need, threaded as one parameter rather than five. +/// +/// [`Default`] means "the driver emitted NO substrate", which makes all three +/// ops LOUD-DECLINE. That default is the fail-safe: a caller that has not +/// placed `__synth_globals` / `__synth_func_table` in the object cannot get code +/// that addresses them (see `CompileConfig::a64_substrate_emitted` and +/// [`crate::substrate::plan`], the single producer of both regions). +#[derive(Debug, Clone, Default)] +pub struct ModuleCtx { + /// The driver has emitted the substrate regions this context describes. + pub substrate_emitted: bool, + /// Per DEFINED global index: true when the slot holds a 64-bit value + /// (i64/f64) and must be read/written through the `x` view. + pub global_is64: Vec, + /// Per table index: `(compile-time slot count, base SLOT index of this + /// table within the contiguous funcref region)`. + pub tables: Vec<(u32, u32)>, + /// Per module type index: the STRUCTURAL class id the dispatch compares + /// (>= 1; 0 means "no class known", which declines). + pub type_class_ids: Vec, + /// Per module type index: AAPCS64 integer-argument slot count. + pub type_arg_counts: Vec, + /// Per module type index: result count (0 = void, 1 = one value). + pub type_result_counts: Vec, + /// Per module type index: the type returns f32/f64 (in `v0`/`d0`, not `x0`) + /// — declined, exactly as for a direct `call`. + pub type_ret_float: Vec, +} + +/// #851 lane L3 — what one `select_typed_cf_calls` call produces: the emitted +/// A64 words, the direct-`call` sites (turned into `R_AARCH64_CALL26` by the +/// driver), and the symbol relocations for the `adrp`+`add :lo12:` pairs that +/// reach the emitted globals region / funcref table. +pub type Selection = (Vec, Vec, Vec); + #[allow(clippy::too_many_arguments)] pub fn select_typed_cf_calls( ops: &[WasmOp], @@ -313,7 +354,8 @@ pub fn select_typed_cf_calls( func_result_counts: &[u32], func_ret_float: &[bool], bounds: MemBounds, -) -> Result<(Vec, Vec), SelectError> { + ctx: &ModuleCtx, +) -> Result { if num_params > 8 { return Err(SelectError(format!( "{num_params} params — supports at most 8 register params" @@ -323,23 +365,42 @@ pub fn select_typed_cf_calls( // #851 — is this function NON-LEAF (contains a `call` we will lower)? A `bl` // clobbers x30, so a non-leaf must save/restore LR. Computed up front so the // prologue can emit the frame; call-free functions stay byte-identical. - let is_non_leaf = ops.iter().any(|op| matches!(op, WasmOp::Call(_))); - - // A non-leaf function that reads a PARAMETER is loud-declined: params arrive - // in x0..x7 (caller-saved), a `bl` clobbers them, and this backend does not - // yet HOME params to callee-saved storage — reading `local.get p` after a - // call would be garbage. Declining here ALSO makes arg marshalling - // hazard-free: with no param-Vals, every value-stack entry lives in a temp - // (x9..x15), disjoint from the arg destinations (x0..x7), so an argument - // move `mov x{arg}, x{temp}` never overwrites a not-yet-read source. - if is_non_leaf - && ops.iter().any( - |op| matches!(op, WasmOp::LocalGet(i) | WasmOp::LocalSet(i) | WasmOp::LocalTee(i) if *i < num_params), - ) - { + // #851 lane L3: `call_indirect` lowers to `blr`, which also clobbers x30. + let is_non_leaf = ops + .iter() + .any(|op| matches!(op, WasmOp::Call(_) | WasmOp::CallIndirect { .. })); + + // #851 lane L3 — PARAM HOMING for non-leaf functions. + // + // Params arrive in x0..x7, which are caller-saved: a `bl`/`blr` clobbers + // them, so reading `local.get p` after a call would be garbage. Before this + // increment that whole shape was loud-declined — which made `call_indirect` + // near-useless, since the table index all but always comes from a parameter. + // + // The fix reuses the non-param-local machinery unchanged: when a non-leaf + // function references a param, EVERY local (params included) gets an 8-byte + // stack slot, the prologue STORES each param register into its slot, and + // `local.get` becomes a `ldr` into a fresh temp exactly like a non-param + // local. That restores both properties the decline was protecting: + // + // * a post-call read hits the SLOT, which the call cannot clobber; + // * every value-stack entry is a temp (x9..x15) again — nothing lives in + // x0..x7 by reference — so argument marshalling stays hazard-free. + // + // A LEAF function is untouched (params stay register-resident, bytes + // identical), so `local.set`/`local.tee` on a param still declines there. + let reads_param = ops.iter().any( + |op| matches!(op, WasmOp::LocalGet(i) | WasmOp::LocalSet(i) | WasmOp::LocalTee(i) if *i < num_params), + ); + let home_params = is_non_leaf && reads_param; + // FLOAT params live in v0..v7 and would need an FP store to home; the + // encoder has no `str s/d` yet, so that shape keeps the old loud decline + // rather than homing the wrong register file. + if home_params && (params_f32.iter().any(|b| *b) || params_f64.iter().any(|b| *b)) { return Err(SelectError( - "non-leaf function references a parameter — param homing across a \ - call is not yet supported for aarch64; loud-declining (#851)" + "non-leaf function references a FLOAT parameter — homing a v-register \ + param needs an FP store this encoder does not have; loud-declining \ + (#851)" .into(), )); } @@ -372,19 +433,25 @@ pub fn select_typed_cf_calls( _ => None, }) .max(); - let num_non_param_locals = match max_local_idx { - Some(m) if m >= num_params => m - num_params + 1, + // #851 lane L3: when params are homed, the frame covers EVERY local + // (index 0..=max), so slot `idx` sits at `idx * 8`; otherwise it covers only + // the non-param locals and slot `idx` sits at `(idx - num_params) * 8`. + let slot_base = if home_params { 0 } else { num_params }; + let num_slots = match max_local_idx { + Some(m) if m >= slot_base => m - slot_base + 1, _ => 0, }; - // Frame size in bytes: one 8-byte slot per non-param local, rounded UP to a - // 16-byte multiple (the ABI requires 16-byte SP alignment). - let frame_size: u32 = if num_non_param_locals == 0 { + // Frame size in bytes: one 8-byte slot per local, rounded UP to a 16-byte + // multiple (the ABI requires 16-byte SP alignment). + let frame_size: u32 = if num_slots == 0 { 0 } else { - (num_non_param_locals * 8).div_ceil(16) * 16 + (num_slots * 8).div_ceil(16) * 16 }; - // Byte offset of non-param local `idx`'s slot from SP. - let local_slot_off = |idx: u32| -> u32 { (idx - num_params) * 8 }; + // Byte offset of local `idx`'s slot from SP. + let local_slot_off = |idx: u32| -> u32 { (idx - slot_base) * 8 }; + // Is local `idx` slot-resident (vs a register-resident param in a leaf)? + let slot_resident = |idx: u32| -> bool { home_params || idx >= num_params }; // Prologue. Order (each step lowers SP; epilogue reverses): // 1. #851 non-leaf: `stp x29,x30,[sp,#-16]!` saves FP/LR (a `bl` clobbers @@ -397,14 +464,50 @@ pub fn select_typed_cf_calls( } if frame_size > 0 { words.push(enc::sub_imm64(enc::SP, enc::SP, frame_size)); - for k in 0..num_non_param_locals { - words.push(enc::str_x_imm(enc::XZR, enc::SP, k * 8)); + for k in 0..num_slots { + let local_idx = slot_base + k; + if home_params && local_idx < num_params { + // #851 lane L3: HOME the incoming param register. The full + // 64-bit store is right for i32 too — a `w`-form producer zeroes + // the upper half, and every reader takes the `w` view back. + words.push(enc::str_x_imm( + params[local_idx as usize].reg, + enc::SP, + k * 8, + )); + } else { + // A non-param local is ZERO-INITIALIZED (WASM's default-value + // rule). + words.push(enc::str_x_imm(enc::XZR, enc::SP, k * 8)); + } } } // #851 — direct-call sites recorded during selection (byte offset of the // `bl`, callee full index) for the backend's R_AARCH64_CALL26 relocations. let mut call_sites: Vec = Vec::new(); + // #851 lane L3 — symbol relocations for the `adrp`+`add :lo12:` pairs that + // reach the emitted globals region / funcref table. + let mut sym_relocs: Vec = Vec::new(); + + // #851 lane L3 — resolve a global index to "is this an 8-byte slot?", or + // LOUD-DECLINE. The `substrate_emitted` gate is the fail-safe: without it + // the driver has placed no `__synth_globals`, so addressing it would be a + // relocation against a symbol that does not exist. + let global_slot = |ctx: &ModuleCtx, idx: u32| -> Result { + if !ctx.substrate_emitted { + return Err(SelectError( + "global.get/global.set needs the emitted `__synth_globals` region, which this compile path does not place — loud-declining (#851)" + .into(), + )); + } + ctx.global_is64.get(idx as usize).copied().ok_or_else(|| { + SelectError(format!( + "global {idx} is out of range for the emitted globals region ({} slots) — loud-declining (#851)", + ctx.global_is64.len() + )) + }) + }; // Control-flow state (#538 cf increment, #851 full control flow). Each open // `block`/`loop`/`if` pushes a frame. The matching `End` pops it. Where a @@ -1083,7 +1186,7 @@ pub fn select_typed_cf_calls( for op in ops { match op { WasmOp::LocalGet(i) => { - if *i >= num_params { + if slot_resident(*i) { // Non-param local (#851): LOAD its stack slot into a FRESH GP // temp — a copy, so a later `local.set` of the same index // cannot alias this value. 64-bit load (both i32 and i64 read @@ -1104,7 +1207,7 @@ pub fn select_typed_cf_calls( // pushed (the miscompile the slot model avoids for non-param locals); // homing written params is a later increment. WasmOp::LocalSet(i) => { - if *i >= num_params { + if slot_resident(*i) { let src = pop_gp(&mut stack, "local.set")?; words.push(enc::str_x_imm(src, enc::SP, local_slot_off(*i))); } else { @@ -1119,7 +1222,7 @@ pub fn select_typed_cf_calls( // Store the top value WITHOUT popping it (peek + `str`); a param // target is declined for the same reason as `local.set`. WasmOp::LocalTee(i) => { - if *i >= num_params { + if slot_resident(*i) { let top = *stack .last() .ok_or_else(|| SelectError("local.tee underflow".into()))?; @@ -1862,6 +1965,206 @@ pub fn select_typed_cf_calls( words.push(enc::csel(t0, t0, t1, Cond::Eq)); stack.push(Val::gp(t0)); } + // --- #851 lane L3: WASM globals ------------------------------ + // + // `global k` lives at `__synth_globals + k*8` in the `.data` region + // THIS object emits ([`crate::substrate::plan`]). The address is + // formed PC-relatively (`adrp`+`add :lo12:`), so globals need NO + // base register and add NO precondition beside `x28`. An i32/f32 + // global occupies the low word of its 8-byte slot (`w` view), an + // i64/f64 global the whole slot (`x` view). The load/store + // immediate is size-SCALED, so slot `k*8` is `k*2` for a word + // access and `k` for a doubleword one. + WasmOp::GlobalGet(idx) => { + let is64 = global_slot(ctx, *idx)?; + let dst = alloc_temp(&stack)?; + emit_sym_addr( + &mut words, + &mut sym_relocs, + dst, + crate::substrate::GLOBALS_SYMBOL, + ); + // `dst` is read as the base and written as the destination by a + // SINGLE instruction (read-before-write) — reusing it is safe. + words.push(if is64 { + enc::ldr_x(dst, dst, *idx) + } else { + enc::ldr_w(dst, dst, *idx * 2) + }); + stack.push(Val::gp(dst)); + } + WasmOp::GlobalSet(idx) => { + let is64 = global_slot(ctx, *idx)?; + let val = pop_gp(&mut stack, "global.set")?; + // Keep `val` marked live while allocating the base temp, so the + // two are guaranteed distinct registers. + stack.push(Val::gp(val)); + let base = alloc_temp(&stack)?; + stack.pop(); + emit_sym_addr( + &mut words, + &mut sym_relocs, + base, + crate::substrate::GLOBALS_SYMBOL, + ); + words.push(if is64 { + enc::str_x(val, base, *idx) + } else { + enc::str_w(val, base, *idx * 2) + }); + } + // --- #851 lane L3: `call_indirect` --------------------------- + // + // WASM Core §4.4.8 requires THREE traps that A64's `blr` does not + // give for free — an out-of-range index, a null (uninitialized) + // slot, and a signature mismatch. All three are emitted here; the + // table itself is the `.text`-resident trampoline array + // [`crate::substrate`] describes, one 8-byte + // `[u32 class id][b func_N]` record per slot (`[0][brk #0]` when + // null). + // + // cmp w_idx, #size ; OOB guard — size is compile-time + // b.lo +2 ; unsigned lower ⇒ in range + // brk #0 + // adrp x16, __synth_func_table + // add x16, x16, :lo12:… ; region base (no base register!) + // add x16, x16, w_idx, uxtw #3 ; + idx*8 + // [add x16, x16, #base*8] ; + this table's base slot + // ldr w17, [x16] ; the slot's structural class id + // cmp w17, #expected ; TYPE check — and, because a null + // b.eq +2 ; slot's id is 0 and expected is + // brk #0 ; >= 1, the NULL check too + // mov x0..x7, args + // add x16, x16, #4 ; the slot's trampoline + // blr x16 + // + // The class id is STRUCTURAL, so structurally-equal duplicate + // types stay interchangeable (§4.4.8) — comparing raw type indices + // would trap where wasmtime calls. + WasmOp::CallIndirect { + type_index, + table_index, + } => { + if !ctx.substrate_emitted { + return Err(SelectError( + "call_indirect needs the emitted `__synth_func_table` \ + region, which this compile path does not place — \ + loud-declining (#851)" + .into(), + )); + } + let ti = *type_index as usize; + let &(table_slots, base_slot) = + ctx.tables.get(*table_index as usize).ok_or_else(|| { + SelectError(format!( + "call_indirect on table {table_index}, which has no \ + compile-time size/base in the emitted funcref region \ + — loud-declining (#851)" + )) + })?; + let expected = ctx.type_class_ids.get(ti).copied().unwrap_or(0); + if expected == 0 { + return Err(SelectError(format!( + "call_indirect type {ti} has no structural class id — the \ + §4.4.8 signature check cannot be encoded; loud-declining \ + (#851)" + ))); + } + let argc = *ctx.type_arg_counts.get(ti).ok_or_else(|| { + SelectError(format!("call_indirect type {ti}: unknown arg count")) + })?; + if argc > 8 { + return Err(SelectError(format!( + "call_indirect type {ti}: {argc} args — at most 8 register \ + args are supported; loud-declining (#851)" + ))); + } + let rc = *ctx.type_result_counts.get(ti).ok_or_else(|| { + SelectError(format!("call_indirect type {ti}: unknown result count")) + })?; + if rc > 1 { + return Err(SelectError(format!( + "call_indirect type {ti}: {rc} results — multi-result calls \ + are not supported for aarch64; loud-declining (#851)" + ))); + } + // AAPCS64 returns floats in v0/d0, not x0 — same decline as a + // direct `call` (pushing x0 would read a stale GP register). + if rc == 1 && ctx.type_ret_float.get(ti).copied().unwrap_or(false) { + return Err(SelectError(format!( + "call_indirect type {ti}: float result (returned in v0/d0, \ + not x0) — not yet supported for aarch64; loud-declining \ + (#851)" + ))); + } + // The table index is on TOP of the stack, above the arguments. + let idx = pop_gp(&mut stack, "call_indirect")?; + if stack.len() != argc as usize { + return Err(SelectError(format!( + "call_indirect type {ti}: value stack holds {} entries \ + below the index but needs exactly {argc} (the call \ + clobbers caller-saved temps below the args); \ + loud-declining (#851)", + stack.len() + ))); + } + for (arg_reg, v) in stack.iter().enumerate() { + if v.file != File::Gp { + return Err(SelectError(format!( + "call_indirect type {ti}: argument {arg_reg} is a \ + float — FP call args are not supported for aarch64; \ + loud-declining (#851)" + ))); + } + } + // (1) OOB guard. `table_slots` and the class ids were range- + // checked against the 12-bit immediate by substrate::plan. + words.push(enc::cmp_imm(idx, table_slots)); + words.push(enc::bcond(Cond::Lo, 2)); // in range: hop the brk + words.push(enc::brk(0)); + // (2) Slot address into IP0 (outside the temp pool and the arg + // registers, so nothing live can alias it). + emit_sym_addr(&mut words, &mut sym_relocs, IP0, FUNC_TABLE_SYMBOL); + words.push(enc::add_ext_uxtw_sh(IP0, IP0, idx, 3)); + let base_bytes = base_slot * crate::substrate::TABLE_SLOT_BYTES; + if base_bytes > 0 { + if base_bytes < 4096 { + words.push(enc::add_imm64(IP0, IP0, base_bytes)); + } else { + // Past the imm12 range (a later table in a multi-table + // module): materialize the byte offset in IP1 first. + for w in enc::mov_imm32(IP1, base_bytes) { + words.push(w); + } + words.push(enc::add64(IP0, IP0, IP1)); + } + } + // (3) Type check — which is the null check too (a null slot + // carries class id 0, and `expected` is >= 1). + words.push(enc::ldr_w(IP1, IP0, 0)); + words.push(enc::cmp_imm(IP1, expected)); + words.push(enc::bcond(Cond::Eq, 2)); // matching type: hop the brk + words.push(enc::brk(0)); + // (4) Marshal args. Sources are temps (x9..x15), destinations + // x0..x7 — disjoint, so the moves need no shuffle, and IP0 + // (holding the verified slot) is untouched. + for (arg_reg, v) in stack.iter().enumerate() { + if v.reg != arg_reg as u8 { + words.push(enc::mov_reg64(arg_reg as u8, v.reg)); + } + } + stack.clear(); + // (5) Branch into the slot's trampoline (slot+4), which tail- + // branches to the callee; `blr` sets x30 so the callee + // returns straight back here. + words.push(enc::add_imm64(IP0, IP0, 4)); + words.push(enc::blr(IP0)); + if rc == 1 { + let dst = alloc_temp(&stack)?; + words.push(enc::mov_reg64(dst, 0)); + stack.push(Val::gp(dst)); + } + } other => { return Err(SelectError(format!( "unsupported wasm op for aarch64 subset: {other:?}" @@ -1874,7 +2177,7 @@ pub fn select_typed_cf_calls( if !matches!(ops.last(), Some(WasmOp::End)) { epilogue(&mut words, stack.last().copied(), frame_size, is_non_leaf); } - Ok((words, call_sites)) + Ok((words, call_sites, sym_relocs)) } /// Emit the function epilogue: move the top-of-stack result into the ABI return @@ -1889,6 +2192,40 @@ pub fn select_typed_cf_calls( /// is byte-identical to the pre-#851 epilogue). The result move is done BEFORE /// the `add sp` (the result lives in a caller-saved temp, unaffected by SP), so /// the sequence is: funnel result → restore SP → ret. +/// #851 lane L3 — emit `adrp xd, sym` + `add xd, xd, :lo12:sym`, recording the +/// two relocations, so `xd` ends up holding `sym`'s ABSOLUTE address. +/// +/// This pair is how the aarch64 backend reaches a region it EMITTED (the +/// globals `.data` image, the funcref table) with NO ambient base register — +/// see [`crate::substrate`] for why that matters (it adds no precondition +/// beside `x28`, and there is no base register to collide with the way #275/ +/// #717 collided on ARM). +fn emit_sym_addr(words: &mut Vec, relocs: &mut Vec, rd: Reg, symbol: &str) { + let off = (words.len() * 4) as u32; + relocs.push(CodeRelocation { + offset: off, + symbol: symbol.to_string(), + kind: RelocKind::AArch64AdrPrelPgHi21, + }); + words.push(enc::adrp(rd, 0)); + relocs.push(CodeRelocation { + offset: off + 4, + symbol: symbol.to_string(), + kind: RelocKind::AArch64AddAbsLo12Nc, + }); + words.push(enc::add_imm64(rd, rd, 0)); +} + +/// #851 lane L3 — the AAPCS64 intra-procedure-call scratch registers. `x16` +/// carries the `call_indirect` slot/target address and `x17` the loaded class +/// id. Both are chosen deliberately OUTSIDE the value-stack temp pool +/// (`x9..x15`) and the argument registers (`x0..x7`), so the dispatch's guards +/// can run after the index is popped and before/after argument marshalling +/// without ever aliasing a live value. They are caller-saved and dead +/// immediately after the `blr`. +const IP0: Reg = 16; +const IP1: Reg = 17; + /// Guard an `imm26` (unconditional `b`) displacement (words) against the A64 /// field width (signed 26-bit → ±2^25 words = ±128 MB). Over-range would wrap /// silently in the encoder's mask, so we LOUD-DECLINE instead (unreachable for @@ -1988,7 +2325,9 @@ mod tests { result_counts, &[], MemBounds::Unchecked, + &ModuleCtx::default(), ) + .map(|(w, s, _)| (w, s)) } #[test] @@ -2047,13 +2386,60 @@ mod tests { assert!(sel_calls(&ops, 0, 1, &[0], &[0]).is_err()); } + /// #851 lane L3 — a non-leaf function that reads a param now HOMES it into + /// a stack slot at the prologue instead of loud-declining. The homing store + /// is what makes a post-call read sound (x0..x7 are caller-saved), and it is + /// the prerequisite for a useful `call_indirect` (the table index almost + /// always comes from a parameter). #[test] - fn non_leaf_referencing_param_loud_declines() { - // A function that both reads a param AND makes a call declines (param - // homing across a call is unsupported — reading x0 after bl is garbage). + fn non_leaf_homes_its_params_to_stack_slots() { let ops = vec![WasmOp::LocalGet(0), WasmOp::Call(1), WasmOp::End]; // func 1 takes 1 arg (the local.get 0 value). - assert!(sel_calls(&ops, 1, 0, &[0, 1], &[0, 1]).is_err()); + let (w, _) = sel_calls(&ops, 1, 0, &[0, 1], &[0, 1]).unwrap(); + // stp x29,x30,[sp,#-16]! ; sub sp,sp,#16 ; str x0,[sp] ; ldr x9,[sp] ... + assert_eq!(w[0], enc::stp_fp_lr_pre16()); + assert_eq!(w[1], enc::sub_imm64(enc::SP, enc::SP, 16)); + assert_eq!( + w[2], + enc::str_x_imm(0, enc::SP, 0), + "the incoming param x0 must be STORED to its slot at the prologue" + ); + // The `local.get 0` then LOADS the slot into a temp (a copy), so the + // value survives the call that follows. + assert_eq!(w[3], enc::ldr_x_imm(9, enc::SP, 0)); + } + + /// A LEAF function is untouched by homing: its params stay register- + /// resident, so writing one still loud-declines (that gap is a separate + /// increment, and its parity-gate entry stays valid). + #[test] + fn leaf_param_write_still_loud_declines() { + let ops = vec![WasmOp::I32Const(42), WasmOp::LocalSet(0), WasmOp::End]; + assert!(sel_calls(&ops, 1, 0, &[0], &[0]).is_err()); + let ops = vec![WasmOp::I32Const(42), WasmOp::LocalTee(0), WasmOp::End]; + assert!(sel_calls(&ops, 1, 0, &[0], &[0]).is_err()); + } + + /// A FLOAT param in a non-leaf function keeps the loud decline: homing a + /// v-register needs an FP store the encoder does not have, and homing the + /// wrong register file would be a silent miscompile. + #[test] + fn non_leaf_float_param_still_loud_declines() { + let ops = vec![WasmOp::LocalGet(0), WasmOp::Call(1), WasmOp::End]; + let r = select_typed_cf_calls( + &ops, + 1, + &[true], // param 0 is f32 → lives in s0 + &[], + &[], + 0, + &[0, 1], + &[0, 1], + &[false, false], + MemBounds::Unchecked, + &ModuleCtx::default(), + ); + assert!(r.is_err(), "float param homing must loud-decline"); } #[test] @@ -2085,6 +2471,7 @@ mod tests { &[1], // 1 result &[true], // ...which is a float MemBounds::Unchecked, + &ModuleCtx::default(), ); assert!(r.is_err(), "float-returning callee must loud-decline"); } @@ -2092,9 +2479,20 @@ mod tests { // --- #865: software bounds check --- fn sel_mem(ops: &[WasmOp], num_params: u32, bounds: MemBounds) -> Vec { - let (w, _) = - select_typed_cf_calls(ops, num_params, &[], &[], &[], 0, &[], &[], &[], bounds) - .unwrap(); + let (w, _, _) = select_typed_cf_calls( + ops, + num_params, + &[], + &[], + &[], + 0, + &[], + &[], + &[], + bounds, + &ModuleCtx::default(), + ) + .unwrap(); w } @@ -3472,6 +3870,7 @@ mod tests { &[], &[], MemBounds::Unchecked, + &ModuleCtx::default(), ); assert!(r.is_err()); } diff --git a/crates/synth-backend-aarch64/src/substrate.rs b/crates/synth-backend-aarch64/src/substrate.rs index 094cd943..d62ec9d1 100644 --- a/crates/synth-backend-aarch64/src/substrate.rs +++ b/crates/synth-backend-aarch64/src/substrate.rs @@ -91,60 +91,74 @@ pub struct Substrate { pub emitted: bool, } -/// Everything [`plan`] needs, so both drivers (the `Backend::compile_module` -/// path and the CLI's own multi-function ELF path) can call it from whatever -/// module state they hold. -#[derive(Debug, Clone, Copy)] -pub struct PlanInputs<'a> { +/// Everything [`plan`] needs, OWNED, so a driver that aggregates module state +/// can build it once while the decoded module is still whole and carry it to +/// wherever the ELF is assembled. Both aarch64 drivers do exactly that. +/// +/// The two `uses_*` flags are set LAST, by the driver, from the op streams it +/// is actually about to compile. +#[derive(Debug, Default, Clone)] +pub struct PlanInputs { /// Defined globals with their decoded constant initializers. - pub globals: &'a [WasmGlobal], + pub globals: Vec, /// How many globals the module IMPORTS (their values arrive at /// instantiation, which this backend cannot perform). pub imported_globals: u32, /// Does any compiled function execute `global.get`/`global.set`? pub uses_globals: bool, - /// The contiguous funcref-region image (`DecodedModule::funcref_region_slots`). - pub funcref_slots: &'a [Option], + /// The contiguous funcref-region image + /// (`DecodedModule::funcref_region_slots`). + pub funcref_slots: Vec>, /// The matching per-slot structural class ids /// (`DecodedModule::funcref_region_class_ids`). - pub funcref_class_ids: &'a [u32], + pub funcref_class_ids: Vec, /// Per-table compile-time sizes (`DecodedModule::table_sizes`). - pub table_sizes: &'a [Option], + pub table_sizes: Vec>, /// Element segments, for the statically-verifiable-image check. - pub elem_segments: &'a [synth_core::wasm_decoder::ElemSegmentInfo], + pub elem_segments: Vec, /// Number of imported functions — a table slot pointing at one has no /// `func_N` body in this object. pub num_imported_funcs: u32, /// Does any compiled function execute `call_indirect`? pub uses_call_indirect: bool, + /// #851 lane L3 — the STRUCTURAL class id per function type, carried here + /// so the driver can hand it to the selector's `ModuleCtx` without keeping + /// the whole decoded module alive. + pub type_class_ids: Vec, + /// Result count per function type, same rationale. + pub type_result_counts: Vec, } -impl<'a> PlanInputs<'a> { - /// Derive the inputs from a whole decoded module plus the two usage flags - /// (which the driver computes from the op streams it is about to compile). - pub fn from_module( - module: &'a DecodedModule, - slots: &'a [Option], - class_ids: &'a [u32], - uses_globals: bool, - uses_call_indirect: bool, - ) -> Self { +impl PlanInputs { + /// Snapshot everything from a whole decoded module. The `uses_*` flags stay + /// `false`; the driver sets them from the op streams it compiles. + pub fn from_module(module: &DecodedModule) -> Self { Self { - globals: &module.globals, + globals: module.globals.clone(), imported_globals: module .imports .iter() .filter(|i| matches!(i.kind, synth_core::ImportKind::Global)) .count() as u32, - uses_globals, - funcref_slots: slots, - funcref_class_ids: class_ids, - table_sizes: &module.table_sizes, - elem_segments: &module.elem_segments, + uses_globals: false, + funcref_slots: module.funcref_region_slots(), + funcref_class_ids: module.funcref_region_class_ids(), + table_sizes: module.table_sizes.clone(), + elem_segments: module.elem_segments.clone(), num_imported_funcs: module.num_imported_funcs, - uses_call_indirect, + uses_call_indirect: false, + type_class_ids: module.structural_type_class_ids(), + type_result_counts: module.type_result_counts.clone(), } } + + /// Set the two usage flags from an op-stream scan over the functions the + /// driver will compile. + pub fn with_usage(mut self, uses_globals: bool, uses_call_indirect: bool) -> Self { + self.uses_globals = uses_globals; + self.uses_call_indirect = uses_call_indirect; + self + } } /// Plan (and materialize) the module-level substrate. @@ -153,14 +167,14 @@ impl<'a> PlanInputs<'a> { /// fails rather than shipping a region whose contents synth cannot vouch for. /// The two features are planned INDEPENDENTLY: a module that uses only globals /// never touches the table checks and vice versa. -pub fn plan(input: PlanInputs<'_>) -> Result { +pub fn plan(input: &PlanInputs) -> Result { let globals = if input.uses_globals { - plan_globals(&input)? + plan_globals(input)? } else { DataBlob::default() }; let table = if input.uses_call_indirect { - Some(plan_table(&input)?) + Some(plan_table(input)?) } else { None }; @@ -172,7 +186,7 @@ pub fn plan(input: PlanInputs<'_>) -> Result { } /// Build the `.data` globals image, or decline. -fn plan_globals(input: &PlanInputs<'_>) -> Result { +fn plan_globals(input: &PlanInputs) -> Result { // An IMPORTED global's value is supplied by the host at instantiation. // This backend emits no instantiation step, so its slot would ship whatever // synth guessed — the silent-wrong-initial-value class. Decline. @@ -239,7 +253,7 @@ fn plan_globals(input: &PlanInputs<'_>) -> Result { } /// Build the `.text` funcref-table trampoline blob, or decline. -fn plan_table(input: &PlanInputs<'_>) -> Result { +fn plan_table(input: &PlanInputs) -> Result { // 1. Every table must have a compile-time size, or its slots have no // constant base offset within the region (and no sound bounds check). if input.table_sizes.is_empty() { @@ -296,7 +310,7 @@ fn plan_table(input: &PlanInputs<'_>) -> Result { } // 3. Size + class-id immediates must fit the guard encodings. - let slots = input.funcref_slots; + let slots = &input.funcref_slots; if slots.len() > MAX_TABLE_SLOTS { return Err(format!( "funcref region holds {} slots; the out-of-range guard compares \ @@ -377,18 +391,8 @@ mod tests { } } - fn base<'a>() -> PlanInputs<'a> { - PlanInputs { - globals: &[], - imported_globals: 0, - uses_globals: false, - funcref_slots: &[], - funcref_class_ids: &[], - table_sizes: &[], - elem_segments: &[], - num_imported_funcs: 0, - uses_call_indirect: false, - } + fn base() -> PlanInputs { + PlanInputs::default() } /// A module using neither feature plans an EMPTY substrate — no `.data`, no @@ -396,7 +400,7 @@ mod tests { /// existing module's bytes are untouched). #[test] fn unused_features_plan_an_empty_substrate() { - let s = plan(base()).unwrap(); + let s = plan(&base()).unwrap(); assert!(s.globals.bytes.is_empty()); assert!(s.table.is_none()); assert!(!s.emitted); @@ -411,8 +415,8 @@ mod tests { g(1, Some(GlobalInit::I64(-2)), 8), g(2, Some(GlobalInit::I32(-1)), 4), ]; - let s = plan(PlanInputs { - globals: &gs, + let s = plan(&PlanInputs { + globals: gs.to_vec(), uses_globals: true, ..base() }) @@ -434,8 +438,8 @@ mod tests { #[test] fn global_without_const_initializer_declines() { let gs = [g(0, Some(GlobalInit::I32(1)), 4), g(1, None, 4)]; - let e = plan(PlanInputs { - globals: &gs, + let e = plan(&PlanInputs { + globals: gs.to_vec(), uses_globals: true, ..base() }) @@ -448,8 +452,8 @@ mod tests { #[test] fn imported_global_declines() { let gs = [g(0, Some(GlobalInit::I32(1)), 4)]; - let e = plan(PlanInputs { - globals: &gs, + let e = plan(&PlanInputs { + globals: gs.to_vec(), imported_globals: 1, uses_globals: true, ..base() @@ -471,11 +475,11 @@ mod tests { offset: Some(0), funcs: Some(vec![0, 9, 1]), }]; - let s = plan(PlanInputs { - funcref_slots: &slots, - funcref_class_ids: &ids, - table_sizes: &sizes, - elem_segments: &segs, + let s = plan(&PlanInputs { + funcref_slots: slots.to_vec(), + funcref_class_ids: ids.to_vec(), + table_sizes: sizes.to_vec(), + elem_segments: segs.to_vec(), uses_call_indirect: true, ..base() }) @@ -517,11 +521,11 @@ mod tests { offset: None, funcs: Some(vec![0, 1]), }]; - let e = plan(PlanInputs { - funcref_slots: &slots, - funcref_class_ids: &ids, - table_sizes: &sizes, - elem_segments: &segs, + let e = plan(&PlanInputs { + funcref_slots: slots.to_vec(), + funcref_class_ids: ids.to_vec(), + table_sizes: sizes.to_vec(), + elem_segments: segs.to_vec(), uses_call_indirect: true, ..base() }) @@ -534,8 +538,8 @@ mod tests { /// sound bounds check and no constant base — decline. #[test] fn unsized_table_declines() { - let e = plan(PlanInputs { - table_sizes: &[None], + let e = plan(&PlanInputs { + table_sizes: vec![None], uses_call_indirect: true, ..base() }) @@ -555,11 +559,11 @@ mod tests { offset: Some(0), funcs: Some(vec![0]), }]; - let e = plan(PlanInputs { - funcref_slots: &slots, - funcref_class_ids: &ids, - table_sizes: &sizes, - elem_segments: &segs, + let e = plan(&PlanInputs { + funcref_slots: slots.to_vec(), + funcref_class_ids: ids.to_vec(), + table_sizes: sizes.to_vec(), + elem_segments: segs.to_vec(), num_imported_funcs: 1, uses_call_indirect: true, ..base() @@ -579,11 +583,11 @@ mod tests { offset: Some(0), funcs: Some(vec![0; slots.len()]), }]; - let e = plan(PlanInputs { - funcref_slots: &slots, - funcref_class_ids: &ids, - table_sizes: &sizes, - elem_segments: &segs, + let e = plan(&PlanInputs { + funcref_slots: slots.to_vec(), + funcref_class_ids: ids.to_vec(), + table_sizes: sizes.to_vec(), + elem_segments: segs.to_vec(), uses_call_indirect: true, ..base() }) diff --git a/crates/synth-backend-riscv/tests/cross_backend_op_parity.rs b/crates/synth-backend-riscv/tests/cross_backend_op_parity.rs index fb080770..0dbf5054 100644 --- a/crates/synth-backend-riscv/tests/cross_backend_op_parity.rs +++ b/crates/synth-backend-riscv/tests/cross_backend_op_parity.rs @@ -112,10 +112,37 @@ fn aarch64_lowers(ops: &[WasmOp], num_params: u32) -> bool { &[0], &[false], synth_backend_aarch64::selector::MemBounds::Software { limit_bytes: 65536 }, + &a64_module_ctx(), ) .is_ok() } +/// #851 lane L3 — the module context the aarch64 probes run under. +/// +/// The globals and `call_indirect` lowerings are MODULE-LEVEL: they address +/// regions the driver emits (`__synth_globals` in `.data`, `__synth_func_table` +/// in `.text`), and the selector's fail-safe gate declines both unless the +/// driver says it placed them. Probing them with a DEFAULT context would +/// therefore measure the gate, not the lowering, and would keep reporting a +/// "gap" that no longer exists. +/// +/// So this mirrors the real call site for a small module that HAS both: two +/// globals (one i32 slot, one i64 slot) and one 4-entry table with two +/// structural signature classes. It is exactly what +/// `synth_backend_aarch64::backend::module_ctx` builds from such a module's +/// `CompileConfig`. +fn a64_module_ctx() -> synth_backend_aarch64::selector::ModuleCtx { + synth_backend_aarch64::selector::ModuleCtx { + substrate_emitted: true, + global_is64: vec![false, true], + tables: vec![(4, 0)], + type_class_ids: vec![1, 2], + type_arg_counts: vec![0, 1], + type_result_counts: vec![0, 1], + type_ret_float: vec![false, false], + } +} + /// The parity class of a `WasmOp` — assigned by the no-wildcard [`classify`] /// match so the WASM-op universe is compiler-enforced complete. enum ParityClass { @@ -910,17 +937,6 @@ fn aarch64_known_divergences() -> &'static [(&'static str, &'static str)] { "aarch64 declines writing a parameter (same homing prerequisite as \ local.set) — deferred, #851", ), - ( - "global.get", - "aarch64 has no globals substrate (no data section / global-region \ - addressing convention beyond the x28 linear-memory base); the \ - RV32 ledger entry above documents the same #798-class stack needed \ - — deferred, #851", - ), - ( - "global.set", - "aarch64 has no globals substrate (see global.get) — deferred, #851", - ), ( "memory.copy", "aarch64 selector has no MemoryCopy arm (loud decline); bulk-memory \ @@ -1008,8 +1024,6 @@ fn a64_extended_surface( lane, mirroring the ARM Helium/MVE exclusion) — deferred, #851"; const MULTI_MEM: &str = "multi-memory wrapper (#406): the aarch64 backend has no per-memory base \ lowering (single x28 base only) — declines, #851"; - const CALL_INDIRECT: &str = "call_indirect needs a function table + type/null/OOB trap guards \ - (§4.4.8); no aarch64 table substrate yet — loud-declined, #851"; let some = |label: &'static str, @@ -1568,6 +1582,11 @@ fn a64_extended_surface( ], Err(MULTI_MEM), ), + // #851 lane L3: `call_indirect` LOWERS — a `.text`-resident funcref + // table (`[u32 class id][b func_N]` per slot) plus the three §4.4.8 + // trap guards (out-of-range index, null slot, signature mismatch). The + // probe dispatches type 0 (void, no args) through table 0 of + // [`a64_module_ctx`]. CallIndirect { .. } => some( "call_indirect", 0, @@ -1578,7 +1597,7 @@ fn a64_extended_surface( table_index: 0, }, ], - Err(CALL_INDIRECT), + Ok(()), ), // ─── v128 / SIMD — GAP (all decline) ───────────────────────────── diff --git a/crates/synth-cli/src/main.rs b/crates/synth-cli/src/main.rs index b962ebd4..3b29092b 100644 --- a/crates/synth-cli/src/main.rs +++ b/crates/synth-cli/src/main.rs @@ -2784,6 +2784,7 @@ fn compile_all_exports( default_memory_nonconst_data, // #851: memory-0 segment with a non-const offset (legacy-dropped at decode) all_call_indirect_guards, // #642: table size + closed-world type verdicts all_funcref_slots, // #275: static funcref-region image (slot -> func index; None = null) + a64_plan_inputs, // #851 lane L3: snapshot of the aarch64 substrate inputs (globals image + funcref table) ) = if path.extension().is_some_and(|ext| ext == "wast") { info!("Parsing WAST (extracting all modules)..."); let contents = String::from_utf8(file_bytes).context("WAST file is not valid UTF-8")?; @@ -2901,6 +2902,11 @@ fn compile_all_exports( synth_core::CallIndirectGuards::default(), // #275: no guards ⇒ no dispatch ⇒ no funcref-region image. Vec::new(), + // #851 lane L3: the multi-module WAST merge has no single module to + // snapshot, so the aarch64 substrate inputs stay DEFAULT — which + // means `plan` emits nothing and the selector LOUD-DECLINES globals + // and call_indirect (the WAST fixture suite uses neither). + synth_backend_aarch64::substrate::PlanInputs::default(), ) } else { let wasm_bytes = if path.extension().is_some_and(|ext| ext == "wat") { @@ -2964,6 +2970,10 @@ fn compile_all_exports( // index) — the self-contained image builder resolves these to laid-out // function addresses and ships the table in flash. let funcref_slots = module.funcref_region_slots(); + // #851 lane L3: snapshot the aarch64 substrate inputs while the module + // is still whole (the `uses_*` flags are set below, from the op streams + // this compile will actually feed the backend). + let a64_inputs = synth_backend_aarch64::substrate::PlanInputs::from_module(&module); let func_arg_counts = module.func_arg_counts; let func_result_counts = module.func_result_counts; // #851 let type_arg_counts = module.type_arg_counts; @@ -3091,6 +3101,7 @@ fn compile_all_exports( module.default_memory_nonconst_data, // #851 guards, // #642 funcref_slots, // #275 + a64_inputs, // #851 lane L3 ) }; @@ -3216,6 +3227,38 @@ fn compile_all_exports( info!(" '{}' (index {})", display_name, f.index); } + // #851 lane L3 — the aarch64 module-level substrate. Planned HERE, before + // any body is compiled, from the op streams this compile will actually feed + // the backend, so an unrepresentable shape declines the whole compile rather + // than being discovered after code addressing it was emitted. + // + // `plan` is the SINGLE producer of both regions (the `.data` globals image + // and the `.text` funcref table), and `a64_substrate_emitted` below is + // derived from its result — so what the code addresses and what the object + // ships cannot disagree. A `plan` DECLINE is deliberately not raised here: + // it is only an error when the aarch64 backend is the one compiling (every + // other backend has its own globals/table story), so the Result is carried + // to the aarch64 ELF branch. + let a64_plan_inputs = a64_plan_inputs.with_usage( + all_exports.iter().any(|f| { + f.ops + .iter() + .any(|op| matches!(op, WasmOp::GlobalGet(_) | WasmOp::GlobalSet(_))) + }), + all_exports.iter().any(|f| { + f.ops + .iter() + .any(|op| matches!(op, WasmOp::CallIndirect { .. })) + }), + ); + let a64_substrate = synth_backend_aarch64::substrate::plan(&a64_plan_inputs); + if backend.name() == "aarch64" + && let Err(reason) = &a64_substrate + { + anyhow::bail!("aarch64: {reason}"); + } + let a64_substrate_emitted = a64_substrate.as_ref().is_ok_and(|s| s.emitted); + // Build compile config from CLI flags let config = CompileConfig { no_optimize, @@ -3289,6 +3332,13 @@ fn compile_all_exports( // #642: call_indirect guard inputs (compile-time table size for the // bounds guard + closed-world type verdicts). Default = decline. call_indirect_guards: all_call_indirect_guards, + // #851 lane L3 — aarch64 globals + call_indirect inputs. The + // `a64_substrate_emitted` gate is FAIL-SAFE: false unless `plan` + // produced a region that the aarch64 ELF branch below actually places, + // so the selector cannot emit code addressing a missing symbol. + type_result_counts: a64_plan_inputs.type_result_counts.clone(), + type_class_ids: a64_plan_inputs.type_class_ids.clone(), + a64_substrate_emitted, // #275: self-contained funcref-table dispatch — enabled ONLY when the // builder that emits and patches the flash-resident table // (`build_multi_func_cortex_m_elf`) will run: Cortex-M image, not @@ -3739,7 +3789,13 @@ fn compile_all_exports( // object. This must precede the `has_external_relocations || relocatable` // arm so `-b aarch64 --relocatable` isn't stolen into the ARM builder. info!("Building AArch64 multi-function relocatable object (EM_AARCH64)"); - build_multi_func_aarch64_elf(&compiled_funcs)? + // #851 lane L3: place the planned substrate — the `.data` globals image + // and the `.text` funcref table (appended LAST, so every real function + // keeps the `.text` offset it had before the table existed). + let substrate = a64_substrate + .as_ref() + .map_err(|e| anyhow::anyhow!("aarch64: {e}"))?; + build_multi_func_aarch64_elf(&compiled_funcs, substrate)? } else if is_riscv { // #798 (the RV32 analogue of #758; found by the VCR-VER-003 phase-2 // probe, #777): the RV32 single-base scheme (s11 = @@ -6803,8 +6859,13 @@ fn build_aarch64_elf(code: &[u8], func_name: &str) -> Result> { /// #546: emit a multi-function `EM_AARCH64` ELF64 (`ET_REL`) object exposing one /// global `STT_FUNC` symbol per compiled export. Mirrors /// `build_multi_func_riscv_elf` — the per-backend ELF path (#538 milestone-1c). -fn build_multi_func_aarch64_elf(funcs: &[ElfFunction]) -> Result> { - use synth_backend_aarch64::elf::{ElfFunction as A64ElfFunction, build_relocatable_object}; +fn build_multi_func_aarch64_elf( + funcs: &[ElfFunction], + substrate: &synth_backend_aarch64::substrate::Substrate, +) -> Result> { + use synth_backend_aarch64::elf::{ + ElfFunction as A64ElfFunction, build_relocatable_object_with_data, + }; let a64_funcs: Vec = funcs .iter() .map(|f| { @@ -6821,7 +6882,15 @@ fn build_multi_func_aarch64_elf(funcs: &[ElfFunction]) -> Result> { A64ElfFunction::code(symbols, f.code.clone(), f.relocations.clone()) }) .collect(); - Ok(build_relocatable_object(&a64_funcs)) + let mut a64_funcs = a64_funcs; + // #851 lane L3: the funcref table is `.text`-resident DATA appended LAST. + if let Some(table) = substrate.table.clone() { + a64_funcs.push(table); + } + Ok(build_relocatable_object_with_data( + &a64_funcs, + &substrate.globals, + )) } /// Build a simple ELF with just the code section (for quick testing) diff --git a/crates/synth-core/src/backend.rs b/crates/synth-core/src/backend.rs index 33b7122b..42cd2901 100644 --- a/crates/synth-core/src/backend.rs +++ b/crates/synth-core/src/backend.rs @@ -401,6 +401,13 @@ pub struct CompileConfig { /// `call_indirect` lowering needs the 0-vs-1 result distinction for a callee /// it knows only by its static type. pub type_result_counts: Vec, + /// #851 lane L3: the STRUCTURAL signature class id per function type (see + /// [`crate::wasm_decoder::DecodedModule::structural_type_class_ids`]). The + /// aarch64 `call_indirect` type check compares this, not the raw type index + /// — WASM type equality is structural. Distinct from + /// `call_indirect_guards.type_class_ids`, which the ARM path populates only + /// when its heterogeneous-table sidecar exists. + pub type_class_ids: Vec, /// #851 lane L3, aarch64 only — the driver has EMITTED the module-level /// substrate the globals and `call_indirect` lowerings address: the `.data` /// globals image (`__synth_globals`) and the `.text` funcref table @@ -513,6 +520,7 @@ impl Default for CompileConfig { // this from the decoded module. call_indirect_guards: crate::wasm_decoder::CallIndirectGuards::default(), type_result_counts: Vec::new(), + type_class_ids: Vec::new(), a64_substrate_emitted: false, // #778 phase 2: no --wcet-hints file ⇒ no hints. Consulted ONLY by // the WCET sidecar computation — never by codegen (the emitted From 44e32c44e7a16beff48bf62c710e95d19038e2f6 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 30 Jul 2026 15:25:03 +0200 Subject: [PATCH 6/9] aarch64: CI-wired execution oracles for globals + call_indirect (#851) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two unicorn-vs-wasmtime differentials, both wired into the `aarch64-oracle` job in this commit with `set -o pipefail` and a non-zero-count grep (the #890 "oracle exists and runs nowhere" class). `aarch64_globals_851_differential.py` — 17 checks, 6 exports. Reads the INITIAL values before anything is written (a region shipping zeros fails), then runs the cases IN SEQUENCE against ONE region so a dropped or misdirected `global.set` shows up in the next `global.get`. i32 and i64 globals are interleaved, so a wrong slot stride shifts every later global. `aarch64_call_indirect_851_differential.py` — 35 checks (23 trap, 12 value), 6 exports. All three §4.4.8 traps, plus the direction an "always trap" lowering would hide: a structurally-DUPLICATE type must NOT trap. Both harnesses act as the LINKER — they place `.text` and `.data` on different pages and resolve ADRP page / ADD lo12 / JUMP26 themselves — so a wrong page delta, lo12, or trampoline displacement diverges rather than passing. RED-FIRST, and it earned its keep: the first version of the call_indirect oracle PASSED a compiler with the bounds guard removed. Past-the-end bytes read as class id 0, so the TYPE check trapped anyway and masked it. The fixture now declares TWO tables, making index 4 of table 0 land on table 1's fully valid, type-matching `$mul` slot — so only the bounds guard can trap there, and the same fixture makes a dropped per-table base offset return 30-vs-13 instead of agreeing by coincidence. Five injected miscompiles are now caught: weakened bounds guard -> differential red (4 BUG lines) dropped base offset -> differential red (2 BUG lines) removed type check -> differential red (6 BUG lines) null slot made callable -> differential red (2 BUG lines) dense globals layout -> differential red (4 BUG lines) One injection is NOT decidable by execution: a SIGNED bounds compare (`b.lt` for `b.lo`). Under emulation a negative index passes the signed guard and then faults on the unmapped scaled address, so it traps either way — but on real silicon that address can be mapped and the dispatch would branch into it. It is pinned instead by `call_indirect_guard_sequence_uses_an_unsigned_bounds_compare`, which asserts the whole guard sequence word-for-word (verified red: exit 101 when only the shipped code, not the expectation, is mutated). Plus fail-safe and scaling unit tests: both features decline under a default `ModuleCtx`, the slot offset is size-scaled per access width, and a global index past the region declines. Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .github/workflows/ci.yml | 25 ++ crates/synth-backend-aarch64/src/selector.rs | 167 ++++++++++ scripts/repro/aarch64_call_indirect_851.wat | 80 +++++ .../aarch64_call_indirect_851_differential.py | 309 ++++++++++++++++++ scripts/repro/aarch64_globals_851.wat | 36 ++ .../repro/aarch64_globals_851_differential.py | 284 ++++++++++++++++ 6 files changed, 901 insertions(+) create mode 100644 scripts/repro/aarch64_call_indirect_851.wat create mode 100644 scripts/repro/aarch64_call_indirect_851_differential.py create mode 100644 scripts/repro/aarch64_globals_851.wat create mode 100644 scripts/repro/aarch64_globals_851_differential.py diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 388a00b5..5eb15b39 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -480,6 +480,31 @@ jobs: # AAPCS64 x-view hazard), drop/nop, fixed-memory size/grow parity # against a min=max module (growth failure is spec-forced there). run: SYNTH=./target/debug/synth python scripts/repro/aarch64_surface_851_differential.py + - name: Run #851 lane L3 GLOBALS execution oracle (emitted .data region + persistence) + # synth EMITS the globals region (a `.data` image carrying the decoded + # initializers) and reaches it `adrp`+`add :lo12:` — no base register, + # no precondition. The harness places `.text` and `.data` on DIFFERENT + # pages and resolves the relocations itself, so a wrong page delta or + # lo12 lands on the wrong bytes. NON-VACUITY: assert a non-zero check + # count (a harness that compiled nothing would otherwise pass silently). + run: | + set -o pipefail + out=$(SYNTH=./target/debug/synth \ + python scripts/repro/aarch64_globals_851_differential.py | tee /dev/stderr) + echo "$out" | grep -Eq '^[1-9][0-9]* checks across [1-9][0-9]* exported' \ + || { echo "VACUOUS: globals oracle reported no checks"; exit 1; } + - name: Run #851 lane L3 CALL_INDIRECT execution oracle (§4.4.8 OOB + null + type traps) + # A64's `blr` is TOTAL; WASM §4.4.8 is not. All three traps must fire + # exactly where wasmtime traps — and the structurally-DUPLICATE type + # must NOT trap (the direction an "always trap" lowering would hide). + # NON-VACUITY: assert non-zero counts in BOTH directions, so a run that + # only trapped (or only returned values) fails. + run: | + set -o pipefail + out=$(SYNTH=./target/debug/synth \ + python scripts/repro/aarch64_call_indirect_851_differential.py | tee /dev/stderr) + echo "$out" | grep -Eq '^[1-9][0-9]* checks \([1-9][0-9]* trap, [1-9][0-9]* value\)' \ + || { echo "VACUOUS: call_indirect oracle reported no trap/value checks"; exit 1; } - name: Run decline-matrix honesty oracle run: SYNTH=./target/debug/synth python scripts/repro/aarch64_m2_decline_538.py diff --git a/crates/synth-backend-aarch64/src/selector.rs b/crates/synth-backend-aarch64/src/selector.rs index 45828fc1..6d07b412 100644 --- a/crates/synth-backend-aarch64/src/selector.rs +++ b/crates/synth-backend-aarch64/src/selector.rs @@ -2379,6 +2379,173 @@ mod tests { assert_eq!(w, vec![enc::add(9, 0, 1), enc::mov_reg64(0, 9), enc::ret()]); } + /// #851 lane L3 — the exact `call_indirect` guard sequence. + /// + /// The execution differential covers BEHAVIOUR, but it cannot distinguish + /// the UNSIGNED bounds compare (`b.lo`) from a signed one (`b.lt`): under + /// emulation a negative index passes a signed guard and then faults on the + /// unmapped scaled address, so it traps either way. On real silicon that + /// address can be MAPPED, and the dispatch would branch into it. The + /// condition is therefore pinned here, where it is decidable. + #[test] + fn call_indirect_guard_sequence_uses_an_unsigned_bounds_compare() { + let ops = vec![ + WasmOp::LocalGet(0), + WasmOp::CallIndirect { + type_index: 0, + table_index: 0, + }, + WasmOp::End, + ]; + let ctx = ModuleCtx { + substrate_emitted: true, + global_is64: vec![], + tables: vec![(4, 0)], + type_class_ids: vec![3], + type_arg_counts: vec![0], + type_result_counts: vec![0], + type_ret_float: vec![false], + }; + let (w, _sites, relocs) = select_typed_cf_calls( + &ops, + 1, + &[], + &[], + &[], + 0, + &[], + &[], + &[], + MemBounds::Unchecked, + &ctx, + ) + .unwrap(); + // Prologue: stp x29,x30 ; sub sp,#16 ; str x0,[sp] (param homing) ; + // ldr x9,[sp] (local.get 0). + assert_eq!(w[0], enc::stp_fp_lr_pre16()); + assert_eq!(w[2], enc::str_x_imm(0, enc::SP, 0)); + assert_eq!(w[3], enc::ldr_x_imm(9, enc::SP, 0)); + // Guard 1 — OOB. UNSIGNED (`Lo`), so 0xFFFFFFFF is ABOVE 4, not below. + assert_eq!(w[4], enc::cmp_imm(9, 4)); + assert_eq!( + w[5], + enc::bcond(Cond::Lo, 2), + "the table bounds compare must be UNSIGNED (b.lo): a signed b.lt \ + lets a negative index through, and uxtw then scales it into an \ + address that can be mapped on real silicon" + ); + assert_eq!(w[6], enc::brk(0)); + // Table address: adrp+add (relocated), then + idx*8. + assert_eq!(w[7], enc::adrp(IP0, 0)); + assert_eq!(w[8], enc::add_imm64(IP0, IP0, 0)); + assert_eq!(w[9], enc::add_ext_uxtw_sh(IP0, IP0, 9, 3)); + // Guard 2 — the structural class id (which is also the null check). + assert_eq!(w[10], enc::ldr_w(IP1, IP0, 0)); + assert_eq!(w[11], enc::cmp_imm(IP1, 3)); + assert_eq!(w[12], enc::bcond(Cond::Eq, 2)); + assert_eq!(w[13], enc::brk(0)); + // Branch into the slot's trampoline at slot+4. + assert_eq!(w[14], enc::add_imm64(IP0, IP0, 4)); + assert_eq!(w[15], enc::blr(IP0)); + // The adrp/add pair must carry its two relocations against the table. + assert_eq!(relocs.len(), 2); + assert!(relocs.iter().all(|r| r.symbol == FUNC_TABLE_SYMBOL)); + assert_eq!(relocs[0].offset, 7 * 4); + assert!(matches!(relocs[0].kind, RelocKind::AArch64AdrPrelPgHi21)); + assert_eq!(relocs[1].offset, 8 * 4); + assert!(matches!(relocs[1].kind, RelocKind::AArch64AddAbsLo12Nc)); + } + + /// Both module-level features are FAIL-SAFE: with the default context (no + /// substrate emitted) they LOUD-DECLINE rather than address a region the + /// driver never placed. + #[test] + fn globals_and_call_indirect_decline_without_an_emitted_substrate() { + for ops in [ + vec![WasmOp::GlobalGet(0), WasmOp::End], + vec![WasmOp::I32Const(1), WasmOp::GlobalSet(0), WasmOp::End], + vec![ + WasmOp::I32Const(0), + WasmOp::CallIndirect { + type_index: 0, + table_index: 0, + }, + WasmOp::End, + ], + ] { + let r = sel_calls(&ops, 0, 0, &[0], &[0]); + assert!( + r.is_err(), + "must decline without an emitted substrate: {ops:?}" + ); + } + } + + /// The globals lowering addresses `__synth_globals + k*8` with a SIZE-SCALED + /// immediate: `k*2` for the `w` view, `k` for the `x` view. Getting the + /// scaling wrong reads a neighbouring slot. + #[test] + fn global_get_scales_the_slot_offset_per_access_width() { + let ctx = ModuleCtx { + substrate_emitted: true, + global_is64: vec![false, true, false], + ..ModuleCtx::default() + }; + let sel = |ops: Vec| { + select_typed_cf_calls( + &ops, + 0, + &[], + &[], + &[], + 0, + &[], + &[], + &[], + MemBounds::Unchecked, + &ctx, + ) + .unwrap() + }; + // global 2 is i32 → byte offset 16 → `ldr w` scaled immediate 4. + let (w, _, _) = sel(vec![WasmOp::GlobalGet(2), WasmOp::End]); + assert_eq!(w[0], enc::adrp(9, 0)); + assert_eq!(w[1], enc::add_imm64(9, 9, 0)); + assert_eq!(w[2], enc::ldr_w(9, 9, 4)); + // global 1 is i64 → byte offset 8 → `ldr x` scaled immediate 1. + let (w, _, _) = sel(vec![WasmOp::GlobalGet(1), WasmOp::End]); + assert_eq!(w[2], enc::ldr_x(9, 9, 1)); + // A store mirrors it, and the base temp must DIFFER from the value. + let (w, _, _) = sel(vec![WasmOp::I32Const(7), WasmOp::GlobalSet(2), WasmOp::End]); + let store = w[w.len() - 2]; + assert_eq!(store, enc::str_w(9, 10, 4)); + } + + /// A global index past the emitted region LOUD-DECLINES. + #[test] + fn global_index_past_the_region_declines() { + let ctx = ModuleCtx { + substrate_emitted: true, + global_is64: vec![false], + ..ModuleCtx::default() + }; + let ops = vec![WasmOp::GlobalGet(5), WasmOp::End]; + let r = select_typed_cf_calls( + &ops, + 0, + &[], + &[], + &[], + 0, + &[], + &[], + &[], + MemBounds::Unchecked, + &ctx, + ); + assert!(r.is_err()); + } + #[test] fn call_to_import_loud_declines() { // func 0 is an import (num_imports = 1); calling it declines. diff --git a/scripts/repro/aarch64_call_indirect_851.wat b/scripts/repro/aarch64_call_indirect_851.wat new file mode 100644 index 00000000..f3d94e39 --- /dev/null +++ b/scripts/repro/aarch64_call_indirect_851.wat @@ -0,0 +1,80 @@ +;; #851 lane L3 — aarch64 `call_indirect` execution differential fixture. +;; +;; Shaped so all THREE WASM §4.4.8 traps are reachable from an exported entry +;; whose index is a PARAMETER (the realistic shape — and the one that needed +;; param homing to compile at all). +;; +;; TWO tables, because the emitted funcref region is CONTIGUOUS across tables: +;; +;; region slot 0 1 2 3 4 5 +;; table 0 $add $sub $neg NULL +;; table 1 $mul $add +;; +;; That makes index 4 of TABLE 0 land on a slot that is fully valid — a real +;; `$bin` trampoline whose structural class id MATCHES what "bin" expects. So +;; the out-of-range trap can only come from the bounds guard: a lowering that +;; dropped it would happily CALL table 1's `$add` and return 13 where wasmtime +;; traps. Without a second table the type check masks a missing bounds guard +;; (past-the-end bytes read as class id 0, which mismatches anyway) and the +;; oracle would pass a genuinely unsound compiler. +;; +;; `$bin2` is a structurally-identical DUPLICATE of `$bin`: dispatching it at a +;; `$bin` function MUST succeed, because WASM type equality is structural. A +;; lowering that compared raw type INDICES would trap there — a trap where +;; wasmtime calls, the mirror-image bug that "just always trap" would hide. +(module + (type $bin (func (param i32 i32) (result i32))) + (type $un (func (param i32) (result i32))) + (type $bin2 (func (param i32 i32) (result i32))) ;; structurally == $bin + (type $void (func)) + + (table 4 funcref) ;; table 0 + (table 2 funcref) ;; table 1 + (elem (i32.const 0) $add $sub $neg) ;; table 0; slot 3 NULL + (elem (table 1) (offset (i32.const 0)) func $mul $add) + + (func $add (type $bin) (i32.add (local.get 0) (local.get 1))) + (func $sub (type $bin) (i32.sub (local.get 0) (local.get 1))) + (func $neg (type $un) (i32.sub (i32.const 0) (local.get 0))) + ;; Table 1 slot 0 deliberately holds a DIFFERENT function than region slot 0, + ;; so dropping the per-table base offset changes the RESULT (30 vs 13) rather + ;; than silently agreeing. + (func $mul (type $bin) (i32.mul (local.get 0) (local.get 1))) + + ;; Dispatch a BINARY callee through TABLE 0. Index from a parameter. + ;; idx 0/1 -> add/sub idx 2 -> TYPE MISMATCH ($neg is unary) + ;; idx 3 -> NULL SLOT idx >= 4 -> OUT OF RANGE (and idx 4/5 land on + ;; table 1's valid, type-matching slots) + (func (export "bin") (param i32 i32 i32) (result i32) + (call_indirect 0 (type $bin) + (local.get 0) (local.get 1) (local.get 2))) + + ;; The DUPLICATE type: must behave EXACTLY like "bin" (structural equality). + (func (export "bin_dup") (param i32 i32 i32) (result i32) + (call_indirect 0 (type $bin2) + (local.get 0) (local.get 1) (local.get 2))) + + ;; TABLE 1 — proves the per-table base offset is applied: index 0 here must + ;; reach REGION slot 4 ($mul), not region slot 0 ($add). The contents differ + ;; deliberately, so a dropped base offset returns 30-vs-13 instead of + ;; agreeing by coincidence. + (func (export "bin_t1") (param i32 i32 i32) (result i32) + (call_indirect 1 (type $bin) + (local.get 0) (local.get 1) (local.get 2))) + + ;; Dispatch a UNARY callee through table 0. + ;; idx 2 -> neg idx 0/1 -> TYPE MISMATCH idx 3 -> NULL >=4 -> OOB + (func (export "un") (param i32 i32) (result i32) + (call_indirect 0 (type $un) (local.get 0) (local.get 1))) + + ;; A dispatch whose expected type matches NOTHING in either table: every + ;; index must trap, including the in-range initialized ones. + (func (export "novoid") (param i32) + (call_indirect 0 (type $void) (local.get 0))) + + ;; The result of an indirect call feeds further arithmetic, so a dispatch that + ;; returned the wrong register (or clobbered the value stack) is visible. + (func (export "chained") (param i32) (result i32) + (i32.mul + (call_indirect 0 (type $bin) (i32.const 7) (i32.const 5) (local.get 0)) + (i32.const 3)))) diff --git a/scripts/repro/aarch64_call_indirect_851_differential.py b/scripts/repro/aarch64_call_indirect_851_differential.py new file mode 100644 index 00000000..213a65d0 --- /dev/null +++ b/scripts/repro/aarch64_call_indirect_851_differential.py @@ -0,0 +1,309 @@ +#!/usr/bin/env python3 +"""#851 lane L3 — aarch64 `call_indirect` execution differential vs wasmtime. + +A64's `blr` is TOTAL: it branches wherever the register points. WASM §4.4.8 is +not — an indirect call TRAPS on an out-of-range index, on a null (uninitialized) +table slot, and on a signature mismatch. That gap is the #709 "more total than +WASM" silent-miscompile class, so the three traps are the POINT of this harness, +not a footnote: every one is asserted to fire exactly where wasmtime traps. + +The dispatch it validates: + + cmp w_idx,#size / b.lo +2 / brk out-of-range index + adrp+add / add x16,x16,w_idx,uxtw#3 slot address (no base register) + ldr w17,[x16] / cmp w17,#class signature mismatch — and, since a + b.eq +2 / brk null slot's id is 0 and every real + class is >= 1, the null check too + add x16,x16,#4 / blr x16 the slot's `b func_N` trampoline + +What makes it non-vacuous: + * the harness acts as the LINKER — it places `.text` itself and resolves the + ADRP page / ADD lo12 / JUMP26 relocations, so a wrong table address or a + wrong trampoline displacement calls the WRONG function and diverges; + * BOTH directions are covered. Traps must fire (a missing guard = a wrong + call), and the STRUCTURALLY-DUPLICATE type must NOT trap — a lowering that + compared raw type indices would reject it, which is a trap where wasmtime + calls (the mirror-image bug that "just always trap" would hide); + * the expected column is taken from wasmtime FIRST, so the table cannot drift; + * trap and value cases are counted separately and both must be non-zero. + +Run (needs wasmtime + unicorn + pyelftools): + SYNTH=/debug/synth python scripts/repro/aarch64_call_indirect_851_differential.py +""" + +import os +import struct +import subprocess +import sys +from pathlib import Path + +import wasmtime +from elftools.elf.elffile import ELFFile +from unicorn import UC_ARCH_ARM64, UC_MODE_ARM, Uc, UcError +from unicorn.arm64_const import ( + UC_ARM64_REG_LR, + UC_ARM64_REG_SP, + UC_ARM64_REG_W0, + UC_ARM64_REG_X0, + UC_ARM64_REG_X1, + UC_ARM64_REG_X2, +) + +WAT = Path(__file__).with_name("aarch64_call_indirect_851.wat") +SYNTH = os.environ.get("SYNTH", "./target/debug/synth") + +CODE, DATA, STK, RET = 0x100000, 0x400000, 0x200000, 0x300000 +X_ARGS = [UC_ARM64_REG_X0, UC_ARM64_REG_X1, UC_ARM64_REG_X2] + +M32 = (1 << 32) - 1 +M64 = (1 << 64) - 1 +TRAP = "TRAP" + +R_AARCH64_ADR_PREL_PG_HI21 = 275 +R_AARCH64_ADD_ABS_LO12_NC = 277 +R_AARCH64_CALL26 = 283 +R_AARCH64_JUMP26 = 282 + +# fn -> ([arg widths], ret width or None for void). +SIGS = { + "bin": ([32, 32, 32], 32), + "bin_dup": ([32, 32, 32], 32), + "bin_t1": ([32, 32, 32], 32), + "un": ([32, 32], 32), + "novoid": ([32], None), + "chained": ([32], 32), +} + +# (fn, args, why). The expected value/trap comes from wasmtime, never from here. +CASES = [ + # ---- in-range, correctly-typed dispatches (the value direction) ---- + ("bin", [10, 3, 0], "slot 0 = add -> 13"), + ("bin", [10, 3, 1], "slot 1 = sub -> 7"), + ("bin", [0, 1, 1], "sub underflow -> -1"), + ("bin", [0x7FFFFFFF, 0xFFFFFFFF, 0], "add wraps"), + ("un", [42, 2], "slot 2 = neg -> -42"), + ("un", [0x80000000, 2], "neg(INT_MIN) wraps to itself"), + ("chained", [0], "(7+5)*3 = 36 — the result feeds more arithmetic"), + ("chained", [1], "(7-5)*3 = 6"), + # ---- STRUCTURAL type equality: a DUPLICATE type must NOT trap ---- + # This is the direction "always trap" would silently pass; a lowering that + # compared raw type indices would reject these, trapping where wasmtime calls. + ("bin_dup", [10, 3, 0], "duplicate type at add -> 13, must NOT trap"), + ("bin_dup", [10, 3, 1], "duplicate type at sub -> 7, must NOT trap"), + # ---- TRAP: signature mismatch ---- + ("bin", [10, 3, 2], "slot 2 is unary, expected binary -> type mismatch"), + ("bin_dup", [10, 3, 2], "same via the duplicate type"), + ("un", [42, 0], "slot 0 is binary, expected unary -> type mismatch"), + ("un", [42, 1], "slot 1 is binary, expected unary -> type mismatch"), + ("novoid", [0], "no table entry has the void type -> mismatch"), + ("novoid", [2], "ditto at another initialized slot"), + # ---- TRAP: null (uninitialized) slot ---- + ("bin", [10, 3, 3], "slot 3 was never initialized -> null element"), + ("un", [42, 3], "null slot via the unary dispatch"), + ("novoid", [3], "null slot via the void dispatch"), + ("chained", [3], "null slot reached through the chained entry"), + # ---- TABLE 1: the per-table BASE OFFSET must be applied ---- + # $mul at region slot 4, NOT $add at region slot 0 — 30 vs 13. + ("bin_t1", [10, 3, 0], "table 1 slot 0 = region slot 4 = mul -> 30"), + ("bin_t1", [10, 3, 1], "table 1 slot 1 = region slot 5 = add -> 13"), + ("bin_t1", [10, 3, 2], "past table 1's 2 entries -> out of range"), + ("bin_t1", [10, 3, 0xFFFFFFFF], "unsigned OOB on table 1"), + # ---- TRAP: out-of-range index ---- + # 4 and 5 are the LOAD-BEARING pair: they land on table 1's slots, which + # are fully valid `$bin` trampolines with a MATCHING class id. Only the + # bounds guard can trap here — drop it and these return 13 / 7 instead. + ("bin", [10, 3, 4], "OOB onto table 1's valid, type-matching mul slot"), + ("bin", [10, 3, 5], "OOB onto table 1's valid, type-matching add slot"), + ("bin_dup", [10, 3, 4], "same, via the duplicate type"), + ("chained", [4], "same, through the chained entry"), + ("bin", [10, 3, 0x7FFFFFFF], "large positive index"), + ("bin", [10, 3, 0xFFFFFFFF], "0xFFFFFFFF — UNSIGNED compare: a signed one " + "would read it as -1 and fall through"), + ("bin", [10, 3, 0x80000000], "sign bit set — same unsigned-compare trap"), + ("un", [42, 4], "out of range via the unary dispatch"), + ("un", [42, 6], "further past the end"), + ("novoid", [9], "out of range via the void dispatch"), + ("chained", [0xFFFFFFFF], "out of range through the chained entry"), +] + + +def wasmtime_run(fn, args, sig): + """Fresh instance per call — the table is immutable here, so no state + needs to carry over, and a trap leaves nothing behind.""" + engine = wasmtime.Engine() + module = wasmtime.Module.from_file(engine, str(WAT)) + store = wasmtime.Store(engine) + f = wasmtime.Instance(store, module, []).exports(store)[fn] + widths, ret = sig + conv = [] + for w, a in zip(widths, args): + if w == 32: + conv.append(struct.unpack("= 0 and shndx == data_idx: + a = DATA + sy["st_value"] + else: + continue + sym_addr[i] = a + if sy.name: + by_name.setdefault(sy.name, a) + + applied = {} + rela = f.get_section_by_name(".rela.text") + if rela is not None: + for r in rela.iter_relocations(): + r_off = r["r_offset"] + r_type = r["r_info_type"] + r_sym = r["r_info"] >> 32 + target = sym_addr.get(r_sym) + if target is None: + sys.exit(f"relocation against an unplaced symbol (index {r_sym})") + site = CODE + r_off + word = struct.unpack_from("> 12) - (site >> 12)) & 0x1FFFFF + word &= ~((0x3 << 29) | (0x7FFFF << 5)) + word |= (v & 0x3) << 29 + word |= ((v >> 2) & 0x7FFFF) << 5 + elif r_type == R_AARCH64_ADD_ABS_LO12_NC: + word = (word & ~(0xFFF << 10)) | ((s & 0xFFF) << 10) + else: + sys.exit(f"unexpected relocation type {r_type}") + struct.pack_into("/debug/synth python scripts/repro/aarch64_globals_851_differential.py +""" + +import os +import struct +import subprocess +import sys +from pathlib import Path + +import wasmtime +from elftools.elf.elffile import ELFFile +from unicorn import UC_ARCH_ARM64, UC_MODE_ARM, Uc, UcError +from unicorn.arm64_const import ( + UC_ARM64_REG_LR, + UC_ARM64_REG_SP, + UC_ARM64_REG_W0, + UC_ARM64_REG_X0, + UC_ARM64_REG_X1, + UC_ARM64_REG_X2, +) + +WAT = Path(__file__).with_name("aarch64_globals_851.wat") +SYNTH = os.environ.get("SYNTH", "./target/debug/synth") + +# Deliberately on DIFFERENT 4 KiB pages, and far enough apart that the ADRP +# page delta is non-zero — a harness that placed them on one page would not +# exercise the relocation at all. +CODE, DATA, STK, RET = 0x100000, 0x400000, 0x200000, 0x300000 +X_ARGS = [UC_ARM64_REG_X0, UC_ARM64_REG_X1, UC_ARM64_REG_X2] + +M32 = (1 << 32) - 1 +M64 = (1 << 64) - 1 +TRAP = "TRAP" + +R_AARCH64_ADR_PREL_PG_HI21 = 275 +R_AARCH64_ADD_ABS_LO12_NC = 277 +R_AARCH64_CALL26 = 283 +R_AARCH64_JUMP26 = 282 + +# fn -> ([arg widths], ret width). None ret = void. +SIGS = { + "get_i32": ([], 32), + "get_i64": ([], 64), + "get_second_i32": ([], 32), + "bump": ([32], 32), + "set_i64": ([64], 64), + "sum_all": ([], 64), +} + +# Executed IN ORDER against ONE region (both oracles), so persistence is tested. +CASES = [ + # --- initial values, read BEFORE anything is written --- + ("get_i32", []), # 41 + ("get_i64", []), # 1234567890123 + ("get_second_i32", []), # -7 + ("sum_all", []), # 41 + 1234567890123 + (-7) + # --- mutation persists --- + ("bump", [1]), # 42 + ("bump", [1]), # 43 + ("get_i32", []), # 43 (the store persisted) + ("bump", [0xFFFFFFFF]), # 42 (add -1) + ("bump", [1000]), # 1042 + # --- 64-bit slot: both words must reach the region --- + ("set_i64", [0x7FFF_FFFF_FFFF_FFFF]), + ("get_i64", []), + ("set_i64", [0xFFFF_FFFF_FFFF_FFFF]), # -1: upper word must not be lost + ("get_i64", []), + ("set_i64", [0x0000_0001_0000_0000]), # only the UPPER word is set + ("get_i64", []), + # --- the other i32 global is unaffected by all of the above --- + ("get_second_i32", []), # still -7 + ("sum_all", []), +] + + +def wasmtime_session(): + """One instance, so globals persist across the case sequence.""" + engine = wasmtime.Engine() + module = wasmtime.Module.from_file(engine, str(WAT)) + store = wasmtime.Store(engine) + inst = wasmtime.Instance(store, module, []) + exports = inst.exports(store) + + def call(fn, args, sig): + widths, _ret = sig + conv = [] + for w, a in zip(widths, args): + if w == 32: + conv.append(struct.unpack(" absolute address; also name -> address. + sym_addr, by_name = {}, {} + symtab = f.get_section_by_name(".symtab") + for i, sy in enumerate(symtab.iter_symbols()): + shndx = sy["st_shndx"] + if shndx == text_idx: + a = CODE + sy["st_value"] + elif shndx == data_idx: + a = DATA + sy["st_value"] + else: + continue + sym_addr[i] = a + if sy.name: + by_name.setdefault(sy.name, a) + + applied = {} + rela = f.get_section_by_name(".rela.text") + if rela is not None: + for r in rela.iter_relocations(): + r_off = r["r_offset"] + r_type = r["r_info_type"] + r_sym = r["r_info"] >> 32 + addend = r["r_addend"] + target = sym_addr.get(r_sym) + if target is None: + sys.exit(f"relocation against an unplaced symbol (index {r_sym})") + site = CODE + r_off + word = struct.unpack_from("> 12) - (site >> 12) + v = delta & 0x1FFFFF + word &= ~((0x3 << 29) | (0x7FFFF << 5)) + word |= (v & 0x3) << 29 + word |= ((v >> 2) & 0x7FFFF) << 5 + elif r_type == R_AARCH64_ADD_ABS_LO12_NC: + word = (word & ~(0xFFF << 10)) | ((s & 0xFFF) << 10) + else: + sys.exit(f"unexpected relocation type {r_type}") + struct.pack_into(" Date: Thu, 30 Jul 2026 15:27:48 +0200 Subject: [PATCH 7/9] =?UTF-8?q?docs:=20aarch64=20globals=20+=20call=5Findi?= =?UTF-8?q?rect=20=E2=80=94=20precondition=20status=20pinned=20(#851)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The FEATURE_MATRIX template row now says plainly what v0.52's cold review caught the last version of this doc getting wrong: the globals region and the funcref table are EMITTED BY SYNTH, not preconditions. `x28` (the linear-memory base) remains the ONE aarch64 precondition, and the row says so in those words, so a reader cannot come away thinking lane L3 added a second ambient input. The row also enumerates the new LOUD DECLINES by name rather than implying full coverage: imported globals, a global with no decoded const initializer, a non-leaf float param, a growable imported table, an unverifiable element segment, and a table slot holding an imported function. Two new `claims.yaml` pins hold those claims to evidence, both verified RED-FIRST: SYNTH-MATRIX-AARCH64-EMITTED-NOT-PRECONDITION — flipping the sentence to "are ALSO preconditions" reddens the gate; pinned to substrate.rs, the `.data` DataBlob, and the ADRP relocation kind actually being emitted. SYNTH-MATRIX-AARCH64-CALL-INDIRECT-TRAPS — unwiring either oracle from ci.yml reddens the gate, so the §4.4.8 trap claim cannot outlive its execution evidence. `aarch64_selector_ops` 161 -> 164 (global.get, global.set, call_indirect). Generated status files regenerated with the script (NOT hand-edited); the coordinator should re-run `--emit-status` once after the lane fan-in, since every aarch64 lane moves this counter. Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- CHANGELOG.md | 59 ++++++++++++++++++++++++ artifacts/status.json | 2 +- claims.yaml | 42 +++++++++++++++++ docs/status/FEATURE_MATRIX.md | 2 +- scripts/templates/feature_matrix.md.tmpl | 2 +- 5 files changed, 104 insertions(+), 3 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index bcd6fdcc..38418d90 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,6 +7,65 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ## [Unreleased] +### Added + +- **aarch64 `call_indirect` and WASM globals — the two largest remaining + structural declines on that backend (#851).** Both were "no substrate" gaps, + not missing selector arms, so the lane is mostly about *where the data lives*. + + **Precondition status, stated plainly: this lane adds NONE.** synth EMITS both + regions into the object and reaches them with an `adrp` + `add :lo12:` pair + the linker resolves. Globals live in a synth-emitted `.data` section + (`__synth_globals`) carrying each global's decoded constant initializer; the + funcref table is a synth-emitted `.text`-resident array (`__synth_func_table`). + Neither needs a base register, a startup, a linker script or an ambient input. + That is deliberately *unlike* `x28` — the linear-memory base, which remains + the ONE aarch64 precondition the embedder must supply, exactly as v0.53 + documented it. Using PC-relative addressing rather than a dedicated base + register also removes the #275/#717 collision class by construction: there is + no base register to collide with. + + `call_indirect` emits all THREE WASM §4.4.8 trap guards inline, because A64's + `blr` is total and gives none of them for free (the #709 + "more-total-than-WASM" class): an **out-of-range index** (an UNSIGNED bounds + compare), a **null slot**, and a **signature mismatch**. Each table slot is an + 8-byte `[u32 structural-class-id][b func_N]` record — null slots are + `[0][brk #0]` — so one compare serves as both the type check and the null + check (id 0 matches no real class, which is ≥ 1). The compared id is + **structural**, so a module carrying duplicate-but-identical types keeps them + interchangeable; comparing raw type indices would trap where wasmtime calls. + + **Param homing** landed as the prerequisite: a non-leaf function referencing a + parameter used to loud-decline, and a table index almost always *is* a + parameter, so `call_indirect` would only have dispatched on constants. Non-leaf + functions now give every local an 8-byte stack slot and store the incoming + argument registers there at the prologue. Leaf functions are byte-identical. + + Execution-verified against wasmtime under unicorn, CI-wired in the + `aarch64-oracle` job: `aarch64_globals_851_differential.py` (17 checks — + initial values, i32/i64 slots, stores persisting across calls) and + `aarch64_call_indirect_851_differential.py` (35 checks, 23 of them traps — + every §4.4.8 trap, plus the duplicate type that must NOT trap). The + `call_indirect` fixture declares TWO tables on purpose: the first version of + that oracle PASSED a compiler with the bounds guard removed, because + past-the-end bytes read as class id 0 and the type check trapped anyway. With + a second table, index 4 of table 0 lands on a fully valid, type-matching slot, + so only the bounds guard can trap there. + + Rather than guess, these shapes LOUD-DECLINE with a machine reason: an + imported global, a global with no decoded constant initializer (float, v128 or + a non-const init expr), a growable imported table, an element segment that is + not statically verifiable, a table slot holding an imported function, a + non-leaf FLOAT parameter, and anything past the 12-bit guard immediates. The + unverifiable-element-segment decline is the load-bearing one: the existing + region reconstruction degrades such a table to all-null, which would trap on + every dispatch — conservative-*looking*, but wrong in the other direction. + + The VCR-SEL-005 third-backend parity gate flips `global.get`, `global.set` and + `call_indirect` from `Err(reason)` to lowering in the same commit that makes + them lower, and two new `claims.yaml` pins hold the precondition and trap + claims to their evidence. + ## [0.53.0] - 2026-07-30 **"The last mile" — seven lanes.** falcon's VFP wall comes down, RISC-V compiles diff --git a/artifacts/status.json b/artifacts/status.json index 5ec9905a..5bf811ae 100644 --- a/artifacts/status.json +++ b/artifacts/status.json @@ -1,5 +1,5 @@ { - "aarch64_selector_ops": 161, + "aarch64_selector_ops": 164, "arm_refinement_assumed_connection": 5, "arm_semantics_axioms": 72, "backends": [ diff --git a/claims.yaml b/claims.yaml index 7602948b..17a520b6 100644 --- a/claims.yaml +++ b/claims.yaml @@ -810,6 +810,48 @@ claims: glob: ['crates/synth-backend-aarch64/src/selector.rs'] min: 1 + # #851 lane L3 — the load-bearing HONESTY claim of this lane. v0.52's cold + # review caught a doc that described a shipped feature as "not yet"; v0.53 + # made the `x28` precondition explicit so the NEXT feature could not quietly + # add a second one. This pin holds that line: if globals or the funcref table + # ever become an ambient input the embedder must supply, the sentence claiming + # they are EMITTED must change with it, and the gate reddens until it does. + - id: SYNTH-MATRIX-AARCH64-EMITTED-NOT-PRECONDITION + doc: scripts/templates/feature_matrix.md.tmpl + text: "The globals region and the funcref table are explicitly **NOT** preconditions: synth EMITS both into the object with their contents" + evidence: + # The single producer of both regions — if this file goes, the claim goes. + - kind: file-exists + path: crates/synth-backend-aarch64/src/substrate.rs + # The regions are placed in the object, not assumed: a `.data` blob and a + # `.text`-resident table, reached PC-relatively (no base register). + - kind: count-min + pattern: 'DataBlob' + glob: ['crates/synth-backend-aarch64/src/elf.rs'] + min: 1 + - kind: count-min + pattern: 'AArch64AdrPrelPgHi21' + glob: ['crates/synth-backend-aarch64/src/selector.rs'] + min: 1 + + # #851 lane L3 — all THREE §4.4.8 traps are EMITTED, not inherited from `blr` + # (which is total). Pinned to both oracles being CI-wired, so the claim cannot + # outlive its evidence. + - id: SYNTH-MATRIX-AARCH64-CALL-INDIRECT-TRAPS + doc: scripts/templates/feature_matrix.md.tmpl + text: "all THREE WASM §4.4.8 trap guards emitted inline: out-of-range index (UNSIGNED bounds compare), null slot, and signature mismatch" + evidence: + - kind: file-exists + path: scripts/repro/aarch64_call_indirect_851_differential.py + - kind: count-min + pattern: 'aarch64_call_indirect_851_differential\.py' + glob: ['.github/workflows/ci.yml'] + min: 1 + - kind: count-min + pattern: 'aarch64_globals_851_differential\.py' + glob: ['.github/workflows/ci.yml'] + min: 1 + - id: SYNTH-MATRIX-AARCH64-DIVREM-POPCNT doc: scripts/templates/feature_matrix.md.tmpl # v0.53: the op list this sentence heads grew (select/CSEL, drop/nop, wrap, diff --git a/docs/status/FEATURE_MATRIX.md b/docs/status/FEATURE_MATRIX.md index 1c00bf09..bdd879c9 100644 --- a/docs/status/FEATURE_MATRIX.md +++ b/docs/status/FEATURE_MATRIX.md @@ -33,7 +33,7 @@ soundness feature, not an absence. | ARM Thumb-2 (primary) | `synth-backend` | `cortex-m3`, `cortex-m4`, `cortex-m4f`, `cortex-m7`, `cortex-m7dp` (+ `cortex-m55` experimental MVE) | i32 + i64 (register pairs) complete; scalar f32/f64 via VFP on FPU targets; control flow (block/loop/if/br/br_table); memory incl. sub-word; direct calls; `call_indirect` in both relocatable and self-contained `--cortex-m` images (v0.47, #275) | | ARM A32 | `synth-backend` | `cortex-r5` | i32 + i64 integer family (221-variant no-wildcard tripwire, #615); self-contained `call_indirect` declines loudly (no flash-table builder) | | RISC-V RV32IMAC | `synth-backend-riscv` | `rv32imac`, `rv32imc`, `rv32im`, `rv32i`, `rv32gc`, `esp32c3` | i32 + i64 integer ops, control flow, calls incl. `call_indirect`, memory loads/stores; relocatable ELF; import/external calls emit `R_RISCV_CALL_PLT` relocations (`.rela.text`, undefined import symbols — #871) with exact-arity marshalling from the module signature tables; >8-arg / i64-arg / multi-value calls decline loudly; floats decline loudly | -| AArch64 (A64, host-native) | `synth-backend-aarch64` | `cortex-a53` (host-linkable ET_REL, `-b aarch64`) | 161 distinct WASM ops handled by the selector: i32 + i64 integer core incl. `div_s/div_u/rem_s/rem_u` (with the ÷0 + INT_MIN/−1 WASM trap guards), `popcnt`, `select` (branchless `CSEL`/`FCSEL`, all four value types), `drop`/`nop`, `i32.wrap_i64`, `i64.extend_i32_{s,u}`, and the five `extend8/16/32_s` sign extensions (#851 v0.53); scalar f32/f64 incl. domain-guarded trapping float→int truncations, IEEE 754-2019 min/max, copysign, and f64↔i64 reinterpret (#538 milestone 4, #851); full control flow — `block`/`loop`/`if`/`else`/`br`/`br_if`/`return` (#538 cf + #851); non-param locals — zero-init stack slots with copy-semantics get/set/tee (#856); linear-memory `i32`/`i64` load/store incl. all sub-word sign/zero forms, **BOUNDS-CHECKED by default** — an out-of-bounds access traps (`brk`) exactly where wasmtime traps, and `--safety-bounds` selects the strategy (`software` = the enforcing default, `none` = explicit opt-out; `mask`/`mpu` hard-error rather than silently degrading) (#851, #865 — execution-verified against the OOB table); fixed-memory `memory.size`/`memory.grow` (declared-min page count; `grow(0)` ≡ size, `grow(n>0)` → −1 — growth failure is spec-permitted and keeps the static bounds limit sound); direct calls (AAPCS64 + `R_AARCH64_CALL26`, #851). **PRECONDITION, not emitted code:** memory-using functions expect `x28` = linear-memory base on entry — synth emits NO startup or prologue that establishes it (no linker script, no data section); the embedder/harness must set it, and a module carrying **active data segments is REFUSED loudly** (v0.53 — previously the segments were silently dropped and initialized regions read zeros). Declines (loud, mechanically enumerated by the VCR-SEL-005 third-backend oracle): `call_indirect`, import calls, value-carrying blocks/loops, `br_table`, writing a PARAM local, globals, `memory.copy`/`fill`, float `ceil`/`floor`/`trunc`/`nearest`, f32/f64 load/store, i64→float converts, trapping i64-target truncations, `>8` args, float-result callees | +| AArch64 (A64, host-native) | `synth-backend-aarch64` | `cortex-a53` (host-linkable ET_REL, `-b aarch64`) | 164 distinct WASM ops handled by the selector: i32 + i64 integer core incl. `div_s/div_u/rem_s/rem_u` (with the ÷0 + INT_MIN/−1 WASM trap guards), `popcnt`, `select` (branchless `CSEL`/`FCSEL`, all four value types), `drop`/`nop`, `i32.wrap_i64`, `i64.extend_i32_{s,u}`, and the five `extend8/16/32_s` sign extensions (#851 v0.53); scalar f32/f64 incl. domain-guarded trapping float→int truncations, IEEE 754-2019 min/max, copysign, and f64↔i64 reinterpret (#538 milestone 4, #851); full control flow — `block`/`loop`/`if`/`else`/`br`/`br_if`/`return` (#538 cf + #851); non-param locals — zero-init stack slots with copy-semantics get/set/tee (#856); linear-memory `i32`/`i64` load/store incl. all sub-word sign/zero forms, **BOUNDS-CHECKED by default** — an out-of-bounds access traps (`brk`) exactly where wasmtime traps, and `--safety-bounds` selects the strategy (`software` = the enforcing default, `none` = explicit opt-out; `mask`/`mpu` hard-error rather than silently degrading) (#851, #865 — execution-verified against the OOB table); fixed-memory `memory.size`/`memory.grow` (declared-min page count; `grow(0)` ≡ size, `grow(n>0)` → −1 — growth failure is spec-permitted and keeps the static bounds limit sound); direct calls (AAPCS64 + `R_AARCH64_CALL26`, #851); **WASM globals** — `global.get`/`global.set` for i32/i64, i.e. every defined global gets an 8-byte slot in a synth-EMITTED `.data` region (`__synth_globals`) carrying its decoded constant initializer (#851 lane L3); **`call_indirect`** — a synth-EMITTED `.text`-resident funcref table (`__synth_func_table`, one `[u32 structural-class-id][b func_N]` record per slot across all tables, null slots `[0][brk #0]`) with all THREE WASM §4.4.8 trap guards emitted inline: out-of-range index (UNSIGNED bounds compare), null slot, and signature mismatch — compared on STRUCTURAL type class, so duplicate-but-identical types stay interchangeable (#851 lane L3, execution-verified against wasmtime incl. every trap); param HOMING for non-leaf functions (incoming argument registers are stored to stack slots at the prologue, so a param survives a call). **PRECONDITIONS — exactly ONE, and it is not new:** memory-using functions expect `x28` = linear-memory base on entry, and synth emits NO startup or prologue that establishes it (no linker script, no data section); the embedder/harness must set it, and a module carrying **active data segments is REFUSED loudly** (v0.53 — previously the segments were silently dropped and initialized regions read zeros). The globals region and the funcref table are explicitly **NOT** preconditions: synth EMITS both into the object with their contents, and code reaches them via an `adrp` + `add :lo12:` pair that the linker resolves — there is no globals base register and no table base register, so no second ambient input and nothing that can collide with the linear-memory base (the #275/#717 class). Loud declines (mechanically enumerated by the VCR-SEL-005 third-backend oracle): import calls, value-carrying blocks/loops, `br_table`, writing a PARAM local in a LEAF function, `memory.copy`/`fill`, float `ceil`/`floor`/`trunc`/`nearest`, f32/f64 load/store, i64→float converts, trapping i64-target truncations, `>8` args, float-result callees; and — rather than guess — an imported global, a global with no decoded constant initializer (float/v128/non-const init expr), a non-leaf FLOAT param, a growable imported table, an element segment that is not statically verifiable, and a table slot holding an imported function | --- diff --git a/scripts/templates/feature_matrix.md.tmpl b/scripts/templates/feature_matrix.md.tmpl index 0c8585ba..b5277e1b 100644 --- a/scripts/templates/feature_matrix.md.tmpl +++ b/scripts/templates/feature_matrix.md.tmpl @@ -33,7 +33,7 @@ soundness feature, not an absence. | ARM Thumb-2 (primary) | `synth-backend` | `cortex-m3`, `cortex-m4`, `cortex-m4f`, `cortex-m7`, `cortex-m7dp` (+ `cortex-m55` experimental MVE) | i32 + i64 (register pairs) complete; scalar f32/f64 via VFP on FPU targets; control flow (block/loop/if/br/br_table); memory incl. sub-word; direct calls; `call_indirect` in both relocatable and self-contained `--cortex-m` images (v0.47, #275) | | ARM A32 | `synth-backend` | `cortex-r5` | i32 + i64 integer family (221-variant no-wildcard tripwire, #615); self-contained `call_indirect` declines loudly (no flash-table builder) | | RISC-V RV32IMAC | `synth-backend-riscv` | `rv32imac`, `rv32imc`, `rv32im`, `rv32i`, `rv32gc`, `esp32c3` | i32 + i64 integer ops, control flow, calls incl. `call_indirect`, memory loads/stores; relocatable ELF; import/external calls emit `R_RISCV_CALL_PLT` relocations (`.rela.text`, undefined import symbols — #871) with exact-arity marshalling from the module signature tables; >8-arg / i64-arg / multi-value calls decline loudly; floats decline loudly | -| AArch64 (A64, host-native) | `synth-backend-aarch64` | `cortex-a53` (host-linkable ET_REL, `-b aarch64`) | {{aarch64_selector_ops}} distinct WASM ops handled by the selector: i32 + i64 integer core incl. `div_s/div_u/rem_s/rem_u` (with the ÷0 + INT_MIN/−1 WASM trap guards), `popcnt`, `select` (branchless `CSEL`/`FCSEL`, all four value types), `drop`/`nop`, `i32.wrap_i64`, `i64.extend_i32_{s,u}`, and the five `extend8/16/32_s` sign extensions (#851 v0.53); scalar f32/f64 incl. domain-guarded trapping float→int truncations, IEEE 754-2019 min/max, copysign, and f64↔i64 reinterpret (#538 milestone 4, #851); full control flow — `block`/`loop`/`if`/`else`/`br`/`br_if`/`return` (#538 cf + #851); non-param locals — zero-init stack slots with copy-semantics get/set/tee (#856); linear-memory `i32`/`i64` load/store incl. all sub-word sign/zero forms, **BOUNDS-CHECKED by default** — an out-of-bounds access traps (`brk`) exactly where wasmtime traps, and `--safety-bounds` selects the strategy (`software` = the enforcing default, `none` = explicit opt-out; `mask`/`mpu` hard-error rather than silently degrading) (#851, #865 — execution-verified against the OOB table); fixed-memory `memory.size`/`memory.grow` (declared-min page count; `grow(0)` ≡ size, `grow(n>0)` → −1 — growth failure is spec-permitted and keeps the static bounds limit sound); direct calls (AAPCS64 + `R_AARCH64_CALL26`, #851). **PRECONDITION, not emitted code:** memory-using functions expect `x28` = linear-memory base on entry — synth emits NO startup or prologue that establishes it (no linker script, no data section); the embedder/harness must set it, and a module carrying **active data segments is REFUSED loudly** (v0.53 — previously the segments were silently dropped and initialized regions read zeros). Declines (loud, mechanically enumerated by the VCR-SEL-005 third-backend oracle): `call_indirect`, import calls, value-carrying blocks/loops, `br_table`, writing a PARAM local, globals, `memory.copy`/`fill`, float `ceil`/`floor`/`trunc`/`nearest`, f32/f64 load/store, i64→float converts, trapping i64-target truncations, `>8` args, float-result callees | +| AArch64 (A64, host-native) | `synth-backend-aarch64` | `cortex-a53` (host-linkable ET_REL, `-b aarch64`) | {{aarch64_selector_ops}} distinct WASM ops handled by the selector: i32 + i64 integer core incl. `div_s/div_u/rem_s/rem_u` (with the ÷0 + INT_MIN/−1 WASM trap guards), `popcnt`, `select` (branchless `CSEL`/`FCSEL`, all four value types), `drop`/`nop`, `i32.wrap_i64`, `i64.extend_i32_{s,u}`, and the five `extend8/16/32_s` sign extensions (#851 v0.53); scalar f32/f64 incl. domain-guarded trapping float→int truncations, IEEE 754-2019 min/max, copysign, and f64↔i64 reinterpret (#538 milestone 4, #851); full control flow — `block`/`loop`/`if`/`else`/`br`/`br_if`/`return` (#538 cf + #851); non-param locals — zero-init stack slots with copy-semantics get/set/tee (#856); linear-memory `i32`/`i64` load/store incl. all sub-word sign/zero forms, **BOUNDS-CHECKED by default** — an out-of-bounds access traps (`brk`) exactly where wasmtime traps, and `--safety-bounds` selects the strategy (`software` = the enforcing default, `none` = explicit opt-out; `mask`/`mpu` hard-error rather than silently degrading) (#851, #865 — execution-verified against the OOB table); fixed-memory `memory.size`/`memory.grow` (declared-min page count; `grow(0)` ≡ size, `grow(n>0)` → −1 — growth failure is spec-permitted and keeps the static bounds limit sound); direct calls (AAPCS64 + `R_AARCH64_CALL26`, #851); **WASM globals** — `global.get`/`global.set` for i32/i64, i.e. every defined global gets an 8-byte slot in a synth-EMITTED `.data` region (`__synth_globals`) carrying its decoded constant initializer (#851 lane L3); **`call_indirect`** — a synth-EMITTED `.text`-resident funcref table (`__synth_func_table`, one `[u32 structural-class-id][b func_N]` record per slot across all tables, null slots `[0][brk #0]`) with all THREE WASM §4.4.8 trap guards emitted inline: out-of-range index (UNSIGNED bounds compare), null slot, and signature mismatch — compared on STRUCTURAL type class, so duplicate-but-identical types stay interchangeable (#851 lane L3, execution-verified against wasmtime incl. every trap); param HOMING for non-leaf functions (incoming argument registers are stored to stack slots at the prologue, so a param survives a call). **PRECONDITIONS — exactly ONE, and it is not new:** memory-using functions expect `x28` = linear-memory base on entry, and synth emits NO startup or prologue that establishes it (no linker script, no data section); the embedder/harness must set it, and a module carrying **active data segments is REFUSED loudly** (v0.53 — previously the segments were silently dropped and initialized regions read zeros). The globals region and the funcref table are explicitly **NOT** preconditions: synth EMITS both into the object with their contents, and code reaches them via an `adrp` + `add :lo12:` pair that the linker resolves — there is no globals base register and no table base register, so no second ambient input and nothing that can collide with the linear-memory base (the #275/#717 class). Loud declines (mechanically enumerated by the VCR-SEL-005 third-backend oracle): import calls, value-carrying blocks/loops, `br_table`, writing a PARAM local in a LEAF function, `memory.copy`/`fill`, float `ceil`/`floor`/`trunc`/`nearest`, f32/f64 load/store, i64→float converts, trapping i64-target truncations, `>8` args, float-result callees; and — rather than guess — an imported global, a global with no decoded constant initializer (float/v128/non-const init expr), a non-leaf FLOAT param, a growable imported table, an element segment that is not statically verifiable, and a table slot holding an imported function | --- From 9f7ebfa03e695badb34dfd840a44dbe8df80b8d7 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 30 Jul 2026 15:31:41 +0200 Subject: [PATCH 8/9] aarch64: the lane's DECLINES are gated by machine reason, not just by failing (#851) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Extends the CI-wired decline-matrix honesty oracle with the seven shapes lane L3 deliberately refuses, and upgrades the oracle itself: an entry may now pin the machine REASON its diagnostic must contain, because "it failed somehow" is not evidence that it failed for the right cause — a decline with the wrong reason is a different bug than a decline. imported global -> "imports 1 global" float global (no decoded const init) -> "no decoded constant initializer" v128 global -> (declines upstream at decode) growable imported table -> "no compile-time size" passive element segment -> "not statically verifiable" table slot holding an import -> "imported function" non-leaf FLOAT param -> "FLOAT parameter" 10/10 loud-decline, 6 with their reason asserted; the oracle also fails if NO entry carries a reason, so the new check cannot rot into a no-op. Also verified across the whole aarch64 gate set: all 14 unicorn oracles exit 0, `aarch64_calls_851.py` is 5/5 bit-identical, the `--relocatable` path emits the funcref table too, and gale's native acceptance matrix now reports 45 ops accepted / 119 native checks with an EMPTY declined frontier (baseline 32). Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- scripts/repro/aarch64_m2_decline_538.py | 69 +++++++++++++++++++++++-- 1 file changed, 65 insertions(+), 4 deletions(-) diff --git a/scripts/repro/aarch64_m2_decline_538.py b/scripts/repro/aarch64_m2_decline_538.py index bcd5f469..e0a1c325 100755 --- a/scripts/repro/aarch64_m2_decline_538.py +++ b/scripts/repro/aarch64_m2_decline_538.py @@ -23,7 +23,10 @@ SYNTH = os.environ.get("SYNTH", "./target/debug/synth") -# Each entry: (label, wat body). All must FAIL to compile with -b aarch64. +# Each entry: (label, wat body) or (label, wat body, reason_substring). All must +# FAIL to compile with -b aarch64; when a reason substring is given, the +# diagnostic must CONTAIN it — a decline with the wrong reason is a different +# bug than a decline, and "it failed somehow" is not evidence. DECLINED = [ # #851 landed div/rem (SDIV/UDIV+MSUB with WASM ÷0 + INT_MIN/-1 trap # guards), popcnt (SIMD CNT/ADDV), and f64<->i64 reinterpret — those are @@ -43,6 +46,50 @@ '(f32.floor (local.get 0)))'), ("i64.trunc_f64_s", '(func (export "f") (param f64) (result i64) ' '(i64.trunc_f64_s (local.get 0)))'), + + # ---- #851 lane L3: globals + call_indirect LOWER, but these shapes + # deliberately do NOT. Each must decline with its own machine reason — + # the lane's rule is that an unrepresentable construct fails the + # compile naming what is missing, never ships a guessed region. + ("imported global", + '(import "env" "g" (global i32)) ' + '(func (export "f") (result i32) (global.get 0))', + "imports 1 global"), + ("float global (no decoded const init)", + '(global $f (mut f32) (f32.const 1.5)) ' + '(func (export "f") (result f32) (global.get $f))', + "no decoded constant initializer"), + ("v128 global", + '(global $v (mut v128) (v128.const i32x4 1 2 3 4)) ' + '(func (export "f") (result v128) (global.get $v))', + None), + ("growable imported table", + '(import "env" "t" (table 4 funcref)) ' + '(type $b (func (param i32 i32) (result i32))) ' + '(func $a (type $b) (i32.add (local.get 0) (local.get 1))) ' + '(func (export "f") (param i32) (result i32) ' + '(call_indirect (type $b) (i32.const 1) (i32.const 2) (local.get 0)))', + "no compile-time size"), + ("passive element segment", + '(type $b (func (param i32 i32) (result i32))) ' + '(table 2 funcref) ' + '(elem func $a) ' + '(func $a (type $b) (i32.add (local.get 0) (local.get 1))) ' + '(func (export "f") (param i32) (result i32) ' + '(call_indirect (type $b) (i32.const 1) (i32.const 2) (local.get 0)))', + "not statically verifiable"), + ("table slot holding an IMPORTED function", + '(type $b (func (param i32 i32) (result i32))) ' + '(import "env" "h" (func $h (type $b))) ' + '(table 2 funcref) (elem (i32.const 0) $h) ' + '(func (export "f") (param i32) (result i32) ' + '(call_indirect (type $b) (i32.const 1) (i32.const 2) (local.get 0)))', + "imported function"), + ("non-leaf FLOAT param (homing needs an FP store)", + '(func $g (result i32) (i32.const 1)) ' + '(func (export "f") (param f32) (result f32) ' + '(drop (call $g)) (local.get 0))', + "FLOAT parameter"), ] @@ -64,14 +111,28 @@ def compiles_ok(body): def main(): fails = 0 - for label, body in DECLINED: + reasoned = 0 + for entry in DECLINED: + label, body = entry[0], entry[1] + want_reason = entry[2] if len(entry) > 2 else None ok, stderr = compiles_ok(body) if ok: print(f"BUG {label}: compiled — expected a LOUD decline (silent miscompile risk)") fails += 1 + elif want_reason is not None and want_reason not in stderr: + print(f"BUG {label}: declined, but WITHOUT its machine reason " + f"({want_reason!r} absent) — got: {stderr.strip()[:180]}") + fails += 1 else: - print(f"OK {label}: loud-declined") - print(f"\n{len(DECLINED) - fails}/{len(DECLINED)} declined ops loud-declined") + if want_reason is not None: + reasoned += 1 + print(f"OK {label}: loud-declined" + + (f" ({want_reason})" if want_reason else "")) + if reasoned == 0: + print("VACUOUS: no decline was checked for its machine reason") + fails += 1 + print(f"\n{len(DECLINED) - fails}/{len(DECLINED)} declined ops loud-declined " + f"({reasoned} with their machine reason asserted)") print("RESULT:", "PASS — decline matrix honest" if not fails else f"FAIL ({fails} silent)") sys.exit(1 if fails else 0) From 5dbd79127d82256c68bf34318b2b78add7413c61 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 30 Jul 2026 15:33:33 +0200 Subject: [PATCH 9/9] aarch64 oracles: ci-status headers + `set -euo pipefail` CI steps (#890, #851) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two corrections from lane L1's oracle-wiring gate, applied to this lane's harnesses. 1. Both new oracles carry `# ci-status: wired`. VERIFIED non-inert: pointing the workflow step at a different filename makes the gate report "declares `wired` but NO workflow STEP runs it — the gate is INERT", so the declaration is checked against the parsed executable surface rather than taken on trust. 2. The CI steps now use `set -euo pipefail`, not bare `set -o pipefail`. `pipefail` alone leaves the step's exit status as its LAST command's, so a harness that printed FAIL and exited 1 could still green the step — the precise #890 class. The verdict is now taken three ways: the script's own exit status (via `-e`), a non-zero check-count grep, and the summary `RESULT: PASS` line. MUTATION-PROVEN, not assumed: perturbing the comparison inside the call_indirect harness (`exp` -> `exp + 1`, so a CORRECT compiler mismatches) makes the exact CI step body exit 1, and restoring it returns exit 0. That is the check L1 found `sret_decide_differential.py` failing — a gate that printed `MISMATCH <-- BUG` and exited 0. Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .github/workflows/ci.yml | 30 +++++++++++-------- .../aarch64_call_indirect_851_differential.py | 1 + .../repro/aarch64_globals_851_differential.py | 1 + 3 files changed, 20 insertions(+), 12 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 5eb15b39..5a79a8ef 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -486,25 +486,31 @@ jobs: # no precondition. The harness places `.text` and `.data` on DIFFERENT # pages and resolves the relocations itself, so a wrong page delta or # lo12 lands on the wrong bytes. NON-VACUITY: assert a non-zero check - # count (a harness that compiled nothing would otherwise pass silently). + # count (a harness that compiled nothing would otherwise pass silently) + # AND the summary verdict. `set -euo pipefail` (not bare `pipefail`, + # which leaves the step's status as the LAST command's) makes the + # script's own non-zero exit fail the step (#890). run: | - set -o pipefail - out=$(SYNTH=./target/debug/synth \ - python scripts/repro/aarch64_globals_851_differential.py | tee /dev/stderr) - echo "$out" | grep -Eq '^[1-9][0-9]* checks across [1-9][0-9]* exported' \ - || { echo "VACUOUS: globals oracle reported no checks"; exit 1; } + set -euo pipefail + SYNTH=./target/debug/synth \ + python scripts/repro/aarch64_globals_851_differential.py | tee globals851.txt + grep -Eq '^[1-9][0-9]* checks across [1-9][0-9]* exported' globals851.txt + grep -q '^RESULT: PASS' globals851.txt - name: Run #851 lane L3 CALL_INDIRECT execution oracle (§4.4.8 OOB + null + type traps) # A64's `blr` is TOTAL; WASM §4.4.8 is not. All three traps must fire # exactly where wasmtime traps — and the structurally-DUPLICATE type # must NOT trap (the direction an "always trap" lowering would hide). # NON-VACUITY: assert non-zero counts in BOTH directions, so a run that - # only trapped (or only returned values) fails. + # only trapped (or only returned values) fails, plus the summary + # verdict. `set -euo pipefail` makes the script's own non-zero exit fail + # the step (bare `pipefail` would leave the status as the last command's + # — the #890 class). run: | - set -o pipefail - out=$(SYNTH=./target/debug/synth \ - python scripts/repro/aarch64_call_indirect_851_differential.py | tee /dev/stderr) - echo "$out" | grep -Eq '^[1-9][0-9]* checks \([1-9][0-9]* trap, [1-9][0-9]* value\)' \ - || { echo "VACUOUS: call_indirect oracle reported no trap/value checks"; exit 1; } + set -euo pipefail + SYNTH=./target/debug/synth \ + python scripts/repro/aarch64_call_indirect_851_differential.py | tee ci851.txt + grep -Eq '^[1-9][0-9]* checks \([1-9][0-9]* trap, [1-9][0-9]* value\)' ci851.txt + grep -q '^RESULT: PASS' ci851.txt - name: Run decline-matrix honesty oracle run: SYNTH=./target/debug/synth python scripts/repro/aarch64_m2_decline_538.py diff --git a/scripts/repro/aarch64_call_indirect_851_differential.py b/scripts/repro/aarch64_call_indirect_851_differential.py index 213a65d0..e51f4c5e 100644 --- a/scripts/repro/aarch64_call_indirect_851_differential.py +++ b/scripts/repro/aarch64_call_indirect_851_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#851 lane L3 — aarch64 `call_indirect` execution differential vs wasmtime. A64's `blr` is TOTAL: it branches wherever the register points. WASM §4.4.8 is diff --git a/scripts/repro/aarch64_globals_851_differential.py b/scripts/repro/aarch64_globals_851_differential.py index 13e0986e..0c5edf40 100644 --- a/scripts/repro/aarch64_globals_851_differential.py +++ b/scripts/repro/aarch64_globals_851_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#851 lane L3 — aarch64 WASM GLOBALS execution differential vs wasmtime. synth emits the globals region ITSELF: a `.data` section carrying each global's