diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 78e647ab..5dc435dd 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -635,6 +635,55 @@ jobs: SYNTH: ./target/debug/synth run: python scripts/repro/call_indirect_664_differential.py + call-indirect-676-heterogeneous-oracle: + name: heterogeneous-table call_indirect oracle (Thumb-2 + A32) + # VCR-ORACLE-001 (#242, #676): a HETEROGENEOUS funcref table (mixed + # signatures — falcon's fused 41-slot dispatch table) can never satisfy + # the closed-world type check, so WASM Core §4.4.8's type check is + # discharged at RUNTIME: the object carries a type-id sidecar + # (`.synth.table_type_ids`, one u32 structural class id per slot, id 0 = + # null) which the layout contract places at R11 + sum(table sizes)*4, + # and the dispatch compares the indexed slot's id against the expected + # class id (compile-time immediate), UDF-trapping on mismatch — which + # subsumes the #664 null trap. EXECUTE the mixed fixture (two signature + # classes INTERLEAVED + a structural duplicate type + null slots) under + # unicorn on BOTH ISAs vs the wasmtime oracle: matching-class calls must + # return wasmtime's values; wrong-class ("indirect call type mismatch"), + # null AND OOB indices must all stop at a UDF. Non-vacuous red: a build + # without the type check CALLS the wrong-typed function and returns a + # wrong value. On <= v0.37.1 this is red at compile: every dispatch + # through the mixed table loud-declined (capability upgrade — red = + # "declines today", green = sound heterogeneous dispatch). Homogeneous + # tables stay byte-identical by construction (type_check=None emits the + # pre-#676 bytes), pinned by the frozen-fixture job, the whole-object + # no-sidecar test (heterogeneous_table_676.rs) and the + # #642/#650/#664/#594/#597 oracles. + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v7 + - uses: dtolnay/rust-toolchain@stable + - name: Cache Cargo dependencies + uses: actions/cache@v6 + with: + path: | + ~/.cargo/registry + ~/.cargo/git + target/ + key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }} + restore-keys: | + ${{ runner.os }}-cargo- + - name: Build synth + run: cargo build -p synth-cli + - uses: actions/setup-python@v6 + with: + python-version: "3.x" + - name: Install emulation deps + run: pip install wasmtime unicorn pyelftools + - name: Run heterogeneous-table call_indirect oracle + env: + SYNTH: ./target/debug/synth + run: python scripts/repro/call_indirect_676_differential.py + block-brif-483-oracle: name: optimized-path block/br_if lowering oracle # VCR-ORACLE-001 (#242, #483): EXECUTE optimized-path functions with forward diff --git a/crates/synth-backend/src/arm_encoder.rs b/crates/synth-backend/src/arm_encoder.rs index 0471afde..717c1c18 100644 --- a/crates/synth-backend/src/arm_encoder.rs +++ b/crates/synth-backend/src/arm_encoder.rs @@ -148,14 +148,21 @@ impl ArmEncoder { /// pointer load and the `BLX` — a call reaching an uninitialized slot /// traps (§4.4.8). `false` keeps the expansion byte-identical. /// - /// The §4.4.8 type check is discharged at COMPILE time by the selector's - /// closed-world verification (the raw code-pointer table carries no - /// runtime type ids) — see the #642 selector guard. + /// #676, `type_check` (heterogeneous table): the §4.4.8 type check is + /// discharged at RUNTIME against the type-id sidecar — after the bounds + /// guard, `MOV r12, idx, LSL #2; ADD r12, r11, r12; + /// LDR r12, [r12, #type_off]; CMP r12, #expected_id; BEQ +1; UDF` + /// (mirror of the Thumb-2 arm; the dispatch tail recomputes `idx*4`). + /// Null slots carry the reserved class id 0, subsuming the #664 null + /// trap. `None` (every homogeneous table — the verdict discharged at + /// COMPILE time by the closed-world verification, see the #642 selector + /// guard) emits nothing and keeps the expansion byte-identical. fn encode_arm_call_indirect( table_index_reg: &Reg, table_size: u32, table_byte_offset: u32, null_check: bool, + type_check: Option<(u32, u32)>, ) -> Vec { let idx = reg_to_bits(table_index_reg); let mut bytes = Vec::with_capacity(32); @@ -178,6 +185,27 @@ impl ArmEncoder { // UDF — permanently undefined (same trap idiom as the A32 div-by-zero // guards): call_indirect out-of-bounds trap. bytes.extend_from_slice(&0xE7F0_00F0u32.to_le_bytes()); + // #676: runtime type check for a heterogeneous table — load the + // indexed slot's structural class id from the type-id sidecar and + // trap on mismatch (§4.4.8). Mirror of the Thumb-2 arm; `None` + // emits nothing (homogeneous tables byte-identical by construction). + if let Some((expected_id, type_off)) = type_check { + debug_assert!(expected_id <= 255, "selector enforces the CMP imm8 range"); + debug_assert!(type_off <= 4095, "selector enforces the LDR imm12 range"); + // MOV r12, idx, LSL #2 (same as the dispatch tail's scale). + bytes.extend_from_slice(&(0xE1A0C000u32 | (2 << 7) | idx).to_le_bytes()); + // ADD r12, r11, r12 — data-processing ADD (register). + bytes.extend_from_slice(&0xE08BC00Cu32.to_le_bytes()); + // LDR r12, [r12, #type_off] — immediate offset, P=1 U=1 L=1. + bytes.extend_from_slice(&(0xE59CC000u32 | (type_off & 0xFFF)).to_le_bytes()); + // CMP r12, #expected_id — data-processing CMP (immediate). + bytes.extend_from_slice(&(0xE35C_0000u32 | (expected_id & 0xFF)).to_le_bytes()); + // BEQ +1 insn (skip the UDF when the class id matches) — + // cond=EQ(0000), imm24=0: target = branch + 8. + bytes.extend_from_slice(&0x0A00_0000u32.to_le_bytes()); + // UDF — the §4.4.8 type-mismatch trap. + bytes.extend_from_slice(&0xE7F0_00F0u32.to_le_bytes()); + } // MOV r12, idx, LSL #2 — data-processing MOV, register op2 with // imm5=2/LSL: cond=E, opcode=1101, S=0, Rd=r12. let mov: u32 = 0xE1A0C000 | (2 << 7) | idx; @@ -1231,6 +1259,7 @@ impl ArmEncoder { table_size, table_byte_offset, null_check, + type_check, .. } = op { @@ -1239,6 +1268,7 @@ impl ArmEncoder { *table_size, *table_byte_offset, *null_check, + *type_check, )); } let instr: u32 = match op { @@ -3751,6 +3781,13 @@ impl ArmEncoder { // #664, null_check (the table has null slots, linked as ZERO // words): the loaded pointer is null-checked before the BLX — // CMP.W R12,#0; BNE +1; UDF #0 + // #676, type_check (heterogeneous table — runtime §4.4.8 type + // check against the type-id sidecar at R11+off): after the + // bounds guard — + // LSL R12,idx,#2; ADD R12,R11,R12; + // LDR R12,[R12,#type_off]; CMP.W R12,#id; + // BEQ +1; UDF #0 + // (the dispatch tail then recomputes idx*4 — idx stays live). ArmOp::CallIndirect { rd: _, type_idx: _, @@ -3758,6 +3795,7 @@ impl ArmEncoder { table_size, table_byte_offset, null_check, + type_check, } => { let idx_reg = reg_to_bits(table_index_reg); let mut bytes = Vec::new(); @@ -3810,6 +3848,51 @@ impl ArmEncoder { // the div-by-zero guards). bytes.extend_from_slice(&0xDE00u16.to_le_bytes()); + // #676: runtime type check — ONLY for a heterogeneous table + // (mixed signatures, closed-world verdict impossible). Load + // the indexed slot's structural class id from the type-id + // sidecar (`R11 + type_off + idx*4`; `type_off` = sidecar + // base + this table's base offset, a compile-time constant) + // and compare it against the expected type's class id — a + // mismatch is the WASM Core §4.4.8 type trap. Null slots + // carry the reserved id 0, so this compare subsumes the + // #664 null trap (the selector passes `null_check: false`). + // `None` emits NOTHING: every homogeneous table keeps the + // pre-#676 bytes identical BY CONSTRUCTION. R12 stays the + // only scratch (#212); the dispatch tail below recomputes + // idx*4 — the index register is never clobbered here. + if let Some((expected_id, type_off)) = type_check { + debug_assert!(*expected_id <= 255, "selector enforces the CMP imm8 range"); + debug_assert!(*type_off <= 4095, "selector enforces the LDR imm12 range"); + // MOV.W R12, idx, LSL #2 (same encoding as the dispatch + // tail's index scale below). + bytes.extend_from_slice(&0xEA4Fu16.to_le_bytes()); + bytes.extend_from_slice( + &(((0x0C00 | (0b10 << 6)) | idx_reg) as u16).to_le_bytes(), + ); + // ADD.W R12, R11, R12 (the #650 base-add form). + bytes.extend_from_slice(&0xEB0Bu16.to_le_bytes()); + bytes.extend_from_slice(&0x0C0Cu16.to_le_bytes()); + // LDR.W R12, [R12, #type_off] — T3 LDR (immediate): + // 1111 1000 1101 Rn=1100 | Rt=1100 imm12. + bytes.extend_from_slice(&0xF8DCu16.to_le_bytes()); + bytes.extend_from_slice( + &(0xC000u16 | (*type_off as u16 & 0x0FFF)).to_le_bytes(), + ); + // CMP.W R12, #expected_id — T2 CMP (immediate), imm8 + // (same form as the #664 null check's CMP.W R12, #0). + bytes.extend_from_slice(&0xF1BCu16.to_le_bytes()); + bytes.extend_from_slice( + &(0x0F00u16 | (*expected_id as u16 & 0xFF)).to_le_bytes(), + ); + // BEQ +1 insn (skip the UDF when the class id matches) — + // B.N imm8=0: target = branch + 4. EQ. + bytes.extend_from_slice(&0xD000u16.to_le_bytes()); + // UDF #0 — the §4.4.8 type-mismatch trap (same idiom as + // the bounds guard above). + bytes.extend_from_slice(&0xDE00u16.to_le_bytes()); + } + // LSL R12, idx_reg, #2 (multiply index by 4) // Thumb-2 MOV with shift: 11101010 010 S 1111 | 0 imm3 Rd imm2 type Rm // LSL: type=00 (bits 5:4), imm5=2 -> imm3=000, imm2=10 (bits 7:6) @@ -8956,6 +9039,7 @@ mod tests { table_size: 4, table_byte_offset: 0, null_check: false, + type_check: None, }) .unwrap(); assert_eq!( @@ -9003,6 +9087,7 @@ mod tests { table_size: 4, table_byte_offset: 0, null_check: false, + type_check: None, }) .unwrap(); let cmp = u32::from_le_bytes(bytes[4..8].try_into().unwrap()); @@ -9025,6 +9110,7 @@ mod tests { table_size: 0x0002_0003, table_byte_offset: 0, null_check: false, + type_check: None, }) .unwrap(); assert_eq!(bytes.len(), 32, "MOVT arm adds one word: {bytes:02x?}"); @@ -9061,6 +9147,7 @@ mod tests { table_size: 4, table_byte_offset: 0, null_check: false, + type_check: None, }) .unwrap(); assert_eq!( @@ -9094,6 +9181,7 @@ mod tests { table_size: 4, table_byte_offset: 0, null_check: false, + type_check: None, }) .unwrap(); assert_eq!(&bytes[4..6], &[0x64, 0x45], "cmp r4, ip: {bytes:02x?}"); @@ -9119,6 +9207,7 @@ mod tests { table_size: 3, table_byte_offset: 0, null_check: false, + type_check: None, }) .unwrap(); // cmp r8, ip — T2: 0x4500 | N(1)<<7 | Rm(12)<<3 | Rn(0) = 0x45E0 @@ -9132,6 +9221,7 @@ mod tests { table_size: 0x0002_0003, table_byte_offset: 0, null_check: false, + type_check: None, }) .unwrap(); // movw ip,#3 then movt ip,#2 — the size must not be truncated. @@ -9160,6 +9250,7 @@ mod tests { table_size: 41, table_byte_offset: 28, null_check: false, + type_check: None, }) .unwrap(); assert_eq!( @@ -9189,6 +9280,7 @@ mod tests { table_size: 41, table_byte_offset: 0, null_check: false, + type_check: None, }) .unwrap(); assert_eq!( @@ -9216,6 +9308,7 @@ mod tests { table_size: 41, table_byte_offset: 28, null_check: false, + type_check: None, }) .unwrap(); let words: Vec = bytes @@ -9260,6 +9353,7 @@ mod tests { table_size: 4, table_byte_offset: 0, null_check, + type_check: None, }; let with = enc.encode(&op(true)).unwrap(); let without = enc.encode(&op(false)).unwrap(); @@ -9299,6 +9393,7 @@ mod tests { table_size: 4, table_byte_offset: 0, null_check, + type_check: None, }; let with = enc.encode(&op(true)).unwrap(); let without = enc.encode(&op(false)).unwrap(); @@ -9315,6 +9410,114 @@ mod tests { assert_eq!(words[3], 0xE12F_FF3C, "BLX r12: {:#010x}", words[3]); } + /// #676: `type_check` splices the runtime type check — scale the index, + /// load the slot's structural class id from the type-id sidecar + /// (`ldr.w ip, [ip, #type_off]`), compare against the expected class id + /// and trap on mismatch (WASM §4.4.8) — between the bounds guard and + /// the dispatch tail. `type_check: None` keeps the expansion + /// byte-identical to the pre-#676 form (by-construction pin, the same + /// trick as #650 offset-0 / #664 `null_check: false`). + #[test] + fn test_encode_thumb_call_indirect_type_check_676() { + use synth_synthesis::{ArmOp, Reg}; + let enc = ArmEncoder::new_thumb2(); + let op = |type_check| ArmOp::CallIndirect { + rd: Reg::R0, + type_idx: 1, + table_index_reg: Reg::R1, + table_size: 5, + table_byte_offset: 0, + null_check: false, + type_check, + }; + let with = enc.encode(&op(Some((2, 20)))).unwrap(); + let without = enc.encode(&op(None)).unwrap(); + // The checked form = the unchecked form with EXACTLY the six-insn + // type check spliced in after the bounds guard (byte identity of + // the shared prefix/suffix — nothing else may move). + assert_eq!( + with.len(), + without.len() + 20, + "lsl.w(4)+add.w(4)+ldr.w(4)+cmp.w(4)+beq(2)+udf(2): {with:02x?}" + ); + // Bounds guard: movw(4) + cmp(2) + blo(2) + udf(2) = 10 bytes. + let guard_end = 10; + assert_eq!(&with[..guard_end], &without[..guard_end], "shared guard"); + assert_eq!( + &with[guard_end..guard_end + 20], + &[ + 0x4F, 0xEA, 0x81, 0x0C, // mov.w ip, r1, lsl #2 + 0x0B, 0xEB, 0x0C, 0x0C, // add.w ip, r11, ip + 0xDC, 0xF8, 0x14, 0xC0, // ldr.w ip, [ip, #20] — sidecar slot id + 0xBC, 0xF1, 0x02, 0x0F, // cmp.w ip, #2 — expected class id + 0x00, 0xD0, // beq .+4 (skip the udf on a match) + 0x00, 0xDE, // udf #0 — §4.4.8 type-mismatch trap (#676) + ], + "type check follows the bounds guard: {with:02x?}" + ); + assert_eq!( + &with[guard_end + 20..], + &without[guard_end..], + "dispatch tail unchanged (idx*4 recomputed)" + ); + } + + /// #676: the A32 twin — `mov r12, idx, lsl #2; add r12, r11, r12; + /// ldr r12, [r12, #type_off]; cmp r12, #id; beq .+8; udf` after the + /// bounds guard; `type_check: None` keeps the #594/#642/#650/#664 + /// bytes identical. + #[test] + fn test_encode_arm32_call_indirect_type_check_676() { + use synth_synthesis::{ArmOp, Reg}; + let enc = ArmEncoder::new_arm32(); + let op = |type_check| ArmOp::CallIndirect { + rd: Reg::R0, + type_idx: 1, + table_index_reg: Reg::R1, + table_size: 5, + table_byte_offset: 0, + null_check: false, + type_check, + }; + let with = enc.encode(&op(Some((2, 20)))).unwrap(); + let without = enc.encode(&op(None)).unwrap(); + assert_eq!(with.len(), without.len() + 24, "6 A32 words: {with:02x?}"); + // Bounds guard: movw + cmp + blo + udf = 4 words = 16 bytes. + let guard_end = 16; + assert_eq!(&with[..guard_end], &without[..guard_end], "shared guard"); + let words: Vec = with[guard_end..guard_end + 24] + .chunks_exact(4) + .map(|w| u32::from_le_bytes(w.try_into().unwrap())) + .collect(); + assert_eq!( + words[0], 0xE1A0_C101, + "MOV r12,r1,LSL#2: {:#010x}", + words[0] + ); + assert_eq!(words[1], 0xE08B_C00C, "ADD r12,r11,r12: {:#010x}", words[1]); + assert_eq!( + words[2], 0xE59C_C014, + "LDR r12,[r12,#20] (sidecar): {:#010x}", + words[2] + ); + assert_eq!( + words[3], 0xE35C_0002, + "CMP r12,#2 (expected class id): {:#010x}", + words[3] + ); + assert_eq!(words[4], 0x0A00_0000, "BEQ +1 insn: {:#010x}", words[4]); + assert_eq!( + words[5], 0xE7F0_00F0, + "UDF (type-mismatch trap): {:#010x}", + words[5] + ); + assert_eq!( + &with[guard_end + 24..], + &without[guard_end..], + "dispatch tail unchanged" + ); + } + /// #178/#180 regression: the Thumb `Add`/`Adds`/`Subs` reg-forms used the /// 16-bit encoding unconditionally. For high registers (R12 base scratch, /// R8-R11 i64 pairs) the 3-bit register fields overflow and corrupt the diff --git a/crates/synth-backend/tests/a32_no_silent_nop_615.rs b/crates/synth-backend/tests/a32_no_silent_nop_615.rs index dbdc77af..39984fc0 100644 --- a/crates/synth-backend/tests/a32_no_silent_nop_615.rs +++ b/crates/synth-backend/tests/a32_no_silent_nop_615.rs @@ -652,6 +652,7 @@ fn representatives() -> Vec { table_size: 4, // #642: bounds-guard immediate table_byte_offset: 0, // #650: table 0 of the contiguous R11 region null_check: false, // #664: fully-initialized table + type_check: None, // #676: homogeneous table }, I64Add { rdlo: dl, diff --git a/crates/synth-cli/src/main.rs b/crates/synth-cli/src/main.rs index f081e0ae..24c65791 100644 --- a/crates/synth-cli/src/main.rs +++ b/crates/synth-cli/src/main.rs @@ -2969,6 +2969,8 @@ fn compile_all_exports( // #598/#637: Thumb-bit handling + `.ARM.attributes` derive from // the selected target inside the builder. target_spec, + // #676: heterogeneous-table type-id sidecar (empty = no section). + &config.call_indirect_guards.type_ids_image, )? } else if cortex_m { // #649: the self-contained image materializes the R9 globals table — @@ -3171,6 +3173,9 @@ fn build_relocatable_elf( // interworking bit) on STT_FUNC symbols + e_entry — A32 (cortex-r5) keeps // it clear — and every object carries a target-derived `.ARM.attributes`. target_spec: &TargetSpec, + // #676: the call_indirect type-id sidecar image (one u32 class id per + // table slot, region order; empty = no heterogeneous table = no section). + table_type_ids: &[u32], ) -> Result> { use std::collections::HashMap; @@ -3898,6 +3903,27 @@ fn build_relocatable_elf( } } + // #676: the call_indirect type-id sidecar — one LE u32 structural class + // id per table slot across ALL tables in region order (0 = null slot). + // Non-empty ONLY for a module with a heterogeneous funcref table, so + // every existing (homogeneous) module's object stays byte-identical. + // Structurally a clone of `.meld_import_table` (non-ALLOC trailing + // PROGBITS, no symbol, no relocation): the runtime/harness that links + // the pointer region at R11 reads this section and copies its words + // VERBATIM to `R11 + sum(all table sizes) * 4` — it never re-derives + // the ids (see the layout contract on `synth_core::CallIndirectGuards`). + if !table_type_ids.is_empty() { + let mut sidecar = Vec::with_capacity(table_type_ids.len() * 4); + for id in table_type_ids { + sidecar.extend_from_slice(&id.to_le_bytes()); + } + let sidecar_section = Section::new(".synth.table_type_ids", ElfSectionType::ProgBits) + .with_flags(0) // Not ALLOC — metadata for the region linker + .with_align(4) + .with_data(sidecar); + elf_builder.add_section(sidecar_section); + } + // VCR-DBG-001 step 4 (#394): emit a FULL DWARF unit (`.debug_info`, // `.debug_abbrev`, `.debug_str`, `.debug_line`, ...) as NON-ALLOC trailing // PROGBITS sections. Each is structurally a clone of `.meld_import_table`: no @@ -5865,6 +5891,7 @@ mod tests { Some(native), None, &TargetSpec::cortex_m3(), + &[], ) .expect("#345: native-pointer zero-linmem object builds"); @@ -5970,6 +5997,7 @@ mod tests { Some(native), None, &TargetSpec::cortex_m3(), + &[], ) .expect("#345: native-pointer literal-pool object builds"); @@ -6063,6 +6091,7 @@ mod tests { Some(native), None, &TargetSpec::cortex_m3(), + &[], ) .expect("#354: mixed-case object builds"); diff --git a/crates/synth-cli/tests/heterogeneous_table_676.rs b/crates/synth-cli/tests/heterogeneous_table_676.rs new file mode 100644 index 00000000..255c9943 --- /dev/null +++ b/crates/synth-cli/tests/heterogeneous_table_676.rs @@ -0,0 +1,113 @@ +//! #676 — heterogeneous funcref tables: runtime type check + type-id sidecar. +//! +//! The cargo-visible complement to `scripts/repro/call_indirect_676_differential.py` +//! (which needs wasmtime + unicorn and runs in the isolated CI differential +//! job). Locks the OBJECT-level contract: +//! +//! - a module with a heterogeneous table COMPILES (pre-#676 every +//! `call_indirect` through it loud-declined and the dispatcher symbols +//! were missing) and its object carries the `.synth.table_type_ids` +//! sidecar — one LE u32 structural class id per slot, region order, +//! id 0 = null slot, structural duplicates sharing one id; +//! - a homogeneous module emits NO sidecar section — its object stays +//! byte-identical by construction (the `.text` half of that pin lives in +//! `frozen_codegen_bytes.rs`). +//! +//! Both ISAs of the expansion (Thumb-2 `cortex-m3`, A32 `cortex-r5`). + +use std::process::Command; + +use object::{Object, ObjectSection, ObjectSymbol}; + +fn synth() -> &'static str { + env!("CARGO_BIN_EXE_synth") +} + +fn fixture(name: &str) -> std::path::PathBuf { + std::path::Path::new(env!("CARGO_MANIFEST_DIR")) + .join("../..") + .join("scripts/repro") + .join(name) +} + +/// Compile a fixture with the exact config the `.py` differentials use and +/// return the parsed object bytes. +fn compile(wasm: &str, target: &str) -> Vec { + let path = fixture(wasm); + let elf = format!("/tmp/hetero676_{target}_{wasm}.o"); + let out = Command::new(synth()) + .args([ + "compile", + path.to_str().unwrap(), + "-o", + &elf, + "--target", + target, + "--all-exports", + "--relocatable", + "--no-optimize", + ]) + .output() + .expect("run synth"); + assert!( + out.status.success(), + "synth compile failed for {wasm} ({target}): {}", + String::from_utf8_lossy(&out.stderr) + ); + std::fs::read(&elf).expect("read object") +} + +/// #676: the heterogeneous fixture compiles (no decline) and the object +/// carries the type-id sidecar with the expected structural class ids. +#[test] +fn test_676_heterogeneous_table_compiles_with_sidecar() { + for target in ["cortex-m3", "cortex-r5"] { + let bytes = compile("call_indirect_676_heterogeneous.wat", target); + let obj = object::File::parse(&*bytes).expect("parse object"); + + // Pre-#676 red: the dispatchers loud-declined → symbols missing. + for need in ["via2", "via1", "func_0", "func_1", "func_2"] { + assert!( + obj.symbols().any(|s| s.name() == Ok(need)), + "{target}: symbol {need} missing — the dispatch declined (#676)" + ); + } + + // The sidecar: slots [$add(bin), $neg(un), $sub(bin2 ≡ bin), null, + // null] → class ids [1, 2, 1, 0, 0] ($bin2 is a structural duplicate + // of $bin — one id; 0 is the reserved null id). + let sidecar = obj + .section_by_name(".synth.table_type_ids") + .unwrap_or_else(|| panic!("{target}: .synth.table_type_ids section missing (#676)")); + let data = sidecar.data().expect("sidecar data"); + let ids: Vec = data + .chunks_exact(4) + .map(|w| u32::from_le_bytes(w.try_into().unwrap())) + .collect(); + assert_eq!( + ids, + vec![1, 2, 1, 0, 0], + "{target}: sidecar class ids (structural dedup + null id 0)" + ); + } +} + +/// #676 by-construction pin: homogeneous modules (the frozen #642/#650/#664 +/// fixtures) emit NO sidecar section — nothing about their objects changes. +#[test] +fn test_676_homogeneous_fixtures_emit_no_sidecar() { + for wasm in [ + "call_indirect_642_oob.wat", + "call_indirect_650_multitable.wat", + "call_indirect_664_nullslot.wat", + ] { + for target in ["cortex-m3", "cortex-r5"] { + let bytes = compile(wasm, target); + let obj = object::File::parse(&*bytes).expect("parse object"); + assert!( + obj.section_by_name(".synth.table_type_ids").is_none(), + "{wasm} ({target}): homogeneous module must emit no sidecar (#676)" + ); + } + } +} diff --git a/crates/synth-core/src/wasm_decoder.rs b/crates/synth-core/src/wasm_decoder.rs index 82bf533d..08c7d76b 100644 --- a/crates/synth-core/src/wasm_decoder.rs +++ b/crates/synth-core/src/wasm_decoder.rs @@ -138,6 +138,19 @@ pub struct TableGuards { /// meaningful when the type verdict is `None` (verified); reject paths /// decline before it is consulted. pub has_null_slots: bool, + /// #676: this table's image is statically known but HETEROGENEOUS — its + /// initialized slots span at least two distinct STRUCTURAL signature + /// classes, so no expected type's closed world can hold + /// (`type_reject[t]` is `Some` for every `t`) — yet the mismatch trap + /// (WASM Core §4.4.8) IS dischargeable at runtime: the type-id sidecar + /// (see [`CallIndirectGuards`]) carries each slot's structural class id, + /// and the dispatch compares the indexed slot's id against the expected + /// type's class id (a compile-time immediate), trapping on inequality. + /// When set (and [`CallIndirectGuards::type_ids_byte_offset`] is known), + /// the lowering emits that runtime check INSTEAD of declining. `false` + /// keeps the pre-#676 behavior: verified tables dispatch unchecked + /// (byte-identical), unverifiable tables decline. + pub runtime_type_check: bool, } /// #642/#650: everything the `call_indirect` lowering needs to emit its @@ -175,6 +188,31 @@ pub struct TableGuards { /// set the dispatch emits a null check on the loaded pointer /// (`CMP #0` → trap) between the bounds guard and the indirect branch. /// A fully-initialized table (`has_null_slots == false`) keeps the +/// pre-#664 dispatch bytes identical BY CONSTRUCTION, and +/// - a HETEROGENEOUS table (mixed signatures — the closed-world property +/// cannot hold for ANY expected type) is dispatched through a runtime +/// type check against the **type-id sidecar** (#676): a parallel `u32` +/// array the layout contract places at `R11 + type_ids_byte_offset` +/// (immediately after the LAST table's pointer words, i.e. at +/// `sum(size(0..num_tables)) * 4`), mirroring the pointer region slot +/// for slot — table N's type-ids start at +/// `R11 + type_ids_byte_offset + base_byte_offset(N)`. Each word is the +/// slot's STRUCTURAL signature class id: structurally-equal function +/// types share one dense id (1-based, first-occurrence order over the +/// type section); id **0 is reserved for null slots**, so the type +/// compare (expected ids are always >= 1) subsumes the #664 null trap +/// in the same `CMP`. The dispatch loads `type_id[idx]`, compares it +/// against the expected type's class id (compile-time immediate) and +/// traps (`UDF`) on mismatch — WASM Core §4.4.8's runtime type check — +/// before the pointer load and `BLX`. The sidecar words are emitted +/// into the relocatable object as the `.synth.table_type_ids` section +/// (non-ALLOC metadata, like `.meld_import_table`): the runtime/harness +/// that links the pointer region copies them to +/// `R11 + type_ids_byte_offset` verbatim — it never re-derives ids. A +/// module with NO heterogeneous table emits no sidecar and no runtime +/// type check anywhere: homogeneous dispatch bytes stay identical BY +/// CONSTRUCTION (the #650 offset-0 / #664 `null_check: false` trick). +/// /// pre-#664 dispatch bytes identical BY CONSTRUCTION. /// /// ## Companion: the self-contained SRAM layout contract (#687) @@ -194,6 +232,26 @@ pub struct CallIndirectGuards { /// Per-table guard inputs, indexed by table index (imports first). The /// default (empty — no module context) DECLINES every `call_indirect`. pub tables: Vec, + /// #676: byte offset of the type-id sidecar within the R11 region — the + /// total pointer-region size, `sum(size(0..num_tables)) * 4`. `Some` + /// only when a sidecar exists: at least one table is heterogeneous + /// (see [`TableGuards::runtime_type_check`]) AND every table's size is + /// compile-time known (otherwise the sidecar base is not a constant and + /// heterogeneous dispatches keep declining). `None` = no sidecar. + pub type_ids_byte_offset: Option, + /// #676: the sidecar image — one `u32` structural class id per slot + /// across ALL tables in region order (0 = null slot). Emitted into the + /// object as `.synth.table_type_ids`; empty exactly when + /// `type_ids_byte_offset` is `None`. A table whose image is not + /// statically known contributes ZERO words (it declines at the + /// lowering, and 0 never equals an expected class id, so even a rogue + /// dispatch would trap, not branch). + pub type_ids_image: Vec, + /// #676: per module type index, that type's structural class id + /// (1-based, dense; structurally-equal duplicate types share an id). + /// The expected-type immediate the dispatch compares against. Empty + /// when `type_ids_byte_offset` is `None` (no sidecar — never consulted). + pub type_class_ids: Vec, } impl CallIndirectGuards { @@ -206,7 +264,9 @@ impl CallIndirectGuards { base_byte_offset: Some(0), type_reject, has_null_slots: false, + runtime_type_check: false, }], + ..Self::default() } } } @@ -321,27 +381,92 @@ 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)); + } + let mut tables = Vec::with_capacity(self.table_sizes.len()); + // #676: per table, the slot class ids (None = image not statically + // known) — concatenated into the sidecar image below. + let mut per_table_slot_ids: Vec>> = + Vec::with_capacity(self.table_sizes.len()); // Running word offset of the next table's base within the R11 region; // `None` once a table of unknown size is passed (every later base is // then not a compile-time constant). let mut base_words: Option = Some(0); for (n, &size) in self.table_sizes.iter().enumerate() { let base_byte_offset = base_words.and_then(|w| w.checked_mul(4)); - let (type_reject, has_null_slots) = - self.table_type_reject(n as u32, size, global_poison, n_types); + let (type_reject, has_null_slots, slot_class_ids) = + self.table_type_reject(n as u32, size, global_poison, n_types, &type_class_ids); + // #676: heterogeneous = the image is statically known and its + // INITIALIZED slots span >= 2 distinct structural classes (null + // slots — id 0 — don't count; a sparse homogeneous table stays + // on the #664 verified-plus-null-check path, bytes identical). + let runtime_type_check = slot_class_ids.as_ref().is_some_and(|ids| { + let mut distinct: Vec = ids.iter().copied().filter(|&c| c != 0).collect(); + distinct.sort_unstable(); + distinct.dedup(); + distinct.len() >= 2 + }); + per_table_slot_ids.push(slot_class_ids); tables.push(TableGuards { table_size: size, base_byte_offset, type_reject, has_null_slots, + runtime_type_check, }); base_words = match (base_words, size) { (Some(w), Some(s)) => w.checked_add(s), _ => None, }; } - CallIndirectGuards { tables } + + // #676: the sidecar exists only when some table actually needs the + // runtime check AND the whole pointer region's size is compile-time + // known (`base_words` survived every table) — otherwise the sidecar + // base is not a constant and heterogeneous dispatches keep declining + // (their `runtime_type_check` flag is cleared so the lowering sees a + // plain reject). + let any_hetero = tables.iter().any(|t| t.runtime_type_check); + let type_ids_byte_offset = base_words + .filter(|_| any_hetero) + .and_then(|w| w.checked_mul(4)); + let type_ids_image = if type_ids_byte_offset.is_some() { + self.table_sizes + .iter() + .zip(&per_table_slot_ids) + .flat_map(|(&size, ids)| match ids { + Some(ids) => ids.clone(), + // Image not statically known: zero words (id 0 never + // matches an expected class id >= 1 — trap, not branch). + None => vec![0u32; size.unwrap_or(0) as usize], + }) + .collect() + } else { + for t in &mut tables { + t.runtime_type_check = false; + } + Vec::new() + }; + CallIndirectGuards { + tables, + type_ids_byte_offset, + type_ids_image, + type_class_ids: if type_ids_byte_offset.is_some() { + type_class_ids + } else { + Vec::new() + }, + } } /// #642/#650: the closed-world type verdicts for ONE table — `None` per @@ -351,15 +476,20 @@ impl DecodedModule { /// the table image left any slot uninitialized — a `call_indirect` /// reaching one must TRAP at runtime (null check on the loaded pointer), /// which the lowering emits only when this is set. Reject paths return - /// `false` (the verdict declines before the flag is consulted). + /// `false` (the verdict declines before the flag is consulted). The + /// third component (#676) is the table's slot class ids — per slot, the + /// structural signature class of the initializing function (0 for a + /// null slot) — `Some` exactly when the table image is statically + /// known; it feeds the type-id sidecar and the heterogeneity verdict. fn table_type_reject( &self, n: u32, size: Option, global_poison: Option<&str>, n_types: usize, - ) -> (Vec>, bool) { - let reject_all = |reason: String| (vec![Some(reason); n_types], false); + type_class_ids: &[u32], + ) -> (Vec>, bool, Option>) { + let reject_all = |reason: String| (vec![Some(reason); n_types], false, None); if let Some(reason) = global_poison { return reject_all(reason.to_string()); @@ -415,15 +545,28 @@ impl DecodedModule { if self.type_signatures.get(fty as usize) != self.type_signatures.get(t) { return Some(format!( "table {n} entry (function {f}, type {fty}) has a different \ - signature than expected type {t} — a runtime type check \ - is not implementable on the raw code-pointer table" + signature than expected type {t}" )); } } None }) .collect(); - (rejects, has_null_slots) + // #676: per-slot structural class ids (0 = null). `None` as soon as + // any initializing function's type is unknown — the image is then + // not statically classifiable and the table can neither verify nor + // carry the runtime check (the rejects above already name it). + let slot_class_ids: Option> = slots + .iter() + .map(|s| match s { + None => Some(0u32), + Some(f) => self + .func_type_indices + .get(*f as usize) + .and_then(|&fty| type_class_ids.get(fty as usize).copied()), + }) + .collect(); + (rejects, has_null_slots, slot_class_ids) } } @@ -2919,6 +3062,23 @@ mod tests { "heterogeneous table must reject every expected type: {:?}", guards.tables[0].type_reject ); + // #676: ... but the image is statically known, so the mismatch trap + // is dischargeable at RUNTIME via the type-id sidecar. + assert!( + guards.tables[0].runtime_type_check, + "heterogeneous-but-known table must offer the runtime check (#676)" + ); + assert_eq!( + guards.type_ids_byte_offset, + Some(8), + "sidecar sits after the 2-slot pointer region" + ); + assert_eq!( + guards.type_ids_image, + vec![1, 2], + "slot 0 = $bin (class 1), slot 1 = $un (class 2)" + ); + assert_eq!(guards.type_class_ids, vec![1, 2]); } /// #664 (relaxes the #642 all-reject): an uninitialized table slot (elem @@ -3009,6 +3169,82 @@ mod tests { "a heterogeneous sparse table must still reject every type: {:?}", guards.tables[0].type_reject ); + // #676: the sparse-heterogeneous case is now dischargeable at + // runtime too — null slots take the reserved class id 0, so ONE + // sidecar compare covers both the type mismatch and the null trap. + assert!(guards.tables[0].runtime_type_check, "#676 runtime check"); + assert_eq!(guards.type_ids_byte_offset, Some(16), "4 pointer slots"); + assert_eq!( + guards.type_ids_image, + vec![0, 1, 0, 2], + "nulls at 0/2 carry the reserved id 0; $t slot 1 = class 1, \ + $u slot 3 = class 2" + ); + } + + /// #676: the heterogeneous type-id sidecar — structural duplicate types + /// share one class id (the meld 31-decls/25-distinct shape), null slots + /// take the reserved id 0, and the sidecar base is the total pointer + /// region size. A module with NO heterogeneous table gets NO sidecar + /// (empty image, `None` offset) — homogeneous modules stay untouched. + #[test] + fn test_call_indirect_guards_heterogeneous_sidecar_676() { + let wat = r#" + (module + (type $bin (func (param i32 i32) (result i32))) + (type $un (func (param i32) (result i32))) + (type $bin2 (func (param i32 i32) (result i32))) + (table 5 5 funcref) + (func $add (type $bin) (i32.add (local.get 0) (local.get 1))) + (func $neg (type $un) (i32.sub (i32.const 0) (local.get 0))) + (func $sub (type $bin2) (i32.sub (local.get 0) (local.get 1))) + (elem (i32.const 0) func $add $neg $sub) + (func (export "via2") (param i32 i32) (result i32) + (call_indirect (type $bin) + (local.get 0) (i32.const 3) (local.get 1))) + (func (export "via1") (param i32 i32) (result i32) + (call_indirect (type $un) (local.get 0) (local.get 1))) + ) + "#; + let wasm = wat::parse_str(wat).expect("parse"); + let module = decode_wasm_module(&wasm).expect("decode"); + let guards = module.call_indirect_guards(); + assert!(guards.tables[0].runtime_type_check); + assert_eq!( + guards.type_class_ids, + vec![1, 2, 1], + "$bin2 is a structural duplicate of $bin — one class id (#676)" + ); + assert_eq!( + guards.type_ids_image, + vec![1, 2, 1, 0, 0], + "slots: $add(bin)=1, $neg(un)=2, $sub(bin2 ≡ bin)=1, null, null" + ); + assert_eq!( + guards.type_ids_byte_offset, + Some(20), + "sidecar starts after the 5 pointer words" + ); + + // Homogeneous module → NO sidecar, no runtime check anywhere. + let wat = r#" + (module + (type $t (func (param i32) (result i32))) + (table 2 2 funcref) + (func $f0 (type $t) (local.get 0)) + (func $f1 (type $t) (i32.const 7)) + (elem (i32.const 0) func $f0 $f1) + (func (export "via") (param i32 i32) (result i32) + (call_indirect (type $t) (local.get 0) (local.get 1))) + ) + "#; + let wasm = wat::parse_str(wat).expect("parse"); + let module = decode_wasm_module(&wasm).expect("decode"); + let guards = module.call_indirect_guards(); + assert!(!guards.tables[0].runtime_type_check); + assert_eq!(guards.type_ids_byte_offset, None, "no heterogeneous table"); + assert!(guards.type_ids_image.is_empty()); + assert!(guards.type_class_ids.is_empty()); } /// #642: no table at all → no compile-time bound → table_size None and diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index 75499db9..e1b25fd2 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -2016,6 +2016,13 @@ fn sel_dsl_from_env() -> bool { std::env::var("SYNTH_SEL_DSL").is_ok_and(|v| v != "0") } +/// #642/#650/#664/#676: resolved `call_indirect` guard inputs — +/// `(table_size, table_byte_offset, null_check, type_check)`. `type_check` +/// is `Some((expected_class_id, type_id_byte_offset))` when the dispatched +/// table is heterogeneous and the §4.4.8 type check is discharged at +/// runtime against the type-id sidecar (#676). +type ResolvedCallIndirectGuards = (u32, u32, bool, Option<(u32, u32)>); + impl InstructionSelector { /// Create a new instruction selector pub fn new(rules: Vec) -> Self { @@ -2177,14 +2184,19 @@ impl InstructionSelector { /// table size (for the encoder's bounds guard), a constant base offset, /// and a verified closed-world type verdict FOR THAT TABLE, this refuses /// rather than let an unchecked indirect branch be emitted. - /// Returns `(table_size, table_byte_offset, null_check)` — `null_check` - /// is set when the table image contains null (uninitialized) slots, so - /// the encoder must trap on a zero loaded pointer (#664). + /// Returns `(table_size, table_byte_offset, null_check, type_check)` — + /// `null_check` is set when the table image contains null + /// (uninitialized) slots, so the encoder must trap on a zero loaded + /// pointer (#664); `type_check` is `Some((expected_class_id, + /// type_id_byte_offset))` when the table is HETEROGENEOUS and §4.4.8's + /// type check is discharged at runtime against the type-id sidecar + /// (#676) — the null trap is then subsumed by the compare (null slots + /// carry the reserved class id 0), so `null_check` is `false`. fn resolve_call_indirect_guards( &self, table_index: u32, type_index: u32, - ) -> Result<(u32, u32, bool)> { + ) -> Result { let n_tables = self.call_indirect_guards.tables.len(); let table = self .call_indirect_guards @@ -2224,6 +2236,18 @@ impl InstructionSelector { match table.type_reject.get(type_index as usize) { Some(None) => {} // closed-world type property verified Some(Some(reason)) => { + // #676: a HETEROGENEOUS table (mixed signatures) fails the + // closed world for every expected type, but the §4.4.8 + // mismatch trap is dischargeable at RUNTIME via the type-id + // sidecar — emit the check instead of declining. + if table.runtime_type_check { + return self.resolve_runtime_type_check( + table_index, + type_index, + table_size, + table_byte_offset, + ); + } return Err(synth_core::Error::synthesis(format!( "call_indirect (expected type {type_index}, table \ {table_index}): closed-world type check failed — {reason}; \ @@ -2238,7 +2262,74 @@ impl InstructionSelector { ))); } } - Ok((table_size, table_byte_offset, table.has_null_slots)) + Ok((table_size, table_byte_offset, table.has_null_slots, None)) + } + + /// #676: guard inputs for a heterogeneous-table dispatch — resolve the + /// expected type's structural class id (the CMP immediate) and the full + /// byte offset from R11 to the dispatched table's type-id subarray, or + /// decline LOUDLY when either exceeds its encoding range. The #664 null + /// check is subsumed: null slots carry the reserved class id 0, which + /// never equals an expected id (>= 1), so the compare traps them too. + fn resolve_runtime_type_check( + &self, + table_index: u32, + type_index: u32, + table_size: u32, + table_byte_offset: u32, + ) -> Result { + let sidecar_base = self + .call_indirect_guards + .type_ids_byte_offset + .ok_or_else(|| { + synth_core::Error::synthesis(format!( + "call_indirect (table {table_index}): heterogeneous table needs \ + the type-id sidecar but the pointer region's total size is not \ + a compile-time constant — #676" + )) + })?; + let expected_id = self + .call_indirect_guards + .type_class_ids + .get(type_index as usize) + .copied() + .ok_or_else(|| { + synth_core::Error::synthesis(format!( + "call_indirect (table {table_index}): no structural class id \ + for expected type {type_index} — #676" + )) + })?; + // The expected id is the CMP immediate: imm8 keeps it encodable on + // BOTH ISAs (Thumb-2 T2 CMP and A32 CMP imm12 alike). Dense + // structural classes make >255 unreachable in practice (meld's + // falcon core has 25); decline loudly rather than truncate. + if expected_id > 255 { + return Err(synth_core::Error::synthesis(format!( + "call_indirect (table {table_index}): expected type \ + {type_index}'s structural class id {expected_id} exceeds the \ + CMP immediate range (255) — #676" + ))); + } + // Full offset from R11 to THIS table's type-id subarray; the encoder + // folds it into the sidecar load's LDR imm12 (<= 4095, the #650 + // decline pattern). + let type_id_byte_offset = sidecar_base + .checked_add(table_byte_offset) + .filter(|&off| off <= 4095) + .ok_or_else(|| { + synth_core::Error::synthesis(format!( + "call_indirect (table {table_index}): type-id sidecar offset \ + {sidecar_base}+{table_byte_offset} exceeds the LDR imm12 \ + addressing range (4095) — #676" + )) + })?; + Ok(( + table_size, + table_byte_offset, + // #664 subsumed: the type compare traps null slots (id 0). + false, + Some((expected_id, type_id_byte_offset)), + )) } /// Enable relocatable host-link mode (#197): import calls emit a direct @@ -2945,7 +3036,7 @@ impl InstructionSelector { // guard), a constant table base offset, and a verified // closed-world type verdict for THAT table, decline loudly // rather than emit an unchecked indirect branch. - let (table_size, table_byte_offset, null_check) = + let (table_size, table_byte_offset, null_check, type_check) = self.resolve_call_indirect_guards(*table_index, *type_index)?; vec![ArmOp::CallIndirect { rd, @@ -2955,6 +3046,9 @@ impl InstructionSelector { table_byte_offset, // #664: trap on a null (zero-linked) slot at runtime. null_check, + // #676: heterogeneous table — runtime type check + // against the type-id sidecar. + type_check, }] } @@ -9462,7 +9556,7 @@ impl InstructionSelector { // table.grow/table.set are unsupported ops that loud-skip // their functions). If any input is missing, DECLINE // loudly — never emit an unchecked indirect branch. - let (table_size, table_byte_offset, null_check) = + let (table_size, table_byte_offset, null_check, type_check) = self.resolve_call_indirect_guards(*table_index, *type_index)?; // Top of stack is the table index; the call arguments sit @@ -9575,9 +9669,12 @@ impl InstructionSelector { // within the contiguous R11 region. #664: a table // with null slots gets a runtime null check on // the loaded pointer (zero-linked slot → trap). + // #676: a heterogeneous table gets the runtime + // type check against the type-id sidecar. table_size, table_byte_offset, null_check, + type_check, }, source_line: Some(idx), }); @@ -14304,7 +14401,9 @@ mod tests { base_byte_offset: Some(0), type_reject: vec![None], // initialized slots verified has_null_slots: true, // slots 0,2 null (the falcon shape) + runtime_type_check: false, }], + ..Default::default() }); let wasm_ops = vec![ WasmOp::I32Const(1), @@ -14329,6 +14428,126 @@ mod tests { ); } + /// #676: a HETEROGENEOUS table (closed-world verdict rejects every + /// expected type, but the image is statically classifiable) lowers with + /// the runtime type check — `type_check: Some((expected_class_id, + /// sidecar_base + table_byte_offset))` — instead of declining. The #664 + /// null check is subsumed by the compare (null slots carry the reserved + /// class id 0), so `null_check` is `false` even though the table has + /// null slots. + #[test] + fn test_676_call_indirect_heterogeneous_emits_runtime_type_check() { + let db = RuleDatabase::new(); + let mut selector = InstructionSelector::new(db.rules().to_vec()); + selector.set_func_arg_counts(Vec::new(), vec![0, 0]); + selector.set_call_indirect_guards(synth_core::CallIndirectGuards { + tables: vec![synth_core::TableGuards { + table_size: Some(5), + base_byte_offset: Some(0), + type_reject: vec![ + Some("mixed signatures".to_string()), + Some("mixed signatures".to_string()), + ], + has_null_slots: true, // slots 3,4 null — subsumed by the compare + runtime_type_check: true, + }], + type_ids_byte_offset: Some(20), // 5 pointer words + type_ids_image: vec![1, 2, 1, 0, 0], + type_class_ids: vec![1, 2], + }); + let wasm_ops = vec![ + WasmOp::I32Const(1), + WasmOp::CallIndirect { + type_index: 1, + table_index: 0, + }, + ]; + let arm = selector + .select_with_stack(&wasm_ops, 0) + .expect("a heterogeneous call_indirect must lower via the runtime check (#676)"); + assert!( + arm.iter().any(|i| matches!( + &i.op, + ArmOp::CallIndirect { + table_size: 5, + null_check: false, // subsumed: null slots carry id 0 + type_check: Some((2, 20)), // class of type 1; sidecar base + offset 0 + .. + } + )), + "the pseudo-op must carry the runtime type check: {arm:#?}" + ); + } + + /// #676: the runtime check declines LOUDLY past its encoding ranges — a + /// sidecar offset beyond LDR imm12 or a class id beyond the CMP imm8 — + /// and a heterogeneous table WITHOUT a sidecar (a later table's size + /// unknown) keeps declining. + #[test] + fn test_676_call_indirect_runtime_check_range_declines() { + let db = RuleDatabase::new(); + let hetero_table = |off| synth_core::TableGuards { + table_size: Some(2), + base_byte_offset: Some(off), + type_reject: vec![Some("mixed signatures".to_string())], + has_null_slots: false, + runtime_type_check: true, + }; + let ops = vec![ + WasmOp::I32Const(0), + WasmOp::CallIndirect { + type_index: 0, + table_index: 0, + }, + ]; + + // Sidecar offset past LDR imm12. + let mut selector = InstructionSelector::new(db.rules().to_vec()); + selector.set_func_arg_counts(Vec::new(), vec![0]); + selector.set_call_indirect_guards(synth_core::CallIndirectGuards { + tables: vec![hetero_table(2000)], + type_ids_byte_offset: Some(3000), // 3000 + 2000 > 4095 + type_ids_image: vec![1, 2], + type_class_ids: vec![1], + }); + let err = selector + .select_with_stack(&ops, 0) + .expect_err("sidecar offset past LDR imm12 must decline"); + assert!( + err.to_string().contains("#676") && err.to_string().contains("4095"), + "loud range decline: {err}" + ); + + // Class id past the CMP immediate. + let mut selector = InstructionSelector::new(db.rules().to_vec()); + selector.set_func_arg_counts(Vec::new(), vec![0]); + selector.set_call_indirect_guards(synth_core::CallIndirectGuards { + tables: vec![hetero_table(0)], + type_ids_byte_offset: Some(8), + type_ids_image: vec![1, 300], + type_class_ids: vec![300], + }); + let err = selector + .select_with_stack(&ops, 0) + .expect_err("class id past the CMP imm8 must decline"); + assert!( + err.to_string().contains("#676") && err.to_string().contains("255"), + "loud range decline: {err}" + ); + + // Heterogeneous but NO sidecar → still a loud decline. + let mut selector = InstructionSelector::new(db.rules().to_vec()); + selector.set_func_arg_counts(Vec::new(), vec![0]); + selector.set_call_indirect_guards(synth_core::CallIndirectGuards { + tables: vec![hetero_table(0)], + ..Default::default() + }); + let err = selector + .select_with_stack(&ops, 0) + .expect_err("no sidecar → the runtime check is not emittable"); + assert!(err.to_string().contains("#676"), "loud decline: {err}"); + } + /// #650: `call_indirect` through table 1 lowers with THAT table's size in /// the bounds guard and its base byte offset (`size(table 0) * 4`) in the /// dispatch — the contiguous R11 region layout. @@ -14344,14 +14563,17 @@ mod tests { base_byte_offset: Some(0), type_reject: vec![None], has_null_slots: false, + runtime_type_check: false, }, synth_core::TableGuards { table_size: Some(41), base_byte_offset: Some(28), type_reject: vec![None], has_null_slots: false, + runtime_type_check: false, }, ], + ..Default::default() }); let wasm_ops = vec![ WasmOp::I32Const(1), @@ -14414,14 +14636,17 @@ mod tests { base_byte_offset: Some(0), type_reject: vec![Some("growable import".to_string())], has_null_slots: false, + runtime_type_check: false, }, synth_core::TableGuards { table_size: Some(4), base_byte_offset: None, type_reject: vec![None], has_null_slots: false, + runtime_type_check: false, }, ], + ..Default::default() }); let wasm_ops = vec![ WasmOp::I32Const(0), diff --git a/crates/synth-synthesis/src/rules.rs b/crates/synth-synthesis/src/rules.rs index 94b9b16e..096a08d8 100644 --- a/crates/synth-synthesis/src/rules.rs +++ b/crates/synth-synthesis/src/rules.rs @@ -554,6 +554,26 @@ pub enum ArmOp { /// load and the `BLX`. `false` (every slot verifiably initialized) /// keeps the pre-#664 expansion byte-identical BY CONSTRUCTION. null_check: bool, + /// #676: `Some((expected_class_id, type_id_byte_offset))` — the + /// dispatched table is HETEROGENEOUS (mixed signatures, so the + /// closed-world verdict cannot hold) and WASM Core §4.4.8's type + /// check is discharged at RUNTIME against the type-id sidecar: a + /// parallel `u32` array mirroring the pointer region slot for slot, + /// placed at `R11 + sum(all table sizes) * 4` per the layout + /// contract (see `synth_core::CallIndirectGuards`). After the + /// bounds guard the encoder emits + /// `MOV ip, idx, LSL #2; ADD ip, r11, ip; + /// LDR ip, [ip, #type_id_byte_offset]; CMP ip, #expected_class_id; + /// BEQ ok; UDF #0` — `type_id_byte_offset` is the FULL byte offset + /// from R11 to THIS table's type-id subarray (sidecar base + + /// `table_byte_offset`, <= 4095 per the LDR imm12 range, enforced + /// by the selector; `expected_class_id` is 1-based and <= 255 for + /// the CMP immediate, likewise enforced). Class id 0 is reserved + /// for null slots, so the compare also subsumes the #664 null trap + /// (the selector then passes `null_check: false`). `None` (every + /// homogeneous table) emits NOTHING — the pre-#676 expansion stays + /// byte-identical BY CONSTRUCTION. + type_check: Option<(u32, u32)>, }, // ======================================================================== diff --git a/crates/synth-verify/src/arm_semantics.rs b/crates/synth-verify/src/arm_semantics.rs index 2f7c7171..ece2aef9 100644 --- a/crates/synth-verify/src/arm_semantics.rs +++ b/crates/synth-verify/src/arm_semantics.rs @@ -487,6 +487,9 @@ impl ArmSemantics { table_size: _, table_byte_offset: _, null_check: _, + // #676: the runtime type check is likewise a trap + // (control-flow effect) on the sidecar-loaded class id. + type_check: _, } => { // Indirect function call through table let _table_index = state.get_reg(table_index_reg).clone(); diff --git a/crates/synth-verify/tests/comprehensive_verification.rs b/crates/synth-verify/tests/comprehensive_verification.rs index d58eadbd..7fd67b47 100644 --- a/crates/synth-verify/tests/comprehensive_verification.rs +++ b/crates/synth-verify/tests/comprehensive_verification.rs @@ -2001,6 +2001,7 @@ fn verify_call_indirect() { table_size: 4, // #642: bounds-guard immediate table_byte_offset: 0, // #650: table 0 of the contiguous R11 region null_check: false, // #664: fully-initialized table + type_check: None, // #676: homogeneous table }, ); diff --git a/scripts/repro/call_indirect_676_differential.py b/scripts/repro/call_indirect_676_differential.py new file mode 100644 index 00000000..2e657f77 --- /dev/null +++ b/scripts/repro/call_indirect_676_differential.py @@ -0,0 +1,264 @@ +#!/usr/bin/env python3 +"""#676 — heterogeneous-table call_indirect oracle: runtime type check. + +The fixture's 5-slot table interleaves TWO structural signature classes +(slots 0/2 = (i32,i32)->i32, slot 1 = (i32)->i32 — via a structurally- +duplicate type decl for slot 2, the meld dedup shape) and leaves slots 3/4 +null. Pre-#676 the closed-world verifier rejected EVERY expected type on +such a table and both dispatchers loud-declined — on origin/main this +harness is RED at the compile step (SYMBOL MISSING). #676 discharges the +WASM Core §4.4.8 type check at RUNTIME: the object carries a type-id +sidecar (`.synth.table_type_ids`, one u32 structural class id per slot, +id 0 = null) which the harness links at `R11 + sum(table sizes)*4` per the +layout contract, and the dispatch compares the indexed slot's id against +the expected class id (compile-time immediate), UDF-trapping on mismatch — +which also subsumes the #664 null trap (0 never equals an expected id). + +For each case both engines run: + - wasmtime (oracle): matching-class calls return values; wrong-class + calls trap ("indirect call type mismatch"); null slots trap + ("uninitialized element"); OOB indices trap ("undefined element"). + - unicorn (synth's code, pointer region at r11 + sidecar words at + r11+20, copied VERBATIM from the object's section): matching calls + must equal wasmtime; wrong-class, null AND OOB indices must all stop + AT A UDF. + +Non-vacuity: a build without the type check BLXes the wrong-typed function +and returns a wrong VALUE (e.g. via2(5,1) would call $neg and yield -5), +which the harness reports as a mismatch — red, not vacuously green. A +missing null check BLXes address 0 (fault, distinguished from the +deterministic UDF); the OOB decoy is inherited from #642/#650/#664 and +seeded PAST the sidecar words. + +Run (needs wasmtime + unicorn + pyelftools): + SYNTH=./target/debug/synth python scripts/repro/call_indirect_676_differential.py +Exits nonzero on any compile decline, missing sidecar, mismatch, or missed +trap. +""" + +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_ARM, UC_MODE_ARM, UC_MODE_THUMB, Uc, UcError +from unicorn.arm_const import ( + UC_ARM_REG_LR, + UC_ARM_REG_PC, + UC_ARM_REG_R0, + UC_ARM_REG_R1, + UC_ARM_REG_R11, + UC_ARM_REG_SP, +) + +WAT = Path(__file__).with_name("call_indirect_676_heterogeneous.wat") +SYNTH = os.environ.get("SYNTH", "./target/debug/synth") + +CODE, TABLE, STK = 0x1000000, 0x3000000, 0x6000000 +RET = CODE + 0xFFF0 # return pad (inside the CODE map) +DECOY = CODE + 0xFF00 # decoy "function" an unguarded/short-guarded build calls +X = 5 +N_SLOTS = 5 +SLOT_FUNCS = {0: "func_0", 1: "func_1", 2: "func_2"} # $add $neg $sub +# Per dispatcher: index -> expected wasmtime outcome kind. +CASES = { + "via2": {"ok": [0, 2], "type": [1], "null": [3, 4], "oob": [5, 99]}, + "via1": {"ok": [1], "type": [0, 2], "null": [3, 4], "oob": [5, 99]}, +} + + +def compile_direct(out: str, target: str) -> None: + """Compile via the direct-selector path (the one that lowers call_indirect).""" + r = subprocess.run( + [ + SYNTH, + "compile", + str(WAT), + "-o", + out, + "--target", + target, + "--all-exports", + "--relocatable", + "--no-optimize", + ], + capture_output=True, + text=True, + ) + if r.returncode != 0: + print(f"COMPILE FAILED:\n{r.stdout}\n{r.stderr}") + sys.exit(1) + + +# The §4.4.8 trap reason wasmtime must report per expected category — the +# CASES table above is itself oracle-checked, not hand-trusted. +TRAP_REASON = { + "type": "indirect call type mismatch", + "null": "uninitialized element", + "oob": "undefined element", +} + + +def wasmtime_oracle(): + """Ground truth: (export, idx) -> result or 'trap:'.""" + engine = wasmtime.Engine() + module = wasmtime.Module(engine, WAT.read_text()) + results = {} + for export, groups in CASES.items(): + for why, idxs in groups.items(): + for idx in idxs: + store = wasmtime.Store(engine) # fresh instance per call + f = wasmtime.Instance(store, module, []).exports(store)[export] + try: + results[(export, idx)] = f(store, X, idx) & 0xFFFFFFFF + assert why == "ok", f"{export}({X},{idx}) must trap ({why})" + except wasmtime.Trap as t: + reason = TRAP_REASON[why] + assert reason in t.message, ( + f"{export}({X},{idx}) must trap with '{reason}': {t.message}" + ) + results[(export, idx)] = f"trap:{reason}" + return results + + +def run_unicorn(text: bytes, syms: dict, sidecar: bytes, export: str, idx: int, a32: bool): + """Execute export(X, idx); returns ('ok', r0) or ('trap-udf', pc) or a failure.""" + mu = Uc(UC_ARCH_ARM, UC_MODE_ARM if a32 else UC_MODE_THUMB) + mu.mem_map(CODE, 0x100000) + mu.mem_map(TABLE, 0x10000) + mu.mem_map(STK, 0x100000) + mu.mem_write(CODE, text) + if a32: + mu.mem_write(RET, struct.pack(" int: + elf_path = f"/tmp/ci676_{'a32' if a32 else 'thumb'}.o" + compile_direct(elf_path, target) + + with open(elf_path, "rb") as fh: + e = ELFFile(fh) + text = bytes(e.get_section_by_name(".text").data()) + sidecar_sec = e.get_section_by_name(".synth.table_type_ids") + if sidecar_sec is None: + print("SIDECAR MISSING: no .synth.table_type_ids section (#676 red)") + return 1 + sidecar = bytes(sidecar_sec.data()) + # Symbols from the symtab, never from disasm text (host-dependent). + st = [s for s in e.iter_sections() if s["sh_type"] == "SHT_SYMTAB"][0] + syms = {s.name: s["st_value"] & ~1 for s in st.iter_symbols() if s.name} + if len(sidecar) != 4 * N_SLOTS: + print(f"SIDECAR SIZE: {len(sidecar)} bytes, want {4 * N_SLOTS} (#676 red)") + return 1 + for need in sorted(CASES) + sorted(SLOT_FUNCS.values()): + if need not in syms: + print(f"SYMBOL MISSING: {need} (a decline drops the function — #676 red)") + return 1 + + isa = "A32" if a32 else "Thumb-2" + ids = struct.unpack(f"<{N_SLOTS}I", sidecar) + print(f"[{isa}] sidecar class ids: {list(ids)}") + fails = 0 + for export, groups in CASES.items(): + for idx in groups["ok"]: + want = oracle[(export, idx)] + kind, got = run_unicorn(text, syms, sidecar, export, idx, a32) + ok = kind == "ok" and got == want + fails += 0 if ok else 1 + got_s = f"{got:#x}" if isinstance(got, int) else got + print( + f"[{isa}] {export}({X},{idx}) = {kind}:{got_s} (wasmtime: {want:#x}) " + f"{'OK' if ok else 'MISMATCH'}" + ) + for why in ["type", "null", "oob"]: + for idx in groups[why]: + want = oracle[(export, idx)] + assert isinstance(want, str) and want.startswith("trap"), ( + f"oracle must trap {export}({X},{idx}): {want}" + ) + kind, got = run_unicorn(text, syms, sidecar, export, idx, a32) + ok = kind == "trap-udf" + fails += 0 if ok else 1 + if ok: + print( + f"[{isa}] {export}({X},{idx}) = udf trap at {got:#x} " + f"({why} — wasmtime: {want}) OK" + ) + elif kind == "ok" and got == 0x5A: + print( + f"[{isa}] {export}({X},{idx}) = {got:#x} — the DECOY past the " + f"region was CALLED ({why}): bounds guard missing or short MISMATCH" + ) + else: + got_s = f"{got:#x}" if isinstance(got, int) else got + print( + f"[{isa}] {export}({X},{idx}) = {kind}:{got_s} ({why} — " + f"wasmtime: {want}) MISMATCH — a missing type check calls the " + "wrong-typed function (wrong value) or BLXes address 0" + ) + return fails + + +def main() -> int: + oracle = wasmtime_oracle() + print(f"wasmtime oracle: {oracle}") + + # Both ISAs share the expansion: Thumb-2 (cortex-m3) and A32 (cortex-r5). + fails = run_isa(oracle, "cortex-m3", a32=False) + fails += run_isa(oracle, "cortex-r5", a32=True) + + if fails == 0: + print("ORACLE: PASS") + return 0 + print(f"ORACLE: FAIL — {fails} case(s) diverged from wasmtime (#676)") + return 1 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/scripts/repro/call_indirect_676_heterogeneous.wat b/scripts/repro/call_indirect_676_heterogeneous.wat new file mode 100644 index 00000000..d555216e --- /dev/null +++ b/scripts/repro/call_indirect_676_heterogeneous.wat @@ -0,0 +1,35 @@ +;; #676 — HETEROGENEOUS funcref table: mixed signatures in one table are +;; valid wasm; a call_indirect selecting a wrong-typed entry is a RUNTIME +;; trap (WASM Core §4.4.8, wasmtime: "indirect call type mismatch"), not a +;; validation error. The closed-world verifier can never verify such a +;; table (every expected type sees a mismatching slot), so the sound +;; lowering is the runtime type check itself: compare the indexed slot's +;; structural class id — from the type-id sidecar — against the expected +;; type's class id, and UDF on mismatch. +;; +;; Layout contract (#650/#664/#676): the runtime/harness links the table as +;; raw 4-byte code pointers at R11 (null slots as ZERO words) and copies +;; the object's `.synth.table_type_ids` section VERBATIM to +;; `R11 + sum(all table sizes) * 4` — here R11+20 (5 slots). Class ids are +;; structural (the $bin2 duplicate shares $bin's id — the meld +;; 31-decls/25-distinct shape); id 0 is reserved for null slots, so the +;; type compare subsumes the #664 null trap. +;; +;; Table image (5 slots): [$add(bin)=1, $neg(un)=2, $sub(bin2≡bin)=1, null=0, +;; null=0] — two signature classes INTERLEAVED, plus nulls, plus OOB past 5. +(module + (type $bin (func (param i32 i32) (result i32))) + (type $un (func (param i32) (result i32))) + (type $bin2 (func (param i32 i32) (result i32))) ;; structural dup of $bin + (table 5 5 funcref) + (func $add (type $bin) (i32.add (local.get 0) (local.get 1))) + (func $neg (type $un) (i32.sub (i32.const 0) (local.get 0))) + (func $sub (type $bin2) (i32.sub (local.get 0) (local.get 1))) + (elem (i32.const 0) func $add $neg $sub) + ;; Expects class 1 (bin): slots 0/2 succeed, slot 1 type-traps, + ;; slots 3/4 null-trap, >= 5 OOB-traps. + (func (export "via2") (param $x i32) (param $sel i32) (result i32) + (call_indirect (type $bin) (local.get $x) (i32.const 3) (local.get $sel))) + ;; Expects class 2 (un): slot 1 succeeds, slots 0/2 type-trap. + (func (export "via1") (param $x i32) (param $sel i32) (result i32) + (call_indirect (type $un) (local.get $x) (local.get $sel))))