From 6dc74d45eeb7044adac787452e5617efa0a49ce6 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 29 Jul 2026 15:01:30 +0200 Subject: [PATCH 1/4] feat(rv32): br_table compare-chain lowering + hard-error on target/backend ISA mismatch (#882) Item A: RV32 br_table lowers as a compare-and-branch chain (entry 0 vs x0, li+beq per entry, jal to default); >16 targets and value-carrying tables (#509 class) LOUD-DECLINE by name. Unit tests cover gale's exact shape, threshold, value-carrying, out-of-range depth, loop head targets. Item B: --target riscv32 with the defaulted arm backend used to silently print 'Using backend: arm' and build Thumb into a RISC-V ELF container. resolve_target_spec now hard-errors on any single-ISA backend/target family mismatch, lists the explicit backend's accepted targets, and from_triple's unknown-target error names the FULL valid set. CLI gate: crates/synth-cli/tests/unknown_target_882.rs. Plus: rv32_br_table_882.wat fixture, unicorn-vs-wasmtime differential (vacuity-guarded), rv32-br-table-oracle CI job, CHANGELOG. Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .github/workflows/ci.yml | 38 +++ CHANGELOG.md | 31 ++ crates/synth-backend-riscv/src/selector.rs | 316 ++++++++++++++++++ crates/synth-cli/src/main.rs | 211 +++++++++++- crates/synth-cli/tests/unknown_target_882.rs | 122 +++++++ crates/synth-core/src/target.rs | 8 +- scripts/repro/rv32_br_table_882.wat | 87 +++++ .../repro/rv32_br_table_882_differential.py | 144 ++++++++ 8 files changed, 937 insertions(+), 20 deletions(-) create mode 100644 crates/synth-cli/tests/unknown_target_882.rs create mode 100644 scripts/repro/rv32_br_table_882.wat create mode 100644 scripts/repro/rv32_br_table_882_differential.py diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index fc448ccc..9c460e39 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -993,6 +993,44 @@ jobs: SYNTH: ./target/debug/synth run: python scripts/repro/const_addr_fold_riscv_differential.py + rv32-br-table-oracle: + name: rv32 br_table execution oracle (#882) + # #882: RV32 lowers `br_table` as a compare-and-branch chain (entry 0 vs + # x0, li+beq per further entry, jal to default) — the last op standing + # between gale's wdg-thin driver and a complete RV32 lowering. The + # differential EXECUTES gale's exact shape (targets [0,1,0] default 1) plus + # 3-distinct-target and default-distinct dispatches under unicorn + # (UC_ARCH_RISCV) vs wasmtime, with indices covering EVERY table entry AND + # out-of-range/unsigned-edge (0x80000000, 0xFFFFFFFF must land on default — + # a wrong default or a signed chain compare is loud). A missing export + # (the pre-fix decline) fails the vacuity guard, so this can never pass + # vacuously. Isolated job: emulation deps pip-installed here ONLY. + 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@v7 + with: + python-version: "3.x" + - name: Install emulation deps + run: pip install wasmtime unicorn pyelftools + - name: Run RV32 br_table execution oracle + env: + SYNTH: ./target/debug/synth + run: python scripts/repro/rv32_br_table_882_differential.py + rv32-extern-call-reloc-oracle: name: rv32 external-call relocation oracle (#871) # #871: the gale thin-seam driver shape — exported functions calling an diff --git a/CHANGELOG.md b/CHANGELOG.md index 987b5f98..899e22f7 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,6 +7,37 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ## [Unreleased] +### Added + +- **RV32 `br_table` lowering (#882)** — the RISC-V selector now lowers + `br_table` as a compare-and-branch chain (entry 0 against `x0`, `li`+`beq` + per further entry, `jal` to the default), closing the last op gap on gale's + `wdg-thin` driver (`wdg_unlock`, `targets: [0, 1, 0], default: 1`). Any index + `>= targets.len()` — including "negative" i32s under the unsigned + interpretation — lands on the default label, per WASM core semantics. Tables + past 16 targets LOUD-DECLINE by name (`BrTableTooLarge`; the jump-table + upgrade is a named follow-up), and value-carrying `br_table` (the #509 + block-arity-threading class) LOUD-DECLINES (`BrTableValueCarrying`) instead + of silently miscompiling path-dependent result registers. Execution-verified + under unicorn RV32 vs wasmtime across every table entry AND out-of-range / + unsigned-edge indices (`scripts/repro/rv32_br_table_882_differential.py`, + CI job `rv32-br-table-oracle`, vacuity-guarded against skipped exports). + +### Fixed + +- **`--target`/backend ISA mismatch is now a hard error (#882)** — `synth + compile --target riscv32` without `-b riscv` silently printed + `Using backend: arm` and built Thumb code into a RISC-V ELF container, + failing only deep in the emitter ("non-CALL_PLT relocation ThmCall reached + the RISC-V ELF emitter") — a plausible-looking wrong-ISA object. A + recognised `--target` whose ISA family does not match the selected + single-ISA backend (arm / riscv / aarch64) now exits non-zero naming the + right `-b`; an explicit mismatched `-b` lists the targets it accepts; and an + unknown `--target` names the full valid set (now including cortex-m55, + cortex-r5, cortex-a53 and riscv32). No behavior change for good input — + every valid target/backend pairing resolves exactly as before (gated by + `crates/synth-cli/tests/unknown_target_882.rs`). + ## [0.52.0] - 2026-07-29 **"Enforce what we promise."** Every backend in this release stopped diff --git a/crates/synth-backend-riscv/src/selector.rs b/crates/synth-backend-riscv/src/selector.rs index 930c52ea..648856ed 100644 --- a/crates/synth-backend-riscv/src/selector.rs +++ b/crates/synth-backend-riscv/src/selector.rs @@ -96,6 +96,12 @@ impl SelectorOptions { } } +/// #882: largest `br_table` the compare-and-branch-chain lowering accepts. +/// Each entry costs at most 2 instructions (`li` + `beq`), so 16 targets is a +/// ≤33-instruction dispatch — past that a real jump table wins and the +/// selector LOUD-DECLINES (`SelectorError::BrTableTooLarge`) instead. +pub const BR_TABLE_MAX_TARGETS: usize = 16; + #[derive(Debug, Error)] pub enum SelectorError { #[error("unsupported wasm op for RV32 skeleton: {0:?}")] @@ -113,6 +119,29 @@ pub enum SelectorError { #[error("br depth {depth} out of range (control stack height {height})")] BrOutOfRange { depth: u32, height: usize }, + /// #882: `br_table` lowers as a compare-and-branch chain (one `li`+`beq` + /// per target), which is only sensible for small tables. A table past the + /// threshold needs a real jump table (PC-relative dispatch + bounds check) + /// — not implemented; decline loudly by name rather than emit a huge chain. + #[error( + "RV32 br_table with {targets} targets exceeds the compare-chain \ + threshold ({max}); jump-table dispatch is not implemented for RV32 — \ + declining loudly (#882)" + )] + BrTableTooLarge { targets: usize, max: usize }, + + /// #882/#509 class: a `br_table` whose targeted frames would carry values + /// (non-zero label arity, or transient values that a taken branch would + /// discard) needs block-arity threading the single-pass selector does not + /// model — a jump would leave the values in path-dependent registers. + /// Loud decline, never a silent path-dependent miscompile. + #[error( + "RV32 br_table with value-carrying targets (vstack height {height} != \ + target frame entry height {entry}) needs block-arity threading (#509) \ + — declining loudly (#882)" + )] + BrTableValueCarrying { height: usize, entry: usize }, + #[error("stack type mismatch at op {op:?}: expected {expected}, found {found} on top of stack")] StackTypeMismatch { op: WasmOp, @@ -1801,6 +1830,7 @@ impl Selector { End => self.lower_end()?, Br(depth) => self.lower_br(*depth, op)?, BrIf(depth) => self.lower_br_if(*depth, op)?, + BrTable { targets, default } => self.lower_br_table(targets, *default, op)?, Return => { self.emit_return_epilogue(); @@ -2985,6 +3015,105 @@ impl Selector { Ok(()) } + /// #882: `br_table` — pop the i32 index, then dispatch: index `i` branches + /// to `targets[i]`; any index `>= targets.len()` (including "negative" + /// i32s, which are huge unsigned values) falls through to `default`, per + /// WASM core semantics (the index is interpreted unsigned and clamps to + /// the default label). + /// + /// Lowering: a COMPARE-AND-BRANCH CHAIN — for each table entry `i`, + /// `li tmp, i; beq idx, tmp, L_target(i)` (entry 0 compares against `x0` + /// directly, no materialization), then an unconditional `jal x0, L_default`. + /// Equality is sign-agnostic, so `beq` against the constants `0..len-1` is + /// exact for the unsigned-index semantics; every non-matching index — + /// in-range-of-i32 or not — lands on the default jump. No jump table, no + /// data section, no PC-relative table: for the small tables real drivers + /// carry (gale's `wdg_unlock` is 3 targets) the chain is both smaller and + /// simpler to verify than an indirect dispatch. Tables past + /// [`BR_TABLE_MAX_TARGETS`] LOUD-DECLINE (`BrTableTooLarge`) rather than + /// emit an unbounded chain — the jump-table upgrade is a named follow-up. + /// + /// Value-carrying `br_table` (targeted frames entered at a different stack + /// height than the post-pop height — i.e. the jump would carry or discard + /// vstack values) is the #509 block-arity-threading class: the single-pass + /// selector cannot reconcile per-path result registers, so it LOUD-DECLINES + /// (`BrTableValueCarrying`) instead of silently miscompiling. Plain + /// `Br`/`BrIf` share the underlying limitation; `br_table` checks it + /// explicitly because the multi-way dispatch makes the path-dependence + /// concrete. + fn lower_br_table( + &mut self, + targets: &[u32], + default: u32, + op: &WasmOp, + ) -> Result<(), SelectorError> { + if targets.len() > BR_TABLE_MAX_TARGETS { + return Err(SelectorError::BrTableTooLarge { + targets: targets.len(), + max: BR_TABLE_MAX_TARGETS, + }); + } + let idx = self.pop_i32(op)?; + // Conservative value-carrying guard (#509 class): every targeted frame + // (including the default) must have been entered at exactly the + // current post-pop vstack height — then a taken branch moves no + // values and the plain-jump lowering is sound. + let height = self.vstack.len(); + for &depth in targets.iter().chain(std::iter::once(&default)) { + let ctrl_height = self.ctrl.len(); + let d = depth as usize; + if d >= ctrl_height { + return Err(SelectorError::BrOutOfRange { + depth, + height: ctrl_height, + }); + } + let entry = self.ctrl[ctrl_height - 1 - d].stack_height_at_entry; + if entry != height { + return Err(SelectorError::BrTableValueCarrying { height, entry }); + } + } + // Compare chain. One scratch register is reused for every non-zero + // constant; `idx` is pinned by `pop_i32` so the scratch can't alias it. + let mut scratch: Option = None; + for (i, &depth) in targets.iter().enumerate() { + let label = self.target_label_for_depth(depth)?; + let rs2 = if i == 0 { + Reg::ZERO + } else { + let tmp = match scratch { + Some(t) => t, + None => { + let t = self.alloc_temp(); + scratch = Some(t); + t + } + }; + // i <= BR_TABLE_MAX_TARGETS - 1 always fits addi's imm12. + self.out.push(RiscVOp::Addi { + rd: tmp, + rs1: Reg::ZERO, + imm: i as i32, + }); + tmp + }; + self.out.push(RiscVOp::Branch { + cond: Branch::Eq, + rs1: idx, + rs2, + label, + }); + } + // No entry matched → default. This is also where every out-of-range + // index (>= targets.len(), unsigned) lands. + let default_label = self.target_label_for_depth(default)?; + self.out.push(RiscVOp::Jal { + rd: Reg::ZERO, + label: default_label, + }); + Ok(()) + } + fn target_label_for_depth(&self, depth: u32) -> Result { let height = self.ctrl.len(); let depth = depth as usize; @@ -5245,6 +5374,193 @@ mod tests { )); } + /// #882: gale's exact `wdg_unlock` shape — `br_table { targets: [0, 1, 0], + /// default: 1 }` over two nested blocks — must LOWER (it was the last op + /// declining on the wdg-thin driver), as a compare-and-branch chain: + /// `beq idx, x0` for entry 0, `li`+`beq` for entries 1 and 2, then an + /// unconditional `jal` to the default label. + #[test] + fn br_table_882_gale_shape_lowers() { + let out = s( + &[ + WasmOp::Block, + WasmOp::Block, + WasmOp::LocalGet(0), + WasmOp::BrTable { + targets: vec![0, 1, 0], + default: 1, + }, + WasmOp::End, + WasmOp::End, + WasmOp::End, + ], + 1, + ); + // 3 targets → 3 beq (entry 0 against x0), plus the default jal. + assert_eq!( + count(&out, |op| matches!( + op, + RiscVOp::Branch { + cond: Branch::Eq, + .. + } + )), + 3, + "one beq per table entry: {out:?}" + ); + assert_eq!( + count(&out, |op| matches!( + op, + RiscVOp::Branch { + cond: Branch::Eq, + rs2: Reg::ZERO, + .. + } + )), + 1, + "entry 0 compares against x0 directly" + ); + // The default dispatch jal (rd = x0) — distinct from the return jalr. + assert!( + count(&out, |op| matches!(op, RiscVOp::Jal { rd: Reg::ZERO, .. })) >= 1, + "unconditional jal to the default label: {out:?}" + ); + } + + /// #882: a table past `BR_TABLE_MAX_TARGETS` must LOUD-DECLINE by name + /// (`BrTableTooLarge`), never emit an unbounded compare chain. + #[test] + fn br_table_882_large_table_loud_declines() { + let targets: Vec = vec![0; BR_TABLE_MAX_TARGETS + 1]; + let ops = [ + WasmOp::Block, + WasmOp::LocalGet(0), + WasmOp::BrTable { + targets, + default: 0, + }, + WasmOp::End, + WasmOp::End, + ]; + match select(&ops, 1) { + Ok(_) => panic!("oversized br_table must decline on RV32"), + Err(err) => assert!( + matches!( + err, + SelectorError::BrTableTooLarge { + targets: 17, + max: BR_TABLE_MAX_TARGETS + } + ), + "must surface as BrTableTooLarge, got: {err:?}" + ), + } + // At the threshold itself it must still lower. + let targets: Vec = vec![0; BR_TABLE_MAX_TARGETS]; + let ops = [ + WasmOp::Block, + WasmOp::LocalGet(0), + WasmOp::BrTable { + targets, + default: 0, + }, + WasmOp::End, + WasmOp::End, + ]; + select(&ops, 1).expect("threshold-sized br_table must lower"); + } + + /// #882/#509 class: a br_table that would carry a vstack value across the + /// jump (target frame entered at a lower stack height) must LOUD-DECLINE — + /// the single-pass selector cannot reconcile path-dependent result + /// registers. + #[test] + fn br_table_882_value_carrying_loud_declines() { + let ops = [ + WasmOp::Block, + WasmOp::I32Const(5), // transient value the jump would discard/carry + WasmOp::LocalGet(0), + WasmOp::BrTable { + targets: vec![0], + default: 0, + }, + WasmOp::End, + WasmOp::End, + ]; + match select(&ops, 1) { + Ok(_) => panic!("value-carrying br_table must decline on RV32"), + Err(err) => assert!( + matches!( + err, + SelectorError::BrTableValueCarrying { + height: 1, + entry: 0 + } + ), + "must surface as BrTableValueCarrying, got: {err:?}" + ), + } + } + + /// #882: a br_table depth past the control-stack height is invalid wasm — + /// surface `BrOutOfRange`, mirroring `br`. + #[test] + fn br_table_882_depth_out_of_range() { + let ops = [ + WasmOp::Block, + WasmOp::LocalGet(0), + WasmOp::BrTable { + targets: vec![0, 7], + default: 0, + }, + WasmOp::End, + WasmOp::End, + ]; + match select(&ops, 1) { + Ok(_) => panic!("out-of-range br_table depth must error"), + Err(err) => assert!( + matches!(err, SelectorError::BrOutOfRange { depth: 7, .. }), + "must surface as BrOutOfRange, got: {err:?}" + ), + } + } + + /// #882: a br_table targeting a LOOP frame branches to the loop HEAD + /// (back-edge), mirroring `br` semantics. + #[test] + fn br_table_882_loop_target_uses_head_label() { + let out = s( + &[ + WasmOp::Loop, + WasmOp::Block, + WasmOp::LocalGet(0), + WasmOp::BrTable { + targets: vec![0, 1], + default: 0, + }, + WasmOp::End, + WasmOp::End, + WasmOp::End, + ], + 1, + ); + // Entry 1 targets the loop → its beq label must be the loop head. + let head = out + .iter() + .find_map(|op| match op { + RiscVOp::Label { name } if name.starts_with("Lloop_head") => Some(name.clone()), + _ => None, + }) + .expect("loop head label emitted"); + assert!( + out.iter().any(|op| matches!( + op, + RiscVOp::Branch { cond: Branch::Eq, label, .. } if *label == head + )), + "br_table entry targeting the loop must branch to the head label: {out:?}" + ); + } + #[test] fn trunc_sat_782_loud_declines_on_rv32() { // #782a: the decoder now delivers the trunc_sat family; RV32 has no diff --git a/crates/synth-cli/src/main.rs b/crates/synth-cli/src/main.rs index d09cd0a0..681c6f2f 100644 --- a/crates/synth-cli/src/main.rs +++ b/crates/synth-cli/src/main.rs @@ -309,9 +309,12 @@ enum Commands { #[arg(long, value_name = "MODE")] safety_bounds: Option, - /// Compilation backend (arm, w2c2, awsm, wasker) - #[arg(short, long, default_value = "arm")] - backend: String, + /// Compilation backend (arm, riscv, aarch64, w2c2, awsm, wasker). + /// Defaults to `arm`. #882: a `--target` whose ISA family does not + /// match the selected backend is a HARD ERROR, never a silent + /// wrong-ISA build. + #[arg(short, long)] + backend: Option, /// Run translation validation after compilation #[arg(long)] @@ -614,8 +617,15 @@ fn main() -> Result<()> { stack_layout, stack_size, } => { + // #882: track whether `-b/--backend` was given explicitly (the + // mismatch diagnostics differ: an explicit backend lists the + // targets IT accepts; the defaulted `arm` backend tells the user + // which `-b` their target needs). + let backend_explicit = backend.is_some(); + let backend = backend.unwrap_or_else(|| "arm".to_string()); // Resolve target spec: --target overrides, --cortex-m is backwards compat - let target_spec = resolve_target_spec(target.as_deref(), cortex_m, &backend)?; + let target_spec = + resolve_target_spec(target.as_deref(), cortex_m, &backend, backend_explicit)?; // #778 phase 2: parse + schema-validate the UNTRUSTED hints file up // front so a malformed oracle input fails loudly, not mid-compile. @@ -1016,25 +1026,103 @@ struct ElfFunction { line_map: synth_core::backend::LineMap, } +/// #882: the `--target` names each single-ISA backend accepts — used by the +/// unknown-target and target/backend-mismatch diagnostics. Transpiler +/// backends (w2c2/awsm/wasker) are target-agnostic and return `None`. +fn backend_accepted_targets(backend: &str) -> Option<&'static str> { + match backend { + "arm" => Some( + "cortex-m3, cortex-m4, cortex-m4f, cortex-m7, cortex-m7dp, cortex-m55, cortex-r5", + ), + "riscv" => Some("rv32imac, rv32imc, rv32im, rv32i, rv32gc, esp32c3, riscv32"), + "aarch64" => Some("cortex-a53"), + _ => None, + } +} + +/// #882: human-readable ISA-family name for the mismatch diagnostics. +fn family_name(family: &synth_core::target::ArchFamily) -> &'static str { + use synth_core::target::ArchFamily; + match family { + ArchFamily::ArmCortexM => "ARM Cortex-M", + ArchFamily::ArmCortexR => "ARM Cortex-R", + ArchFamily::ArmCortexA => "AArch64", + ArchFamily::RiscV => "RISC-V", + } +} + /// Resolve --target / --cortex-m into a TargetSpec -fn resolve_target_spec(target: Option<&str>, cortex_m: bool, backend: &str) -> Result { - match target { - // from_triple already lists the supported ARM + RV32 names in its error. - Some(name) => TargetSpec::from_triple(name).map_err(|e| anyhow::anyhow!("{e}")), +/// +/// #882: an unrecognised `--target` HARD-ERRORS listing the valid names +/// (`TargetSpec::from_triple`'s error, plus the explicit backend's accepted +/// set when `-b` was given), and a RECOGNISED target whose ISA family does +/// not match the selected single-ISA backend (arm / riscv / aarch64) ALSO +/// hard-errors. Pre-fix, `--target riscv32` with the defaulted `arm` backend +/// silently printed "Using backend: arm" and built Thumb code into a RISC-V +/// ELF container, failing only deep in the emitter ("non-CALL_PLT relocation +/// ThmCall reached the RISC-V ELF emitter") — a plausible-looking wrong-ISA +/// object is exactly how someone ships the wrong build. +fn resolve_target_spec( + target: Option<&str>, + cortex_m: bool, + backend: &str, + backend_explicit: bool, +) -> Result { + use synth_core::target::ArchFamily; + let (name, spec) = match target { + // from_triple lists the supported target names in its error. + Some(name) => { + let spec = TargetSpec::from_triple(name).map_err(|e| { + match backend_accepted_targets(backend) { + Some(list) if backend_explicit => anyhow::anyhow!( + "{e}\ntargets accepted by backend '{backend}': {list}" + ), + _ => anyhow::anyhow!("{e}"), + } + })?; + (name, spec) + } // No --target given: pick a backend-appropriate default so `-b riscv` // doesn't inherit the ARM profile and bail (#218). - None if backend == "riscv" => Ok(TargetSpec::riscv32("imac")), + None if backend == "riscv" => return Ok(TargetSpec::riscv32("imac")), // #538: `-b aarch64` without --target defaults to the A64 host profile. - None if backend == "aarch64" => Ok(TargetSpec::cortex_a53()), - None if cortex_m => Ok(TargetSpec::cortex_m3()), + None if backend == "aarch64" => return Ok(TargetSpec::cortex_a53()), + None if cortex_m => return Ok(TargetSpec::cortex_m3()), None => { // Default: Arm32 ISA (non-Cortex-M, no vector table) - Ok(TargetSpec { + return Ok(TargetSpec { isa: synth_core::target::IsaVariant::Arm32, ..TargetSpec::cortex_m4() - }) + }); } + }; + // #882: cross-check the resolved target's ISA family against the + // single-ISA backends; unchecked combinations (w2c2/awsm/wasker) keep + // their previous behavior. + let required_backend = match spec.family { + ArchFamily::ArmCortexM | ArchFamily::ArmCortexR => "arm", + ArchFamily::ArmCortexA => "aarch64", + ArchFamily::RiscV => "riscv", + }; + let backend_is_isa = matches!(backend, "arm" | "riscv" | "aarch64"); + if backend_is_isa && backend != required_backend { + let family = family_name(&spec.family); + if backend_explicit { + let accepted = backend_accepted_targets(backend).unwrap_or("(none)"); + anyhow::bail!( + "backend '{backend}' does not accept --target {name} ({family}).\n\ + targets accepted by backend '{backend}': {accepted}\n\ + for {name}, use `-b {required_backend}`" + ); + } + anyhow::bail!( + "--target {name} is a {family} target, but no backend was selected, so the \ + default 'arm' backend would silently produce a wrong-ISA object — refusing.\n\ + pass `-b {required_backend}` for this target, or pick an ARM target: {arm}", + arm = backend_accepted_targets("arm").unwrap_or("(none)"), + ); } + Ok(spec) } /// Build the backend registry with all available backends @@ -8591,37 +8679,124 @@ mod tests { fn test_resolve_target_spec_default_no_cortex_m() { // When neither --target nor --cortex-m is given, the default is an // Arm32-ISA cortex_m4 spec (used by the non-Cortex-M flow). - let spec = resolve_target_spec(None, false, "arm").unwrap(); + let spec = resolve_target_spec(None, false, "arm", false).unwrap(); assert_eq!(spec.isa, synth_core::target::IsaVariant::Arm32); } #[test] fn test_resolve_target_spec_cortex_m_flag() { // --cortex-m without --target maps to cortex-m3. - let spec = resolve_target_spec(None, true, "arm").unwrap(); + let spec = resolve_target_spec(None, true, "arm", false).unwrap(); assert_eq!(spec.triple, "thumbv7m-none-eabi"); } #[test] fn test_resolve_target_spec_explicit_target_wins_over_cortex_m() { // --target overrides --cortex-m. - let spec = resolve_target_spec(Some("cortex-m7"), true, "arm").unwrap(); + let spec = resolve_target_spec(Some("cortex-m7"), true, "arm", false).unwrap(); assert_eq!(spec.triple, "thumbv7em-none-eabihf"); } #[test] fn test_resolve_target_spec_unknown_triple_errors() { - let err = resolve_target_spec(Some("totally-bogus-triple"), false, "arm").unwrap_err(); + let err = + resolve_target_spec(Some("totally-bogus-triple"), false, "arm", false).unwrap_err(); let msg = err.to_string(); assert!(msg.contains("totally-bogus-triple")); assert!(msg.contains("Supported")); } + /// #882: an unknown target with an EXPLICIT backend additionally lists the + /// targets that backend accepts. + #[test] + fn test_resolve_target_spec_unknown_triple_lists_backend_targets_882() { + let err = + resolve_target_spec(Some("totally-bogus-triple"), false, "riscv", true).unwrap_err(); + let msg = err.to_string(); + assert!(msg.contains("Supported"), "{msg}"); + assert!( + msg.contains("targets accepted by backend 'riscv'"), + "explicit -b must list its accepted targets: {msg}" + ); + assert!(msg.contains("esp32c3"), "{msg}"); + } + + /// #882 (gale): `--target riscv32` with the DEFAULTED arm backend must + /// HARD-ERROR pointing at `-b riscv` — pre-fix it silently printed + /// "Using backend: arm" and built Thumb code into a RISC-V ELF container. + #[test] + fn test_resolve_target_spec_riscv_target_arm_default_backend_errors_882() { + for name in ["riscv32", "rv32imac", "esp32c3", "riscv32imac-unknown-none-elf"] { + let err = resolve_target_spec(Some(name), false, "arm", false).unwrap_err(); + let msg = err.to_string(); + assert!(msg.contains("RISC-V"), "{name}: {msg}"); + assert!(msg.contains("-b riscv"), "{name}: {msg}"); + } + } + + /// #882: an EXPLICIT mismatched backend errors naming the targets that + /// backend accepts. + #[test] + fn test_resolve_target_spec_explicit_backend_mismatch_errors_882() { + let err = resolve_target_spec(Some("cortex-m3"), false, "riscv", true).unwrap_err(); + let msg = err.to_string(); + assert!( + msg.contains("does not accept --target cortex-m3"), + "{msg}" + ); + assert!(msg.contains("rv32imac"), "{msg}"); + assert!(msg.contains("-b arm"), "{msg}"); + + let err = resolve_target_spec(Some("riscv32"), false, "arm", true).unwrap_err(); + let msg = err.to_string(); + assert!(msg.contains("does not accept --target riscv32"), "{msg}"); + assert!(msg.contains("cortex-m3"), "{msg}"); + assert!(msg.contains("-b riscv"), "{msg}"); + + let err = resolve_target_spec(Some("cortex-a53"), false, "arm", true).unwrap_err(); + assert!(err.to_string().contains("-b aarch64"), "{err}"); + } + + /// #882: every currently-valid target/backend PAIRING keeps resolving to + /// the same spec as before — no behavior change for good input. + #[test] + fn test_resolve_target_spec_good_input_unchanged_882() { + let arm_targets = [ + "cortex-m3", + "cortex-m4", + "cortex-m4f", + "cortex-m7", + "cortex-m7dp", + "cortex-m55", + "cortex-r5", + ]; + for name in arm_targets { + for explicit in [false, true] { + let spec = resolve_target_spec(Some(name), false, "arm", explicit) + .unwrap_or_else(|e| panic!("{name} must resolve on arm: {e}")); + assert_eq!(spec, TargetSpec::from_triple(name).unwrap(), "{name}"); + } + } + let rv_targets = [ + "rv32imac", "rv32imc", "rv32im", "rv32i", "rv32gc", "esp32c3", "riscv32", + ]; + for name in rv_targets { + let spec = resolve_target_spec(Some(name), false, "riscv", true) + .unwrap_or_else(|e| panic!("{name} must resolve on riscv: {e}")); + assert_eq!(spec.family, synth_core::target::ArchFamily::RiscV, "{name}"); + } + let spec = resolve_target_spec(Some("cortex-a53"), false, "aarch64", true).unwrap(); + assert_eq!(spec.family, synth_core::target::ArchFamily::ArmCortexA); + // Transpiler backends stay target-unchecked (previous behavior). + let spec = resolve_target_spec(Some("riscv32"), false, "w2c2", true).unwrap(); + assert_eq!(spec.family, synth_core::target::ArchFamily::RiscV); + } + /// #218: `-b riscv` with no `--target` must default to an RV32 profile, not /// inherit the ARM default (which makes the RISC-V backend bail). #[test] fn test_resolve_target_spec_riscv_default_218() { - let spec = resolve_target_spec(None, false, "riscv").unwrap(); + let spec = resolve_target_spec(None, false, "riscv", true).unwrap(); assert_eq!(spec.family, synth_core::target::ArchFamily::RiscV); assert_eq!( spec.isa, diff --git a/crates/synth-cli/tests/unknown_target_882.rs b/crates/synth-cli/tests/unknown_target_882.rs new file mode 100644 index 00000000..a22dab7d --- /dev/null +++ b/crates/synth-cli/tests/unknown_target_882.rs @@ -0,0 +1,122 @@ +//! #882 — the `--target` seam must never silently select a wrong-ISA build. +//! +//! gale's papercut: `synth compile … --target riscv32` (no `-b`) printed +//! "Using backend: arm" and produced Thumb code in a RISC-V ELF container, +//! failing only deep in the emitter ("non-CALL_PLT relocation ThmCall +//! reached the RISC-V ELF emitter"). This gate pins the CLI behavior: +//! +//! 1. an UNKNOWN `--target` exits non-zero naming the valid set; +//! 2. a KNOWN target whose ISA family mismatches the (defaulted or explicit) +//! single-ISA backend exits non-zero pointing at the right `-b`; +//! 3. every currently-valid target/backend pairing still compiles (no +//! behavior change for good input). + +use std::path::PathBuf; +use std::process::Command; + +fn synth() -> &'static str { + env!("CARGO_BIN_EXE_synth") +} + +fn fixture() -> PathBuf { + PathBuf::from(env!("CARGO_MANIFEST_DIR")) + .join("../..") + .join("scripts/repro/rv32_br_table_882.wat") +} + +fn run(args: &[&str]) -> (bool, String) { + use std::sync::atomic::{AtomicU32, Ordering}; + static N: AtomicU32 = AtomicU32::new(0); + let out_path = std::env::temp_dir().join(format!( + "synth_882_{}_{}.o", + std::process::id(), + N.fetch_add(1, Ordering::Relaxed) + )); + let out = Command::new(synth()) + .arg("compile") + .arg(fixture()) + .args(args) + .arg("-o") + .arg(&out_path) + .output() + .expect("spawn synth"); + let text = format!( + "{}{}", + String::from_utf8_lossy(&out.stdout), + String::from_utf8_lossy(&out.stderr) + ); + (out.status.success(), text) +} + +/// #882 (1): unknown --target → non-zero, message names the valid set. +#[test] +fn unknown_target_hard_errors_with_valid_set() { + let (ok, text) = run(&["--target", "riscv32xyz"]); + assert!(!ok, "unknown target must exit non-zero, got:\n{text}"); + assert!( + text.contains("unknown target triple: riscv32xyz"), + "must name the bad target:\n{text}" + ); + for name in ["cortex-m3", "rv32imac", "esp32c3", "cortex-a53"] { + assert!(text.contains(name), "valid set must include {name}:\n{text}"); + } + // And it must never have reached backend selection. + assert!( + !text.contains("Using backend"), + "must fail BEFORE backend selection:\n{text}" + ); +} + +/// #882 (1b): unknown --target with an EXPLICIT backend additionally lists +/// that backend's accepted targets. +#[test] +fn unknown_target_with_explicit_backend_lists_its_targets() { + let (ok, text) = run(&["--target", "riscv32xyz", "-b", "riscv"]); + assert!(!ok, "unknown target must exit non-zero, got:\n{text}"); + assert!( + text.contains("targets accepted by backend 'riscv'"), + "explicit -b must list its accepted set:\n{text}" + ); +} + +/// #882 (2) — gale's exact shape: `--target riscv32` with NO `-b` must +/// hard-error pointing at `-b riscv`, not print "Using backend: arm". +#[test] +fn riscv_target_with_defaulted_arm_backend_hard_errors() { + let (ok, text) = run(&["--target", "riscv32", "--all-exports", "--relocatable"]); + assert!( + !ok, + "--target riscv32 without -b riscv must exit non-zero, got:\n{text}" + ); + assert!(text.contains("RISC-V"), "{text}"); + assert!(text.contains("-b riscv"), "must point at -b riscv:\n{text}"); + assert!( + !text.contains("Using backend"), + "must fail BEFORE backend selection:\n{text}" + ); +} + +/// #882 (2b): explicit mismatched backend errors naming its accepted targets. +#[test] +fn explicit_backend_target_mismatch_hard_errors() { + let (ok, text) = run(&["--target", "cortex-m3", "-b", "riscv"]); + assert!(!ok, "cortex-m3 on -b riscv must exit non-zero, got:\n{text}"); + assert!( + text.contains("does not accept --target cortex-m3"), + "{text}" + ); + assert!(text.contains("rv32imac"), "{text}"); +} + +/// #882 (3): good input unchanged — the matched pairings still compile. +#[test] +fn good_target_backend_pairings_still_compile() { + for args in [ + &["--target", "cortex-m3", "--all-exports"][..], + &["--target", "rv32imac", "-b", "riscv", "--all-exports", "--relocatable"][..], + &["--target", "esp32c3", "-b", "riscv", "--all-exports", "--relocatable"][..], + ] { + let (ok, text) = run(args); + assert!(ok, "good input {args:?} must still compile:\n{text}"); + } +} diff --git a/crates/synth-core/src/target.rs b/crates/synth-core/src/target.rs index 6191b52b..c2023491 100644 --- a/crates/synth-core/src/target.rs +++ b/crates/synth-core/src/target.rs @@ -516,10 +516,14 @@ impl TargetSpec { "riscv32gc" | "rv32gc" => Ok(Self::riscv32("gc")), // Generic RV32 default → the broadly-supported imac profile. "riscv32" | "rv32" => Ok(Self::riscv32("imac")), + // #882: name the FULL valid set — an unrecognised target is a + // hard error at the CLI seam and this message is the user's map. _ => Err(format!( "unknown target triple: {triple}. Supported: \ - cortex-m3, cortex-m4, cortex-m4f, cortex-m7, cortex-m7dp; \ - rv32imac, rv32imc, rv32im, rv32i, rv32gc, esp32c3" + cortex-m3, cortex-m4, cortex-m4f, cortex-m7, cortex-m7dp, \ + cortex-m55, cortex-r5 (ARM); \ + rv32imac, rv32imc, rv32im, rv32i, rv32gc, esp32c3, riscv32 \ + (RISC-V, -b riscv); cortex-a53 (-b aarch64)" )), } } diff --git a/scripts/repro/rv32_br_table_882.wat b/scripts/repro/rv32_br_table_882.wat new file mode 100644 index 00000000..a28feb68 --- /dev/null +++ b/scripts/repro/rv32_br_table_882.wat @@ -0,0 +1,87 @@ +;; #882 — RV32 br_table compare-chain lowering fixture. +;; +;; `dispatch` is gale's exact wdg_unlock shape: br_table { targets: [0, 1, 0], +;; default: 1 } — the last op standing between the wdg-thin driver and a +;; complete RV32 lowering. `dispatch3` covers three DISTINCT targets plus +;; default (the ARM #507 shape), so a wrong chain entry or a wrong default is +;; observable as a wrong return value, not just a shared-landing coincidence. +;; +;; Landings write through a local and fall to a common end (no mid-block +;; `return` — that is the separate #882 fixture-2 `Lend0` class). +;; +;; Semantics under test (WASM core): index i < len → targets[i]; any index +;; >= len (unsigned interpretation — "negative" i32s included) → default. +(module + (memory 1) + + ;; gale wdg_unlock shape: targets [0, 1, 0], default 1. + ;; index 0 → depth 0 (inner) → 10 + ;; index 1 → depth 1 (outer) → 20 + ;; index 2 → depth 0 (inner) → 10 + ;; else → depth 1 (outer) → 20 + (func (export "dispatch") (param i32) (result i32) + (local i32) + (block $end + (block $outer + (block $inner + local.get 0 + br_table $inner $outer $inner $outer + ) + ;; depth-0 landing (index 0 or 2) + i32.const 10 + local.set 1 + br $end + ) + ;; depth-1 landing (index 1 or out-of-range) + i32.const 20 + local.set 1 + ) + local.get 1) + + ;; three distinct targets: 0→10, 1→20, 2→30, out-of-range→30 (default). + (func (export "dispatch3") (param i32) (result i32) + (local i32) + (block $end + (block $b2 + (block $b1 + (block $b0 + local.get 0 + br_table $b0 $b1 $b2 $b2 + ) + i32.const 10 + local.set 1 + br $end + ) + i32.const 20 + local.set 1 + br $end + ) + i32.const 30 + local.set 1 + ) + local.get 1) + + ;; default DISTINCT from every table entry: 0→11, 1→22, out-of-range→33. + ;; A lowering that folds the default into the last chain entry (or clamps + ;; the index to the table instead of to default) fails here. + (func (export "dispatch_default") (param i32) (result i32) + (local i32) + (block $end + (block $bd + (block $b1 + (block $b0 + local.get 0 + br_table $b0 $b1 $bd + ) + i32.const 11 + local.set 1 + br $end + ) + i32.const 22 + local.set 1 + br $end + ) + i32.const 33 + local.set 1 + ) + local.get 1)) diff --git a/scripts/repro/rv32_br_table_882_differential.py b/scripts/repro/rv32_br_table_882_differential.py new file mode 100644 index 00000000..2ebeacda --- /dev/null +++ b/scripts/repro/rv32_br_table_882_differential.py @@ -0,0 +1,144 @@ +#!/usr/bin/env python3 +"""#882 — RV32 br_table compare-chain execution oracle. + +RV32 lowers `br_table` as a compare-and-branch chain (`beq idx, x0` for entry +0, `li`+`beq` per further entry, `jal` to the default) — no jump table. This +oracle compiles scripts/repro/rv32_br_table_882.wat (gale's exact wdg_unlock +shape `targets: [0,1,0], default: 1`, plus a 3-distinct-target dispatch and a +default-distinct-from-every-entry dispatch), runs every export under unicorn +(UC_ARCH_RISCV / UC_MODE_RISCV32) and compares with wasmtime ground truth. + +Index vectors cover EVERY table entry AND out-of-range — including the +unsigned-interpretation edge (0x80000000, 0xFFFFFFFF must land on default, +never wrap into the table): a wrong default target or a signed chain compare +is loud here. + +Symbols come from the ELF .symtab (SHT_SYMTAB), not `synth disasm` text. + +Run: + synth compile scripts/repro/rv32_br_table_882.wat -b riscv \ + --target riscv32imac --relocatable --all-exports -o /tmp/brtable.o + python scripts/repro/rv32_br_table_882_differential.py /tmp/brtable.o +""" + +import os +import subprocess +import sys +import tempfile + +import wasmtime +from elftools.elf.elffile import ELFFile +from unicorn import UC_ARCH_RISCV, UC_MODE_RISCV32, Uc, UcError +from unicorn.riscv_const import ( + UC_RISCV_REG_A0, + UC_RISCV_REG_RA, + UC_RISCV_REG_S11, + UC_RISCV_REG_SP, +) + +WAT = "scripts/repro/rv32_br_table_882.wat" + +CODE, LIN, RET = 0x100000, 0x40000, 0x200000 + +FUNCS = ["dispatch", "dispatch3", "dispatch_default"] + +# Every table entry + first-out-of-range + far-out-of-range + the unsigned +# edge (INT32_MIN and -1 are huge unsigned indices → default, always). +INDICES = [0, 1, 2, 3, 4, 100, 0x7FFFFFFF, 0x80000000, 0xFFFFFFFF] + + +def to_i32(v): + v &= 0xFFFFFFFF + return v - 0x100000000 if v >= 0x80000000 else v + + +def symbols(path): + f = ELFFile(open(path, "rb")) + st = f.get_section_by_name(".symtab") + syms = {} + for s in st.iter_symbols(): + if s.name and s["st_info"]["type"] == "STT_FUNC": + syms[s.name] = s["st_value"] + code = f.get_section_by_name(".text").data() + return syms, code + + +def main(): + synth = os.environ.get("SYNTH", "./target/debug/synth") + if len(sys.argv) > 1: + elf = sys.argv[1] + else: + elf = os.path.join(tempfile.mkdtemp(prefix="brtable882"), "brtable.o") + subprocess.run( + [ + synth, + "compile", + WAT, + "-b", + "riscv", + "--target", + "riscv32imac", + "--relocatable", + "--all-exports", + "-o", + elf, + ], + check=True, + ) + + engine = wasmtime.Engine() + module = wasmtime.Module.from_file(engine, WAT) + + def wt(name, idx): + store = wasmtime.Store(engine) + inst = wasmtime.Instance(store, module, []) + return inst.exports(store)[name](store, to_i32(idx)) & 0xFFFFFFFF + + syms, code = symbols(elf) + + # RED-GUARD (vacuity): every export must be PRESENT — a build that skips + # a function (the pre-fix decline) must fail loudly here, not pass + # because nothing was compared. + missing = [f for f in FUNCS if f not in syms] + if missing: + print(f"exports missing from ELF (function skipped?): {missing}") + print("RV32 br_table #882 ORACLE: FAIL (vacuous — missing exports)") + sys.exit(1) + + def run(name, idx): + mu = Uc(UC_ARCH_RISCV, UC_MODE_RISCV32) + for base, size in [(CODE, 0x20000), (LIN, 0x20000), (RET, 0x1000)]: + mu.mem_map(base, size) + mu.mem_write(CODE, code) + mu.reg_write(UC_RISCV_REG_SP, 0x110000) + mu.reg_write(UC_RISCV_REG_S11, LIN) + mu.reg_write(UC_RISCV_REG_A0, idx & 0xFFFFFFFF) + mu.reg_write(UC_RISCV_REG_RA, RET) + try: + mu.emu_start(CODE + syms[name], RET, count=4000) + except UcError as e: + return None, str(e) + return mu.reg_read(UC_RISCV_REG_A0) & 0xFFFFFFFF, "" + + fails = 0 + for name in FUNCS: + for idx in INDICES: + gt = wt(name, idx) + res, err = run(name, idx) + ok = res == gt + fails += 0 if ok else 1 + if not ok: + shown = f"0x{res:08x}" if res is not None else f"ERR({err})" + print(f"{name}(0x{idx:x}) = {shown} wasmtime=0x{gt:08x} FAIL") + print(f"{len(FUNCS) * len(INDICES)} vectors, {fails} failures") + + print( + "RV32 br_table #882 ORACLE: PASS" + if not fails + else f"RV32 br_table #882 ORACLE: FAIL ({fails})" + ) + sys.exit(1 if fails else 0) + + +if __name__ == "__main__": + main() From 28ef9d07ff2bd6d75e5ae050d9c7a882ef468691 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 29 Jul 2026 18:48:52 +0200 Subject: [PATCH 2/4] style: cargo fmt (#882) Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- crates/synth-cli/src/main.rs | 35 +++++++++++--------- crates/synth-cli/tests/unknown_target_882.rs | 28 +++++++++++++--- 2 files changed, 43 insertions(+), 20 deletions(-) diff --git a/crates/synth-cli/src/main.rs b/crates/synth-cli/src/main.rs index 681c6f2f..0cb1039e 100644 --- a/crates/synth-cli/src/main.rs +++ b/crates/synth-cli/src/main.rs @@ -1031,9 +1031,9 @@ struct ElfFunction { /// backends (w2c2/awsm/wasker) are target-agnostic and return `None`. fn backend_accepted_targets(backend: &str) -> Option<&'static str> { match backend { - "arm" => Some( - "cortex-m3, cortex-m4, cortex-m4f, cortex-m7, cortex-m7dp, cortex-m55, cortex-r5", - ), + "arm" => { + Some("cortex-m3, cortex-m4, cortex-m4f, cortex-m7, cortex-m7dp, cortex-m55, cortex-r5") + } "riscv" => Some("rv32imac, rv32imc, rv32im, rv32i, rv32gc, esp32c3, riscv32"), "aarch64" => Some("cortex-a53"), _ => None, @@ -1072,14 +1072,15 @@ fn resolve_target_spec( let (name, spec) = match target { // from_triple lists the supported target names in its error. Some(name) => { - let spec = TargetSpec::from_triple(name).map_err(|e| { - match backend_accepted_targets(backend) { - Some(list) if backend_explicit => anyhow::anyhow!( - "{e}\ntargets accepted by backend '{backend}': {list}" - ), - _ => anyhow::anyhow!("{e}"), - } - })?; + let spec = + TargetSpec::from_triple(name).map_err(|e| { + match backend_accepted_targets(backend) { + Some(list) if backend_explicit => { + anyhow::anyhow!("{e}\ntargets accepted by backend '{backend}': {list}") + } + _ => anyhow::anyhow!("{e}"), + } + })?; (name, spec) } // No --target given: pick a backend-appropriate default so `-b riscv` @@ -8726,7 +8727,12 @@ mod tests { /// "Using backend: arm" and built Thumb code into a RISC-V ELF container. #[test] fn test_resolve_target_spec_riscv_target_arm_default_backend_errors_882() { - for name in ["riscv32", "rv32imac", "esp32c3", "riscv32imac-unknown-none-elf"] { + for name in [ + "riscv32", + "rv32imac", + "esp32c3", + "riscv32imac-unknown-none-elf", + ] { let err = resolve_target_spec(Some(name), false, "arm", false).unwrap_err(); let msg = err.to_string(); assert!(msg.contains("RISC-V"), "{name}: {msg}"); @@ -8740,10 +8746,7 @@ mod tests { fn test_resolve_target_spec_explicit_backend_mismatch_errors_882() { let err = resolve_target_spec(Some("cortex-m3"), false, "riscv", true).unwrap_err(); let msg = err.to_string(); - assert!( - msg.contains("does not accept --target cortex-m3"), - "{msg}" - ); + assert!(msg.contains("does not accept --target cortex-m3"), "{msg}"); assert!(msg.contains("rv32imac"), "{msg}"); assert!(msg.contains("-b arm"), "{msg}"); diff --git a/crates/synth-cli/tests/unknown_target_882.rs b/crates/synth-cli/tests/unknown_target_882.rs index a22dab7d..71134214 100644 --- a/crates/synth-cli/tests/unknown_target_882.rs +++ b/crates/synth-cli/tests/unknown_target_882.rs @@ -58,7 +58,10 @@ fn unknown_target_hard_errors_with_valid_set() { "must name the bad target:\n{text}" ); for name in ["cortex-m3", "rv32imac", "esp32c3", "cortex-a53"] { - assert!(text.contains(name), "valid set must include {name}:\n{text}"); + assert!( + text.contains(name), + "valid set must include {name}:\n{text}" + ); } // And it must never have reached backend selection. assert!( @@ -100,7 +103,10 @@ fn riscv_target_with_defaulted_arm_backend_hard_errors() { #[test] fn explicit_backend_target_mismatch_hard_errors() { let (ok, text) = run(&["--target", "cortex-m3", "-b", "riscv"]); - assert!(!ok, "cortex-m3 on -b riscv must exit non-zero, got:\n{text}"); + assert!( + !ok, + "cortex-m3 on -b riscv must exit non-zero, got:\n{text}" + ); assert!( text.contains("does not accept --target cortex-m3"), "{text}" @@ -113,8 +119,22 @@ fn explicit_backend_target_mismatch_hard_errors() { fn good_target_backend_pairings_still_compile() { for args in [ &["--target", "cortex-m3", "--all-exports"][..], - &["--target", "rv32imac", "-b", "riscv", "--all-exports", "--relocatable"][..], - &["--target", "esp32c3", "-b", "riscv", "--all-exports", "--relocatable"][..], + &[ + "--target", + "rv32imac", + "-b", + "riscv", + "--all-exports", + "--relocatable", + ][..], + &[ + "--target", + "esp32c3", + "-b", + "riscv", + "--all-exports", + "--relocatable", + ][..], ] { let (ok, text) = run(args); assert!(ok, "good input {args:?} must still compile:\n{text}"); From 0f6b4c7793d446df78e0321a82826d01b1dd833b Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 29 Jul 2026 18:53:29 +0200 Subject: [PATCH 3/4] test(VCR-SEL-005): close the stale br_table divergence + state the sub-shape residual (#882) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit RV32 now lowers br_table (#882), so the op-level known-divergence entry ("RV32 selector has no BrTable arm") is STALE and the parity gate correctly demanded it be closed. Deleted. But br_table is not ONE shape and the RV32 lowering is deliberately PARTIAL, so deleting the whole-op entry alone would erase a real residual from the gate. Measured 2026-07-29 on the real backends: probed shape (<=16 targets, non-value-carrying) arm=ok rv32=ok 17 targets arm=ok rv32=BrTableTooLarge value-carrying (#509) arm=ok rv32=BrTableValueCarrying Both residuals are now asserted BY NAME in br_table_subshape_asymmetry_882, pinning the DECLINE REASON (not a bare is_err(), which a stack-underflow artifact would satisfy vacuously) and failing in BOTH directions like the ledger: if RV32 later lands the jump table or #509 arity threading, the test goes red and the claim must be deleted. Honest read recorded in the test: arm=ok means "the ARM selector returns Ok", NOT "ARM is verified correct on that shape" — ARM shares the #509 limitation on Br/BrIf and performs no value-carrying check. This is a CAPABILITY asymmetry, not a correctness verdict on ARM. No wildcard added, no op moved to StructurallyExcluded, gate not weakened. Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .../tests/cross_backend_op_parity.rs | 142 +++++++++++++++++- 1 file changed, 136 insertions(+), 6 deletions(-) diff --git a/crates/synth-backend-riscv/tests/cross_backend_op_parity.rs b/crates/synth-backend-riscv/tests/cross_backend_op_parity.rs index 4833a31e..3c8e39ec 100644 --- a/crates/synth-backend-riscv/tests/cross_backend_op_parity.rs +++ b/crates/synth-backend-riscv/tests/cross_backend_op_parity.rs @@ -58,7 +58,17 @@ //! RV32 is evidence the i32 Zbb deferral is closable by routing i32 rotate //! through the same shift+or sequence — the concrete next VCR-SEL-005 codegen //! step (byte-changing, gated; not asserted here). +//! +//! SUB-SHAPE NOTE (#882). The ledger is one probe per `WasmOp` variant, so it +//! speaks about an op as a whole. When a lowering lands that is deliberately +//! PARTIAL, closing the whole-op entry must not erase the residual: `br_table` +//! lowers on both backends as of v0.53 (entry deleted), but RV32 still +//! loud-declines >16 targets and value-carrying tables where ARM does not. +//! That residual is asserted by name in `br_table_subshape_asymmetry_882`, +//! which fails in both directions just like the ledger. A future partial +//! lowering should follow the same pattern rather than widen the probe. +use synth_backend_riscv::SelectorError; use synth_backend_riscv::selector::select as riscv_select; use synth_synthesis::{BoundsCheckConfig, InstructionSelector, RuleDatabase, WasmOp, WasmOp::*}; @@ -779,12 +789,15 @@ fn known_divergences() -> &'static [(&'static str, &'static str)] { "RV32 selector has no MemoryFill arm (loud Unsupported); RV32 bulk-memory \ (#374) not yet lowered — deferred, VCR-SEL-005", ), - // ---- structured control-flow multi-target branch (measured 2026-07-17) ---- - ( - "br_table", - "RV32 selector has no BrTable arm (loud Unsupported); the jump-table \ - dispatch is not yet lowered on RV32 — deferred, VCR-SEL-005", - ), + // ---- structured control-flow multi-target branch ---- + // (br_table CLOSED v0.53, #882 — RV32 now lowers it as a compare-and- + // branch chain, so the whole-op divergence is gone and the ledger entry + // was deleted. The op is at parity on the probed shape. The two + // REMAINING sub-shape asymmetries (>16 targets; value-carrying) are NOT + // hidden by that deletion — they are asserted BY NAME in + // `br_table_subshape_asymmetry_882` below, which goes red in both + // directions exactly like this ledger does. Execution differential: + // scripts/repro/rv32_br_table_882_differential.py.) // ---- sub-word i64 memory (measured 2026-07-17; the full-word i64.load / // i64.store DO lower on both — only the sub-word extend/truncate // variants are the gap) ---- @@ -966,3 +979,120 @@ fn ledger_labels_are_live_integer_core_ops() { IntegerCore ops (typo, removed op, or reclassified): {dangling:?}" ); } + +/// SUB-SHAPE ASYMMETRY, STATED NOT HIDDEN (#882, measured 2026-07-29). +/// +/// The op-level ledger is one probe per `WasmOp` variant, so closing +/// `br_table` on RV32 (#882) correctly deletes the whole-op divergence entry — +/// the probed shape now lowers on BOTH backends. But `br_table` is not ONE +/// shape, and RV32's lowering is deliberately partial: it LOUD-DECLINES two +/// sub-shapes that ARM still accepts. Deleting the ledger entry without saying +/// so would let that residual disappear from the gate, which is exactly the +/// dishonesty the op-parity ledger exists to prevent. So the residual is +/// asserted here, by name, with the decline reason: +/// +/// * `>16 targets` → `BrTableTooLarge`. The RV32 lowering is a compare-and- +/// branch CHAIN (no data section, no PC-relative table), so cost is linear +/// in the target count; past `BR_TABLE_MAX_TARGETS` it refuses rather than +/// emit an unbounded chain. The jump-table upgrade is the named follow-up. +/// * `value-carrying` → `BrTableValueCarrying`. The #509 block-arity- +/// threading class: the single-pass RV32 selector cannot reconcile +/// per-path result registers, so it refuses rather than silently +/// miscompile a path-dependent value. +/// +/// HONEST READ OF THE ARM SIDE: `arm_lowers == true` here means only "the ARM +/// selector returns Ok", NOT "ARM is verified correct on that shape" — the ARM +/// selector shares the #509 limitation on plain `Br`/`BrIf` and does not +/// perform the value-carrying check at all. This test therefore records a +/// CAPABILITY asymmetry, not a correctness verdict on ARM. +/// +/// Like the ledger, this fails in BOTH directions: if RV32 later lowers these +/// shapes (jump table / #509 arity threading), this test goes red and whoever +/// closed the gap must delete the corresponding claim — a documented gap must +/// not outlive the gap it documents. +#[test] +fn br_table_subshape_asymmetry_882() { + // The shape the op-level ledger probes: <=16 targets, non-value-carrying, + // in-range depths. AT PARITY — this is why the ledger entry was deleted. + let at_parity = [ + Block, + Block, + LocalGet(0), + BrTable { + targets: vec![0], + default: 1, + }, + End, + End, + ]; + assert!( + arm_lowers(&at_parity, 1) && riscv_lowers(&at_parity, 1), + "the br_table shape the op-parity ledger probes must lower on BOTH \ + backends (#882); if it stopped, re-add the known-divergence entry" + ); + + // Residual 1: past BR_TABLE_MAX_TARGETS (16) the RV32 chain refuses. + let too_large = [ + Block, + Block, + LocalGet(0), + BrTable { + targets: vec![0; 17], + default: 1, + }, + End, + End, + ]; + assert!( + arm_lowers(&too_large, 1), + "ARM is expected to still lower a 17-target br_table; if it now \ + declines too, this is no longer an asymmetry — delete this claim" + ); + // Pin the DECLINE REASON, not merely "Err": a bare `is_err()` would also be + // satisfied by an unrelated stack-underflow artifact in the probe, which + // would make this claim vacuous. + assert!( + matches!( + riscv_select(&too_large, 1), + Err(SelectorError::BrTableTooLarge { + targets: 17, + max: 16 + }) + ), + "RV32 must decline a 17-target br_table AS BrTableTooLarge; got {:?}. \ + If it now lowers, the jump-table upgrade landed — delete this claim; \ + if it errors differently, the probe is no longer measuring this gap.", + riscv_select(&too_large, 1).map(|_| "Ok") + ); + + // Residual 2: value-carrying (#509 block-arity threading). + let value_carrying = [ + Block, + Block, + I32Const(7), + LocalGet(0), + BrTable { + targets: vec![0], + default: 1, + }, + Drop, + End, + Drop, + End, + ]; + assert!( + arm_lowers(&value_carrying, 1), + "ARM is expected to still accept a value-carrying br_table (it does \ + not perform the #509 check); if it now declines, delete this claim" + ); + assert!( + matches!( + riscv_select(&value_carrying, 1), + Err(SelectorError::BrTableValueCarrying { .. }) + ), + "RV32 must decline a value-carrying br_table AS BrTableValueCarrying; \ + got {:?}. If it now lowers, #509 arity threading landed — delete this \ + claim; if it errors differently, the probe stopped measuring the gap.", + riscv_select(&value_carrying, 1).map(|_| "Ok") + ); +} From facc6b40ed1ce4ae44d77641cb80ad83f10a801a Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 29 Jul 2026 19:04:23 +0200 Subject: [PATCH 4/4] fix(cli): correct article in the wrong-ISA target refusal (#882) The refusal read "--target cortex-a53 is a AArch64 target". The family names are a closed set, so pick the article by lookup rather than a vowel heuristic ("an ARM" is right, "an RISC-V" is not). Verified by running the built CLI, not just the unit tests: --target riscv32 -> exit 1, "is a RISC-V target", names `-b riscv` --target cortex-a53 -> exit 1, "is an AArch64 target", names `-b aarch64` --target totally-bogus-cpu -> exit 1, names the FULL valid set --target cortex-m3 -b riscv-> exit 1, lists riscv's accepted targets None print "Using backend: arm"; all 9 good target/backend pairings still compile and select the expected backend. Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- crates/synth-cli/src/main.rs | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/crates/synth-cli/src/main.rs b/crates/synth-cli/src/main.rs index 0cb1039e..172fc902 100644 --- a/crates/synth-cli/src/main.rs +++ b/crates/synth-cli/src/main.rs @@ -1116,8 +1116,14 @@ fn resolve_target_spec( for {name}, use `-b {required_backend}`" ); } + // "an AArch64", "a RISC-V" — the family names are a closed set, so a + // lookup beats a vowel heuristic ("an ARM" is right, "an RISC-V" is not). + let article = match spec.family { + ArchFamily::ArmCortexA => "an", + _ => "a", + }; anyhow::bail!( - "--target {name} is a {family} target, but no backend was selected, so the \ + "--target {name} is {article} {family} target, but no backend was selected, so the \ default 'arm' backend would silently produce a wrong-ISA object — refusing.\n\ pass `-b {required_backend}` for this target, or pick an ARM target: {arm}", arm = backend_accepted_targets("arm").unwrap_or("(none)"),