fix(codegen): call_indirect bounds guard + compile-time type check — OOB/wrong-type traps per WASM §4.4.8 (#642)

.github/workflows/ci.yml

@@ -450,6 +450,45 @@ jobs:
           SYNTH: ./target/debug/synth
         run: python scripts/repro/callee_saved_490_differential.py
 
+  call-indirect-642-oracle:
+    name: call_indirect bounds-guard oracle (Thumb-2 + A32)
+    # VCR-ORACLE-001 (#242, #642): call_indirect emitted NO table bounds check
+    # and NO type check — an out-of-bounds index read past the table and BLXed
+    # whatever word lay there (uncontrolled indirect branch) where WASM Core
+    # §4.4.8 mandates a trap. EXECUTE the fixture under unicorn on BOTH ISAs
+    # (Thumb-2 cortex-m3 + A32 cortex-r5, table linked at r11) vs the wasmtime
+    # oracle: in-bounds indices must match; OOB indices must stop AT A UDF.
+    # Non-vacuous red: the words past the table are seeded with a valid decoy
+    # function, so an unguarded build "succeeds" at the OOB call and the
+    # harness fails loudly on the decoy's return value. The type check is
+    # discharged at compile time (closed-world table verification in the
+    # selector); its decline paths are unit-gated in synth-core/synth-synthesis.
+    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 call_indirect bounds-guard oracle
+        env:
+          SYNTH: ./target/debug/synth
+        run: python scripts/repro/call_indirect_642_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

crates/synth-backend/src/arm_backend.rs

@@ -350,6 +350,10 @@ fn compile_wasm_to_arm(
         // imports (rewritten to the wasm field name by build_relocatable_elf)
         // instead of `__meld_dispatch_import`.
         selector.set_relocatable(config.relocatable);
+        // #642: call_indirect guard inputs (compile-time table size for the
+        // bounds guard + closed-world type verdicts). Without them, every
+        // call_indirect lowering declines loudly.
+        selector.set_call_indirect_guards(config.call_indirect_guards.clone());
         // #237: native-pointer ABI — wasm statics become __synth_wasm_data-relative.
         selector.set_native_pointer_abi(config.native_pointer_abi, config.linear_memory_bytes);
         // #311: i64 call results are register PAIRS — tag them.

crates/synth-backend/tests/a32_no_silent_nop_615.rs

@@ -649,6 +649,7 @@ fn representatives() -> Vec<ArmOp> {
             rd: Reg::R0,
             type_idx: 0,
             table_index_reg: Reg::R2,
+            table_size: 4, // #642: bounds-guard immediate
         },
         I64Add {
             rdlo: dl,

crates/synth-cli/src/main.rs

@@ -1260,6 +1260,9 @@ fn compile_command(
     // consumed by any codegen path (Phase 2 is the gated elision).
     let mut wsc_facts: Vec<WscFact> = Vec::new();
     let mut current_func_facts: Vec<WscFact> = Vec::new();
+    // #642: call_indirect guard inputs (compile-time table size + closed-world
+    // type verdicts). Default = decline every call_indirect (demo path).
+    let mut call_indirect_guards = synth_core::CallIndirectGuards::default();
     let (wasm_ops, func_name): (Vec<WasmOp>, String) = match (&input, &demo) {
         (Some(path), _) => {
             info!("Compiling WASM file: {}", path.display());
@@ -1290,6 +1293,9 @@ fn compile_command(
             // conditionally for the SBOM, so the tables never reached the config.
             let module = decode_wasm_module(&wasm_bytes)
                 .context("Failed to decode WASM module (signature tables)")?;
+            // #642: compute the call_indirect guard inputs BEFORE the
+            // module's vectors are moved out below.
+            call_indirect_guards = module.call_indirect_guards();
             func_ret_i64 = module.func_ret_i64;
             type_ret_i64 = module.type_ret_i64;
             // #643: capture the declared global slot widths (indexed by
@@ -1471,6 +1477,9 @@ fn compile_command(
         // empty unless SYNTH_FACT_SPEC + facts + a discharged obligation.
         fact_div_zero_elide,
         fact_div_ovf_elide,
+        // #642: call_indirect guard inputs — the default declines every
+        // call_indirect lowering, so the demo path (no module) stays safe.
+        call_indirect_guards,
         ..CompileConfig::default()
     };
 
@@ -2153,6 +2162,7 @@ fn compile_all_exports(
         all_type_ret_i64,  // #311: per-type returns-i64 (call_indirect)
         all_func_params_i64, // #359: per-function declared param widths (stack-arg ABI)
         all_wsc_facts,     // VCR-PERF-002 Phase 1 (#494): loom wsc.facts premises
+        all_call_indirect_guards, // #642: table size + closed-world type verdicts
     ) = if path.extension().is_some_and(|ext| ext == "wast") {
         info!("Parsing WAST (extracting all modules)...");
         let contents = String::from_utf8(file_bytes).context("WAST file is not valid UTF-8")?;
@@ -2251,6 +2261,10 @@ fn compile_all_exports(
             Vec::new(),
             Vec::new(), // #359: WAST fixture suite is i32-only — no stack params
             Vec::new(), // #494: facts are a loom-emitted-.wasm channel; WAST fixtures carry none
+            // #642: the multi-module WAST merge has no single table image to
+            // verify — the default guards DECLINE any call_indirect (the WAST
+            // fixture suite carries none), never an unchecked branch.
+            synth_core::CallIndirectGuards::default(),
         )
     } else {
         let wasm_bytes = if path.extension().is_some_and(|ext| ext == "wat") {
@@ -2268,6 +2282,9 @@ fn compile_all_exports(
         let module = decode_wasm_module(&wasm_bytes).context("Failed to decode WASM module")?;
         sbom_wasm_bytes = Some(wasm_bytes);
 
+        // #642: call_indirect guard inputs — computed while the module is
+        // still whole (before its vectors are moved out below).
+        let guards = module.call_indirect_guards();
         let func_arg_counts = module.func_arg_counts;
         let type_arg_counts = module.type_arg_counts;
         let memories = module.memories;
@@ -2342,6 +2359,7 @@ fn compile_all_exports(
             module.type_ret_i64,
             module.func_params_i64,
             module.wsc_facts,
+            guards, // #642
         )
     };
 
@@ -2428,6 +2446,9 @@ fn compile_all_exports(
         // `current_func_facts` in the compile loop below; Phase 2 reads it in
         // the selector behind SYNTH_FACT_SPEC.
         wsc_facts: all_wsc_facts.clone(),
+        // #642: call_indirect guard inputs (compile-time table size for the
+        // bounds guard + closed-world type verdicts). Default = decline.
+        call_indirect_guards: all_call_indirect_guards,
         ..CompileConfig::default()
     };
 

crates/synth-core/src/backend.rs

@@ -270,6 +270,14 @@ pub struct CompileConfig {
     /// divisor-nonzero fact alone NEVER lands here: divisor ≠ 0 does not
     /// exclude -1 (#633/#634 two-guard distinction). Empty ⇒ guard emitted.
     pub fact_div_ovf_elide: Vec<usize>,
+    /// #642: `call_indirect` guard inputs — the compile-time table size for
+    /// the runtime bounds check and the per-expected-type closed-world type
+    /// verdicts — computed from the decoded module by
+    /// [`crate::wasm_decoder::DecodedModule::call_indirect_guards`] and set by
+    /// the driver loops. The default (`table_size: None`, empty verdicts)
+    /// DECLINES every `call_indirect` lowering: an unchecked indirect branch
+    /// is never emitted (WASM Core §4.4.8 requires OOB/type-mismatch traps).
+    pub call_indirect_guards: crate::wasm_decoder::CallIndirectGuards,
 }
 
 /// #543 — an integrator-marked volatile linear-memory segment (the DMA transfer
@@ -339,6 +347,10 @@ impl Default for CompileConfig {
             // every div/rem trap guard is emitted, byte-identical.
             fact_div_zero_elide: Vec::new(),
             fact_div_ovf_elide: Vec::new(),
+            // #642: no guard inputs ⇒ every call_indirect lowering declines
+            // loudly (never an unchecked indirect branch). Driver loops fill
+            // this from the decoded module.
+            call_indirect_guards: crate::wasm_decoder::CallIndirectGuards::default(),
         }
     }
 }

crates/synth-core/src/lib.rs

@@ -25,8 +25,8 @@ pub use safety_manifest::SafetyManifest;
 pub use sbom::{CycloneDxSbom, SbomInputs};
 pub use target::*;
 pub use wasm_decoder::{
-    DecodedModule, FunctionOps, ImportEntry, ImportKind, WasmMemory, decode_wasm_functions,
-    decode_wasm_module,
+    CallIndirectGuards, DecodedModule, ElemSegmentInfo, FunctionOps, ImportEntry, ImportKind,
+    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};