From 2fc963f0d04d1c4e2eb65e68724f08fadff9f087 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 8 Jul 2026 17:31:18 +0200 Subject: [PATCH] =?UTF-8?q?feat(codegen):=20multi-table=20call=5Findirect?= =?UTF-8?q?=20=E2=80=94=20contiguous=20R11=20table=20region=20(#650)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Tables become ONE contiguous region of raw 4-byte code pointers at R11, in declaration order: table 0 at R11+0 (unchanged), table N at R11 + sum(size(0..N))*4 — a compile-time constant, since tables are provably fixed-size (#642: table.grow/table.set loud-skip at decode). - decoder: per-table sizes (table_sizes), per-segment table attribution (ElemSegmentInfo.table_index), CallIndirectGuards restructured to per-table TableGuards { table_size, base_byte_offset, type_reject } — the #646 closed-world type verification now runs per (table, type), and an unverifiable segment poisons only the table it targets (passive/declared/non-const-offset segments still poison all). - selector: shared resolve_call_indirect_guards() feeds both arms; the bounds guard compares against the DISPATCHED table's own size; a table past the linked region, an unknown size, an unknown base (preceding growable import), or a base past LDR imm12 (4095) each loud-decline with a named reason. - encoder (Thumb-2 + A32): non-zero base folds into the pointer load (add ip, r11, ip; ldr ip, [ip, #off]); offset 0 emits the exact pre-#650 bytes, so single-table modules are byte-identical BY CONSTRUCTION (verified: whole-ELF identity vs origin/main on the #642/#594/#597 fixtures, cortex-m3/-r5/-m7dp, ±relocatable; frozen anchors 10/10). - oracle: call_indirect_650_differential.py (CI-gated) — two tables, overlapping indices, aliasing canary (table0[1] != table1[1]), OOB traps per-table, both ISAs; 26/26 green here, red on <= v0.33.1 (compile-time decline — this is a capability upgrade). Unblocks falcon's multi-table fused components (20 of 146 functions dispatched through table 1). Fixes #650. Builds on #646 (#642 guards) and the #275 R11 arc. Co-Authored-By: Claude Fable 5 --- .github/workflows/ci.yml | 40 ++ crates/synth-backend/src/arm_encoder.rs | 190 +++++++- .../tests/a32_no_silent_nop_615.rs | 3 +- crates/synth-core/src/lib.rs | 2 +- crates/synth-core/src/wasm_decoder.rs | 431 +++++++++++++----- .../src/instruction_selector.rs | 313 +++++++++---- crates/synth-synthesis/src/rules.rs | 27 +- crates/synth-verify/src/arm_semantics.rs | 5 +- .../tests/comprehensive_verification.rs | 3 +- .../repro/call_indirect_650_differential.py | 225 +++++++++ .../repro/call_indirect_650_multitable.wat | 27 ++ 11 files changed, 1034 insertions(+), 232 deletions(-) create mode 100644 scripts/repro/call_indirect_650_differential.py create mode 100644 scripts/repro/call_indirect_650_multitable.wat diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index fff95d7..e824f51 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -489,6 +489,46 @@ jobs: SYNTH: ./target/debug/synth run: python scripts/repro/call_indirect_642_differential.py + call-indirect-650-multitable-oracle: + name: multi-table call_indirect oracle (Thumb-2 + A32) + # VCR-ORACLE-001 (#242, #650): tables are ONE contiguous region of 4-byte + # code pointers at R11 (table N at sum(size(0..N))*4, a compile-time + # constant -- tables are provably fixed-size, #642). EXECUTE a TWO-table + # fixture with OVERLAPPING indices and DISTINCT functions under unicorn on + # BOTH ISAs vs the wasmtime oracle: dispatch through both tables must + # match, OOB on EITHER table must stop at a UDF (bounds guard against THAT + # table's own size), and the aliasing canary (table0[1] != table1[1]) + # catches a backend that drops the table index. On <= v0.33.1 this is red + # at compile: table-1 call_indirect loud-declined (capability upgrade -- + # red = "declines today", green = correct dispatch). Single-table modules + # stay byte-identical by construction (offset 0 = the pre-#650 expansion), + # pinned by the frozen-fixture job and the #642/#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 multi-table call_indirect oracle + env: + SYNTH: ./target/debug/synth + run: python scripts/repro/call_indirect_650_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 d9ae472..6bc6462 100644 --- a/crates/synth-backend/src/arm_encoder.rs +++ b/crates/synth-backend/src/arm_encoder.rs @@ -137,10 +137,20 @@ impl ArmEncoder { /// BLX r12 ; indirect call /// ``` /// + /// #650, `table_byte_offset != 0` (a non-zero table of the contiguous + /// R11 region): the pointer load becomes + /// `ADD r12, r11, r12; LDR r12, [r12, #offset]` — offset 0 keeps the + /// single-load form (single-table modules byte-identical by + /// construction). + /// /// 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. - fn encode_arm_call_indirect(table_index_reg: &Reg, table_size: u32) -> Vec { + fn encode_arm_call_indirect( + table_index_reg: &Reg, + table_size: u32, + table_byte_offset: u32, + ) -> Vec { let idx = reg_to_bits(table_index_reg); let mut bytes = Vec::with_capacity(32); // MOVW r12, #(size & 0xFFFF) — cond=E 0011 0000 imm4 Rd imm12. @@ -166,9 +176,25 @@ impl ArmEncoder { // imm5=2/LSL: cond=E, opcode=1101, S=0, Rd=r12. let mov: u32 = 0xE1A0C000 | (2 << 7) | idx; bytes.extend_from_slice(&mov.to_le_bytes()); - // LDR r12, [r11, r12] — register offset, P=1 U=1 B=0 W=0 L=1. - let ldr: u32 = 0xE79BC00C; - bytes.extend_from_slice(&ldr.to_le_bytes()); + if table_byte_offset == 0 { + // Table 0 (base = R11 itself): the pre-#650 single-load form. + // LDR r12, [r11, r12] — register offset, P=1 U=1 B=0 W=0 L=1. + let ldr: u32 = 0xE79BC00C; + bytes.extend_from_slice(&ldr.to_le_bytes()); + } else { + // #650: fold the table's compile-time base offset into the + // pointer load via the LDR imm12 form. + assert!( + table_byte_offset <= 4095, + "call_indirect table base offset {table_byte_offset} exceeds \ + LDR imm12 — the selector must have declined this (#650)" + ); + // ADD r12, r11, r12 — data-processing ADD (register). + bytes.extend_from_slice(&0xE08BC00Cu32.to_le_bytes()); + // LDR r12, [r12, #offset] — immediate offset, P=1 U=1 L=1. + let ldr: u32 = 0xE59CC000 | (table_byte_offset & 0xFFF); + bytes.extend_from_slice(&ldr.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()); @@ -1184,10 +1210,15 @@ impl ArmEncoder { if let ArmOp::CallIndirect { table_index_reg, table_size, + table_byte_offset, .. } = op { - return Ok(Self::encode_arm_call_indirect(table_index_reg, *table_size)); + return Ok(Self::encode_arm_call_indirect( + table_index_reg, + *table_size, + *table_byte_offset, + )); } let instr: u32 = match op { // Data processing instructions @@ -3672,11 +3703,15 @@ impl ArmEncoder { // table_index_reg contains the table index // Generates (#642): MOVW ip,#size [; MOVT]; CMP idx,ip; BLO +1; // UDF #0; LSL R12,idx,#2; LDR R12,[R11,R12]; BLX R12 + // #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] ArmOp::CallIndirect { rd: _, type_idx: _, table_index_reg, table_size, + table_byte_offset, } => { let idx_reg = reg_to_bits(table_index_reg); let mut bytes = Vec::new(); @@ -3741,13 +3776,38 @@ impl ArmEncoder { bytes.extend_from_slice(&hw1.to_le_bytes()); bytes.extend_from_slice(&hw2.to_le_bytes()); - // LDR R12, [R11, R12] - load function pointer - // Thumb-2 LDR (register): 1111 1000 0101 Rn | Rt 0000 00 imm2 Rm - // Rn=R11, Rt=R12, Rm=R12, imm2=00 (no shift) - let ldr_hw1: u16 = 0xF85B; // LDR.W Rt, [R11, Rm] - let ldr_hw2: u16 = 0xC00C; // Rt=R12, imm2=00, Rm=R12 - bytes.extend_from_slice(&ldr_hw1.to_le_bytes()); - bytes.extend_from_slice(&ldr_hw2.to_le_bytes()); + if *table_byte_offset == 0 { + // Table 0 (base = R11 itself): the pre-#650 single-load + // form — a single-table module's bytes stay identical BY + // CONSTRUCTION. + // LDR R12, [R11, R12] - load function pointer + // Thumb-2 LDR (register): 1111 1000 0101 Rn | Rt 0000 00 imm2 Rm + // Rn=R11, Rt=R12, Rm=R12, imm2=00 (no shift) + let ldr_hw1: u16 = 0xF85B; // LDR.W Rt, [R11, Rm] + let ldr_hw2: u16 = 0xC00C; // Rt=R12, imm2=00, Rm=R12 + bytes.extend_from_slice(&ldr_hw1.to_le_bytes()); + bytes.extend_from_slice(&ldr_hw2.to_le_bytes()); + } else { + // #650: table N of the contiguous R11 region — fold the + // compile-time base offset into the pointer load via the + // LDR imm12 form (R12 stays the only scratch, per the + // #212 convention). + assert!( + *table_byte_offset <= 4095, + "call_indirect table base offset {table_byte_offset} exceeds \ + LDR imm12 — the selector must have declined this (#650)" + ); + // ADD.W R12, R11, R12 — T3 ADD (register): + // 11101011000 S=0 Rn=1011 | 0 imm3=000 Rd=1100 imm2=00 type=00 Rm=1100 + bytes.extend_from_slice(&0xEB0Bu16.to_le_bytes()); + bytes.extend_from_slice(&0x0C0Cu16.to_le_bytes()); + // LDR.W R12, [R12, #offset] — T3 LDR (immediate): + // 1111 1000 1101 Rn=1100 | Rt=1100 imm12 + bytes.extend_from_slice(&0xF8DCu16.to_le_bytes()); + bytes.extend_from_slice( + &((0xC000u16) | (*table_byte_offset as u16 & 0x0FFF)).to_le_bytes(), + ); + } // BLX R12 (call function indirectly) // BLX Rm (16-bit): 0100 0111 1 Rm 000 @@ -8820,6 +8880,7 @@ mod tests { type_idx: 0, table_index_reg: Reg::R0, table_size: 4, + table_byte_offset: 0, }) .unwrap(); assert_eq!( @@ -8865,6 +8926,7 @@ mod tests { type_idx: 0, table_index_reg: Reg::R4, table_size: 4, + table_byte_offset: 0, }) .unwrap(); let cmp = u32::from_le_bytes(bytes[4..8].try_into().unwrap()); @@ -8885,6 +8947,7 @@ mod tests { type_idx: 0, table_index_reg: Reg::R0, table_size: 0x0002_0003, + table_byte_offset: 0, }) .unwrap(); assert_eq!(bytes.len(), 32, "MOVT arm adds one word: {bytes:02x?}"); @@ -8919,6 +8982,7 @@ mod tests { type_idx: 0, table_index_reg: Reg::R0, table_size: 4, + table_byte_offset: 0, }) .unwrap(); assert_eq!( @@ -8950,6 +9014,7 @@ mod tests { type_idx: 0, table_index_reg: Reg::R4, table_size: 4, + table_byte_offset: 0, }) .unwrap(); assert_eq!(&bytes[4..6], &[0x64, 0x45], "cmp r4, ip: {bytes:02x?}"); @@ -8973,6 +9038,7 @@ mod tests { type_idx: 0, table_index_reg: Reg::R8, table_size: 3, + table_byte_offset: 0, }) .unwrap(); // cmp r8, ip — T2: 0x4500 | N(1)<<7 | Rm(12)<<3 | Rn(0) = 0x45E0 @@ -8984,6 +9050,7 @@ mod tests { type_idx: 0, table_index_reg: Reg::R0, table_size: 0x0002_0003, + table_byte_offset: 0, }) .unwrap(); // movw ip,#3 then movt ip,#2 — the size must not be truncated. @@ -8994,6 +9061,105 @@ mod tests { ); } + /// #650: a non-zero table base offset (table N of the contiguous R11 + /// region) routes the Thumb-2 pointer load through + /// `add.w ip, r11, ip; ldr.w ip, [ip, #offset]` — and offset 0 keeps the + /// pre-#650 single-load bytes IDENTICAL (the by-construction pin). + #[test] + fn test_encode_thumb_call_indirect_table_offset_650() { + use synth_synthesis::{ArmOp, Reg}; + let enc = ArmEncoder::new_thumb2(); + // falcon's fused-component shape: table 0 has 7 entries, so table 1 + // sits at byte offset 28. + let bytes = enc + .encode(&ArmOp::CallIndirect { + rd: Reg::R0, + type_idx: 0, + table_index_reg: Reg::R1, + table_size: 41, + table_byte_offset: 28, + }) + .unwrap(); + assert_eq!( + bytes, + vec![ + // #642 bounds guard against TABLE 1's OWN size (41) + 0x40, 0xF2, 0x29, 0x0C, // movw ip, #41 + 0x61, 0x45, // cmp r1, ip + 0x00, 0xD3, // blo .+4 (skip the udf) + 0x00, 0xDE, // udf #0 — OOB trap (WASM §4.4.8) + // dispatch through table 1's base (R11 + 28) + 0x4F, 0xEA, 0x81, 0x0C, // mov.w ip, r1, lsl #2 + 0x0B, 0xEB, 0x0C, 0x0C, // add.w ip, r11, ip + 0xDC, 0xF8, 0x1C, 0xC0, // ldr.w ip, [ip, #28] + 0xE0, 0x47, // blx ip + ], + "Thumb-2 table-1 dispatch (#650): {bytes:02x?}" + ); + + // Offset 0 must stay the #597-pinned single-load form (no add.w, no + // imm-form ldr) — single-table byte identity by construction. + let zero = enc + .encode(&ArmOp::CallIndirect { + rd: Reg::R0, + type_idx: 0, + table_index_reg: Reg::R1, + table_size: 41, + table_byte_offset: 0, + }) + .unwrap(); + assert_eq!( + &zero[10..], + &[ + 0x4F, 0xEA, 0x81, 0x0C, // mov.w ip, r1, lsl #2 + 0x5B, 0xF8, 0x0C, 0xC0, // ldr.w ip, [r11, ip] + 0xE0, 0x47, // blx ip + ], + "offset 0 keeps the pre-#650 dispatch bytes: {zero:02x?}" + ); + } + + /// #650: the A32 twin — `add r12, r11, r12; ldr r12, [r12, #offset]` for + /// a non-zero table base offset; offset 0 keeps the #594/#642 form. + #[test] + fn test_encode_arm32_call_indirect_table_offset_650() { + use synth_synthesis::{ArmOp, Reg}; + let enc = ArmEncoder::new_arm32(); + let bytes = enc + .encode(&ArmOp::CallIndirect { + rd: Reg::R0, + type_idx: 0, + table_index_reg: Reg::R1, + table_size: 41, + table_byte_offset: 28, + }) + .unwrap(); + let words: Vec = bytes + .chunks_exact(4) + .map(|w| u32::from_le_bytes(w.try_into().unwrap())) + .collect(); + assert_eq!(words[0], 0xE300_C029, "MOVW r12,#41: {:#010x}", words[0]); + assert_eq!(words[1], 0xE151_000C, "CMP r1,r12: {:#010x}", words[1]); + assert_eq!(words[2], 0x3A00_0000, "BLO +1 insn: {:#010x}", words[2]); + assert_eq!(words[3], 0xE7F0_00F0, "UDF: {:#010x}", words[3]); + assert_eq!( + words[4], 0xE1A0_C101, + "MOV r12,r1,LSL#2: {:#010x}", + words[4] + ); + assert_eq!( + words[5], 0xE08B_C00C, + "ADD r12,r11,r12 (#650): {:#010x}", + words[5] + ); + assert_eq!( + words[6], 0xE59C_C01C, + "LDR r12,[r12,#28] (#650): {:#010x}", + words[6] + ); + assert_eq!(words[7], 0xE12F_FF3C, "BLX r12: {:#010x}", words[7]); + } + /// #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 226d4ed..d96849e 100644 --- a/crates/synth-backend/tests/a32_no_silent_nop_615.rs +++ b/crates/synth-backend/tests/a32_no_silent_nop_615.rs @@ -649,7 +649,8 @@ fn representatives() -> Vec { rd: Reg::R0, type_idx: 0, table_index_reg: Reg::R2, - table_size: 4, // #642: bounds-guard immediate + table_size: 4, // #642: bounds-guard immediate + table_byte_offset: 0, // #650: table 0 of the contiguous R11 region }, I64Add { rdlo: dl, diff --git a/crates/synth-core/src/lib.rs b/crates/synth-core/src/lib.rs index 3212961..f36d894 100644 --- a/crates/synth-core/src/lib.rs +++ b/crates/synth-core/src/lib.rs @@ -26,7 +26,7 @@ pub use sbom::{CycloneDxSbom, SbomInputs}; pub use target::*; pub use wasm_decoder::{ CallIndirectGuards, DecodedModule, ElemSegmentInfo, FunctionOps, ImportEntry, ImportKind, - WasmMemory, decode_wasm_functions, decode_wasm_module, + TableGuards, WasmMemory, decode_wasm_functions, decode_wasm_module, }; pub use wasm_op::WasmOp; pub use wsc_facts::{FactKind, WSC_FACTS_SECTION_NAME, WscFact, WscFactsParse, parse_wsc_facts}; diff --git a/crates/synth-core/src/wasm_decoder.rs b/crates/synth-core/src/wasm_decoder.rs index e3dcca8..6a6ae6a 100644 --- a/crates/synth-core/src/wasm_decoder.rs +++ b/crates/synth-core/src/wasm_decoder.rs @@ -83,41 +83,83 @@ impl WasmMemory { /// [`DecodedModule::elem_segments`]. #[derive(Debug, Clone, PartialEq, Eq)] pub struct ElemSegmentInfo { - /// Const i32 offset of an ACTIVE table-0 segment; `None` = placement not - /// statically verifiable (passive/declared segment, non-const offset, or - /// a table other than 0). + /// #650: the table this ACTIVE segment initializes (0 for the pre-#650 + /// single-table form). Meaningless when `offset` is `None`. + pub table_index: u32, + /// Const i32 offset of an ACTIVE segment into its table; `None` = + /// placement not statically verifiable (passive/declared segment or a + /// non-const offset expression). pub offset: Option, /// The segment's function indices in slot order; `None` = contents not /// statically verifiable (an entry was not a plain `ref.func`). pub funcs: Option>, } -/// #642: everything the `call_indirect` lowering needs to emit its guards — -/// computed once per module by [`DecodedModule::call_indirect_guards`] and -/// threaded to the instruction selector via `CompileConfig`. +/// #642/#650: one table's `call_indirect` guard inputs — see +/// [`CallIndirectGuards`] for the layout contract and soundness argument. +#[derive(Debug, Clone, Default, PartialEq, Eq)] +pub struct TableGuards { + /// Compile-time size of this table (entries); `None` = no sound bound + /// known (an imported table with growable limits). + pub table_size: Option, + /// #650: byte offset of this table's base within the contiguous R11 + /// region — `sum(size(0..N)) * 4`, a compile-time constant. `None` when + /// any PRECEDING table's size is unknown (the base is then not a + /// compile-time constant and the lowering declines). + pub base_byte_offset: Option, + /// Per expected-type index: `None` = closed-world type property VERIFIED + /// against THIS table; `Some(reason)` = not verifiable (the lowering + /// declines). + pub type_reject: Vec>, +} + +/// #642/#650: everything the `call_indirect` lowering needs to emit its +/// guards — computed once per module by +/// [`DecodedModule::call_indirect_guards`] and threaded to the instruction +/// selector via `CompileConfig`. +/// +/// ## The R11 multi-table layout contract (#650) +/// +/// The runtime/harness links every funcref table as ONE contiguous region of +/// raw 4-byte code pointers based at R11, in declaration order (imported +/// tables first): table 0 at `R11 + 0`, table N at +/// `R11 + sum(size(0..N)) * 4`. The offsets are compile-time constants +/// because tables are provably fixed-size (`table.grow`/`table.set` are +/// unsupported ops whose functions loud-skip at decode — #642). A +/// single-table module degenerates to the pre-#650 contract (table 0 at +/// R11, offset 0) BY CONSTRUCTION, keeping its emitted bytes identical. /// /// WASM Core §4.4.8 requires `call_indirect` to trap when `index >= /// table.size` and when the callee's type does not match the instruction's -/// expected type. synth's table is a raw array of 4-byte code pointers -/// (linked at R11 by the runtime/harness) with no size field and no type -/// ids, so: -/// - the BOUNDS check is emitted at runtime against the compile-time -/// `table_size` immediate (sound: the table cannot change size — -/// `table.grow`/`table.set` are unsupported ops whose functions -/// loud-skip at decode), and +/// expected type. The region stores no size fields and no type ids, so, per +/// table: +/// - 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`, -/// `type_reject[t]` is `None` only when every slot of the table is -/// verifiably initialized with a function whose signature structurally +/// `tables[n].type_reject[t]` is `None` only when every slot of table `n` +/// is verifiably initialized with 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. #[derive(Debug, Clone, Default, PartialEq, Eq)] pub struct CallIndirectGuards { - /// Compile-time size of table 0 (entries); `None` = no sound bound known. - pub table_size: Option, - /// Per type index: `None` = closed-world type property VERIFIED for this - /// expected type; `Some(reason)` = not verifiable (the lowering declines). - pub type_reject: Vec>, + /// Per-table guard inputs, indexed by table index (imports first). The + /// default (empty — no module context) DECLINES every `call_indirect`. + pub tables: Vec, +} + +impl CallIndirectGuards { + /// Single-table (table 0 at R11 offset 0) guards — the pre-#650 shape, + /// used by tests and single-table call sites. + pub fn single_table(table_size: Option, type_reject: Vec>) -> Self { + Self { + tables: vec![TableGuards { + table_size, + base_byte_offset: Some(0), + type_reject, + }], + } + } } /// Decoded WASM module with functions and memory @@ -166,18 +208,23 @@ pub struct DecodedModule { /// reachable function performs a `call_indirect`. Empty for modules with no /// element section (every leaf/direct-call module), keeping output identical. pub elem_func_indices: Vec, - /// #642: compile-time size (in entries) of table 0, from the table section - /// or an imported table whose limits pin it exactly (`max == initial`). - /// `None` = no table, or an imported table with growable limits — the - /// `call_indirect` bounds guard then has no sound immediate and the - /// lowering declines. A DEFINED table's size is exact: `table.grow`/ - /// `table.set` are unsupported ops (their functions loud-skip at decode), - /// so nothing synth compiles can resize or retype the table. + /// #642: compile-time size (in entries) of table 0 — `table_sizes[0]`, + /// kept as a convenience accessor. See [`Self::table_sizes`]. pub table_size: Option, + /// #650: compile-time size (in entries) per table, indexed by table index + /// (imported tables first, then the table section, in declaration order). + /// A DEFINED table's size is exact: `table.grow`/`table.set` are + /// unsupported ops (their functions loud-skip at decode), so nothing + /// synth compiles can resize or retype a table. An imported table only + /// yields a sound bound when its limits pin the size (`max == initial`); + /// otherwise its entry is `None` and the `call_indirect` lowering + /// declines (for that table AND for any later table, whose base offset + /// within the contiguous R11 region is then unknown). + pub table_sizes: Vec>, /// #642: per element segment, everything the closed-world `call_indirect` /// type check needs. `offset` is the const i32 placement of an ACTIVE - /// table-0 segment (`None` = passive/declared/non-const offset/other - /// table — statically unverifiable placement); `funcs` are the segment's + /// segment into table `table_index` (`None` = passive/declared/non-const + /// offset — statically unverifiable placement); `funcs` are the segment's /// function indices in slot order (`None` = an entry was not a plain /// `ref.func`, e.g. `ref.null` — statically unverifiable contents). pub elem_segments: Vec, @@ -201,46 +248,92 @@ pub struct DecodedModule { } impl DecodedModule { - /// #642: compute the `call_indirect` guard inputs — the compile-time table - /// size for the runtime bounds check, and the per-expected-type + /// #642/#650: compute the `call_indirect` guard inputs — per table, the + /// compile-time size for the runtime bounds check, the base byte offset + /// within the contiguous R11 region, and the per-expected-type /// closed-world verdict that discharges the type check at compile time. - /// See [`CallIndirectGuards`] for the soundness argument. + /// See [`CallIndirectGuards`] for the layout contract and soundness + /// argument. pub fn call_indirect_guards(&self) -> CallIndirectGuards { let n_types = self.type_signatures.len(); - let reject_all = |table_size: Option, reason: String| CallIndirectGuards { - table_size, - type_reject: vec![Some(reason); n_types], - }; - let Some(size) = self.table_size else { - return reject_all( - None, - "module has no table with a compile-time-fixed size".to_string(), + // A segment whose PLACEMENT is not statically attributable + // (passive/declared segment, non-const offset, or a table index the + // module does not declare) poisons EVERY table: `table.init` (itself + // an unsupported op) or a computed offset could land its entries + // anywhere, so no table's image is verifiable. + let global_poison: Option<&'static str> = self + .elem_segments + .iter() + .any(|seg| seg.offset.is_none() || seg.table_index as usize >= self.table_sizes.len()) + .then_some( + "element segment is not statically verifiable (passive/declared \ + segment, non-const offset, out-of-range table, or non-`ref.func` \ + entry)", ); + + let mut tables = 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 = self.table_type_reject(n as u32, size, global_poison, n_types); + tables.push(TableGuards { + table_size: size, + base_byte_offset, + type_reject, + }); + base_words = match (base_words, size) { + (Some(w), Some(s)) => w.checked_add(s), + _ => None, + }; + } + CallIndirectGuards { tables } + } + + /// #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. + 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]; + + if let Some(reason) = global_poison { + return reject_all(reason.to_string()); + } + let Some(size) = size else { + return reject_all(format!( + "table {n} has no compile-time-fixed size (imported table with \ + growable limits)" + )); }; // Reconstruct the table image: slot -> initializing function index. let mut slots: Vec> = vec![None; size as usize]; - for seg in &self.elem_segments { + for seg in self.elem_segments.iter().filter(|s| s.table_index == n) { let (Some(off), Some(funcs)) = (seg.offset, seg.funcs.as_ref()) else { - return reject_all( - Some(size), - "element segment is not statically verifiable (passive/declared \ - segment, non-const offset, non-zero table, or non-`ref.func` \ - entry)" - .to_string(), - ); + // Placement is known (global_poison ruled `offset: None` out), + // so this is an unverifiable CONTENTS case — it poisons only + // the table it targets. + return reject_all(format!( + "element segment targeting table {n} is not statically \ + verifiable (non-`ref.func` entry)" + )); }; for (k, &f) in funcs.iter().enumerate() { let Some(slot) = slots.get_mut(off as usize + k) else { - return reject_all( - Some(size), - format!( - "element segment (offset {off}, {} entries) writes past the \ - declared table size {size}", - funcs.len() - ), - ); + return reject_all(format!( + "element segment (offset {off}, {} entries) writes past \ + table {n}'s declared size {size}", + funcs.len() + )); }; *slot = Some(f); } @@ -249,27 +342,24 @@ impl DecodedModule { // 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( - Some(size), - format!( - "table 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" - ), - ); + 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" + )); } - let type_reject = (0..n_types) + (0..n_types) .map(|t| { for f in slots.iter().flatten() { let Some(&fty) = self.func_type_indices.get(*f as usize) else { return Some(format!( - "table entry references function {f} with no known type" + "table {n} entry references function {f} with no known type" )); }; if self.type_signatures.get(fty as usize) != self.type_signatures.get(t) { return Some(format!( - "table entry (function {f}, type {fty}) has a different \ + "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" )); @@ -277,12 +367,7 @@ impl DecodedModule { } None }) - .collect(); - - CallIndirectGuards { - table_size: Some(size), - type_reject, - } + .collect() } } @@ -308,10 +393,10 @@ pub fn decode_wasm_module(wasm_bytes: &[u8]) -> Result { // #509: (param_count, result_count) per type index, for FuncType blocktypes. let mut type_block_arity: Vec<(u8, u8)> = Vec::new(); let mut elem_func_indices: Vec = Vec::new(); - // #642: call_indirect guard inputs — table 0's fixed size, per-segment + // #642/#650: call_indirect guard inputs — per-table fixed sizes (imports + // first, then the table section, in declaration order), per-segment // static shapes, per-function type index, per-type canonical signature. - let mut table_size: Option = None; - let mut saw_table = false; + let mut table_sizes: Vec> = Vec::new(); let mut elem_segments: Vec = Vec::new(); let mut func_type_indices: Vec = Vec::new(); let mut type_signatures: Vec = Vec::new(); @@ -427,18 +512,17 @@ pub fn decode_wasm_module(wasm_bytes: &[u8]) -> Result { } wasmparser::TypeRef::Memory(_) => (ImportKind::Memory, 0), wasmparser::TypeRef::Table(t) => { - // #642: an imported table 0 only yields a SOUND + // #642: an imported table only yields a SOUND // compile-time bound when its limits pin the size // exactly (max == initial) — a growable import // could be larger at runtime, and a bounds guard // against `initial` would trap spec-valid calls. - if !saw_table { - saw_table = true; - table_size = match (u32::try_from(t.initial), t.maximum) { - (Ok(init), Some(max)) if u64::from(init) == max => Some(init), - _ => None, - }; - } + // #650: imported tables take the leading table + // indices, in declaration order. + table_sizes.push(match (u32::try_from(t.initial), t.maximum) { + (Ok(init), Some(max)) if u64::from(init) == max => Some(init), + _ => None, + }); (ImportKind::Table, 0) } wasmparser::TypeRef::Global(g) => { @@ -492,14 +576,12 @@ pub fn decode_wasm_module(wasm_bytes: &[u8]) -> Result { // #642: a DEFINED table's compile-time size is exact — its // initial size is its permanent size, because nothing synth // compiles can resize it (`table.grow` is an unsupported op - // whose function loud-skips at decode). Only table 0 matters: - // the call_indirect lowering declines non-zero table indices. + // whose function loud-skips at decode). #650: EVERY table is + // recorded — the contiguous R11 region places table N at + // byte offset `sum(size(0..N)) * 4`. for table in reader { let table = table.context("Failed to parse table")?; - if !saw_table { - saw_table = true; - table_size = u32::try_from(table.ty.initial).ok(); - } + table_sizes.push(u32::try_from(table.ty.initial).ok()); } } Payload::MemorySection(reader) => { @@ -578,23 +660,26 @@ pub fn decode_wasm_module(wasm_bytes: &[u8]) -> Result { // form whose `ref.func` entries name the functions. for elem in reader { let elem = elem.context("Failed to parse element segment")?; - // #642: the segment's static placement — a const i32 - // offset of an ACTIVE table-0 segment; anything else is - // unverifiable and poisons the closed-world type check. - let seg_offset: Option = match &elem.kind { + // #642/#650: the segment's static placement — a const i32 + // offset of an ACTIVE segment into its target table (any + // table index: the R11 region is contiguous, #650); + // anything else is unverifiable and poisons the + // closed-world type check. + let (seg_table, seg_offset): (u32, Option) = match &elem.kind { wasmparser::ElementKind::Active { table_index, offset_expr, - } if table_index.unwrap_or(0) == 0 => { + } => { let mut ops = offset_expr.get_operators_reader(); - match ops.read() { + let off = match ops.read() { Ok(wasmparser::Operator::I32Const { value }) => { u32::try_from(value).ok() } _ => None, - } + }; + (table_index.unwrap_or(0), off) } - _ => None, + _ => (0, None), }; let mut seg_funcs: Option> = Some(Vec::new()); match elem.items { @@ -641,6 +726,7 @@ pub fn decode_wasm_module(wasm_bytes: &[u8]) -> Result { } } elem_segments.push(ElemSegmentInfo { + table_index: seg_table, offset: seg_offset, funcs: seg_funcs, }); @@ -721,7 +807,8 @@ pub fn decode_wasm_module(wasm_bytes: &[u8]) -> Result { func_params_i64, globals, elem_func_indices, - table_size, + table_size: table_sizes.first().copied().flatten(), + table_sizes, elem_segments, func_type_indices, type_signatures, @@ -2313,9 +2400,11 @@ mod tests { let module = decode_wasm_module(&wasm).expect("decode"); assert_eq!(module.table_size, Some(3), "table section min size"); + assert_eq!(module.table_sizes, vec![Some(3)], "#650 per-table sizes"); assert_eq!( module.elem_segments, vec![ElemSegmentInfo { + table_index: 0, offset: Some(0), funcs: Some(vec![0, 1, 2]), }] @@ -2326,14 +2415,20 @@ mod tests { assert_eq!(module.func_type_indices.len(), 4); let guards = module.call_indirect_guards(); - assert_eq!(guards.table_size, Some(3)); + assert_eq!(guards.tables.len(), 1); + assert_eq!(guards.tables[0].table_size, Some(3)); + assert_eq!( + guards.tables[0].base_byte_offset, + Some(0), + "#650: a single-table module keeps table 0 at R11 offset 0 by construction" + ); // Type index 0 ($bin) must be VERIFIED: every table entry has its // exact signature. assert_eq!( - guards.type_reject.first(), + guards.tables[0].type_reject.first(), Some(&None), "closed-world type check must verify the homogeneous table: {:?}", - guards.type_reject + guards.tables[0].type_reject ); } @@ -2360,13 +2455,13 @@ mod tests { 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.table_size, Some(2)); + assert_eq!(guards.tables[0].table_size, Some(2)); // BOTH expected types must be rejected: the table holds one function // of each signature, so neither type's closed world holds. assert!( - guards.type_reject[0].is_some() && guards.type_reject[1].is_some(), + guards.tables[0].type_reject[0].is_some() && guards.tables[0].type_reject[1].is_some(), "heterogeneous table must reject every expected type: {:?}", - guards.type_reject + guards.tables[0].type_reject ); } @@ -2389,16 +2484,19 @@ mod tests { 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.table_size, Some(3)); + assert_eq!(guards.tables[0].table_size, Some(3)); assert!( - guards.type_reject.iter().all(|r| r.is_some()), + guards.tables[0].type_reject.iter().all(|r| r.is_some()), "slot 2 is a null funcref — every type must be rejected: {:?}", - guards.type_reject + guards.tables[0].type_reject ); assert!( - guards.type_reject[0].as_deref().unwrap().contains("slot 2"), + guards.tables[0].type_reject[0] + .as_deref() + .unwrap() + .contains("slot 2"), "reason names the uninitialized slot: {:?}", - guards.type_reject[0] + guards.tables[0].type_reject[0] ); } @@ -2414,9 +2512,12 @@ mod tests { let wasm = wat::parse_str(wat).expect("parse"); let module = decode_wasm_module(&wasm).expect("decode"); assert_eq!(module.table_size, None); + assert!(module.table_sizes.is_empty(), "#650: no tables declared"); let guards = module.call_indirect_guards(); - assert_eq!(guards.table_size, None); - assert!(guards.type_reject.iter().all(|r| r.is_some())); + assert!( + guards.tables.is_empty(), + "no table → no guard entry → every call_indirect declines" + ); } /// #642: duplicate-but-structurally-identical types stay interchangeable — @@ -2441,14 +2542,114 @@ mod tests { // BOTH type indices must verify. (A third type — the export's // (i32)->i32 — is correctly rejected: different signature.) assert_eq!( - &guards.type_reject[0..2], + &guards.tables[0].type_reject[0..2], &[None, None], "structural signature comparison must accept duplicate types: {:?}", - guards.type_reject + guards.tables[0].type_reject ); assert!( - guards.type_reject[2].is_some(), + guards.tables[0].type_reject[2].is_some(), "the structurally-different third type must still be rejected" ); } + + /// #650: TWO tables become a contiguous R11 region — table 0 at offset 0 + /// (byte-identical single-table degeneration), table 1 at + /// `size(table 0) * 4`. Each table gets its OWN size, base offset, and + /// per-type closed-world verdicts (segments only poison the table they + /// target). + #[test] + fn test_call_indirect_guards_multi_table_650() { + // The #650 repro shape: overlapping indices, distinct functions — + // table0[1] != table1[1] (the aliasing canary). + let wat = r#" + (module + (type $t (func (param i32) (result i32))) + (type $u (func (param i32 i32) (result i32))) + (table $t0 3 3 funcref) + (table $t1 2 2 funcref) + (func $a0 (type $t) (i32.add (local.get 0) (i32.const 100))) + (func $a1 (type $t) (i32.add (local.get 0) (i32.const 200))) + (func $a2 (type $t) (i32.add (local.get 0) (i32.const 300))) + (func $b0 (type $u) (i32.add (local.get 0) (local.get 1))) + (func $b1 (type $u) (i32.sub (local.get 0) (local.get 1))) + (elem (table $t0) (i32.const 0) func $a0 $a1 $a2) + (elem (table $t1) (i32.const 0) func $b0 $b1) + (func (export "f") (param i32 i32) (result i32) + (call_indirect $t1 (type $u) + (local.get 0) (i32.const 10) (local.get 1))) + ) + "#; + let wasm = wat::parse_str(wat).expect("parse"); + let module = decode_wasm_module(&wasm).expect("decode"); + assert_eq!(module.table_sizes, vec![Some(3), Some(2)]); + assert_eq!(module.table_size, Some(3), "compat accessor = table 0"); + assert_eq!( + module.elem_segments[0].table_index, 0, + "segment 0 targets table 0" + ); + assert_eq!( + module.elem_segments[1], + ElemSegmentInfo { + table_index: 1, + offset: Some(0), + funcs: Some(vec![3, 4]), + }, + "segment 1 is statically attributed to table 1 (#650)" + ); + + let guards = module.call_indirect_guards(); + assert_eq!(guards.tables.len(), 2); + assert_eq!(guards.tables[0].table_size, Some(3)); + assert_eq!(guards.tables[0].base_byte_offset, Some(0)); + assert_eq!(guards.tables[1].table_size, Some(2)); + assert_eq!( + guards.tables[1].base_byte_offset, + Some(12), + "table 1 base = size(table 0) * 4 within the contiguous R11 region" + ); + // Table 0 is homogeneous in $t (type 0); table 1 in $u (type 1) — + // each verifies ITS type and rejects the other's. + assert_eq!(guards.tables[0].type_reject[0], None, "table 0 vs $t"); + assert!(guards.tables[0].type_reject[1].is_some(), "table 0 vs $u"); + assert!(guards.tables[1].type_reject[0].is_some(), "table 1 vs $t"); + assert_eq!(guards.tables[1].type_reject[1], None, "table 1 vs $u"); + } + + /// #650: an unknown-size table (growable import) declines ITSELF and + /// makes every LATER table's base offset non-constant — but a table + /// BEFORE it is unaffected. + #[test] + fn test_call_indirect_guards_unknown_size_poisons_later_bases_650() { + let wat = r#" + (module + (type $t (func (result i32))) + (import "env" "tbl" (table 4 funcref)) + (table $d 1 1 funcref) + (func $f (type $t) (i32.const 7)) + (elem (table $d) (i32.const 0) func $f) + (func (export "run") (param i32) (result i32) + (call_indirect $d (type $t) (local.get 0))) + ) + "#; + let wasm = wat::parse_str(wat).expect("parse"); + let module = decode_wasm_module(&wasm).expect("decode"); + assert_eq!( + module.table_sizes, + vec![None, Some(1)], + "growable import (no max) has no sound compile-time size" + ); + let guards = module.call_indirect_guards(); + assert_eq!(guards.tables[0].base_byte_offset, Some(0)); + assert!( + guards.tables[0].type_reject.iter().all(|r| r.is_some()), + "unknown-size table rejects every type" + ); + assert_eq!( + guards.tables[1].base_byte_offset, None, + "a later table's base is not a compile-time constant when a \ + preceding table's size is unknown (#650)" + ); + assert_eq!(guards.tables[1].table_size, Some(1)); + } } diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index 075713c..76f335f 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -2169,6 +2169,75 @@ impl InstructionSelector { self.call_indirect_guards = guards; } + /// #642/#650: resolve the guard inputs for a `call_indirect` through + /// `table_index` expecting `type_index` — the dispatched table's + /// compile-time size and its base byte offset within the contiguous R11 + /// table region — or decline LOUDLY with a named reason. WASM Core + /// §4.4.8 requires OOB/type-mismatch traps, so without a compile-time + /// 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. + fn resolve_call_indirect_guards( + &self, + table_index: u32, + type_index: u32, + ) -> Result<(u32, u32)> { + let n_tables = self.call_indirect_guards.tables.len(); + let table = self + .call_indirect_guards + .tables + .get(table_index as usize) + .ok_or_else(|| { + synth_core::Error::synthesis(format!( + "call_indirect: table index {table_index} is not linked (the \ + contiguous R11 table region covers the module's {n_tables} \ + declared table(s); no module context means none) — #642/#650" + )) + })?; + let table_size = table.table_size.ok_or_else(|| { + synth_core::Error::synthesis(format!( + "call_indirect: no compile-time size for table {table_index} \ + (imported table with growable limits) — refusing to emit an \ + unchecked indirect branch (#642)" + )) + })?; + let table_byte_offset = table.base_byte_offset.ok_or_else(|| { + synth_core::Error::synthesis(format!( + "call_indirect: table {table_index}'s base offset within the \ + contiguous R11 region is not a compile-time constant (a \ + preceding table's size is unknown) — #650" + )) + })?; + // The non-zero-offset expansion loads through `LDR ip, [ip, #offset]` + // whose imm12 tops out at 4095 (> 1023 preceding table entries — + // far beyond any fused component seen; falcon's is 28). + if table_byte_offset > 4095 { + return Err(synth_core::Error::synthesis(format!( + "call_indirect: table {table_index}'s base offset \ + {table_byte_offset} exceeds the LDR imm12 addressing range \ + (4095) — #650" + ))); + } + match table.type_reject.get(type_index as usize) { + Some(None) => {} // closed-world type property verified + Some(Some(reason)) => { + return Err(synth_core::Error::synthesis(format!( + "call_indirect (expected type {type_index}, table \ + {table_index}): closed-world type check failed — {reason}; \ + refusing to emit an unchecked indirect branch (#642)" + ))); + } + None => { + return Err(synth_core::Error::synthesis(format!( + "call_indirect: no closed-world type verdict for type index \ + {type_index} (table {table_index}) — refusing to emit an \ + unchecked indirect branch (#642)" + ))); + } + } + Ok((table_size, table_byte_offset)) + } + /// Enable relocatable host-link mode (#197): import calls emit a direct /// `BL func_N` (rewritten to the wasm field name by the relocatable-ELF /// builder) instead of dispatching through `__meld_dispatch_import`. @@ -2811,47 +2880,20 @@ impl InstructionSelector { table_index, } => { // Table index is on top of stack (in rn), call target via table lookup. - // #642: same guard preconditions as the select_with_stack arm — - // WASM §4.4.8 requires OOB/type-mismatch traps, so without a - // compile-time table size (for the encoder's bounds guard) and - // a verified closed-world type verdict, decline loudly rather - // than emit an unchecked indirect branch. - let table_size = self.call_indirect_guards.table_size.ok_or_else(|| { - synth_core::Error::synthesis( - "call_indirect: no compile-time table size available for the \ - bounds guard — refusing to emit an unchecked indirect branch \ - (#642)" - .to_string(), - ) - })?; - if *table_index != 0 { - return Err(synth_core::Error::synthesis(format!( - "call_indirect: table index {table_index} is not supported \ - (only table 0 is linked at R11) — #642" - ))); - } - match self - .call_indirect_guards - .type_reject - .get(*type_index as usize) - { - Some(None) => {} // closed-world type property verified - other => { - return Err(synth_core::Error::synthesis(format!( - "call_indirect (expected type {type_index}): closed-world \ - type check not verified ({}) — refusing to emit an \ - unchecked indirect branch (#642)", - other - .and_then(|r| r.as_deref()) - .unwrap_or("no verdict for this type index") - ))); - } - } + // #642/#650: same guard preconditions as the select_with_stack + // arm — WASM §4.4.8 requires OOB/type-mismatch traps, so + // without a compile-time table size (for the encoder's bounds + // 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) = + self.resolve_call_indirect_guards(*table_index, *type_index)?; vec![ArmOp::CallIndirect { rd, type_idx: *type_index, table_index_reg: rn, // Table index from stack table_size, + table_byte_offset, }] } @@ -9114,52 +9156,21 @@ impl InstructionSelector { type_index, table_index, } => { - // #642: WASM Core §4.4.8 requires call_indirect to TRAP on - // an out-of-bounds index and on a type mismatch. The - // bounds check needs the compile-time table size (the raw - // code-pointer table has no runtime size field); the type - // check is discharged HERE at compile time via the - // closed-world verdict (every table slot verifiably holds - // a function of the expected signature — the table cannot - // change: table.grow/table.set are unsupported ops that - // loud-skip their functions). If either input is missing, - // DECLINE loudly — never emit an unchecked indirect branch. - let table_size = self.call_indirect_guards.table_size.ok_or_else(|| { - synth_core::Error::synthesis( - "call_indirect: no compile-time table size available for the \ - bounds guard (module has no table, or an imported table \ - without exact limits) — refusing to emit an unchecked \ - indirect branch (#642)" - .to_string(), - ) - })?; - if *table_index != 0 { - return Err(synth_core::Error::synthesis(format!( - "call_indirect: table index {table_index} is not supported \ - (only table 0 is linked at R11) — #642" - ))); - } - match self - .call_indirect_guards - .type_reject - .get(*type_index as usize) - { - Some(None) => {} // closed-world type property verified - Some(Some(reason)) => { - return Err(synth_core::Error::synthesis(format!( - "call_indirect (expected type {type_index}): closed-world \ - type check failed — {reason}; refusing to emit an \ - unchecked indirect branch (#642)" - ))); - } - None => { - return Err(synth_core::Error::synthesis(format!( - "call_indirect: no closed-world type verdict for type \ - index {type_index} — refusing to emit an unchecked \ - indirect branch (#642)" - ))); - } - } + // #642/#650: WASM Core §4.4.8 requires call_indirect to + // TRAP on an out-of-bounds index and on a type mismatch. + // The bounds check needs the dispatched table's + // compile-time size (the raw code-pointer region has no + // runtime size fields); the dispatch needs the table's + // constant base offset within the contiguous R11 region + // (#650); the type check is discharged HERE at compile + // time via the per-table closed-world verdict (every slot + // of THAT table verifiably holds a function of the + // expected signature — tables cannot change: + // 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) = + self.resolve_call_indirect_guards(*table_index, *type_index)?; // Top of stack is the table index; the call arguments sit // BELOW it on the operand stack. @@ -9266,8 +9277,11 @@ impl InstructionSelector { type_idx: *type_index, table_index_reg: table_idx_reg, // #642: the encoder emits `CMP idx, size; BLO ok; - // UDF #0` before the table load. + // UDF #0` before the table load. #650: a non-zero + // offset routes the load through the table's base + // within the contiguous R11 region. table_size, + table_byte_offset, }, source_line: Some(idx), }); @@ -13251,10 +13265,10 @@ mod tests { 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 { - table_size: Some(3), - type_reject: vec![None], // type 0 verified - }); + selector.set_call_indirect_guards(synth_core::CallIndirectGuards::single_table( + Some(3), + vec![None], // type 0 verified + )); let wasm_ops = vec![ WasmOp::I32Const(1), // table index WasmOp::CallIndirect { @@ -13266,12 +13280,125 @@ mod tests { .select_with_stack(&wasm_ops, 0) .expect("verified call_indirect must lower"); assert!( - arm.iter() - .any(|i| matches!(&i.op, ArmOp::CallIndirect { table_size: 3, .. })), + arm.iter().any(|i| matches!( + &i.op, + ArmOp::CallIndirect { + table_size: 3, + table_byte_offset: 0, // #650: table 0 stays at R11 offset 0 + .. + } + )), "the pseudo-op must carry the compile-time table size: {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. + #[test] + fn test_650_call_indirect_table1_carries_offset_and_own_size() { + 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(7), + base_byte_offset: Some(0), + type_reject: vec![None], + }, + synth_core::TableGuards { + table_size: Some(41), + base_byte_offset: Some(28), + type_reject: vec![None], + }, + ], + }); + let wasm_ops = vec![ + WasmOp::I32Const(1), + WasmOp::CallIndirect { + type_index: 0, + table_index: 1, + }, + ]; + let arm = selector + .select_with_stack(&wasm_ops, 0) + .expect("verified table-1 call_indirect must lower (#650)"); + assert!( + arm.iter().any(|i| matches!( + &i.op, + ArmOp::CallIndirect { + table_size: 41, // table 1's OWN bound + table_byte_offset: 28, // sum(size(0..1)) * 4 + .. + } + )), + "table-1 dispatch must carry its own size + base offset: {arm:#?}" + ); + } + + /// #650: a table index past the linked region must DECLINE loudly, and a + /// table whose base offset is unknown (a preceding growable import) too. + #[test] + fn test_650_call_indirect_unlinked_table_declines() { + 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::single_table( + Some(3), + vec![None], + )); + let wasm_ops = vec![ + WasmOp::I32Const(0), + WasmOp::CallIndirect { + type_index: 0, + table_index: 2, + }, + ]; + let err = selector + .select_with_stack(&wasm_ops, 0) + .expect_err("a table index past the linked region must decline"); + assert!( + err.to_string().contains("#650") && err.to_string().contains("table index 2"), + "the decline names the table and the tracking issue: {err}" + ); + + // A known-size table whose BASE is unknown (preceded by a growable + // import) must also decline — the dispatch offset would not be a + // compile-time constant. + 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: None, + base_byte_offset: Some(0), + type_reject: vec![Some("growable import".to_string())], + }, + synth_core::TableGuards { + table_size: Some(4), + base_byte_offset: None, + type_reject: vec![None], + }, + ], + }); + let wasm_ops = vec![ + WasmOp::I32Const(0), + WasmOp::CallIndirect { + type_index: 0, + table_index: 1, + }, + ]; + let err = selector + .select_with_stack(&wasm_ops, 0) + .expect_err("an unknown base offset must decline"); + assert!( + err.to_string().contains("base offset") + && err.to_string().contains("not a compile-time constant"), + "the decline names the unknown-base reason: {err}" + ); + } + /// #642: WITHOUT guard inputs (no module context — the default), the /// CallIndirect lowering must DECLINE with a typed error, never emit the /// unchecked indirect branch. @@ -13304,10 +13431,10 @@ mod tests { 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 { - table_size: Some(3), - type_reject: vec![Some("table slot 2 is uninitialized".to_string())], - }); + selector.set_call_indirect_guards(synth_core::CallIndirectGuards::single_table( + Some(3), + vec![Some("table slot 2 is uninitialized".to_string())], + )); let wasm_ops = vec![ WasmOp::I32Const(0), WasmOp::CallIndirect { diff --git a/crates/synth-synthesis/src/rules.rs b/crates/synth-synthesis/src/rules.rs index cb5f67e..358b552 100644 --- a/crates/synth-synthesis/src/rules.rs +++ b/crates/synth-synthesis/src/rules.rs @@ -526,15 +526,26 @@ pub enum ArmOp { rd: Reg, type_idx: u32, table_index_reg: Reg, - /// #642: compile-time size of table 0 in entries. The encoder emits a - /// bounds guard (`CMP idx, size; BLO ok; UDF #0`) before the table - /// load — WASM Core §4.4.8 requires `index >= table.size` to TRAP, - /// not perform an uncontrolled indirect branch. The size is a - /// compile-time immediate because the raw code-pointer table synth - /// targets has no runtime size field, and the table cannot change - /// size at runtime (`table.grow`/`table.set` are unsupported ops → - /// their functions loud-skip at decode). + /// #642: compile-time size of the DISPATCHED table in entries. The + /// encoder emits a bounds guard (`CMP idx, size; BLO ok; UDF #0`) + /// before the table load — WASM Core §4.4.8 requires + /// `index >= table.size` to TRAP, not perform an uncontrolled + /// indirect branch. The size is a compile-time immediate because the + /// raw code-pointer table synth targets has no runtime size field, + /// and the table cannot change size at runtime (`table.grow`/ + /// `table.set` are unsupported ops → their functions loud-skip at + /// decode). table_size: u32, + /// #650: byte offset of the dispatched table's base within the + /// contiguous R11 table region — tables are linked back-to-back in + /// declaration order, so table N sits at `sum(size(0..N)) * 4`, a + /// compile-time constant (tables are provably fixed-size, see + /// `table_size`). `0` for table 0 keeps the pre-#650 expansion + /// byte-identical BY CONSTRUCTION; a non-zero offset routes the + /// pointer load through `ADD ip, r11, ip; LDR ip, [ip, #offset]` + /// (offset <= 4095 — the LDR imm12 range — enforced by the + /// selector's loud decline). + table_byte_offset: u32, }, // ======================================================================== diff --git a/crates/synth-verify/src/arm_semantics.rs b/crates/synth-verify/src/arm_semantics.rs index 980990d..421bb31 100644 --- a/crates/synth-verify/src/arm_semantics.rs +++ b/crates/synth-verify/src/arm_semantics.rs @@ -480,8 +480,11 @@ impl ArmSemantics { type_idx, table_index_reg, // #642: the bounds guard is a control-flow effect (trap), not - // modeled by the symbolic call result. + // modeled by the symbolic call result. #650: the table base + // offset only changes WHICH pointer is loaded, not the + // symbolic result shape. table_size: _, + table_byte_offset: _, } => { // 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 6ac5a4b..9e89091 100644 --- a/crates/synth-verify/tests/comprehensive_verification.rs +++ b/crates/synth-verify/tests/comprehensive_verification.rs @@ -1998,7 +1998,8 @@ fn verify_call_indirect() { rd: Reg::R0, type_idx, table_index_reg: Reg::R1, - table_size: 4, // #642: bounds-guard immediate + table_size: 4, // #642: bounds-guard immediate + table_byte_offset: 0, // #650: table 0 of the contiguous R11 region }, ); diff --git a/scripts/repro/call_indirect_650_differential.py b/scripts/repro/call_indirect_650_differential.py new file mode 100644 index 0000000..c06705d --- /dev/null +++ b/scripts/repro/call_indirect_650_differential.py @@ -0,0 +1,225 @@ +#!/usr/bin/env python3 +"""#650 — multi-table call_indirect oracle: the contiguous R11 region. + +Layout contract (#650): the runtime/harness links every funcref table as ONE +contiguous region of raw 4-byte code pointers based at R11, in declaration +order — table 0 at R11+0, table N at R11 + sum(size(0..N))*4. The dispatch +expansion for table N adds the compile-time base offset +(`add ip, r11, ip; ldr ip, [ip, #off]`), and the #642 bounds guard compares +against THAT table's own size. Offset 0 (table 0 / any single-table module) +keeps the pre-#650 bytes identical by construction. + +The fixture carries TWO tables with OVERLAPPING indices and DISTINCT +functions — the aliasing canary: table0[1] (x+200) != table1[1] (1000-x). A +backend that drops the table index and always dispatches table 0 returns +table 0's results for `f1`. + +For each case both engines run: + - wasmtime (oracle): f0/f1 over in-bounds indices; OOB indices trap. + - unicorn (synth's code, region linked at r11 per the contract): in-bounds + results must match wasmtime; OOB on EITHER table must stop at a `udf` + (the §4.4.8 trap). Words past the 6-entry region are seeded with a valid + decoy so a missing/short bounds guard "succeeds" (returns 0x5A) instead + of faulting — a loud, non-vacuous red. + +On origin/main (≤ v0.33.1) this harness is RED at the compile step: every +`call_indirect` through table 1 loud-declines ("table index 1 is not +supported (only table 0 is linked at R11)"). That red documents the +capability gap this oracle upgrades — green = correct multi-table dispatch. + +Run (needs wasmtime + unicorn + pyelftools): + SYNTH=./target/debug/synth python scripts/repro/call_indirect_650_differential.py +Exits nonzero on any compile decline, mismatch, missed trap, or aliasing. +""" + +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_650_multitable.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 +IN_BOUNDS = [0, 1, 2] +OOB = [3, 5, 99] +T0 = ["func_0", "func_1", "func_2"] # $a0 $a1 $a2 — table 0 image +T1 = ["func_3", "func_4", "func_5"] # $b0 $b1 $b2 — table 1 image + + +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: (export, idx) -> result or 'trap'.""" + engine = wasmtime.Engine() + module = wasmtime.Module(engine, WAT.read_text()) + results = {} + for name in ("f0", "f1"): + for idx in IN_BOUNDS + OOB: + store = wasmtime.Store(engine) # fresh instance per call (stateful) + f = wasmtime.Instance(store, module, []).exports(store)[name] + try: + results[(name, idx)] = f(store, X, idx) & 0xFFFFFFFF + except wasmtime.Trap: + results[(name, idx)] = "trap" + return results + + +def run_unicorn(text: bytes, syms: dict, entry: str, idx: int, a32: bool): + """Execute entry(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/ci650_{'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 ["f0", "f1"] + T0 + T1: + if need not in syms: + print(f"SYMBOL MISSING: {need} (a decline drops the function — #650 red)") + return 1 + + isa = "A32" if a32 else "Thumb-2" + fails = 0 + for name in ("f0", "f1"): + for idx in IN_BOUNDS: + want = oracle[(name, idx)] + kind, got = run_unicorn(text, syms, name, 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}] {name}({X},{idx}) = {kind}:{got_s} (wasmtime: {want:#x}) " + f"{'OK' if ok else 'MISMATCH'}" + ) + for idx in OOB: + assert oracle[(name, idx)] == "trap", f"oracle must trap {name} idx {idx}" + kind, got = run_unicorn(text, syms, name, idx, a32) + ok = kind == "trap-udf" + fails += 0 if ok else 1 + if ok: + print(f"[{isa}] {name}({X},{idx}) = udf trap at {got:#x} (wasmtime: trap) OK") + elif kind == "ok" and got == 0x5A: + print( + f"[{isa}] {name}({X},{idx}) = {got:#x} — the DECOY past the region " + "was CALLED: bounds guard missing or against the wrong size MISMATCH" + ) + else: + print(f"[{isa}] {name}({X},{idx}) = {kind}:{got} (wasmtime: trap) MISMATCH") + + # The aliasing canary, asserted explicitly: overlapping index, different + # table, DIFFERENT result (a table-index-dropping backend fails here). + _, r0 = run_unicorn(text, syms, "f0", 1, a32) + _, r1 = run_unicorn(text, syms, "f1", 1, a32) + if r0 == r1: + print(f"[{isa}] ALIASING: f0({X},1) == f1({X},1) == {r0:#x} — table index dropped") + fails += 1 + else: + print(f"[{isa}] aliasing canary: f0({X},1)={r0:#x} != f1({X},1)={r1:#x} OK") + 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 (#650)") + return 1 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/scripts/repro/call_indirect_650_multitable.wat b/scripts/repro/call_indirect_650_multitable.wat new file mode 100644 index 0000000..1f7bd0a --- /dev/null +++ b/scripts/repro/call_indirect_650_multitable.wat @@ -0,0 +1,27 @@ +;; #650 — multi-table call_indirect: the contiguous R11 region. +;; +;; Two funcref tables with OVERLAPPING indices but DISTINCT functions — the +;; aliasing canary: table0[i] and table1[i] must dispatch to different code +;; (a backend that ignores the table index and always indexes table 0 returns +;; table 0's results for f1). Layout contract: table 0 at R11+0 (3 entries), +;; table 1 at R11 + 3*4 = R11+12 (3 entries). +;; +;; Each table is homogeneous in the shared type $t, so the #642 closed-world +;; type verification discharges per (table, type). OOB on EITHER table must +;; trap against THAT table's own size. +(module + (type $t (func (param i32) (result i32))) + (table $t0 3 3 funcref) + (table $t1 3 3 funcref) + (func $a0 (type $t) (i32.add (local.get 0) (i32.const 100))) + (func $a1 (type $t) (i32.add (local.get 0) (i32.const 200))) + (func $a2 (type $t) (i32.add (local.get 0) (i32.const 300))) + (func $b0 (type $t) (i32.mul (local.get 0) (i32.const 3))) + (func $b1 (type $t) (i32.sub (i32.const 1000) (local.get 0))) + (func $b2 (type $t) (i32.xor (local.get 0) (i32.const 0xFF))) + (elem (table $t0) (i32.const 0) func $a0 $a1 $a2) + (elem (table $t1) (i32.const 0) func $b0 $b1 $b2) + (func (export "f0") (param $x i32) (param $sel i32) (result i32) + (call_indirect $t0 (type $t) (local.get $x) (local.get $sel))) + (func (export "f1") (param $x i32) (param $sel i32) (result i32) + (call_indirect $t1 (type $t) (local.get $x) (local.get $sel))))