diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index e824f511..3a98e35a 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -529,6 +529,51 @@ jobs: SYNTH: ./target/debug/synth run: python scripts/repro/call_indirect_650_differential.py + call-indirect-664-nullslot-oracle: + name: null-funcref-slot call_indirect oracle (Thumb-2 + A32) + # VCR-ORACLE-001 (#242, #664): a table with null (uninitialized funcref) + # slots no longer poisons the closed world — the type check verifies the + # INITIALIZED slots only, and the null-slot trap (WASM Core §4.4.8: + # calling an uninitialized element traps) is discharged at RUNTIME: the + # layout contract links null slots as ZERO words and the dispatch + # null-checks the loaded pointer (`cmp ip,#0; bne ok; udf`) between the + # #642 bounds guard and the BLX. EXECUTE the sparse-table fixture (4 + # slots, only 1 and 3 initialized — the falcon fused-component shape) + # under unicorn on BOTH ISAs vs the wasmtime oracle: initialized slots + # must match, null AND OOB indices must stop at a UDF. Non-vacuous red: a + # build without the null check BLXes address 0 and faults (not a udf). + # On <= v0.35.0 this is red at compile: the null slot rejected every type + # and the function loud-declined (capability upgrade — red = "declines + # today", green = sound sparse-table dispatch). Fully-initialized tables + # stay byte-identical by construction (null_check=false emits the + # pre-#664 bytes), pinned by the frozen-fixture job and the + # #642/#650/#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 null-funcref-slot call_indirect oracle + env: + SYNTH: ./target/debug/synth + run: python scripts/repro/call_indirect_664_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 6bc64629..06ea93d8 100644 --- a/crates/synth-backend/src/arm_encoder.rs +++ b/crates/synth-backend/src/arm_encoder.rs @@ -143,6 +143,11 @@ impl ArmEncoder { /// single-load form (single-table modules byte-identical by /// construction). /// + /// #664, `null_check` (the table has null slots, linked as ZERO words + /// per the layout contract): `CMP r12, #0; BNE +1; UDF` between the + /// 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. @@ -150,6 +155,7 @@ impl ArmEncoder { table_index_reg: &Reg, table_size: u32, table_byte_offset: u32, + null_check: bool, ) -> Vec { let idx = reg_to_bits(table_index_reg); let mut bytes = Vec::with_capacity(32); @@ -195,6 +201,19 @@ impl ArmEncoder { let ldr: u32 = 0xE59CC000 | (table_byte_offset & 0xFFF); bytes.extend_from_slice(&ldr.to_le_bytes()); } + // #664: null-slot trap — only when the table image has null slots + // (zero-linked words). A fully-initialized table keeps the pre-#664 + // bytes identical by construction. + if null_check { + // CMP r12, #0 — data-processing CMP (immediate), Rn=r12. + bytes.extend_from_slice(&0xE35C_0000u32.to_le_bytes()); + // BNE +1 insn (skip the UDF when the pointer is non-null) — + // cond=NE(0001), imm24=0: target = branch + 8. + bytes.extend_from_slice(&0x1A00_0000u32.to_le_bytes()); + // UDF — the §4.4.8 uninitialized-element trap (same idiom as + // the bounds guard). + bytes.extend_from_slice(&0xE7F0_00F0u32.to_le_bytes()); + } // BLX r12 — cond=E, 0001 0010 1111 1111 1111 0011, Rm=r12. let blx: u32 = 0xE12FFF3C; bytes.extend_from_slice(&blx.to_le_bytes()); @@ -1211,6 +1230,7 @@ impl ArmEncoder { table_index_reg, table_size, table_byte_offset, + null_check, .. } = op { @@ -1218,6 +1238,7 @@ impl ArmEncoder { table_index_reg, *table_size, *table_byte_offset, + *null_check, )); } let instr: u32 = match op { @@ -3706,12 +3727,16 @@ impl ArmEncoder { // #650, table_byte_offset != 0 (a non-zero table in the contiguous // R11 region): the pointer load becomes // ADD R12,R11,R12; LDR R12,[R12,#offset] + // #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 ArmOp::CallIndirect { rd: _, type_idx: _, table_index_reg, table_size, table_byte_offset, + null_check, } => { let idx_reg = reg_to_bits(table_index_reg); let mut bytes = Vec::new(); @@ -3809,6 +3834,26 @@ impl ArmEncoder { ); } + // #664: null-slot trap — ONLY when the table image carries + // null (uninitialized) slots, which the layout contract + // requires to be linked as ZERO words. A fully-initialized + // table skips this branch entirely, keeping the pre-#664 + // expansion byte-identical BY CONSTRUCTION (the #650 + // offset-0 trick). + if *null_check { + // CMP.W R12, #0 — T2 CMP (immediate): 11110 i 0 1101 1 + // Rn(4) | 0 imm3 1111 imm8, Rn=R12, imm=0. + bytes.extend_from_slice(&0xF1BCu16.to_le_bytes()); + bytes.extend_from_slice(&0x0F00u16.to_le_bytes()); + // BNE +1 insn (skip the UDF when the pointer is non-null) + // — B.N imm8=0: target = branch + 4. NE. + bytes.extend_from_slice(&0xD100u16.to_le_bytes()); + // UDF #0 — call_indirect null-funcref trap (WASM Core + // §4.4.8: calling an uninitialized element traps; same + // trap idiom as the bounds guard above). + bytes.extend_from_slice(&0xDE00u16.to_le_bytes()); + } + // BLX R12 (call function indirectly) // BLX Rm (16-bit): 0100 0111 1 Rm 000 let blx: u16 = 0x47E0; // BLX R12 @@ -8881,6 +8926,7 @@ mod tests { table_index_reg: Reg::R0, table_size: 4, table_byte_offset: 0, + null_check: false, }) .unwrap(); assert_eq!( @@ -8927,6 +8973,7 @@ mod tests { table_index_reg: Reg::R4, table_size: 4, table_byte_offset: 0, + null_check: false, }) .unwrap(); let cmp = u32::from_le_bytes(bytes[4..8].try_into().unwrap()); @@ -8948,6 +8995,7 @@ mod tests { table_index_reg: Reg::R0, table_size: 0x0002_0003, table_byte_offset: 0, + null_check: false, }) .unwrap(); assert_eq!(bytes.len(), 32, "MOVT arm adds one word: {bytes:02x?}"); @@ -8983,6 +9031,7 @@ mod tests { table_index_reg: Reg::R0, table_size: 4, table_byte_offset: 0, + null_check: false, }) .unwrap(); assert_eq!( @@ -9015,6 +9064,7 @@ mod tests { table_index_reg: Reg::R4, table_size: 4, table_byte_offset: 0, + null_check: false, }) .unwrap(); assert_eq!(&bytes[4..6], &[0x64, 0x45], "cmp r4, ip: {bytes:02x?}"); @@ -9039,6 +9089,7 @@ mod tests { table_index_reg: Reg::R8, table_size: 3, table_byte_offset: 0, + null_check: false, }) .unwrap(); // cmp r8, ip — T2: 0x4500 | N(1)<<7 | Rm(12)<<3 | Rn(0) = 0x45E0 @@ -9051,6 +9102,7 @@ mod tests { table_index_reg: Reg::R0, table_size: 0x0002_0003, table_byte_offset: 0, + null_check: false, }) .unwrap(); // movw ip,#3 then movt ip,#2 — the size must not be truncated. @@ -9078,6 +9130,7 @@ mod tests { table_index_reg: Reg::R1, table_size: 41, table_byte_offset: 28, + null_check: false, }) .unwrap(); assert_eq!( @@ -9106,6 +9159,7 @@ mod tests { table_index_reg: Reg::R1, table_size: 41, table_byte_offset: 0, + null_check: false, }) .unwrap(); assert_eq!( @@ -9132,6 +9186,7 @@ mod tests { table_index_reg: Reg::R1, table_size: 41, table_byte_offset: 28, + null_check: false, }) .unwrap(); let words: Vec = bytes @@ -9160,6 +9215,77 @@ mod tests { assert_eq!(words[7], 0xE12F_FF3C, "BLX r12: {:#010x}", words[7]); } + /// #664: `null_check` inserts a null-funcref trap between the Thumb-2 + /// pointer load and the `BLX` (`cmp.w ip, #0; bne .+4; udf #0`) — a + /// zero-linked (uninitialized) slot must TRAP (WASM §4.4.8), never + /// branch to address 0. `null_check: false` keeps the expansion + /// byte-identical to the pre-#664 form (by-construction pin). + #[test] + fn test_encode_thumb_call_indirect_null_check_664() { + use synth_synthesis::{ArmOp, Reg}; + let enc = ArmEncoder::new_thumb2(); + let op = |null_check| ArmOp::CallIndirect { + rd: Reg::R0, + type_idx: 0, + table_index_reg: Reg::R1, + table_size: 4, + table_byte_offset: 0, + null_check, + }; + let with = enc.encode(&op(true)).unwrap(); + let without = enc.encode(&op(false)).unwrap(); + // The checked form = the unchecked form with EXACTLY the three-insn + // null check spliced in before the final BLX (byte identity of the + // shared prefix/suffix — nothing else may move). + assert_eq!( + with.len(), + without.len() + 8, + "cmp.w (4) + bne (2) + udf (2): {with:02x?}" + ); + let blx_at = without.len() - 2; + assert_eq!(&with[..blx_at], &without[..blx_at], "shared prefix"); + assert_eq!( + &with[blx_at..], + &[ + 0xBC, 0xF1, 0x00, 0x0F, // cmp.w ip, #0 + 0x00, 0xD1, // bne .+4 (skip the udf) + 0x00, 0xDE, // udf #0 — null-funcref trap (#664) + 0xE0, 0x47, // blx ip + ], + "null check precedes the BLX: {with:02x?}" + ); + assert_eq!(&with[with.len() - 2..], &without[blx_at..], "same BLX"); + } + + /// #664: the A32 twin — `cmp r12, #0; bne .+8; udf` before the `BLX`; + /// `null_check: false` keeps the #594/#642/#650 bytes identical. + #[test] + fn test_encode_arm32_call_indirect_null_check_664() { + use synth_synthesis::{ArmOp, Reg}; + let enc = ArmEncoder::new_arm32(); + let op = |null_check| ArmOp::CallIndirect { + rd: Reg::R0, + type_idx: 0, + table_index_reg: Reg::R1, + table_size: 4, + table_byte_offset: 0, + null_check, + }; + let with = enc.encode(&op(true)).unwrap(); + let without = enc.encode(&op(false)).unwrap(); + assert_eq!(with.len(), without.len() + 12, "3 A32 words: {with:02x?}"); + let blx_at = without.len() - 4; + assert_eq!(&with[..blx_at], &without[..blx_at], "shared prefix"); + let words: Vec = with[blx_at..] + .chunks_exact(4) + .map(|w| u32::from_le_bytes(w.try_into().unwrap())) + .collect(); + assert_eq!(words[0], 0xE35C_0000, "CMP r12,#0: {:#010x}", words[0]); + assert_eq!(words[1], 0x1A00_0000, "BNE +1 insn: {:#010x}", words[1]); + assert_eq!(words[2], 0xE7F0_00F0, "UDF (null trap): {:#010x}", words[2]); + assert_eq!(words[3], 0xE12F_FF3C, "BLX r12: {:#010x}", words[3]); + } + /// #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 d96849e1..dbdc77af 100644 --- a/crates/synth-backend/tests/a32_no_silent_nop_615.rs +++ b/crates/synth-backend/tests/a32_no_silent_nop_615.rs @@ -651,6 +651,7 @@ fn representatives() -> Vec { table_index_reg: Reg::R2, 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 }, I64Add { rdlo: dl, diff --git a/crates/synth-core/src/wasm_decoder.rs b/crates/synth-core/src/wasm_decoder.rs index fca069ed..718f495f 100644 --- a/crates/synth-core/src/wasm_decoder.rs +++ b/crates/synth-core/src/wasm_decoder.rs @@ -128,6 +128,16 @@ pub struct TableGuards { /// against THIS table; `Some(reason)` = not verifiable (the lowering /// declines). pub type_reject: Vec>, + /// #664: whether this table's image contains at least one uninitialized + /// (null funcref) slot. WASM Core §4.4.8 requires a `call_indirect` + /// reaching a null slot to TRAP — the closed-world type check verifies + /// the INITIALIZED slots only, and the lowering must emit a runtime + /// null check (pointer == 0 → trap) before the indirect branch when + /// this is set. `false` for a fully-initialized table keeps today's + /// exact dispatch bytes (no null check) BY CONSTRUCTION. Only + /// meaningful when the type verdict is `None` (verified); reject paths + /// decline before it is consulted. + pub has_null_slots: bool, } /// #642/#650: everything the `call_indirect` lowering needs to emit its @@ -153,11 +163,19 @@ pub struct TableGuards { /// - the BOUNDS check is emitted at runtime against THAT table's /// compile-time `table_size` immediate (sound: fixed-size, see above), and /// - the TYPE check is discharged at COMPILE time: for expected type `t`, -/// `tables[n].type_reject[t]` is `None` only when every slot of table `n` -/// is verifiably initialized with a function whose signature structurally +/// `tables[n].type_reject[t]` is `None` only when every INITIALIZED slot +/// of table `n` verifiably holds a function whose signature structurally /// equals type `t` (the closed-world property — no runtime mismatch is /// then possible). Otherwise it holds the reason, and the lowering -/// declines LOUDLY rather than emit an unchecked indirect branch. +/// declines LOUDLY rather than emit an unchecked indirect branch, and +/// - a NULL (uninitialized) slot traps at RUNTIME (#664): the layout +/// contract requires the runtime/harness to link every uninitialized +/// slot as a ZERO word (null funcref has no code address; 0 is never a +/// valid function pointer in the region), and when `has_null_slots` is +/// 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. #[derive(Debug, Clone, Default, PartialEq, Eq)] pub struct CallIndirectGuards { /// Per-table guard inputs, indexed by table index (imports first). The @@ -174,6 +192,7 @@ impl CallIndirectGuards { table_size, base_byte_offset: Some(0), type_reject, + has_null_slots: false, }], } } @@ -296,11 +315,13 @@ impl DecodedModule { 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 = self.table_type_reject(n as u32, size, global_poison, n_types); + let (type_reject, has_null_slots) = + self.table_type_reject(n as u32, size, global_poison, n_types); tables.push(TableGuards { table_size: size, base_byte_offset, type_reject, + has_null_slots, }); base_words = match (base_words, size) { (Some(w), Some(s)) => w.checked_add(s), @@ -311,16 +332,21 @@ impl DecodedModule { } /// #642/#650: the closed-world type verdicts for ONE table — `None` per - /// expected type when every slot of table `n` verifiably holds a function - /// of that exact structural signature; `Some(reason)` otherwise. + /// expected type when every INITIALIZED slot of table `n` verifiably + /// holds a function of that exact structural signature; `Some(reason)` + /// otherwise. The second component is `has_null_slots` (#664): whether + /// 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). fn table_type_reject( &self, n: u32, size: Option, global_poison: Option<&str>, n_types: usize, - ) -> Vec> { - let reject_all = |reason: String| vec![Some(reason); n_types]; + ) -> (Vec>, bool) { + let reject_all = |reason: String| (vec![Some(reason); n_types], false); if let Some(reason) = global_poison { return reject_all(reason.to_string()); @@ -355,18 +381,17 @@ impl DecodedModule { *slot = Some(f); } } - // An uninitialized slot is a null funcref: calling it must trap, and - // the raw code-pointer table has no runtime representation of null to - // check against — so it breaks the closed world for EVERY type. - if let Some(i) = slots.iter().position(|s| s.is_none()) { - return reject_all(format!( - "table {n} slot {i} is uninitialized (null funcref) — a \ - `call_indirect` reaching it must trap, and the raw \ - code-pointer table has no runtime null/type id to check" - )); - } - - (0..n_types) + // #664: an uninitialized slot is a null funcref — calling it must + // trap (WASM Core §4.4.8). It no longer poisons the closed world + // (pre-#664 it rejected EVERY type): the layout contract requires + // null slots to be linked as ZERO words, so the lowering discharges + // the trap at RUNTIME with a null check on the loaded pointer. The + // type check below therefore covers the INITIALIZED slots only — + // a null slot can never produce a live callee of the wrong type, + // because the null check traps before the branch. + let has_null_slots = slots.iter().any(|s| s.is_none()); + + let rejects = (0..n_types) .map(|t| { for f in slots.iter().flatten() { let Some(&fty) = self.func_type_indices.get(*f as usize) else { @@ -384,7 +409,8 @@ impl DecodedModule { } None }) - .collect() + .collect(); + (rejects, has_null_slots) } } @@ -2493,6 +2519,11 @@ mod tests { "closed-world type check must verify the homogeneous table: {:?}", guards.tables[0].type_reject ); + assert!( + !guards.tables[0].has_null_slots, + "#664: a fully-initialized table must NOT request the runtime \ + null check (dispatch bytes stay identical by construction)" + ); } /// #642: a heterogeneous table (an entry whose signature differs from the @@ -2528,11 +2559,13 @@ mod tests { ); } - /// #642: an uninitialized table slot (elem covers less than the declared - /// size) is a null funcref — calling it must trap, which the raw - /// code-pointer table cannot express at runtime → reject all types. + /// #664 (relaxes the #642 all-reject): an uninitialized table slot (elem + /// covers less than the declared size) is a null funcref — calling it + /// must trap, which is now discharged at RUNTIME (null check on the + /// zero-linked pointer), so the closed-world verdict verifies the + /// INITIALIZED slots and sets `has_null_slots` for the lowering. #[test] - fn test_call_indirect_guards_null_slot_rejects_642() { + fn test_call_indirect_guards_null_slot_verifies_with_flag_664() { let wat = r#" (module (type $s (func (result i32))) @@ -2548,18 +2581,71 @@ mod tests { let module = decode_wasm_module(&wasm).expect("decode"); let guards = module.call_indirect_guards(); assert_eq!(guards.tables[0].table_size, Some(3)); + assert_eq!( + guards.tables[0].type_reject.first(), + Some(&None), + "initialized slots are homogeneous in $s — the verdict must \ + verify despite the null slot (#664): {:?}", + guards.tables[0].type_reject + ); assert!( - guards.tables[0].type_reject.iter().all(|r| r.is_some()), - "slot 2 is a null funcref — every type must be rejected: {:?}", + guards.tables[0].has_null_slots, + "slot 2 is uninitialized — the lowering must emit the runtime \ + null check (#664)" + ); + } + + /// #664: the falcon shape — a SPARSE table (only slots 1 and 3 of 4 + /// initialized, by two separate segments) verifies with the null flag; + /// a sparse table whose INITIALIZED slots are heterogeneous still + /// rejects (the runtime null check cannot discharge a TYPE mismatch). + #[test] + fn test_call_indirect_guards_sparse_table_664() { + let wat = r#" + (module + (type $t (func (param i32) (result i32))) + (table 4 4 funcref) + (func $f1 (type $t) (i32.add (local.get 0) (i32.const 100))) + (func $f3 (type $t) (i32.sub (i32.const 1000) (local.get 0))) + (elem (i32.const 1) $f1) + (elem (i32.const 3) $f3) + (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_eq!(guards.tables[0].table_size, Some(4)); + assert_eq!( + guards.tables[0].type_reject.first(), + Some(&None), + "slots 1,3 are homogeneous in $t — verified: {:?}", guards.tables[0].type_reject ); + assert!(guards.tables[0].has_null_slots, "slots 0,2 are null"); + + // Heterogeneous INITIALIZED slots in a sparse table: still rejected. + let wat = r#" + (module + (type $t (func (param i32) (result i32))) + (type $u (func (param i32 i32) (result i32))) + (table 4 4 funcref) + (func $f1 (type $t) (local.get 0)) + (func $f3 (type $u) (i32.add (local.get 0) (local.get 1))) + (elem (i32.const 1) $f1) + (elem (i32.const 3) $f3) + (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].type_reject[0] - .as_deref() - .unwrap() - .contains("slot 2"), - "reason names the uninitialized slot: {:?}", - guards.tables[0].type_reject[0] + guards.tables[0].type_reject[0].is_some() && guards.tables[0].type_reject[1].is_some(), + "a heterogeneous sparse table must still reject every type: {:?}", + guards.tables[0].type_reject ); } diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index b20f518a..6bc3faab 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -2177,11 +2177,14 @@ 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). fn resolve_call_indirect_guards( &self, table_index: u32, type_index: u32, - ) -> Result<(u32, u32)> { + ) -> Result<(u32, u32, bool)> { let n_tables = self.call_indirect_guards.tables.len(); let table = self .call_indirect_guards @@ -2235,7 +2238,7 @@ impl InstructionSelector { ))); } } - Ok((table_size, table_byte_offset)) + Ok((table_size, table_byte_offset, table.has_null_slots)) } /// Enable relocatable host-link mode (#197): import calls emit a direct @@ -2886,7 +2889,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) = + let (table_size, table_byte_offset, null_check) = self.resolve_call_indirect_guards(*table_index, *type_index)?; vec![ArmOp::CallIndirect { rd, @@ -2894,6 +2897,8 @@ impl InstructionSelector { table_index_reg: rn, // Table index from stack table_size, table_byte_offset, + // #664: trap on a null (zero-linked) slot at runtime. + null_check, }] } @@ -9419,7 +9424,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) = + let (table_size, table_byte_offset, null_check) = self.resolve_call_indirect_guards(*table_index, *type_index)?; // Top of stack is the table index; the call arguments sit @@ -9529,9 +9534,12 @@ impl InstructionSelector { // #642: the encoder emits `CMP idx, size; BLO ok; // UDF #0` before the table load. #650: a non-zero // offset routes the load through the table's base - // within the contiguous R11 region. + // within the contiguous R11 region. #664: a table + // with null slots gets a runtime null check on + // the loaded pointer (zero-linked slot → trap). table_size, table_byte_offset, + null_check, }, source_line: Some(idx), }); @@ -13910,6 +13918,7 @@ mod tests { ArmOp::CallIndirect { table_size: 3, table_byte_offset: 0, // #650: table 0 stays at R11 offset 0 + null_check: false, // #664: fully-initialized → no check .. } )), @@ -13917,6 +13926,45 @@ mod tests { ); } + /// #664: a VERIFIED table whose image carries null (uninitialized) slots + /// lowers with `null_check: true` — the encoder traps on a zero-linked + /// pointer between the table load and the `BLX`. + #[test] + fn test_664_call_indirect_null_slots_carry_null_check() { + let db = RuleDatabase::new(); + 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![synth_core::TableGuards { + table_size: Some(4), + base_byte_offset: Some(0), + type_reject: vec![None], // initialized slots verified + has_null_slots: true, // slots 0,2 null (the falcon shape) + }], + }); + let wasm_ops = vec![ + WasmOp::I32Const(1), + WasmOp::CallIndirect { + type_index: 0, + table_index: 0, + }, + ]; + let arm = selector + .select_with_stack(&wasm_ops, 0) + .expect("a sparse-but-verified call_indirect must lower (#664)"); + assert!( + arm.iter().any(|i| matches!( + &i.op, + ArmOp::CallIndirect { + table_size: 4, + null_check: true, + .. + } + )), + "the pseudo-op must request the runtime null check: {arm:#?}" + ); + } + /// #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. @@ -13931,11 +13979,13 @@ mod tests { table_size: Some(7), base_byte_offset: Some(0), type_reject: vec![None], + has_null_slots: false, }, synth_core::TableGuards { table_size: Some(41), base_byte_offset: Some(28), type_reject: vec![None], + has_null_slots: false, }, ], }); @@ -13999,11 +14049,13 @@ mod tests { table_size: None, base_byte_offset: Some(0), type_reject: vec![Some("growable import".to_string())], + has_null_slots: false, }, synth_core::TableGuards { table_size: Some(4), base_byte_offset: None, type_reject: vec![None], + has_null_slots: false, }, ], }); diff --git a/crates/synth-synthesis/src/rules.rs b/crates/synth-synthesis/src/rules.rs index 358b5523..94b9b16e 100644 --- a/crates/synth-synthesis/src/rules.rs +++ b/crates/synth-synthesis/src/rules.rs @@ -546,6 +546,14 @@ pub enum ArmOp { /// (offset <= 4095 — the LDR imm12 range — enforced by the /// selector's loud decline). table_byte_offset: u32, + /// #664: the dispatched table contains null (uninitialized funcref) + /// slots, which the layout contract requires the runtime/harness to + /// link as ZERO words. WASM Core §4.4.8 requires a `call_indirect` + /// reaching one to TRAP, so the encoder inserts a null check on the + /// loaded pointer (`CMP ip, #0; BNE ok; UDF #0`) between the table + /// load and the `BLX`. `false` (every slot verifiably initialized) + /// keeps the pre-#664 expansion byte-identical BY CONSTRUCTION. + null_check: bool, }, // ======================================================================== diff --git a/crates/synth-verify/src/arm_semantics.rs b/crates/synth-verify/src/arm_semantics.rs index 421bb31b..2f7c7171 100644 --- a/crates/synth-verify/src/arm_semantics.rs +++ b/crates/synth-verify/src/arm_semantics.rs @@ -482,9 +482,11 @@ impl ArmSemantics { // #642: the bounds guard is a control-flow effect (trap), not // modeled by the symbolic call result. #650: the table base // offset only changes WHICH pointer is loaded, not the - // symbolic result shape. + // symbolic result shape. #664: the null check is likewise a + // trap (control-flow effect) on the loaded pointer. table_size: _, table_byte_offset: _, + null_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 9e890918..d58eadbd 100644 --- a/crates/synth-verify/tests/comprehensive_verification.rs +++ b/crates/synth-verify/tests/comprehensive_verification.rs @@ -2000,6 +2000,7 @@ fn verify_call_indirect() { table_index_reg: Reg::R1, 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 }, ); diff --git a/scripts/repro/call_indirect_664_differential.py b/scripts/repro/call_indirect_664_differential.py new file mode 100644 index 00000000..2eb12995 --- /dev/null +++ b/scripts/repro/call_indirect_664_differential.py @@ -0,0 +1,215 @@ +#!/usr/bin/env python3 +"""#664 — null-funcref-slot call_indirect oracle: sparse tables trap, not decline. + +The fixture's 4-slot table has only slots 1 and 3 initialized; 0 and 2 are +null funcrefs. Pre-#664 the closed-world verifier POISONED such a table +(every type rejected) and the whole function loud-declined — on origin/main +this harness is RED at the compile step (SYMBOL MISSING). #664 relaxes the +verdict to "every INITIALIZED slot type-equal" and discharges the null-slot +trap at RUNTIME: the layout contract requires the runtime/harness to link +every uninitialized slot as a ZERO word, and the dispatch null-checks the +loaded pointer (`cmp ip, #0; bne ok; udf`) between the #642 bounds guard +and the BLX. + +For each case both engines run: + - wasmtime (oracle): via(x, 1/3) return values; via(x, 0/2) trap with + "uninitialized element"; via(x, 4/99) trap OOB. + - unicorn (synth's code, table linked at r11 per the contract — null + slots as ZERO words, words past the region decoy-seeded): initialized + slots must match wasmtime; null AND OOB indices must stop AT A UDF. + +Non-vacuity: a build without the null check BLXes address 0 — an unmapped +fetch fault, which the harness distinguishes from the deterministic UDF +trap (red, not vacuously green). The OOB decoy is inherited from #642/#650. + +Run (needs wasmtime + unicorn + pyelftools): + SYNTH=./target/debug/synth python scripts/repro/call_indirect_664_differential.py +Exits nonzero on any compile decline, 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_664_nullslot.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 +INIT = [1, 3] # initialized slots -> $f1 (x+100), $f3 (1000-x) +NULL = [0, 2] # uninitialized slots -> must trap (§4.4.8) +OOB = [4, 99] # past the table -> must trap (#642 bounds guard) +SLOT_FUNCS = {1: "func_0", 3: "func_1"} # table image: slot -> symbol + + +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) + + +def wasmtime_oracle(): + """Ground truth: idx -> result or 'trap'.""" + engine = wasmtime.Engine() + module = wasmtime.Module(engine, WAT.read_text()) + results = {} + for idx in INIT + NULL + OOB: + store = wasmtime.Store(engine) # fresh instance per call (stateful) + f = wasmtime.Instance(store, module, []).exports(store)["via"] + try: + results[idx] = f(store, X, idx) & 0xFFFFFFFF + except wasmtime.Trap: + results[idx] = "trap" + return results + + +def run_unicorn(text: bytes, syms: dict, idx: int, a32: bool): + """Execute via(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/ci664_{'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()) + # 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} + for need in ["via"] + sorted(SLOT_FUNCS.values()): + if need not in syms: + print(f"SYMBOL MISSING: {need} (a decline drops the function — #664 red)") + return 1 + + isa = "A32" if a32 else "Thumb-2" + fails = 0 + for idx in INIT: + want = oracle[idx] + kind, got = run_unicorn(text, syms, 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}] via({X},{idx}) = {kind}:{got_s} (wasmtime: {want:#x}) " + f"{'OK' if ok else 'MISMATCH'}" + ) + for idx in NULL + OOB: + assert oracle[idx] == "trap", f"oracle must trap idx {idx}" + why = "null slot" if idx in NULL else "OOB" + kind, got = run_unicorn(text, syms, idx, a32) + ok = kind == "trap-udf" + fails += 0 if ok else 1 + if ok: + print(f"[{isa}] via({X},{idx}) = udf trap at {got:#x} ({why}, wasmtime: trap) OK") + elif kind == "ok" and got == 0x5A: + print( + f"[{isa}] via({X},{idx}) = {got:#x} — the DECOY past the table was " + f"CALLED ({why}): bounds guard missing or short MISMATCH" + ) + else: + print( + f"[{isa}] via({X},{idx}) = {kind}:{got} ({why}, wasmtime: trap) " + "MISMATCH — a missing null check BLXes address 0 and faults here" + ) + 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 (#664)") + return 1 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/scripts/repro/call_indirect_664_nullslot.wat b/scripts/repro/call_indirect_664_nullslot.wat new file mode 100644 index 00000000..b5c5d358 --- /dev/null +++ b/scripts/repro/call_indirect_664_nullslot.wat @@ -0,0 +1,20 @@ +;; #664 — sparse funcref table: null (uninitialized) slots must TRAP, not +;; decline the whole function. 4 slots, only 1 and 3 initialized (by two +;; separate element segments — the falcon fused-component shape); slots 0 +;; and 2 are null funcrefs. WASM Core §4.4.8: call_indirect through a null +;; slot traps ("uninitialized element" in wasmtime); through 1/3 it calls +;; $f1/$f3; index >= 4 is the OOB trap. +;; +;; Layout contract (#650/#664): the runtime/harness links the table as raw +;; 4-byte code pointers at R11 and MUST link every uninitialized slot as a +;; ZERO word — the emitted null check (`cmp ip, #0; bne ok; udf`) turns +;; that zero into the §4.4.8 trap. +(module + (type $t (func (param i32) (result i32))) + (table 4 4 funcref) + (func $f1 (type $t) (i32.add (local.get 0) (i32.const 100))) + (func $f3 (type $t) (i32.sub (i32.const 1000) (local.get 0))) + (elem (i32.const 1) func $f1) + (elem (i32.const 3) func $f3) + (func (export "via") (param $x i32) (param $sel i32) (result i32) + (call_indirect (type $t) (local.get $x) (local.get $sel))))