thumb-2: call_indirect emits no bounds-check and no type-check — OOB/wrong-type index does an uncontrolled indirect branch instead of trapping (WASM 4.4.8)

[avrabe]

Summary

On the Thumb-2 backend (-t cortex-m3), call_indirect emits no bounds check and no type/signature check — it computes table[index] from a runtime index and branches to it directly. WASM Core §4.4.8 requires call_indirect to trap when index >= table.size and when the table entry's runtime type does not match the static type. synth does neither, so an out-of-bounds or wrong-type index performs an uncontrolled indirect branch (arbitrary/garbage call) instead of a deterministic trap — a safety/security hole on the safety-critical embedded target synth exists for.

• synth 0.32.1
• oracle: wasmtime 42.0.1 (traps correctly)

The emitted code (Thumb-2)

For (call_indirect (type $bin) <args> (local.get 1)) with a runtime index in local 1:

lsl.w  r12, r4, #2        ; r12 = index * 4
ldr.w  r12, [r11, r12]    ; r12 = table[index]   (r11 = table base)
blx    r12                ; call it

Three instructions, zero cmp/bounds-branch/udf, zero type-tag comparison. Confirmed by disassembly (llvm-objdump --triple=thumbv7m; note synth disasm mis-decodes thumb as A32, see #637) and pinned in source:

• arm_encoder.rs (the CallIndirect expansion test): mov.w ip, rm, LSL #2; ldr.w ip, [r11, ip]; blx ip — the call_indirect on the A32 path (--target cortex-r5) compiles to a NOP — silently returns wrong result instead of calling the target #594/Thumb-2 CallIndirect shift lands in the type field (mov.w ip, rm, ASR #32) — always dispatches table entry 0 (shipped miscompile, masked by index-0 probes) #597 history only ever corrected the index computation (LSL #2 vs the ASR #32 type-field bug); a bounds/type check was never added.
• The CallIndirect lowering discards type_idx and a source comment admits full support still needs "Type signature checking / Bounds checking."

Reproducer

(module
  (type $bin (func (param i32 i32)(result i32)))
  (table 3 funcref)
  (elem (i32.const 0) $add $sub $mul)
  (func $add (param i32 i32)(result i32)(i32.add (local.get 0)(local.get 1)))
  (func $sub (param i32 i32)(result i32)(i32.sub (local.get 0)(local.get 1)))
  (func $mul (param i32 i32)(result i32)(i32.mul (local.get 0)(local.get 1)))
  (func (export "f")(param i32 i32)(result i32)
    (call_indirect (type $bin) (local.get 0)(i32.const 10)(local.get 1))))  ;; index = local 1

Executed under QEMU (Cortex-M semihosting) with the table linked at r11, vs wasmtime:

index	table size	WASM spec	wasmtime	synth (qemu)
0	3	add(a,10)	15	15 ✓
1	3	sub(a,10)	−5	−5 ✓
2	3	mul(a,10)	50	50 ✓
5	3	trap (OOB)	wasm trap	no trap — reads [r11 + 5*4] past the table and blx to that word (in this layout an invalid address → HardFault; with a different memory layout, a valid code/data word there is called = arbitrary indirect call)
99	3	trap (OOB)	wasm trap	no trap — same uncontrolled branch

In-bounds calls are correct; the OOB index produces behavior that depends entirely on whatever lies past the table in memory — undefined and uncontrolled, where the spec mandates a deterministic trap.

Two missing checks (WASM Core §4.4.8)

1. Bounds check — before the load: if (index >= table.size) trap;. Currently absent → OOB indirect branch. (Same defect class as the closed encoder: load/store imm12 offset truncated (& 0xFFF) with no bounds check — silent wrong-address class (cf #253/#255) #259 "load/store no bounds check — silent wrong-address".)
2. Type check — after the load: compare the callee's runtime type id against the static type_idx and trap on mismatch. Currently type_idx is discarded, so a table holding a differently-typed funcref is called with a mismatched signature → register/stack corruption.

Suggested fix

Emit, per call site: a bounds compare against the table length (trap via udf on hs), then load the entry, then (for the type check) load the entry's type id and compare against type_idx (trap on mismatch). This mirrors what wasmtime and every conformant engine do, and matches the trap sequences synth already emits for div-by-zero / INT_MIN overflow.

Distinct from #594 (A32 NOP, closed) and #597 (index shift in the type field, closed) — both were about reaching/indexing the table; this is about the safety checks around the access, which have never been present.

Found via the QEMU full-image execution-differential harness (all functions linked, table at r11) vs wasmtime; source-confirmed independently.

[avrabe]

Follow-up on v0.33.1: the bounds check is confirmed fixed here, but the type/signature check is still missing — so the wrong-type half of this issue is not yet resolved.

v0.33.1 call_indirect disasm (-t cortex-m3, llvm-objdump --triple=thumbv7m):

movw r12, #0x3        ; table size
cmp  r4, r12          ; index vs size          <-- BOUNDS CHECK (new, good)
blo  .ok
udf  #0               ; OOB -> trap
.ok:
lsl.w r12, r4, #2
ldr.w r12, [r11, r12] ; table[index]
blx   r12             ; call  -- NO type-id compare between the load and the call

Exactly one cmp before blx (the bounds compare); there is no comparison of the callee's runtime type against the static type_idx. WASM Core §4.4.8 requires a trap on signature mismatch as well.

Repro (in-bounds entry of the WRONG type must trap):

(module
  (type $unary (func (param i32)(result i32)))
  (type $nullary (func (result i32)))
  (table 2 funcref)
  (elem (i32.const 0) $u $n)
  (func $u (type $unary)(i32.mul (local.get 0)(i32.const 3)))
  (func $n (type $nullary)(i32.const 999))
  (func (export "f")(param i32 i32)(result i32)
    (call_indirect (type $unary)(i32.const 7)(local.get 1))))   ;; index in local 1

• idx 0 ($u, correct type): wasmtime 21 (7*3).
• idx 1 ($n, wrong type ()->i32): wasmtime traps (indirect call type mismatch); synth has no type check, so it calls $n with the $unary calling convention instead of trapping — type confusion.

Could this issue be reopened for the type-check half, or should I file a focused follow-up? Bounds half looks great.

[avrabe]

Confirmed on v0.37.0: the type-check half is now soundly addressed via a compile-time closed-world check — thanks. Verified by the campaign harness:

• Homogeneous table (all entries match the call's type): compiles, with the bounds check (cmp idx,size; blo; udf) present. No runtime type check is needed because closed-world analysis proves every reachable entry matches. ✓
• Heterogeneous table (an entry's signature differs from the call's expected type): refused at compile time —
  closed-world type check failed — table 0 entry (function 1, type 1) has a different signature than expected type 0 — refusing to emit an unchecked indirect branch (#642).
• call_indirect with a type matching no table entry: also refused (same closed-world path). ✓

That's a sound approach for a closed-world AOT compiler: prove type-safety statically or reject, instead of a runtime type check on a raw code-pointer table. Combined with the bounds check added earlier, both halves of this issue are resolved for the closed-world model. No further action needed from my side; flagging only so the campaign's tracker reflects it. (If an open-world path — imported/mutable tables via table.set of externally-typed funcrefs — is ever added, the runtime type check would come back into scope, but those ops are currently rejected.)