synth compiles WASM unreachable to a no-op on both thumb-2 and rv32 — falls through instead of trapping (WASM 4.4.5)

[avrabe]

Summary

The WASM unreachable instruction is compiled to a no-op (zero instructions) on both the Thumb-2 and RISC-V rv32 backends. WASM Core §4.4.5 requires unreachable to trap unconditionally. synth emits nothing, so control falls through and the function returns undefined state instead of trapping — every panic/abort, exhaustiveness default, and error-guard else (unreachable) silently continues.

• synth 0.34.0, -t cortex-m3 and -b riscv -t rv32imac
• oracle: wasmtime 42.0.1 (traps)

Reproducers

Minimal — a function that is just unreachable:

(module (func (export "f") (param i32 i32) (result i32) (unreachable)))

Thumb-2 disasm of f contains 0 udf instructions; rv32 contains 0 ebreak. wasmtime traps immediately; synth returns whatever is in r0/a0.

Realistic — an error guard:

(module (func (export "f") (param i32 i32) (result i32)
  (if (result i32) (i32.ge_s (local.get 0) (i32.const 0))
    (then (i32.const 1))
    (else (unreachable)))))

input	WASM spec	wasmtime	synth thumb-2	synth rv32
f(-5,_) (hits unreachable)	trap	wasm trap	returns 0 (no trap)	falls through

The else branch must trap; synth falls through and returns 0.

Impact

unreachable is how every front-end lowers panic!/abort/__builtin_unreachable/unmatched-switch-default/failed-assert. Compiling it to a no-op means those safety exits silently continue with undefined register/memory state on a safety-critical target — a serious correctness and security hole, and it affects both shipped backends.

Suggested fix

Emit an unconditional trap for unreachable: udf #0 (Thumb-2) / ebreak (rv32) — the same trap sequences synth already emits for div-by-zero and INT_MIN/-1 overflow. It must be an actual instruction, not elided.

Found via the pulseengine challenge harness (qemu thumb + rv32 execution differential vs wasmtime); disasm-confirmed (no udf/ebreak emitted) on both backends.