diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index b699e2e6..a5d11c24 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -217,7 +217,7 @@ jobs: run: | set -euo pipefail python3 scripts/oracle_wiring_check.py --json /tmp/oracle-wiring.json --list \ - --min-emulation-floor 295333 \ + --min-emulation-floor 295421 \ | tee /tmp/oracle-wiring.log python3 - <<'PY' import json, sys @@ -576,9 +576,15 @@ jobs: # CNT/ADDV), and f64<->i64 reinterpret. v0.54 L2 completes the SCALAR float # surface — rounding (FRINT), f32/f64 load/store (bounds-checked), i64-> # float converts, and the DOMAIN-GUARDED trapping i64-target truncations — - # so the decline-matrix probe now asserts the STRUCTURAL declines - # (call_indirect, br_table, param writes, globals, bulk memory, - # value-carrying blocks, SIMD) still LOUD-decline. + # so the decline-matrix probe moved on to the STRUCTURAL declines. v0.54 L3 + # then landed call_indirect + globals and v0.55 L6 (VCR-A64-CF-001) + # `br_table` + value-carrying block/loop/if, so what the probe asserts today + # is the NARROWER residue: param writes in a LEAF function, bulk memory, + # SIMD, a `br_table` past 16 targets or with value-carrying targets, a block + # type with params / multi-value results, and a non-leaf FLOAT param. Each + # entry LEAVES this list the day its lowering lands — asserting a decline + # for a capability that now ships is the same doc-honesty defect as claiming + # one that does not. runs-on: ubuntu-latest steps: - uses: actions/checkout@v7 @@ -689,6 +695,41 @@ jobs: echo "float-completion oracle ran $n checks, $t of them trap cases" [ "$n" -ge 300 ] [ "$t" -ge 40 ] + - name: Run v0.55 L6 br_table + VALUE-CARRYING block/loop/if oracle (VCR-A64-CF-001) + # The two largest entries in the mechanically-derived aarch64 decline + # complement, now lowered. `br_table` is a compare-and-branch CHAIN, so + # a wrong destination is a wrong RESULT: the harness walks the index + # lattice per table (every arm, the index AT the bound, one OVER it, and + # 0xFFFFFFFF — which a SIGNED compare would mis-dispatch, since WASM + # reads the index UNSIGNED), and puts a LOOP HEADER in the same table as + # a forward block end so a wrong branch DIRECTION shows up as a wrong + # trip count. The value-carrying frames are driven down BOTH edges of + # every join, including a frame containing a `bl` — the one soundness + # claim (a call cannot clobber a live reconciliation slot) that nothing + # else executes. + # + # ANTI-VACUITY (#890). `set -euo pipefail`, NOT bare `pipefail`: with + # pipefail ALONE the step's exit status is the LAST command's, so an + # oracle that printed FAIL and exited 1 still went GREEN. The verdict is + # then taken from the script's OWN summary line, and the counts are + # asserted NON-ZERO in both outcome classes — an oracle that stopped + # trapping (or stopped returning values) must go RED. The relocation + # count is asserted too: the harness APPLIES the `R_AARCH64_CALL26` + # relocations itself, and if they vanished the calls would become + # self-branches and the clobber claim would go untested while the gate + # stayed green. + run: | + set -euo pipefail + SYNTH=./target/debug/synth \ + python scripts/oracle_run.py \ + scripts/repro/aarch64_brtable_blockvals_851_differential.py \ + | tee /tmp/a64_brtable.log + grep -q '^RESULT: PASS' /tmp/a64_brtable.log + grep -Eq '^[1-9][0-9]* checks \([1-9][0-9]* trap, [1-9][0-9]* value\) across [1-9][0-9]* exported' /tmp/a64_brtable.log + grep -Eq '\[[1-9][0-9]* direct-call relocations applied\]' /tmp/a64_brtable.log + n=$(sed -n 's/^\([0-9]*\) checks .*/\1/p' /tmp/a64_brtable.log) + echo "br_table/value-carrying oracle ran $n checks" + [ "$n" -ge 60 ] - name: Run decline-matrix honesty oracle run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/aarch64_m2_decline_538.py # #910: close the job with what it EXECUTED. Asserts every oracle diff --git a/CHANGELOG.md b/CHANGELOG.md index f02a2544..c8968bf2 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -55,12 +55,12 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 not "checks", because naming a measurement after something it does not measure is the defect this lane exists to remove. -- **The differential population is reported, and ratcheted.** **135 oracles - assert 295,333 emulator entries per CI run**; 7 assert a printed count, 9 +- **The differential population is reported, and ratcheted.** **136 oracles + assert 295,421 emulator entries per CI run**; 7 assert a printed count, 9 assert compilations, 1 can bind to nothing. Reported **per mode and never summed across modes** — three different units, and one impressive combined figure is exactly the instrument defect being fixed. - `oracle_wiring_check.py --min-emulation-floor 295333` enforces the total in + `oracle_wiring_check.py --min-emulation-floor 295421` enforces the total in the already-required `Claim Check` job (a brand-new job is not a required context on `main` and could sit red for weeks — the #890 failure), sharing the driver's header parser by import rather than re-implementing the grammar. @@ -157,6 +157,29 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ### Added +- **aarch64 `br_table` + value-carrying `block`/`loop`/`if` (VCR-A64-CF-001, + #851).** The two largest entries left in the VCR-SEL-005 third-backend + complement were structural, not arithmetic — and both made whole functions + skip on `-b aarch64`. `br_table` now lowers as a compare-and-branch chain + (`cbz` for entry 0, `cmp`+`b.eq` per further entry, then the default `b`), + deliberately the same construction #882 chose for RV32 so the two backends + stay reviewable against each other; the index is compared in the W view, so + the UNSIGNED index rule holds exactly and every out-of-range index — + including the "negative" i32s that denote huge unsigned values — reaches the + DEFAULT. One table may MIX a backward loop header with forward block ends. + A value-carrying frame reserves a reconciliation register that every incoming + edge deposits into (`br`/`br_if` at the branch, the then-arm at `else`, the + fall-through at `end`), so the frame's result sits in ONE register on every + path — i32/i64 through `mov x`, f32/f64 through `fmov d`. The aarch64 + selector goes **184 → 185 ops**. +- **The soundness-critical asymmetry is by construction, not by test.** A `br` + to a LOOP label targets the header and carries the loop's PARAMETERS, not its + results, so a `loop (result T)` back-edge must reconcile NOTHING — the frame + carries `label_arity` separately from `result_arity` and branch + reconciliation is driven off the former. The natural wrong implementation + (reconcile whenever the frame has a result) stamps a garbage value into the + result register on every iteration. + - **VCR-DEC-001 increment 4 (VCR-REACH-001, #242) — the graph-colouring allocator models the i64 register-PAIR ops.** Increments 2 (joins) and 3 (calls) both returned *do not flip*, and both for the same reason: the @@ -295,6 +318,22 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ### Changed +- **Three named residuals replace two blanket declines.** `br_table` past 16 + targets (`BR_TABLE_MAX_TARGETS`, the same threshold RV32 uses — the chain is + O(n) and PC-relative jump-table dispatch is a follow-up), a `br_table` whose + targets are value-carrying (the flat chain has no per-path edge to deposit a + result on), and a block type with PARAMETERS or MULTI-VALUE results (the slot + is one register). Each loud-declines with a machine reason and is pinned BY + NAME in `br_table_subshape_asymmetry_882`, which fails in both directions — + partial coverage with named gaps rather than a claim that cannot be backed. + The `br_table` whole-op entry is deleted from `aarch64_known_divergences()`; + the parity gate's stale-entry check is what forced the deletion. +- **The #554 float-honesty fixture moves again.** It targeted a value-carrying + f32-result `block`; that shape now lowers, so the fixture re-points at a + float construct that genuinely still declines — a NON-LEAF function reading + an f32 parameter (float params live in `v0..v7`, which a `bl` clobbers, and + the encoder has no FP store to home them with). + - **VCR-RA-003's join-availability half now covers the i64-pair family — on the DEFAULT build.** It built its CFG from `reg_effect` alone, so every i64-containing function returned `NotAttempted`: the interesting half of the @@ -305,6 +344,30 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 and self-contained paths, and all 633 pre-existing relocatable functions plus all 1059 self-contained ones byte-identical to v0.54. +### Verified + +- `scripts/repro/aarch64_brtable_blockvals_851_differential.py` (CI-wired): 88 + checks over 19 exported functions against wasmtime, under unicorn AND + natively on an arm64 host. Per table it walks the index lattice — every arm, + the index exactly AT the bound, one OVER it, and `0xFFFFFFFF` (the case a + SIGNED compare would mis-dispatch) — plus a table at exactly 16 targets, a + `br_table` arm falling into a trap, and both join edges of every + value-carrying frame including a value-carrying loop's back-edge. Two cases + put a `bl` INSIDE a value-carrying frame — the one soundness claim (a call + cannot clobber a live reconciliation slot) that nothing else executes; the + harness applies the `R_AARCH64_CALL26` relocations itself, so the emitted + relocation is part of what is checked rather than a hang. + NON-VACUITY was demonstrated by MUTATION, not asserted: taking the join + position before the fall-through's reconciliation move reddens 16 checks, an + off-by-one in the chain constants reddens 22, and using `result_arity` where + `label_arity` belongs (the loop back-edge bug) makes two functions fail to + compile at all. +- Void control flow is **byte-identical**: 13 of the 14 aarch64 repro fixtures + compile to the same object as v0.54.0, and the one that differs + (`aarch64_f32_unsupported_554`) differs exactly because its declined function + now lowers. A void frame reserves no register and emits no reconciliation + move, so the property holds by construction. + ### Notes - `SYNTH_GRAPH_ALLOC` remains **off by default**; flag-off output is diff --git a/artifacts/status.json b/artifacts/status.json index 2ea55f37..3639f3b4 100644 --- a/artifacts/status.json +++ b/artifacts/status.json @@ -1,5 +1,5 @@ { - "aarch64_selector_ops": 184, + "aarch64_selector_ops": 185, "arm_refinement_assumed_connection": 5, "arm_semantics_axioms": 72, "backends": [ diff --git a/artifacts/sw-verification.yaml b/artifacts/sw-verification.yaml index 0a3b41e7..8187425f 100644 --- a/artifacts/sw-verification.yaml +++ b/artifacts/sw-verification.yaml @@ -669,3 +669,49 @@ artifacts: DEFAULT build with 0 hard errors across the corpus (thumb2 AND the cortex-r5 A32 path, whose expansions differ) + - id: SWVER-024 + type: sw-verification + title: AArch64 br_table + value-carrying block/loop/if (#851 — VCR-A64-CF-001) + description: > + Verifies VCR-A64-CF-001 in both directions. CAPABILITY: an execution + differential compiles a WAT carrying the new shapes with `-b aarch64`, + reads the emitted `.text` out of the object's symtab, and runs every + exported function under unicorn (UC_ARCH_ARM64) — and NATIVELY in a forked + child on an arm64 host — against wasmtime as the reference. The cases are + chosen so a wrong branch destination changes the RESULT rather than + merely the schedule: br_table default arm, index exactly AT the table + bound, index OVER the bound, index 0xFFFFFFFF (the unsigned-index rule), a + table whose targets mix a backward loop header with forward block ends, + and a value-carrying `loop` back-edge (the case where reconciling on the + back-edge — the natural wrong implementation — silently returns a garbage + result). A guarded `unreachable` gives a TRAP case so the harness cannot + collapse to "every case returns a value", and non-vacuity is asserted on + both the trap and the value counts. + DECLINE-HONESTY: the residuals (>16 targets, value-carrying br_table + targets, block/loop params, multi-value results) are asserted by name at + selector level in `br_table_subshape_asymmetry_882`, which fails in BOTH + directions — a residual that closes must delete its assertion, and a + capability that regresses reddens the same test. The whole-op ledger entry + for `br_table` is deleted from `aarch64_known_divergences()`; the parity + gate's stale-entry check is what forces that deletion. + FROZEN-SAFETY: a void frame reserves no register and emits no + reconciliation move, so the pre-existing aarch64 control-flow oracles must + stay green with unchanged output, and the ARM/RV32 frozen goldens (10/10) + are untouched. + status: implemented + tags: [aarch64, control-flow, br-table, differential, vcr-sel, issue-851] + links: + - type: verifies + target: VCR-A64-CF-001 + fields: + method: automated-test + steps: + run: "cargo test -p synth-backend-aarch64 && cargo test -p synth-backend-riscv --test cross_backend_op_parity" + coverage: > + scripts/repro/aarch64_brtable_blockvals_851_differential.py (wasmtime + vs unicorn/native execution over the br_table index lattice + the + value-carrying block/loop/if shapes, CI-wired) + + crates/synth-backend-riscv/tests/cross_backend_op_parity.rs + (br_table_subshape_asymmetry_882 — the three aarch64 residuals pinned + by name) + crates/synth-backend-aarch64/src/selector.rs unit tests + + scripts/repro/aarch64_m2_decline_538.py (decline-matrix honesty) diff --git a/artifacts/verified-codegen-roadmap.yaml b/artifacts/verified-codegen-roadmap.yaml index 8c417990..2da81efe 100644 --- a/artifacts/verified-codegen-roadmap.yaml +++ b/artifacts/verified-codegen-roadmap.yaml @@ -658,6 +658,102 @@ artifacts: line is deleted, so a parity claim cannot outlive the gap it documents. CI-wired as vcr-sel-005-cross-backend-op-parity-gate. + - id: VCR-A64-CF-001 + type: sw-req + title: AArch64 multi-way dispatch (br_table) + value-carrying structured control flow + description: > + The VCR-SEL-005 third-backend enumeration (#851) is a MECHANICALLY DERIVED + complement: whatever the aarch64 selector does not lower is named, by op, + in `aarch64_known_divergences()` and in the `a64_extended_surface` gap + column. After v0.53/v0.54 closed the integer core, the floats, globals and + `call_indirect`, the TWO LARGEST remaining entries in that complement were + structural, not arithmetic: + + (a) `br_table` — the multi-way branch. Declined outright ("aarch64 + selector has no BrTable arm"), so any wasm switch/jump-table shape + skipped the whole function on `-b aarch64`. + (b) VALUE-CARRYING `block`/`loop`/`if` — a typed (`(result T)`) frame. + Declined because the straight-line value-stack model had no + RESULT-REGISTER RECONCILIATION: two paths reaching one `end` leave + the result in path-dependent temps. This is the #509 block-arity + class, and it is what makes `(block (result i32) … br_if …)` — the + shape every non-trivial optimizing producer emits — uncompilable. + + THIS REQUIREMENT closes both, with the residual named rather than widened: + + br_table lowers as a COMPARE-AND-BRANCH CHAIN, deliberately the same + construction #882 chose for RV32 so the two backends stay reviewable + against each other: `cbz w_idx, L0` for entry 0, then `cmp w_idx, #i` + + `b.eq L_i` per further entry, then an unconditional `b L_default`. The + index is compared in the W view, so the i32 UNSIGNED semantics hold + exactly: only 0..len-1 match, and every other index — including the + "negative" i32s that are huge unsigned values — falls to the default + label, per WASM core semantics. Targets may mix FORWARD (block/if end, + patched at `End`) and BACKWARD (loop header, resolved eagerly to a + negative offset) destinations in one table, since the chain dispatches on + the TARGET FRAME's kind exactly like `br`/`br_if` already do. + + Value-carrying frames get a RESERVED RECONCILIATION REGISTER PAIR (one GP, + one FP — the file is not known from the arity side-table, which carries + counts only) allocated at frame entry and withheld from the temp + allocator for the frame's whole extent. Every path that reaches the + frame's label MOVES its result into that register before transferring: + `br` and `br_if` at the branch, the then-arm at `else`, the fall-through + at `end`. At `end` the frame pushes the reserved register as the frame's + value, so the result is in ONE register on every path by construction — + the reconciliation the old decline said was missing. + + SOUNDNESS-CRITICAL DISTINCTION (named because getting it wrong is a silent + miscompile, not a decline): a `br` to a `loop` targets the loop HEADER and + carries the loop's PARAMETER count, NOT its result count. So a + `loop (result i32)` — arity (0,1) — must NOT reconcile on its back-edge; + its reserved register is written only by the fall-through `end`. The frame + therefore carries `label_arity` (= params for Loop, results for Block/If) + SEPARATELY from `result_arity`, and branch reconciliation is driven off + `label_arity`. Reconciling the back-edge would deposit a garbage value + into the result register on every iteration. + + HONEST RESIDUALS (loud declines with machine reasons, each pinned by name + in `br_table_subshape_asymmetry_882` so the gap claim cannot outlive the + gap, and each MOVED not deleted): + * `br_table` past BR_TABLE_MAX_TARGETS (16) — the chain is O(n); a real + jump table (PC-relative dispatch + bounds check) is the follow-up. + Same threshold and same decline as RV32 #882. + * `br_table` with VALUE-CARRYING targets — a per-path result move would + have to sit on the taken edge of each compare, which the flat chain + has no room for. Conservatively refused when any targeted frame + (default included) has non-zero label arity or was entered at a + different height than the post-pop height. + * block/loop/if with PARAMETERS, or with MORE THAN ONE result + (multi-value) — the reserved pair is a single slot. + Frozen-safe by construction: a VOID frame reserves nothing and emits no + reconciliation move, so all pre-existing aarch64 control-flow output is + byte-identical. + status: implemented + tags: [codegen, selector, aarch64, control-flow, parity, track-a, issue-851] + links: + - type: derives-from + target: VCR-001 + - type: traces-to + target: VCR-SEL-005 + fields: + req-type: functional + priority: should + verification-criteria: > + (1) The aarch64 leg of the op-parity gate no longer ledgers `br_table` + as an ARM-lowers/aarch64-declines divergence, and the stale-entry check + proves it (the gate reddens if the line survives the lowering). + (2) `br_table_subshape_asymmetry_882` asserts the THREE aarch64 + residuals by name in both directions: a 17-target table declines, a + value-carrying table declines, and the probed in-scope shape LOWERS. + (3) Execution-differential vs wasmtime under unicorn (and natively on an + arm64 host): br_table default arm, index at the table bound, index over + the bound, index 0xFFFFFFFF, a table mixing loop and block targets, and + a value-carrying loop's back-edge — plus a trap case, so the gate cannot + collapse to "everything returns a value". + (4) The pre-existing void control-flow differentials stay green with + UNCHANGED output (no spurious reconciliation move on a void frame). + # --------------------------------------------------------------------------- # Track B — authoritative semantics (independent; parallel with Track A) # --------------------------------------------------------------------------- diff --git a/claims.yaml b/claims.yaml index a2adfd54..a8e2efae 100644 --- a/claims.yaml +++ b/claims.yaml @@ -1076,7 +1076,7 @@ claims: # --------------------------------------------------------------------------- - id: SYNTH-ORACLE-CHECK-FLOORS-910 doc: scripts/repro/ORACLE_WIRING.md - text: "**295,333 emulator entries**" + text: "**295,421 emulator entries**" evidence: - kind: file-exists path: scripts/oracle_run.py @@ -1089,13 +1089,13 @@ claims: - kind: count-min # the EXECUTION population, per script pattern: '^# ci-checks: emulations >= ' glob: ['scripts/repro/*.py', 'scripts/repro/*.sh'] - min: 135 + min: 136 - kind: count-max # the "nothing can be bound" hatch pattern: '^# ci-checks: none' glob: ['scripts/repro/*.py', 'scripts/repro/*.sh'] max: 1 - kind: verbatim # the doc carries the per-mode split - text: "**135 oracles**" + text: "**136 oracles**" - kind: verbatim text: "Reported per mode and never summed across modes." - kind: verbatim # the itemized weak-floor list stays @@ -1116,14 +1116,14 @@ claims: # --------------------------------------------------------------------------- - id: SYNTH-ORACLE-CHECK-FLOORS-910-MATRIX doc: scripts/templates/feature_matrix.md.tmpl - text: "**135 oracles assert 295,333 emulator" + text: "**136 oracles assert 295,421 emulator" evidence: - kind: file-exists path: scripts/oracle_run.py - kind: count-min # same population the other two pin pattern: '^# ci-checks: emulations >= ' glob: ['scripts/repro/*.py', 'scripts/repro/*.sh'] - min: 135 + min: 136 # --------------------------------------------------------------------------- # #910 — the CI side of the same claim, pinned so the doc's number and the @@ -1133,7 +1133,7 @@ claims: # --------------------------------------------------------------------------- - id: SYNTH-ORACLE-CHECK-FLOORS-910-CI doc: .github/workflows/ci.yml - text: "--min-emulation-floor 295333" + text: "--min-emulation-floor 295421" evidence: - kind: count-min # oracle steps routed through the driver pattern: 'oracle_run\.py scripts/repro/' diff --git a/crates/synth-backend-aarch64/src/backend.rs b/crates/synth-backend-aarch64/src/backend.rs index e71b91f9..18de0ce6 100644 --- a/crates/synth-backend-aarch64/src/backend.rs +++ b/crates/synth-backend-aarch64/src/backend.rs @@ -55,9 +55,12 @@ impl AArch64Backend { }; // m3: thread the per-param float masks so float params resolve to their // AAPCS64 V registers (an independent counter from the GP arg registers). - // #538 cf: also thread the decoder's blocktype-arity side-table so the - // void-block control-flow lowering can gate on `(0,0)` and loud-decline - // value-carrying (typed) blocks. + // #538 cf: also thread the decoder's blocktype-arity side-table, which + // is the ONLY channel carrying a frame's block type. VCR-A64-CF-001 + // reads it to reserve a reconciliation register for a value-carrying + // `(0,1)` frame — and to distinguish a loop's PARAMETER count (what a + // back-edge carries) from its RESULT count (what its `end` produces). + // Block params and multi-value results still loud-decline from it. // #851: thread the call metadata so direct `call` lowers to `bl func_N` // + an R_AARCH64_CALL26 relocation (call-free bodies are unaffected). // #865: resolve `--safety-bounds` into the selector's explicit diff --git a/crates/synth-backend-aarch64/src/selector.rs b/crates/synth-backend-aarch64/src/selector.rs index a6ec5543..55d54969 100644 --- a/crates/synth-backend-aarch64/src/selector.rs +++ b/crates/synth-backend-aarch64/src/selector.rs @@ -40,9 +40,7 @@ //! float-result callees (returned in v0/d0, not x0), a caller reading its own //! params across a call (param-homing is a later increment), and WRITING a //! parameter (`local.set`/`tee` on a param index). -//! - `br_table`, value-carrying `block`/`loop`/`if`, register spilling, -//! `global.get`/`global.set` (no globals substrate), and bulk memory -//! (`memory.copy`/`memory.fill`). +//! - register spilling and bulk memory (`memory.copy`/`memory.fill`). //! - Float rounding (`ceil`/`floor`/`trunc`/`nearest`), f32/f64 linear-memory //! load/store, i64→float converts, and the TRAPPING i64-target truncations //! (the saturating forms do lower). @@ -71,6 +69,30 @@ //! f32 param (delivered in `s0..` under AAPCS64, a counter INDEPENDENT of the //! GP arg registers) is never confused with a GP operand. //! +//! **VCR-A64-CF-001 (v0.55) — `br_table` + VALUE-CARRYING control flow.** The +//! two largest entries in the mechanically-derived decline complement: +//! +//! - `br_table` lowers as a COMPARE-AND-BRANCH CHAIN (`cbz` for entry 0, then +//! `cmp`+`b.eq` per further entry, then an unconditional `b` to the default), +//! deliberately the same construction #882 chose for RV32. The index is +//! compared in the W view, so the UNSIGNED index semantics hold exactly: +//! only `0..len-1` match and every other index — including the "negative" +//! i32s that denote huge unsigned values — reaches the DEFAULT. One table may +//! MIX a backward loop header with forward block ends. +//! - A VALUE-CARRYING `block`/`loop`/`if` reserves a reconciliation register +//! pair (one GP, one FP — the arity side-table carries counts only, so the +//! result's register FILE is not known at frame entry) that is withheld from +//! the temp allocator for the frame's whole extent. Every edge into the +//! frame's join deposits there, so the result is in ONE register on every +//! path. See [`reconcile_into`] for why no clobber window exists. +//! +//! SOUNDNESS-CRITICAL: a `br` to a LOOP label targets the loop HEADER and +//! carries the loop's PARAMETERS, not its results, so a `loop (result T)` +//! back-edge reconciles NOTHING (`Frame::label_arity` vs `Frame::result_arity`). +//! Still declined by name: a `br_table` past [`BR_TABLE_MAX_TARGETS`], a +//! `br_table` with value-carrying targets, and a block type with PARAMETERS or +//! MULTI-VALUE results. +//! //! **Milestone 4 converts the #709-class declines into SOUND capabilities:** //! //! - The trapping float→int truncations (`i32.trunc_f32_{s,u}`, @@ -106,6 +128,14 @@ const TEMPS: [Reg; 7] = [9, 10, 11, 12, 13, 14, 15]; /// carry incoming float params, `v8..v15` are callee-saved). 8 scratch slots. const FTEMPS: [FReg; 8] = [16, 17, 18, 19, 20, 21, 22, 23]; +/// VCR-A64-CF-001 — the largest `br_table` the compare-and-branch-chain +/// lowering accepts. Each entry past the first costs 2 instructions +/// (`cmp` + `b.eq`), so 16 targets is a ≤32-instruction dispatch; past that a +/// real PC-relative jump table wins and the selector LOUD-DECLINES instead of +/// emitting an unbounded chain. Same threshold as the RV32 lowering (#882), +/// deliberately — the two backends' `br_table` frontiers stay comparable. +pub const BR_TABLE_MAX_TARGETS: usize = 16; + /// #851 — the WASM linear-memory base register. A memory-using function expects /// `x28 = __linear_memory_base` on entry — the same dedicated-base convention /// the ARM (R11) and RV32 (s11) backends use, chosen OUTSIDE the temp pool @@ -532,6 +562,15 @@ pub fn select_typed_cf_calls( /// at `else` (to the else arm) or at `end` (past the then arm). If { else_fixup: Option }, } + /// VCR-A64-CF-001 — the reconciliation registers a VALUE-CARRYING frame + /// reserves. Both files are reserved because the blocktype-arity side-table + /// carries counts only; `file` records which one the first reconciliation + /// actually used, so `End` pushes the right one. + struct Slot { + gp: Reg, + fp: FReg, + file: Option, + } struct Frame { kind: Kind, /// Word positions in `words` of FORWARD branches targeting this frame's @@ -540,6 +579,20 @@ pub fn select_typed_cf_calls( pending: Vec, /// Value-stack height on entry — a void frame must restore it at `End`. stack_entry: usize, + /// How many values a `br`/`br_if`/`br_table` to THIS frame's LABEL + /// carries. For a Block/If the label is its END, so this is the frame's + /// RESULT count; for a Loop the label is its HEADER, so this is the + /// frame's PARAMETER count. Getting that distinction wrong is a SILENT + /// MISCOMPILE, not a decline: reconciling on a `loop (result i32)` + /// back-edge would overwrite the result register with a garbage value + /// on every iteration. Only 0 or 1 (params and multi-value decline). + label_arity: u8, + /// How many values the frame's FALL-THROUGH `End` leaves on the stack + /// (the frame's result count). Only 0 or 1. + result_arity: u8, + /// Reserved reconciliation registers — `Some` iff the frame is + /// value-carrying (`result_arity == 1`). + slot: Option, } let mut ctrl: Vec = Vec::new(); // Ordinal counter over Block/Loop/If in op order — the key into @@ -555,23 +608,177 @@ pub fn select_typed_cf_calls( // fall-through). `br_if` is conditional, so its fall-through stays reachable. let mut reachable = true; - // Pick a GP temp not holding a live GP value-stack entry. + // VCR-A64-CF-001 (#851/#509) — RESERVED reconciliation registers. + // + // A value-carrying frame (`block (result T)`, `if (result T)`, + // `loop (result T)`) needs ONE register that holds the frame's value on + // EVERY path reaching its `end`. That register must be withheld from the + // temp allocator for the frame's whole extent, otherwise code between a + // `br` that deposited into it and the `end` that reads it could allocate + // the same temp and clobber a live result. + // + // The reservation is a BITMASK (bit r = register r reserved), not a value- + // stack entry: the value stack is consumed WHOLESALE by the `call` / + // `call_indirect` argument marshalling (`stack.iter().enumerate()` + + // `stack.clear()`), so a placeholder pushed there would be marshalled as an + // argument and then erased. A separate mask cannot be reached by any of + // those whole-stack consumers, and `epilogue(stack.last())` can never + // return a reservation. + // + // Both files are reserved per frame, because the blocktype arity side-table + // carries COUNTS ONLY — whether the result is i32/i64 (GP) or f32/f64 (FP) + // is not known until the first value is reconciled. + let reserved_gp = std::cell::Cell::::new(0); + let reserved_fp = std::cell::Cell::::new(0); + let gp_free = |t: Reg, stack: &[Val]| { + reserved_gp.get() & (1u32 << t) == 0 + && !stack.iter().any(|v| v.file == File::Gp && v.reg == t) + }; + let fp_free = |t: FReg, stack: &[Val]| { + reserved_fp.get() & (1u32 << t) == 0 + && !stack.iter().any(|v| v.file == File::Fp && v.reg == t) + }; + + // Pick a GP temp holding neither a live GP value-stack entry nor an open + // frame's reserved result register. let alloc_temp = |stack: &[Val]| -> Result { TEMPS .iter() .copied() - .find(|t| !stack.iter().any(|v| v.file == File::Gp && v.reg == *t)) + .find(|t| gp_free(*t, stack)) .ok_or_else(|| SelectError("value-stack too deep (GP temp regs exhausted)".into())) }; - // Pick an FP temp not holding a live FP value-stack entry. + // Pick an FP temp holding neither a live FP value-stack entry nor an open + // frame's reserved result register. let alloc_ftemp = |stack: &[Val]| -> Result { FTEMPS .iter() .copied() - .find(|t| !stack.iter().any(|v| v.file == File::Fp && v.reg == *t)) + .find(|t| fp_free(*t, stack)) .ok_or_else(|| SelectError("value-stack too deep (FP temp regs exhausted)".into())) }; + // VCR-A64-CF-001 — validate a `block`/`loop`/`if` blocktype arity and, when + // it is VALUE-CARRYING, reserve its reconciliation register pair. + // + // Returns `(label_arity, result_arity, slot)`. `is_loop` picks the LABEL + // arity: a `br` to a Loop targets its HEADER and carries the loop's + // PARAMETERS, while a `br` to a Block/If targets its END and carries the + // frame's RESULTS. A `loop (result i32)` therefore has label arity 0 — + // its back-edge must reconcile NOTHING, or every iteration would stamp a + // garbage value into the result register. + let open_slot = |what: &str, + ord: usize, + arity: (u8, u8), + is_loop: bool, + stack: &[Val]| + -> Result<(u8, u8, Option), SelectError> { + let (params, results) = arity; + if params != 0 { + return Err(SelectError(format!( + "{what} #{ord} has type {arity:?} — a PARAMETER-taking block \ + type (multi-value) is not lowered on aarch64: the \ + reconciliation slot is ONE register, so block params would \ + need a per-path multi-register shuffle; loud-declining \ + (VCR-A64-CF-001)" + ))); + } + if results > 1 { + return Err(SelectError(format!( + "{what} #{ord} has type {arity:?} — a MULTI-VALUE result block \ + type is not lowered on aarch64 (the reconciliation slot is ONE \ + register); loud-declining (VCR-A64-CF-001)" + ))); + } + let slot = if results == 1 { + let gp = alloc_temp(stack)?; + reserved_gp.set(reserved_gp.get() | 1u32 << gp); + let fp = match alloc_ftemp(stack) { + Ok(f) => f, + Err(e) => { + // Roll the GP reservation back so a decline leaves no + // stranded register behind. + reserved_gp.set(reserved_gp.get() & !(1u32 << gp)); + return Err(e); + } + }; + reserved_fp.set(reserved_fp.get() | 1u32 << fp); + Some(Slot { gp, fp, file: None }) + } else { + None + }; + Ok((if is_loop { params } else { results }, results, slot)) + }; + + /// VCR-A64-CF-001 — move `v` into a value-carrying frame's reconciliation + /// register, recording which register FILE the frame's result lives in. + /// + /// The 64-bit forms are deliberate and match [`epilogue`]: `mov x` carries + /// an i32 intact (w-form producers zero the upper half) and `fmov d` + /// carries an f32's low 32 bits intact. + /// + /// SOUNDNESS NOTE — why no clobber window exists. `v.reg` can never BE the + /// slot register (the slot is reserved, so the temp allocator cannot have + /// handed it out to a live value), so this move never destroys a live + /// operand. And every call site writes the slot IMMEDIATELY before a + /// transfer to the frame's join point: `br`/`br_if` before the branch, + /// `else` before the `b end`, `end` before the push. So on the path that + /// WRITES the slot, the very next thing executed is the join — nothing + /// (not even a `bl`, which clobbers the caller-saved x9..x15 temp pool) + /// runs in between. On any other path the written value is dead and is + /// re-written before that path reaches the join. + fn reconcile_into(words: &mut Vec, slot: &mut Slot, v: Val) { + match v.file { + File::Gp => { + if v.reg != slot.gp { + words.push(enc::mov_reg64(slot.gp, v.reg)); + } + } + File::Fp => { + if v.reg != slot.fp { + words.push(enc::fmov_d(slot.fp, v.reg)); + } + } + } + slot.file = Some(v.file); + } + + /// VCR-A64-CF-001 — reconcile a `br`/`br_if` that targets `ctrl[target]`. + /// + /// A no-op unless the target's LABEL arity is 1 (results for a Block/If, + /// PARAMS for a Loop — see [`Frame::label_arity`]). The value is PEEKED, + /// never popped: `br_if`'s not-taken path keeps it on the operand stack, + /// and `br`'s fall-through is unreachable so the stale entry is truncated + /// away at the frame's `End`. + fn reconcile_branch( + words: &mut Vec, + ctrl: &mut [Frame], + stack: &[Val], + target: usize, + ctx: &str, + ) -> Result<(), SelectError> { + if ctrl[target].label_arity == 0 { + return Ok(()); + } + if stack.len() <= ctrl[target].stack_entry { + return Err(SelectError(format!( + "{ctx}: branch to a value-carrying label with no result on the \ + value stack (height {}, target frame entry height {})", + stack.len(), + ctrl[target].stack_entry + ))); + } + let v = stack[stack.len() - 1]; + let slot = ctrl[target].slot.as_mut().ok_or_else(|| { + SelectError(format!( + "{ctx}: value-carrying label has no reconciliation slot \ + (internal invariant)" + )) + })?; + reconcile_into(words, slot, v); + Ok(()) + } + // Pop a GP operand, erroring if the top value is actually an FP value (a // type confusion that would otherwise silently read the wrong file). fn pop_gp(stack: &mut Vec, ctx: &str) -> Result { @@ -805,10 +1012,7 @@ pub fn select_typed_cf_calls( let b = pop_fp(stack, "copysign")?; // z2: sign source let a = pop_fp(stack, "copysign")?; // z1: magnitude // Three DISTINCT free GP temps (a-bits, b-bits, mask). - let mut free = TEMPS - .iter() - .copied() - .filter(|t| !stack.iter().any(|v| v.file == File::Gp && v.reg == *t)); + let mut free = TEMPS.iter().copied().filter(|t| gp_free(*t, stack)); let (Some(ta), Some(tb), Some(tm)) = (free.next(), free.next(), free.next()) else { return Err(SelectError( "value-stack too deep (copysign needs 3 GP temps)".into(), @@ -893,10 +1097,7 @@ pub fn select_typed_cf_calls( stack.push(Val::gp(b)); // Need up to three DISTINCT scratch regs beyond a/b: quotient, and (for // the signed-div overflow guard) two const-materialization temps. - let mut free = TEMPS - .iter() - .copied() - .filter(|t| !stack.iter().any(|v| v.file == File::Gp && v.reg == *t)); + let mut free = TEMPS.iter().copied().filter(|t| gp_free(*t, stack)); let (Some(q), Some(s0), Some(s1)) = (free.next(), free.next(), free.next()) else { stack.pop(); stack.pop(); @@ -1008,7 +1209,7 @@ pub fn select_typed_cf_calls( let vtmp = FTEMPS .iter() .copied() - .find(|t| !stack.iter().any(|v| v.file == File::Fp && v.reg == *t)) + .find(|t| fp_free(*t, stack)) .ok_or_else(|| SelectError("value-stack too deep (popcnt needs an FP temp)".into()))?; if is64 { words.push(enc::fmov_d_from_x(vtmp, a)); @@ -1360,29 +1561,29 @@ pub fn select_typed_cf_calls( reachable = false; } - // --- control flow (#538 cf increment): VOID-result forward blocks --- + // --- control flow (#538 cf increment; VCR-A64-CF-001 value-carrying) --- // - // `block` opens a new control frame. Only a `(0,0)` (void, no params, - // no result) block is accepted — a typed block would leave a value on - // the stack whose result register the branch would have to reconcile, - // which this straight-line model does not do. The arity comes from the - // decoder's ordinal side-table (`unreachable`-polymorphic fall-through - // makes a stack-height proxy UNSOUND — the arity table is the signal). + // `block` opens a new control frame. Since VCR-A64-CF-001 a + // VALUE-CARRYING `(0,1)` block is accepted as well as the void + // `(0,0)` one: it reserves a reconciliation register that every + // path deposits its result into (see [`reconcile_into`]). Block + // PARAMETERS and MULTI-VALUE results still loud-decline by name. + // The arity comes from the decoder's ordinal side-table + // (`unreachable`-polymorphic fall-through makes a stack-height + // proxy UNSOUND — the arity table is the signal). WasmOp::Block => { let ord = ctrl_ord; ctrl_ord += 1; let arity = block_arity.get(ord).copied().unwrap_or((0, 0)); - if arity != (0, 0) { - return Err(SelectError(format!( - "block #{ord} has type {arity:?} — only void (0,0) blocks \ - are supported (value-carrying blocks need result-register \ - reconciliation across the branch); loud-declining" - ))); - } + let (label_arity, result_arity, slot) = + open_slot("block", ord, arity, false, &stack)?; ctrl.push(Frame { kind: Kind::Block, pending: Vec::new(), stack_entry: stack.len(), + label_arity, + result_arity, + slot, }); } // `br N` — unconditional branch to the END of the block N levels out. @@ -1401,6 +1602,11 @@ pub fn select_typed_cf_calls( ))); } let target = ctrl.len() - 1 - d; + // VCR-A64-CF-001 — a branch to a VALUE-CARRYING label hands the + // label its result: move the top-of-stack into the target + // frame's reserved register FIRST, so the join reads one + // register on every incoming edge. + reconcile_branch(&mut words, &mut ctrl, &stack, target, "br")?; let pos = words.len(); if let Kind::Loop { entry } = ctrl[target].kind { // BACKWARD branch to the loop header — resolve immediately. @@ -1427,6 +1633,10 @@ pub fn select_typed_cf_calls( } let cond = pop_gp(&mut stack, "br_if")?; let target = ctrl.len() - 1 - d; + // VCR-A64-CF-001 — the condition sat ABOVE the branch's result, + // so reconcile only after popping it. PEEK, don't pop: the + // not-taken path still owns the value. + reconcile_branch(&mut words, &mut ctrl, &stack, target, "br_if")?; let pos = words.len(); if let Kind::Loop { entry } = ctrl[target].kind { // BACKWARD conditional branch to the loop header. @@ -1438,51 +1648,165 @@ pub fn select_typed_cf_calls( ctrl[target].pending.push(pos); } } + // `br_table` (VCR-A64-CF-001) — WASM's multi-way branch: pop the + // i32 index; index `i` branches to `targets[i]`, and ANY index + // `>= targets.len()` goes to `default`. The index is UNSIGNED, so + // the "negative" i32s are huge unsigned values and also land on + // the default label. + // + // Lowering: a COMPARE-AND-BRANCH CHAIN, deliberately the same + // construction #882 chose for RV32 so the two backends stay + // reviewable against each other. Entry 0 is `cbz w_idx, L0` (one + // instruction, no constant to materialize); every further entry is + // `cmp w_idx, #i` + `b.eq L_i`; the chain ends in an unconditional + // `b L_default`, which is exactly where every non-matching index — + // in-range-of-i32 or not — lands. The compares are the W view, so + // a dirty upper half (an i64 producer feeding the index) cannot + // affect the dispatch, and equality against the constants + // `0..len-1` is exact for the unsigned-index semantics. + // + // Targets may MIX destinations: a `loop` target is the loop HEADER + // (backward, resolved eagerly to a negative offset) while a + // block/if target is its END (forward, patched at that `End`) — + // the same dispatch-on-the-TARGET-frame's-kind rule `br`/`br_if` + // already use. + // + // No jump table, no data section, no PC-relative table: for the + // small tables real drivers carry, the chain is smaller and simpler + // to verify than an indirect dispatch. Past + // [`BR_TABLE_MAX_TARGETS`] it LOUD-DECLINES rather than emit an + // unbounded chain — the jump-table upgrade is a named follow-up. + WasmOp::BrTable { targets, default } => { + if targets.len() > BR_TABLE_MAX_TARGETS { + return Err(SelectError(format!( + "br_table with {} targets exceeds the aarch64 \ + compare-chain threshold ({BR_TABLE_MAX_TARGETS}); \ + PC-relative jump-table dispatch is not implemented for \ + aarch64 — loud-declining (VCR-A64-CF-001)", + targets.len() + ))); + } + let idx = pop_gp(&mut stack, "br_table")?; + // Conservative VALUE-CARRYING guard (#509 class, mirroring the + // RV32 #882 rule). A flat compare chain has no room for a + // per-path result move: the deposit would have to sit on the + // TAKEN edge of each individual compare. So every targeted + // frame (the default included) must have a VOID label and must + // have been entered at exactly the current post-pop height — + // then a taken branch moves no values and the plain-jump + // lowering is sound. + let height = stack.len(); + for &depth in targets.iter().chain(std::iter::once(default)) { + let d = depth as usize; + if d >= ctrl.len() { + return Err(SelectError(format!( + "br_table target depth {depth} exceeds open block \ + nesting ({} open)", + ctrl.len() + ))); + } + let frame = &ctrl[ctrl.len() - 1 - d]; + if frame.label_arity != 0 || frame.stack_entry != height { + return Err(SelectError(format!( + "br_table with VALUE-CARRYING targets (target depth \ + {depth}: label arity {}, frame entry height {} vs \ + post-pop height {height}) — the flat compare chain \ + has no per-path edge to deposit a result on; \ + loud-declining (VCR-A64-CF-001, the #509 class)", + frame.label_arity, frame.stack_entry + ))); + } + } + // The chain. `idx` was popped, so no value-stack entry holds it + // and nothing below can be disturbed. + for (i, &depth) in targets.iter().enumerate() { + let target = ctrl.len() - 1 - depth as usize; + if i > 0 { + // i <= BR_TABLE_MAX_TARGETS - 1 always fits imm12. + words.push(enc::cmp_imm(idx, i as u32)); + } + let pos = words.len(); + if let Kind::Loop { entry } = ctrl[target].kind { + let off = check_imm19((entry as i64 - pos as i64) as i32)?; + words.push(if i == 0 { + enc::cbz(idx, off) + } else { + enc::bcond(Cond::Eq, off) + }); + } else { + words.push(if i == 0 { + enc::cbz(idx, 0) // placeholder; patched at End + } else { + enc::bcond(Cond::Eq, 0) // placeholder; patched at End + }); + ctrl[target].pending.push(pos); + } + } + // No entry matched → default. Also where every out-of-range + // (unsigned) index lands. + let dflt = ctrl.len() - 1 - *default as usize; + let pos = words.len(); + if let Kind::Loop { entry } = ctrl[dflt].kind { + let off = check_imm26((entry as i64 - pos as i64) as i32)?; + words.push(enc::b_uncond(off)); + } else { + words.push(enc::b_uncond(0)); // placeholder + ctrl[dflt].pending.push(pos); + } + // Every index transfers control: the fall-through is dead. + reachable = false; + } // `loop` (#851): opens a control frame whose branch target is the // loop HEADER (the current position), so a `br`/`br_if` to it is a - // BACKWARD branch. Only a VOID `(0,0)` loop is accepted: a - // value/param loop would need the value stack non-empty across the - // back-edge, and the deterministic temp-restart (`alloc_temp` picks - // the same register when the stack is empty) would no longer hold. - // The `(0,0)` gate enforces exactly the sound shape — loop-carried - // state must live in non-param LOCAL SLOTS (memory), reloaded each - // iteration. `br_table` still declines (catch-all). + // BACKWARD branch. + // + // VCR-A64-CF-001 — a `loop (result T)` is now accepted, and the + // asymmetry with `block` is SOUNDNESS-CRITICAL rather than + // cosmetic: a branch to a LOOP label targets the header and carries + // the loop's PARAMETERS, not its results. `open_slot(is_loop=true)` + // therefore sets `label_arity = params` (0 here), so the back-edge + // reconciles NOTHING and the reserved register is written by the + // fall-through `End` alone. Reconciling on the back-edge — the + // natural wrong implementation, and what treating `label_arity` as + // "the frame is value-carrying" would do — would stamp a garbage + // value into the result register on every iteration. + // + // Loop PARAMETERS still loud-decline: they would need the value + // stack live across the back-edge, and the deterministic + // temp-restart (`alloc_temp` picks the same register at the same + // height) would no longer hold. Loop-carried state must live in + // non-param LOCAL SLOTS (memory), reloaded each iteration. WasmOp::Loop => { let ord = ctrl_ord; ctrl_ord += 1; let arity = block_arity.get(ord).copied().unwrap_or((0, 0)); - if arity != (0, 0) { - return Err(SelectError(format!( - "loop #{ord} has type {arity:?} — only void (0,0) loops \ - are supported (a value/param loop needs the value stack \ - live across the back-edge); loud-declining" - ))); - } + let (label_arity, result_arity, slot) = + open_slot("loop", ord, arity, true, &stack)?; ctrl.push(Frame { kind: Kind::Loop { entry: words.len() }, pending: Vec::new(), stack_entry: stack.len(), + label_arity, + result_arity, + slot, }); } // `if` (#851): pop the i32 condition; emit `cbz cond, ` to // SKIP the then-arm when the condition is false. The skip target is // patched at the matching `else` (to the else-arm entry) or, if - // there is no `else`, at `end` (past the then-arm). Only VOID `(0,0)` - // `if` is accepted — a value-producing `if` would need both arms to - // leave the result in the same register, which this straight-line - // model does not guarantee, so it LOUD-DECLINES. + // there is no `else`, at `end` (past the then-arm). VCR-A64-CF-001: + // a value-producing `(0,1)` `if` is now accepted — "both arms must + // land the result in one register" is exactly what the reserved + // reconciliation slot guarantees (the then-arm deposits at `else`, + // the else-arm at `end`). WasmOp::If => { let ord = ctrl_ord; ctrl_ord += 1; let arity = block_arity.get(ord).copied().unwrap_or((0, 0)); - if arity != (0, 0) { - return Err(SelectError(format!( - "if #{ord} has type {arity:?} — only void (0,0) if/else \ - is supported (a value-producing if needs both arms to \ - land the result in one register); loud-declining" - ))); - } let cond = pop_gp(&mut stack, "if")?; + // Reserve AFTER popping the condition so the condition's temp + // is a candidate for the slot (it is dead from here on). + let (label_arity, result_arity, slot) = open_slot("if", ord, arity, false, &stack)?; let else_pos = words.len(); // cbz: fall THROUGH into the then-arm when cond != 0; branch to // the else/end when cond == 0. Offset patched at else/end. @@ -1493,6 +1817,9 @@ pub fn select_typed_cf_calls( }, pending: Vec::new(), stack_entry: stack.len(), + label_arity, + result_arity, + slot, }); } // `else` (#851): closes the then-arm of the innermost `if`. Emit an @@ -1512,6 +1839,27 @@ pub fn select_typed_cf_calls( return Err(SelectError("else does not close an if block".into())); } }; + // VCR-A64-CF-001 — a value-producing then-arm hands the join + // its result here, immediately before the `b end` below (the + // no-clobber-window property [`reconcile_into`] documents). + if frame.result_arity == 1 && reachable { + let v = *stack.last().ok_or_else(|| { + SelectError( + "else: value-producing then-arm left no result on \ + the value stack" + .into(), + ) + })?; + let slot = frame.slot.as_mut().ok_or_else(|| { + SelectError( + "else: value-carrying if has no reconciliation slot \ + (internal invariant)" + .into(), + ) + })?; + reconcile_into(&mut words, slot, v); + stack.pop(); + } // A void then-arm leaves the stack at its entry height — but // only on a REACHABLE fall-through (a then-arm ending in // `return`/`br` is polymorphic). Truncate unconditionally (fixes @@ -1748,7 +2096,30 @@ pub fn select_typed_cf_calls( // when no block is open — ends the FUNCTION body (funnel the result // into x0/d0 and return). WasmOp::End => { - if let Some(frame) = ctrl.pop() { + if let Some(mut frame) = ctrl.pop() { + // VCR-A64-CF-001 — the FALL-THROUGH edge of a + // value-carrying frame deposits its result. This MUST be + // emitted before `here` is taken: the forward branches + // reconciled at their own sites, so they have to land PAST + // this move, not on it. + if frame.result_arity == 1 && reachable { + let v = *stack.last().ok_or_else(|| { + SelectError( + "end: value-carrying block left no result on the \ + value stack" + .into(), + ) + })?; + let slot = frame.slot.as_mut().ok_or_else(|| { + SelectError( + "end: value-carrying frame has no reconciliation \ + slot (internal invariant)" + .into(), + ) + })?; + reconcile_into(&mut words, slot, v); + stack.pop(); + } // Frame close. Every recorded FORWARD branch (block/if exit, // else-arm skip) targets HERE (fall-through). A Loop's // branches were backward and already resolved. Patch each @@ -1776,6 +2147,21 @@ pub fn select_typed_cf_calls( stack.len() ); stack.truncate(frame.stack_entry); + // VCR-A64-CF-001 — release the frame's reservations and + // push its value. Every edge into this join has deposited + // into the same register, so the frame's result IS that + // register. `file` is `None` only when NO edge ever + // reconciled (an unreachable-only frame such as + // `block (result i32) unreachable end`); the pushed value + // is then dead by construction, so the GP default is safe. + if let Some(slot) = frame.slot { + reserved_gp.set(reserved_gp.get() & !(1u32 << slot.gp)); + reserved_fp.set(reserved_fp.get() & !(1u32 << slot.fp)); + stack.push(match slot.file.unwrap_or(File::Gp) { + File::Gp => Val::gp(slot.gp), + File::Fp => Val::fp(slot.fp), + }); + } // After closing a frame the position is reachable again: a // forward branch could target this fall-through, and a loop's // continuation follows. (A dead nested block would want the @@ -2084,10 +2470,7 @@ pub fn select_typed_cf_calls( let delta = pop_gp(&mut stack, "memory.grow")?; // Reserve `delta` so the two scratch temps are distinct from it. stack.push(Val::gp(delta)); - let mut free = TEMPS - .iter() - .copied() - .filter(|t| !stack.iter().any(|v| v.file == File::Gp && v.reg == *t)); + let mut free = TEMPS.iter().copied().filter(|t| gp_free(*t, &stack)); let (Some(t0), Some(t1)) = (free.next(), free.next()) else { stack.pop(); return Err(SelectError( @@ -2393,12 +2776,17 @@ fn check_imm19(off: i32) -> Result { } /// Re-encode a placeholder FORWARD branch at `words[pos]` to land at `target` -/// (a word index in `words`), preserving its kind. The three kinds we emit as -/// forward placeholders are `b` (0x14…, imm26), `cbnz` (0x35…, imm19+Rt), and -/// `cbz` (0x34…, imm19+Rt); the opcode's high bits discriminate them so the Rt -/// field and op class survive the patch. Centralizing this prevents a `cbz` -/// (added in #851) from being mis-patched as a `cbnz`. Over-range displacements -/// LOUD-DECLINE (no silent field wrap). +/// (a word index in `words`), preserving its kind. The FOUR kinds we emit as +/// forward placeholders are `b` (0x14…, imm26), `cbnz` (0x35…, imm19+Rt), `cbz` +/// (0x34…, imm19+Rt), and — since VCR-A64-CF-001's `br_table` chain — `b.` +/// (0x54…, imm19 + a 4-bit condition); the opcode's high bits discriminate them +/// so the Rt field, the condition field and the op class survive the patch. +/// Centralizing this prevents a `cbz` (added in #851) from being mis-patched as +/// a `cbnz`. Over-range displacements LOUD-DECLINE (no silent field wrap). +/// +/// The `b.` case rebuilds the word directly instead of round-tripping +/// through [`enc::bcond`]: that keeps whatever condition the emitter chose +/// without needing to invert the private `Cond` mapping back out of the word. fn patch_branch(words: &mut [u32], pos: usize, target: usize) -> Result<(), SelectError> { let off = (target as i64 - pos as i64) as i32; let w = words[pos]; @@ -2406,6 +2794,7 @@ fn patch_branch(words: &mut [u32], pos: usize, target: usize) -> Result<(), Sele 0x1400_0000 => enc::b_uncond(check_imm26(off)?), 0x3500_0000 => enc::cbnz((w & 0x1F) as u8, check_imm19(off)?), 0x3400_0000 => enc::cbz((w & 0x1F) as u8, check_imm19(off)?), + 0x5400_0000 => 0x5400_0000 | (((check_imm19(off)? as u32) & 0x7FFFF) << 5) | (w & 0xF), _ => unreachable!("patch_branch: not a placeholder branch: {w:#010x}"), }; Ok(()) @@ -3946,46 +4335,287 @@ mod tests { assert_eq!(w.len(), 4); } + // ---- VCR-A64-CF-001 — value-carrying frames + br_table ----------------- + + #[test] + fn typed_block_reconciles_its_result_into_one_register() { + // `(func (param i32) (result i32) (block (result i32) (local.get 0)))` + // — the shape that used to loud-decline. The fall-through `end` + // deposits into the frame's reserved register; the function epilogue + // then funnels THAT register into x0. + let ops = vec![ + WasmOp::Block, // arity (0,1) + WasmOp::LocalGet(0), + WasmOp::End, + WasmOp::End, + ]; + let w = select_typed_cf(&ops, 1, &[], &[], &[(0, 1)]).unwrap(); + // The block reserves x9 (first free temp); `local.get 0` is a leaf + // param read, so the value is w0 by reference. end: mov x9, x0 ; + // fn-end: mov x0, x9 ; ret. + assert_eq!( + w, + vec![enc::mov_reg64(9, 0), enc::mov_reg64(0, 9), enc::ret()] + ); + } + + #[test] + fn value_carrying_br_if_deposits_into_the_same_register_as_the_fallthrough() { + // `(block (result i32) (br_if 0 (i32.const 7) (local.get 0)) + // (drop) (i32.const 9))` — the two edges into the + // join must land the result in ONE register. The whole point of the + // reconciliation slot. + let ops = vec![ + WasmOp::Block, // (0,1) + WasmOp::I32Const(7), + WasmOp::LocalGet(0), + WasmOp::BrIf(0), + WasmOp::Drop, + WasmOp::I32Const(9), + WasmOp::End, + WasmOp::End, + ]; + let w = select_typed_cf(&ops, 1, &[], &[], &[(0, 1)]).unwrap(); + // Slot = x9. const 7 -> x10 (x9 reserved). br_if: mov x9, x10 ; + // cbnz w0, . drop pops x10. const 9 -> x10. end: mov x9, x10. + // Both edges write x9 — that is the assertion. + let movs: Vec = w + .iter() + .enumerate() + .filter(|(_, x)| **x == enc::mov_reg64(9, 10)) + .map(|(i, _)| i) + .collect(); + assert_eq!( + movs.len(), + 2, + "both the br_if edge and the fall-through must deposit into the \ + slot register: {w:#010x?}" + ); + // The cbnz must target the word AFTER the fall-through's deposit. + let cbnz_at = w + .iter() + .position(|x| x & 0xFF00_0000 == 0x3500_0000) + .expect("br_if emits a cbnz"); + let off = ((w[cbnz_at] >> 5) & 0x7FFFF) as usize; + assert_eq!( + cbnz_at + off, + movs[1] + 1, + "the taken edge must land PAST the fall-through's reconciliation \ + move, not on it (or it would re-run with a dead operand)" + ); + } + #[test] - fn typed_block_is_loud_declined() { - // A value-carrying block (result i32) must decline — the straight-line - // model can't reconcile the result register across the branch. + fn value_carrying_loop_does_not_reconcile_on_the_back_edge() { + // SOUNDNESS-CRITICAL asymmetry. A `br` to a LOOP label carries the + // loop's PARAMETERS (0 here), NOT its results — so a `loop (result + // i32)` back-edge must emit NO reconciliation move. If it did, every + // iteration would stamp a garbage value into the result register. + // + // `(block (loop (result i32) ... ) )` is awkward to write with raw + // ops; use the direct shape: loop (0,1) whose body branches back on a + // condition, then falls through with the result. let ops = vec![ - WasmOp::Block, // arity (0,1) → declined + WasmOp::Loop, // (0,1) WasmOp::LocalGet(0), + WasmOp::BrIf(0), // back-edge: label arity 0 → NO deposit + WasmOp::I32Const(5), WasmOp::End, WasmOp::End, ]; + let w = select_typed_cf(&ops, 1, &[], &[], &[(0, 1)]).unwrap(); + // Words: cbnz w0, -0 (back to header) ; mov x10, #5 ; mov x9, x10 ; + // mov x0, x9 ; ret. Exactly ONE mov into the slot (the fall-through). + let deposits = w.iter().filter(|x| **x == enc::mov_reg64(9, 10)).count(); + assert_eq!( + deposits, 1, + "a loop's back-edge must NOT reconcile (label arity = PARAMS): \ + {w:#010x?}" + ); + // And the back-edge is a real backward branch (negative imm19). + let cbnz = w[0]; + assert_eq!(cbnz & 0xFF00_0000, 0x3500_0000, "back-edge is a cbnz"); + assert_eq!( + (cbnz >> 5) & 0x7FFFF, + 0, + "the back-edge targets the loop header at offset 0" + ); + } + + #[test] + fn value_producing_if_else_lands_both_arms_in_one_register() { + // `(if (result i32) (then (i32.const 1)) (else (i32.const 2)))`. + let ops = vec![ + WasmOp::LocalGet(0), + WasmOp::If, // (0,1) + WasmOp::I32Const(1), + WasmOp::Else, + WasmOp::I32Const(2), + WasmOp::End, + WasmOp::End, + ]; + let w = select_typed_cf(&ops, 1, &[], &[], &[(0, 1)]).unwrap(); + let deposits = w.iter().filter(|x| **x == enc::mov_reg64(9, 10)).count(); + assert_eq!( + deposits, 2, + "then-arm (at `else`) and else-arm (at `end`) must BOTH deposit \ + into the slot: {w:#010x?}" + ); + } + + #[test] + fn block_params_and_multi_value_results_still_loud_decline() { + // The residuals, named. The slot is ONE register: block PARAMS would + // need a per-path multi-register shuffle, multi-value more than one + // slot. Both must decline rather than silently drop a value. + let block = vec![WasmOp::Block, WasmOp::End, WasmOp::End]; + let e = select_typed_cf(&block, 0, &[], &[], &[(1, 1)]).unwrap_err(); + assert!( + e.0.contains("PARAMETER-taking block type"), + "block params must decline by name, got: {}", + e.0 + ); + let e = select_typed_cf(&block, 0, &[], &[], &[(0, 2)]).unwrap_err(); + assert!( + e.0.contains("MULTI-VALUE result block type"), + "multi-value must decline by name, got: {}", + e.0 + ); + // Same for `loop`: a PARAM loop is the shape whose back-edge would need + // the value stack live across the header. + let lp = vec![WasmOp::Loop, WasmOp::End, WasmOp::End]; assert!( - select_typed_cf(&ops, 1, &[], &[], &[(0, 1)]).is_err(), - "typed (0,1) block must loud-decline" + select_typed_cf(&lp, 0, &[], &[], &[(1, 0)]) + .unwrap_err() + .0 + .contains("PARAMETER-taking block type") ); } #[test] - fn br_table_and_typed_loop_if_are_loud_declined() { - // #851: `loop`, `if`/`else` are now LOWERED for the void (0,0) shape. - // What still declines: `br_table` (jump table, catch-all) and any - // VALUE-carrying loop/if (arity != (0,0)). - let brtable = vec![ + fn br_table_emits_a_compare_chain_with_a_default_fallthrough() { + // `(block (block (block (br_table 0 1 2 (local.get 0)))))` — three + // targets at depths 0/1/2, default = 2. + let ops = vec![ + WasmOp::Block, + WasmOp::Block, WasmOp::Block, WasmOp::LocalGet(0), + WasmOp::BrTable { + targets: vec![0, 1], + default: 2, + }, + WasmOp::End, + WasmOp::End, + WasmOp::End, + WasmOp::End, + ]; + let w = select_typed_cf(&ops, 3, &[], &[], &[(0, 0), (0, 0), (0, 0)]).unwrap(); + // idx = w0 (leaf param, by reference). Chain: + // [0] cbz w0, (entry 0) + // [1] cmp w0, #1 + // [2] b.eq (entry 1) + // [3] b (default) + // [4] ret + assert_eq!(w.len(), 5, "{w:#010x?}"); + assert_eq!( + w[0], + enc::cbz(0, 4), + "entry 0 is a bare cbz to the innermost end" + ); + assert_eq!(w[1], enc::cmp_imm(0, 1)); + assert_eq!(w[2], enc::bcond(Cond::Eq, 2), "entry 1 -> middle end"); + assert_eq!(w[3], enc::b_uncond(1), "default -> outer end"); + assert_eq!(w[4], enc::ret()); + } + + #[test] + fn br_table_can_target_a_loop_header_backward_and_a_block_end_forward() { + // One table, MIXED destinations: depth 0 = the enclosing loop (its + // HEADER, backward, eagerly resolved) and depth 1 = a block END + // (forward, patched). A lowering that assumed one direction would + // emit a wrong offset for the other. + let ops = vec![ + WasmOp::Block, // depth 1 from inside the loop + WasmOp::Loop, // depth 0 + WasmOp::LocalGet(0), WasmOp::BrTable { targets: vec![0], + default: 1, + }, + WasmOp::End, // loop end + WasmOp::End, // block end + WasmOp::End, // fn end + ]; + let w = select_typed_cf(&ops, 1, &[], &[], &[(0, 0), (0, 0)]).unwrap(); + // [0] cbz w0, 0 (loop header is word 0 → offset 0-0 = 0, BACKWARD/self) + // [1] b +1 (default → block end at word 2) + // [2] ret + assert_eq!(w.len(), 3, "{w:#010x?}"); + assert_eq!( + w[0], + enc::cbz(0, 0), + "loop target resolves eagerly to the header" + ); + assert_eq!( + w[1], + enc::b_uncond(1), + "default is a patched forward branch" + ); + assert_eq!(w[2], enc::ret()); + } + + #[test] + fn br_table_residuals_loud_decline_by_name() { + // (1) Past the compare-chain threshold. + let big = vec![ + WasmOp::Block, + WasmOp::LocalGet(0), + WasmOp::BrTable { + targets: vec![0; BR_TABLE_MAX_TARGETS + 1], default: 0, }, WasmOp::End, WasmOp::End, ]; - assert!(select_typed_cf(&brtable, 1, &[], &[], &[(0, 0)]).is_err()); - - // A VALUE-producing if (result i32 → arity (0,1)) loud-declines. - let typed_if = vec![WasmOp::LocalGet(0), WasmOp::If, WasmOp::End, WasmOp::End]; - assert!(select_typed_cf(&typed_if, 1, &[], &[], &[(0, 1)]).is_err()); + let e = select_typed_cf(&big, 1, &[], &[], &[(0, 0)]).unwrap_err(); + assert!( + e.0.contains("exceeds the aarch64 compare-chain threshold"), + "oversized br_table must decline by name, got: {}", + e.0 + ); + // Exactly at the threshold still lowers (the boundary is not off-by-one). + let at = vec![ + WasmOp::Block, + WasmOp::LocalGet(0), + WasmOp::BrTable { + targets: vec![0; BR_TABLE_MAX_TARGETS], + default: 0, + }, + WasmOp::End, + WasmOp::End, + ]; + assert!(select_typed_cf(&at, 1, &[], &[], &[(0, 0)]).is_ok()); - // A VALUE-producing loop (arity (0,1)) loud-declines. - let typed_loop = vec![WasmOp::Loop, WasmOp::End, WasmOp::End]; - assert!(select_typed_cf(&typed_loop, 0, &[], &[], &[(0, 1)]).is_err()); + // (2) A VALUE-CARRYING target. The flat chain has no per-path edge to + // deposit a result on, so it refuses rather than miscompile. + let vc = vec![ + WasmOp::Block, // (0,1) — value-carrying label + WasmOp::I32Const(1), + WasmOp::LocalGet(0), + WasmOp::BrTable { + targets: vec![0], + default: 0, + }, + WasmOp::End, + WasmOp::End, + ]; + let e = select_typed_cf(&vc, 1, &[], &[], &[(0, 1)]).unwrap_err(); + assert!( + e.0.contains("VALUE-CARRYING targets"), + "value-carrying br_table must decline by name, got: {}", + e.0 + ); } #[test] 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 3be37ec3..ee26d96e 100644 --- a/crates/synth-backend-riscv/tests/cross_backend_op_parity.rs +++ b/crates/synth-backend-riscv/tests/cross_backend_op_parity.rs @@ -90,6 +90,29 @@ fn riscv_lowers(ops: &[WasmOp], num_params: u32) -> bool { riscv_select(ops, num_params).is_ok() } +/// The AArch64 selector's DECLINE REASON for a sequence, or `Ok(())` when it +/// lowers. `aarch64_lowers` collapses the reason away, which makes a +/// sub-shape claim vacuous (a bare `is_err()` is also satisfied by an unrelated +/// artifact in the probe). VCR-A64-CF-001's residual assertions match on the +/// message text, the aarch64 analogue of RV32's typed `SelectorError` variants. +fn aarch64_decline_reason(ops: &[WasmOp], num_params: u32) -> Result<(), String> { + synth_backend_aarch64::selector::select_typed_cf_calls( + ops, + num_params, + &[], + &[], + &[], + 0, + &[0], + &[0], + &[false], + synth_backend_aarch64::selector::MemBounds::Software { limit_bytes: 65536 }, + &a64_module_ctx(), + ) + .map(|_| ()) + .map_err(|e| e.0) +} + /// Does the AArch64 (A64 host-native) selector lower this sequence? (#851 — /// the THIRD backend in the VCR-SEL-005 enumeration.) /// @@ -922,19 +945,26 @@ fn known_divergences() -> &'static [(&'static str, &'static str)] { /// the initial enumeration surfaced TWENTY ARM-lowers/aarch64-declines gaps. /// Thirteen were closed in the same change (v0.53 #851: `select` via /// CSEL/FCSEL, `drop`, `nop`, `i32.wrap_i64`, `i64.extend_i32_{s,u}`, the five -/// `extend8/16/32_s` forms, fixed-memory `memory.size`/`memory.grow`), leaving -/// seven. v0.54 (#851 lane L3) closed two more — `global.get`/`global.set` — -/// leaving the **FIVE** below. This ledger — the COMPLEMENT of what aarch64 -/// lowers — is the mechanically-derived answer to "what is missing on armv8?" -/// (#851); the float-surface complement lives in [`a64_extended_surface`]. +/// `extend8/16/32_s` forms, fixed-memory `memory.size`/`memory.grow`). Later +/// lanes closed `global.get`/`global.set` and `call_indirect` (v0.54) and +/// `br_table` (v0.55, VCR-A64-CF-001), leaving the FOUR below. This ledger — +/// the COMPLEMENT of what aarch64 lowers — is the mechanically-derived answer +/// to "what is missing on armv8?" (#851); the float-surface complement lives in +/// [`a64_extended_surface`]. /// Keep this count in step with the array (#893). fn aarch64_known_divergences() -> &'static [(&'static str, &'static str)] { &[ - ( - "br_table", - "aarch64 selector has no BrTable arm (loud decline); the jump-table \ - dispatch is not yet lowered — deferred, VCR-SEL-005/#851", - ), + // (br_table CLOSED v0.55, VCR-A64-CF-001 — the aarch64 selector now + // lowers it as a compare-and-branch chain (`cbz`/`cmp`+`b.eq`, then a + // default `b`), so the whole-op divergence is gone and the ledger + // entry was deleted; the stale-entry check is what forced the + // deletion. The THREE remaining sub-shape asymmetries (>16 targets, + // value-carrying targets, and — shared with the `block`/`loop`/`if` + // lowering — block params / multi-value) 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/aarch64_brtable_blockvals_851_differential.py.) ( "local.set+get(param)", "aarch64 declines WRITING a parameter: params live in arg registers \ @@ -1957,6 +1987,15 @@ fn ledger_labels_are_live_integer_core_ops() { /// 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. +/// +/// AARCH64 LEG (VCR-A64-CF-001, v0.55). The aarch64 `br_table` lowering landed +/// with the same deliberately-partial shape, so its whole-op ledger entry was +/// deleted and THREE residuals are pinned here by name: `>16 targets`, +/// `value-carrying targets`, and — the residue of the old blanket +/// "value-carrying blocks decline" — block PARAMETERS / MULTI-VALUE results. +/// The complement of that third one is asserted positively in the same loop: a +/// `(0,1)` value-carrying block must now LOWER, so the claim cannot quietly +/// widen back into "typed blocks decline". #[test] fn br_table_subshape_asymmetry_882() { // The shape the op-level ledger probes: <=16 targets, non-value-carrying, @@ -2042,4 +2081,81 @@ fn br_table_subshape_asymmetry_882() { claim; if it errors differently, the probe stopped measuring the gap.", riscv_select(&value_carrying, 1).map(|_| "Ok") ); + + // ---- AArch64 leg (VCR-A64-CF-001, v0.55) ------------------------------- + // + // The aarch64 `br_table` lowering landed with the SAME deliberate partial + // shape as RV32's, and its whole-op ledger entry was deleted for the same + // reason. Its residuals are pinned here rather than left to the deleted + // entry — same both-directions contract: if aarch64 later grows a jump + // table or per-path arity threading, these go red and whoever closed the + // gap must delete the claim. + assert!( + aarch64_lowers(&at_parity, 1), + "the br_table shape the op-parity ledger probes must lower on aarch64 \ + (VCR-A64-CF-001); if it stopped, re-add the known-divergence entry" + ); + + // Residual A1: past BR_TABLE_MAX_TARGETS (16) the aarch64 chain refuses, + // exactly as RV32's does — the two backends share the threshold on purpose. + assert_eq!( + synth_backend_aarch64::selector::BR_TABLE_MAX_TARGETS, + 16, + "the aarch64 br_table threshold moved; this claim probes 17 targets" + ); + let a64_too_large = aarch64_decline_reason(&too_large, 1); + assert!( + a64_too_large + .as_ref() + .err() + .is_some_and(|m| m.contains("exceeds the aarch64 compare-chain threshold")), + "aarch64 must decline a 17-target br_table by NAME (compare-chain \ + threshold); got {a64_too_large:?}. If it now lowers, the jump-table \ + upgrade landed — delete this claim." + ); + + // Residual A2: value-carrying targets (the #509 class). The flat compare + // chain has no per-path edge to deposit a result on. + let a64_value_carrying = aarch64_decline_reason(&value_carrying, 1); + assert!( + a64_value_carrying + .as_ref() + .err() + .is_some_and(|m| m.contains("VALUE-CARRYING targets")), + "aarch64 must decline a value-carrying br_table by NAME; got \ + {a64_value_carrying:?}. If it now lowers, per-path arity threading \ + landed — delete this claim." + ); + + // Residual A3: block PARAMETERS / MULTI-VALUE results. VCR-A64-CF-001 + // lowers the `(0,1)` value-carrying frame (one reserved reconciliation + // register), so these two are what is LEFT of the old blanket + // "value-carrying blocks decline". Probed through the arity side-table, + // which is the only channel that carries a block type. + // `(block (result i32) (i32.const 1))` — a MINIMALLY-VALID value-carrying + // frame (a bare `[Block, End]` at arity (0,1) is invalid wasm: the block + // produces nothing, and the selector rejects it for that unrelated reason, + // which would make the positive claim below vacuous). + let plain_block = [Block, I32Const(1), End, End]; + assert!( + synth_backend_aarch64::selector::select_typed_cf(&plain_block, 0, &[], &[], &[(0, 1)]) + .is_ok(), + "a (0,1) VALUE-CARRYING block must now LOWER on aarch64 \ + (VCR-A64-CF-001); if it declines, the capability regressed" + ); + for (arity, needle) in [ + ((1u8, 1u8), "PARAMETER-taking block type"), + ((0, 2), "MULTI-VALUE result block type"), + ] { + let got = + synth_backend_aarch64::selector::select_typed_cf(&plain_block, 0, &[], &[], &[arity]) + .map(|_| ()) + .map_err(|e| e.0); + assert!( + got.as_ref().err().is_some_and(|m| m.contains(needle)), + "aarch64 must decline a {arity:?} block type by NAME ({needle}); \ + got {got:?}. If it now lowers, multi-value support landed — delete \ + this claim." + ); + } } diff --git a/crates/synth-cli/tests/aarch64_f32_loudskip_554.rs b/crates/synth-cli/tests/aarch64_f32_loudskip_554.rs index e49daa57..cb8b4dd3 100644 --- a/crates/synth-cli/tests/aarch64_f32_loudskip_554.rs +++ b/crates/synth-cli/tests/aarch64_f32_loudskip_554.rs @@ -1,13 +1,15 @@ //! synth#554 — `-b aarch64` must fail HONESTLY on an UNSUPPORTED float op, never //! emit a silent miscompile. //! -//! m3 (#787) landed the non-trapping scalar floats; m4 (#538) landed the -//! #709-class conversions (domain-guarded `i32.trunc_f32/f64_{s,u}`, FMIN/FMAX -//! min/max, copysign), so this test now targets a float op that DELIBERATELY -//! stays declined: `f64.floor` (rounding). It is DECODED (the ARM32 m7dp -//! backend lowers it), so it reaches the aarch64 SELECTOR, which must -//! loud-decline (`unsupported wasm op`) — the strongest form of the honesty -//! check (nothing upstream masks it). +//! The honesty target MOVES as the surface closes: m3 (#787) landed the +//! non-trapping scalar floats, m4 (#538) the #709-class conversions, v0.54 L2 +//! the last four scalar-float classes, and v0.55 L6 (VCR-A64-CF-001) the +//! VALUE-CARRYING f32-result `block` this test used to target. It now targets a +//! float construct that DELIBERATELY stays declined: a NON-LEAF function +//! reading an f32 PARAMETER (float params live in v0..v7, which a `bl` +//! clobbers, and this encoder has no FP store to home them with). It is fully +//! DECODED, so it reaches the aarch64 SELECTOR, which must loud-decline — the +//! strongest form of the honesty check (nothing upstream masks it). //! //! These tests lock: (1) the declined-float function is REJECTED with a non-zero //! exit and an "unsupported" diagnostic; (2) a supported integer function still @@ -34,7 +36,7 @@ fn aarch64_rejects_f32_function_instead_of_silent_miscompile_554() { "-b", "aarch64", "-n", - "f32block", + "f32nonleaf", "-o", "/tmp/aarch64_f32_554.o", ]) @@ -42,9 +44,9 @@ fn aarch64_rejects_f32_function_instead_of_silent_miscompile_554() { .expect("run synth"); assert!( !out.status.success(), - "expected a non-zero exit for a declined float construct (f32-result \ - block) on -b aarch64; got success (silent miscompile). stdout={} \ - stderr={}", + "expected a non-zero exit for a declined float construct (an f32 param \ + read in a NON-LEAF function) on -b aarch64; got success (silent \ + miscompile). stdout={} stderr={}", String::from_utf8_lossy(&out.stdout), String::from_utf8_lossy(&out.stderr), ); diff --git a/docs/status/FEATURE_MATRIX.md b/docs/status/FEATURE_MATRIX.md index 4c19b56d..edd8e3cd 100644 --- a/docs/status/FEATURE_MATRIX.md +++ b/docs/status/FEATURE_MATRIX.md @@ -33,7 +33,7 @@ soundness feature, not an absence. | ARM Thumb-2 (primary) | `synth-backend` | `cortex-m3`, `cortex-m4`, `cortex-m4f`, `cortex-m7`, `cortex-m7dp` (+ `cortex-m55` experimental MVE) | i32 + i64 (register pairs) complete; scalar f32/f64 via VFP on FPU targets; control flow (block/loop/if/br/br_table); memory incl. sub-word; direct calls; `call_indirect` in both relocatable and self-contained `--cortex-m` images (v0.47, #275) | | ARM A32 | `synth-backend` | `cortex-r5` | i32 + i64 integer family (221-variant no-wildcard tripwire, #615); self-contained `call_indirect` declines loudly (no flash-table builder) | | RISC-V RV32IMAC | `synth-backend-riscv` | `rv32imac`, `rv32imc`, `rv32im`, `rv32i`, `rv32gc`, `esp32c3` | i32 + i64 integer ops, control flow, calls incl. `call_indirect`, memory loads/stores; relocatable ELF; import/external calls emit `R_RISCV_CALL_PLT` relocations (`.rela.text`, undefined import symbols — #871) with exact-arity marshalling from the module signature tables; >8-arg / i64-arg / multi-value calls decline loudly; floats decline loudly | -| AArch64 (A64, host-native) | `synth-backend-aarch64` | `cortex-a53` (host-linkable ET_REL, `-b aarch64`) | 184 distinct WASM ops handled by the selector: i32 + i64 integer core incl. `div_s/div_u/rem_s/rem_u` (with the ÷0 + INT_MIN/−1 WASM trap guards), `popcnt`, `select` (branchless `CSEL`/`FCSEL`, all four value types), `drop`/`nop`, `i32.wrap_i64`, `i64.extend_i32_{s,u}`, and the five `extend8/16/32_s` sign extensions (#851 v0.53); scalar f32/f64 incl. domain-guarded trapping float→int truncations, IEEE 754-2019 min/max, copysign, and f64↔i64 reinterpret (#538 milestone 4, #851); full control flow — `block`/`loop`/`if`/`else`/`br`/`br_if`/`return` (#538 cf + #851); non-param locals — zero-init stack slots with copy-semantics get/set/tee (#856); linear-memory `i32`/`i64` load/store incl. all sub-word sign/zero forms, **BOUNDS-CHECKED by default** — an out-of-bounds access traps (`brk`) exactly where wasmtime traps, and `--safety-bounds` selects the strategy (`software` = the enforcing default, `none` = explicit opt-out; `mask`/`mpu` hard-error rather than silently degrading) (#851, #865 — execution-verified against the OOB table); fixed-memory `memory.size`/`memory.grow` (declared-min page count; `grow(0)` ≡ size, `grow(n>0)` → −1 — growth failure is spec-permitted and keeps the static bounds limit sound); direct calls (AAPCS64 + `R_AARCH64_CALL26`, #851); **WASM globals** — `global.get`/`global.set` for i32/i64, i.e. every defined global gets an 8-byte slot in a synth-EMITTED `.data` region (`__synth_globals`) carrying its decoded constant initializer (#851 lane L3); **`call_indirect`** — a synth-EMITTED `.text`-resident funcref table (`__synth_func_table`, one `[u32 structural-class-id][b func_N]` record per slot across all tables, null slots `[0][brk #0]`) with all THREE WASM §4.4.8 trap guards emitted inline: out-of-range index (UNSIGNED bounds compare), null slot, and signature mismatch — compared on STRUCTURAL type class, so duplicate-but-identical types stay interchangeable (#851 lane L3, execution-verified against wasmtime incl. every trap); param HOMING for non-leaf functions (incoming argument registers are stored to stack slots at the prologue, so a param survives a call). **PRECONDITIONS — exactly ONE, and it is not new:** memory-using functions expect `x28` = linear-memory base on entry, and synth emits NO startup or prologue that establishes it (no linker script, no data section); the embedder/harness must set it, and a module carrying **active data segments is REFUSED loudly** (v0.53 — previously the segments were silently dropped and initialized regions read zeros). The globals region and the funcref table are explicitly **NOT** preconditions: synth EMITS both into the object with their contents, and code reaches them via an `adrp` + `add :lo12:` pair that the linker resolves — there is no globals base register and no table base register, so no second ambient input and nothing that can collide with the linear-memory base (the #275/#717 class). Loud declines (mechanically enumerated by the VCR-SEL-005 third-backend oracle): import calls, value-carrying blocks/loops, `br_table`, writing a PARAM local in a LEAF function, `memory.copy`/`fill`, v128/SIMD, multi-memory, `>8` args, float-result callees; and — rather than guess — an imported global, a global with no decoded constant initializer (float/v128/non-const init expr), a non-leaf FLOAT param, a growable imported table, an element segment that is not statically verifiable, and a table slot holding an imported function | +| AArch64 (A64, host-native) | `synth-backend-aarch64` | `cortex-a53` (host-linkable ET_REL, `-b aarch64`) | 185 distinct WASM ops handled by the selector: i32 + i64 integer core incl. `div_s/div_u/rem_s/rem_u` (with the ÷0 + INT_MIN/−1 WASM trap guards), `popcnt`, `select` (branchless `CSEL`/`FCSEL`, all four value types), `drop`/`nop`, `i32.wrap_i64`, `i64.extend_i32_{s,u}`, and the five `extend8/16/32_s` sign extensions (#851 v0.53); scalar f32/f64 incl. domain-guarded trapping float→int truncations, IEEE 754-2019 min/max, copysign, and f64↔i64 reinterpret (#538 milestone 4, #851); full control flow — `block`/`loop`/`if`/`else`/`br`/`br_if`/`return` (#538 cf + #851), plus **`br_table`** as a compare-and-branch chain (`cbz` / `cmp`+`b.eq` per arm, then the default `b`; the index is compared in the W view, so an out-of-range index — including the "negative" i32s that denote huge unsigned values — reaches the DEFAULT exactly as WASM requires, and one table may MIX a backward loop header with forward block ends) and **VALUE-CARRYING `block`/`loop`/`if`** (a reserved reconciliation register per frame that every incoming edge deposits into — `br`/`br_if` at the branch, the then-arm at `else`, the fall-through at `end` — so the frame's result is in ONE register on every path; i32/i64 through `mov x`, f32/f64 through `fmov d`. A `br` to a LOOP label carries the loop's PARAMETERS, not its results, so a `loop (result T)` back-edge reconciles nothing) (VCR-A64-CF-001, #851 — execution-verified against wasmtime over the index lattice and both join edges); non-param locals — zero-init stack slots with copy-semantics get/set/tee (#856); linear-memory `i32`/`i64` load/store incl. all sub-word sign/zero forms, **BOUNDS-CHECKED by default** — an out-of-bounds access traps (`brk`) exactly where wasmtime traps, and `--safety-bounds` selects the strategy (`software` = the enforcing default, `none` = explicit opt-out; `mask`/`mpu` hard-error rather than silently degrading) (#851, #865 — execution-verified against the OOB table); fixed-memory `memory.size`/`memory.grow` (declared-min page count; `grow(0)` ≡ size, `grow(n>0)` → −1 — growth failure is spec-permitted and keeps the static bounds limit sound); direct calls (AAPCS64 + `R_AARCH64_CALL26`, #851); **WASM globals** — `global.get`/`global.set` for i32/i64, i.e. every defined global gets an 8-byte slot in a synth-EMITTED `.data` region (`__synth_globals`) carrying its decoded constant initializer (#851 lane L3); **`call_indirect`** — a synth-EMITTED `.text`-resident funcref table (`__synth_func_table`, one `[u32 structural-class-id][b func_N]` record per slot across all tables, null slots `[0][brk #0]`) with all THREE WASM §4.4.8 trap guards emitted inline: out-of-range index (UNSIGNED bounds compare), null slot, and signature mismatch — compared on STRUCTURAL type class, so duplicate-but-identical types stay interchangeable (#851 lane L3, execution-verified against wasmtime incl. every trap); param HOMING for non-leaf functions (incoming argument registers are stored to stack slots at the prologue, so a param survives a call). **PRECONDITIONS — exactly ONE, and it is not new:** memory-using functions expect `x28` = linear-memory base on entry, and synth emits NO startup or prologue that establishes it (no linker script, no data section); the embedder/harness must set it, and a module carrying **active data segments is REFUSED loudly** (v0.53 — previously the segments were silently dropped and initialized regions read zeros). The globals region and the funcref table are explicitly **NOT** preconditions: synth EMITS both into the object with their contents, and code reaches them via an `adrp` + `add :lo12:` pair that the linker resolves — there is no globals base register and no table base register, so no second ambient input and nothing that can collide with the linear-memory base (the #275/#717 class). Loud declines (mechanically enumerated by the VCR-SEL-005 third-backend oracle): import calls, writing a PARAM local in a LEAF function, `memory.copy`/`fill`, v128/SIMD, multi-memory, `>8` args, float-result callees; the three NAMED residuals of the v0.55 control-flow increment — a `br_table` past 16 targets (the chain is O(n); PC-relative jump-table dispatch is a follow-up), a `br_table` whose targets are VALUE-CARRYING (the flat chain has no per-path edge to deposit a result on), and a block type with PARAMETERS or MULTI-VALUE results (the reconciliation slot is one register); and — rather than guess — an imported global, a global with no decoded constant initializer (float/v128/non-const init expr), a non-leaf FLOAT param, a growable imported table, an element segment that is not statically verifiable, and a table slot holding an imported function | --- @@ -148,7 +148,7 @@ see [coq/STATUS.md](../../coq/STATUS.md) for the per-file matrix. the newly wired ones; exactly 8 asserted a printed verdict or count. Every `wired` oracle now declares a `# ci-checks:` floor that `scripts/oracle_run.py` enforces per run by counting real emulator entries, - wasmtime executions and compilations: **135 oracles assert 295,333 emulator + wasmtime executions and compilations: **136 oracles assert 295,421 emulator entries**, 7 assert a printed count, 9 assert compilations, and 1 (`aarch64_matrix.sh`, a POSIX shell oracle the in-process driver cannot instrument) is itemized as unbindable in `scripts/repro/ORACLE_WIRING.md` diff --git a/scripts/repro/ORACLE_WIRING.md b/scripts/repro/ORACLE_WIRING.md index 6ba6ddc2..94ce3618 100644 --- a/scripts/repro/ORACLE_WIRING.md +++ b/scripts/repro/ORACLE_WIRING.md @@ -306,7 +306,7 @@ whole lane is about. So the counter keeps the name of the thing it counts. | mode | oracles | floor total | |---|---|---| -| `emulations` | **135 oracles** | **295,333 emulator entries** | +| `emulations` | **136 oracles** | **295,421 emulator entries** | | `stdout` | 7 oracles | 458 printed counts | | `compiles` | 9 oracles | 43 compilations | | `none` | **1 oracle** | — | @@ -315,7 +315,7 @@ whole lane is about. So the counter keeps the name of the thing it counts. compilations and printed counts are three different units; one impressive combined figure is precisely the instrument defect #910 is about. -`scripts/oracle_wiring_check.py --min-emulation-floor 295333` enforces the +`scripts/oracle_wiring_check.py --min-emulation-floor 295421` enforces the emulations total, in the **already-required** `Claim Check` job. It shares the driver's header parser by import rather than re-implementing the grammar. Pinned in `claims.yaml` (`SYNTH-ORACLE-CHECK-FLOORS-910`) so the number here, the @@ -365,11 +365,11 @@ so there is no transcription drift between what was proved and what CI runs. ===== BASELINE: wiring gate + floor ratchet ===== STEP EXIT=0 ci-checks compiles 9 scripts, floor total 43 - ci-checks emulations 135 scripts, floor total 295333 + ci-checks emulations 136 scripts, floor total 295421 ci-checks none 1 scripts, floor total 0 ci-checks stdout 7 scripts, floor total 458 oracle-wiring gate is non-vacuous: ... 150 of them wired ... and every wired -oracle declares a check floor (295333 emulator entries asserted across 135 of them). +oracle declares a check floor (295421 emulator entries asserted across 136 of them). ===== BASELINE: one oracle step through the driver ===== STEP EXIT=0 @@ -388,7 +388,7 @@ is a gate that cannot fail, not a passing gate. ===== M2: one floor lowered to 0 -> --min-emulation-floor ratchet ===== STEP EXIT=1 FAIL check-floor RATCHET BROKEN: summed `ci-checks: emulations` floors 294912 < -recorded minimum 295333. An oracle lost execution, or a floor was lowered. +recorded minimum 295421. An oracle lost execution, or a floor was lowered. ===== M3: `# ci-checks:` header deleted -> wiring gate ===== STEP EXIT=1 diff --git a/scripts/repro/aarch64_brtable_blockvals_851.wat b/scripts/repro/aarch64_brtable_blockvals_851.wat new file mode 100644 index 00000000..771e69aa --- /dev/null +++ b/scripts/repro/aarch64_brtable_blockvals_851.wat @@ -0,0 +1,226 @@ +;; VCR-A64-CF-001 (#851) — aarch64 `br_table` + VALUE-CARRYING block/loop/if. +;; +;; Every function here compiled to NOTHING on `-b aarch64` before v0.55 L6: +;; `br_table` had no selector arm at all, and any `(result T)` frame was +;; loud-declined for want of result-register reconciliation. The cases are +;; chosen so a WRONG BRANCH DESTINATION or a wrong reconciliation register +;; changes the RESULT, not merely the schedule — a harness that only checked +;; "it compiled" would be vacuous. +(module + (memory 1) + + ;; ---- br_table: the index lattice ------------------------------------ + ;; Classic dense switch. Index 0/1/2 pick distinct constants; ANY other + ;; index (including the huge unsigned values the "negative" i32s denote) + ;; falls to the default arm. The at-bound (3) and over-bound cases are what + ;; a signed compare or an off-by-one chain would get wrong. + (func (export "switch3") (param i32) (result i32) + (block $d + (block $c2 + (block $c1 + (block $c0 + (br_table $c0 $c1 $c2 $d (local.get 0))) + (return (i32.const 100))) + (return (i32.const 200))) + (return (i32.const 300))) + (i32.const 999)) + + ;; Default-ONLY table (zero targets): every index must reach the default. + ;; The degenerate chain — a bare `b` with no compare at all. + (func (export "default_only") (param i32) (result i32) + (block $d + (br_table $d (local.get 0))) + (i32.const 42)) + + ;; DUPLICATE depths in one table: entries 0 and 2 share a destination. + ;; A chain that de-duplicated or reordered compares would break the + ;; index->arm mapping. + (func (export "dup_targets") (param i32) (result i32) + (block $d + (block $b + (block $a + (br_table $a $b $a $d (local.get 0))) + (return (i32.const 11))) + (return (i32.const 22))) + (i32.const 33)) + + ;; MIXED destinations in ONE table, DEFAULT = the backward edge. Depth 1 is + ;; the enclosing LOOP header (BACKWARD, resolved eagerly to a negative + ;; offset) and depth 0 a block END (FORWARD, patched at `end`). A lowering + ;; that assumed one direction emits a wrong offset for the other. The trip + ;; count is data-dependent, so a wrong offset changes the result. + (func (export "table_loop_default_back") (param i32) (result i32) + (local $n i32) (local $steps i32) + (local.set $n (local.get 0)) + (block $out + (loop $again + (local.set $steps (i32.add (local.get $steps) (i32.const 1))) + (local.set $n (i32.sub (local.get $n) (i32.const 1))) + ;; index 0 -> $out (exit); anything else -> default $again (loop). + (br_table $out $again (i32.gt_s (local.get $n) (i32.const 0))))) + (local.get $steps)) + + ;; Same, but TARGET 0 is the backward edge — the `cbz` form of the chain's + ;; first entry, resolved eagerly against the loop header. + (func (export "table_loop_target0_back") (param i32) (result i32) + (local $n i32) (local $steps i32) + (local.set $n (local.get 0)) + (block $out + (loop $again + (local.set $steps (i32.add (local.get $steps) (i32.const 1))) + (local.set $n (i32.sub (local.get $n) (i32.const 1))) + ;; index 0 -> $again (loop); index 1 -> default $out (exit). + (br_table $again $out (i32.le_s (local.get $n) (i32.const 0))))) + (local.get $steps)) + + ;; A table at exactly BR_TABLE_MAX_TARGETS (16 targets + default) — the + ;; boundary the >16 decline is measured against. It must LOWER and be right + ;; on every arm, including the last compare in the chain. + (func (export "switch16") (param i32) (result i32) + (block $d + (block $p15 (block $p14 (block $p13 (block $p12 + (block $p11 (block $p10 (block $p9 (block $p8 + (block $p7 (block $p6 (block $p5 (block $p4 + (block $p3 (block $p2 (block $p1 (block $p0 + (br_table $p0 $p1 $p2 $p3 $p4 $p5 $p6 $p7 $p8 $p9 + $p10 $p11 $p12 $p13 $p14 $p15 $d (local.get 0))) + (return (i32.const 0))) (return (i32.const 1))) + (return (i32.const 2))) (return (i32.const 3))) + (return (i32.const 4))) (return (i32.const 5))) + (return (i32.const 6))) (return (i32.const 7))) + (return (i32.const 8))) (return (i32.const 9))) + (return (i32.const 10))) (return (i32.const 11))) + (return (i32.const 12))) (return (i32.const 13))) + (return (i32.const 14))) (return (i32.const 15))) + (i32.const -1)) + + ;; br_table guarding a TRAP: index 0 falls into `unreachable`. A dispatch + ;; that landed on the wrong arm would return a value where wasmtime traps. + (func (export "table_trap") (param i32) (result i32) + (block $ok + (block $bad + (br_table $bad $ok $ok (local.get 0))) + (unreachable)) + (i32.const 7)) + + ;; ---- value-carrying block / if / loop -------------------------------- + ;; TWO edges into one join: the `br_if` edge carries `a`, the fall-through + ;; carries `b`. Both must land in the SAME register or the result is + ;; path-dependent — the exact defect the old decline was protecting. + (func (export "block_two_edges") (param i32 i32 i32) (result i32) + (i32.add + (block (result i32) + (br_if 0 (local.get 1) (local.get 0)) + (drop) + (local.get 2)) + (i32.const 1000))) + + ;; A value-carrying block whose branch comes from a NESTED frame (depth 1), + ;; so the reconciliation must target the OUTER frame's register. + (func (export "block_nested_br") (param i32 i32) (result i32) + (block (result i32) + (block + (br_if 0 (i32.eqz (local.get 0))) + (br 1 (local.get 1))) + (i32.const -5))) + + ;; Value-producing if/else: the then-arm deposits at `else`, the else-arm at + ;; `end`. Both arms must reach the join in one register. + (func (export "if_value") (param i32 i32 i32) (result i32) + (if (result i32) (local.get 0) + (then (i32.mul (local.get 1) (i32.const 3))) + (else (i32.sub (local.get 2) (i32.const 7))))) + + ;; VALUE-CARRYING LOOP — the soundness-critical shape. A `br` to a loop + ;; label targets the HEADER and carries the loop's PARAMETERS (none here), + ;; NOT its result. An implementation that reconciled on the back-edge would + ;; stamp a garbage value into the result register every iteration; here the + ;; loop runs a data-dependent number of times before falling through with + ;; its value, so that bug changes the RESULT. + (func (export "loop_value") (param i32) (result i32) + (local $i i32) (local $acc i32) + (loop (result i32) + (local.set $acc (i32.add (local.get $acc) (local.get $i))) + (local.set $i (i32.add (local.get $i) (i32.const 1))) + (br_if 0 (i32.lt_u (local.get $i) (local.get 0))) + (i32.mul (local.get $acc) (i32.const 2)))) + + ;; A value-carrying block nested INSIDE a value-carrying loop: two live + ;; reservations at once, which is where a single shared slot register would + ;; collide. + (func (export "nested_value_frames") (param i32) (result i32) + (local $i i32) (local $acc i32) + (loop (result i32) + (local.set $acc + (i32.add (local.get $acc) + (block (result i32) + (br_if 0 (i32.const 1) (i32.and (local.get $i) (i32.const 1))) + (drop) + (i32.const 10)))) + (local.set $i (i32.add (local.get $i) (i32.const 1))) + (br_if 0 (i32.lt_u (local.get $i) (local.get 0))) + (local.get $acc))) + + ;; i64 result through the reconciliation register (the `mov x` width claim). + (func (export "block_i64") (param i32 i64 i64) (result i64) + (block (result i64) + (br_if 0 (local.get 1) (local.get 0)) + (drop) + (local.get 2))) + + ;; f64 result through the reconciliation register (`fmov d`). The FP file is + ;; reserved separately, and the f32 case below proves the 64-bit move keeps + ;; a single-precision pattern intact. + (func (export "block_f64") (param i32 f64 f64) (result f64) + (block (result f64) + (br_if 0 (local.get 1) (local.get 0)) + (drop) + (local.get 2))) + + (func (export "block_f32") (param i32 f32 f32) (result f32) + (block (result f32) + (br_if 0 (local.get 1) (local.get 0)) + (drop) + (local.get 2))) + + ;; A value-carrying block whose reconciled value came from LINEAR MEMORY, + ;; so the slot register must not collide with the address/base temps. + (func (export "block_from_memory") (param i32) (result i32) + (i32.store (i32.const 16) (i32.const 0x5A5A)) + (i32.store (i32.const 32) (i32.const 0x1234)) + (block (result i32) + (br_if 0 (i32.load (i32.const 16)) (local.get 0)) + (drop) + (i32.load (i32.const 32)))) + + ;; A value-carrying block reached ONLY through the branch (the fall-through + ;; is `unreachable`) — proves the join reads the branch's deposit and that a + ;; dead fall-through does not corrupt it. + (func (export "block_branch_only") (param i32) (result i32) + (block (result i32) + (br_if 0 (i32.const 77) (local.get 0)) + (unreachable))) + + ;; ---- a CALL inside a value-carrying frame ---------------------------- + ;; The one soundness claim in `reconcile_into` that nothing else here + ;; executes: `bl` CLOBBERS the caller-saved x9..x15 pool the reconciliation + ;; slot lives in. The claim is that this is harmless, because a branch that + ;; deposited into the slot has ALREADY transferred control — so on any path + ;; that reaches the `bl`, the slot's value is dead and the fall-through + ;; re-writes it. Cond nonzero takes the branch (the `bl` never runs and the + ;; deposited 7 must survive); cond zero runs the call (the clobber must be + ;; invisible). These shapes also force the HOMED-PARAM path (non-leaf + + ;; reads a param), which no other value-carrying case here touches. + (func $three (result i32) (i32.const 3)) + + (func (export "block_over_call") (param i32) (result i32) + (block (result i32) + (br_if 0 (i32.const 7) (local.get 0)) + (drop) + (call $three))) + + ;; Same property across the `else` deposit rather than the `end` one. + (func (export "if_value_over_call") (param i32) (result i32) + (if (result i32) (local.get 0) + (then (i32.const 7)) + (else (call $three))))) diff --git a/scripts/repro/aarch64_brtable_blockvals_851_differential.py b/scripts/repro/aarch64_brtable_blockvals_851_differential.py new file mode 100644 index 00000000..9199b124 --- /dev/null +++ b/scripts/repro/aarch64_brtable_blockvals_851_differential.py @@ -0,0 +1,481 @@ +#!/usr/bin/env python3 +# ci-status: wired +# ci-checks: emulations >= 88 +"""VCR-A64-CF-001 (#851) — aarch64 `br_table` + VALUE-CARRYING block/loop/if. + +Both constructs used to compile to NOTHING on `-b aarch64`: `br_table` had no +selector arm, and any `(result T)` frame was loud-declined for want of +result-register reconciliation. This harness proves the new lowering EXECUTES +bit-identically to wasmtime. + +WHAT MAKES IT NON-VACUOUS. + + * `br_table` is a compare-and-branch CHAIN, so a wrong destination is a wrong + RESULT, not a slower one. The index lattice is walked per table: every + in-range arm, the index exactly AT the bound, one OVER it, and 0xFFFFFFFF — + the case a SIGNED compare would send to the wrong arm, since WASM reads the + index UNSIGNED and everything out of range must reach the DEFAULT. + * Two tables put the enclosing LOOP HEADER in the table — once as the default + (backward) and once as target 0 (the eager `cbz` form) — mixed with a + forward block end in the SAME table. A lowering that assumed one branch + direction emits a wrong offset for the other, and the trip count is + data-dependent, so it shows up as a wrong count. + * A table at exactly BR_TABLE_MAX_TARGETS (16) walks the whole chain, + including its last compare. + * A `br_table` arm that falls into `unreachable` gives a TRAP case: a + dispatch landing on the wrong arm returns a value where wasmtime traps. + * For the value-carrying frames, every function is driven down BOTH edges of + its join (the `br_if` edge and the fall-through), so a lowering that + reconciled only one of them returns the other path's register. + * `loop_value` is the SOUNDNESS-CRITICAL shape: a `br` to a LOOP label + carries the loop's PARAMETERS, not its results, so the back-edge must + reconcile NOTHING. An implementation that treated "the frame has a result" + as "reconcile on every branch to it" stamps a garbage value into the result + register each iteration — which this test's data-dependent trip counts turn + into a wrong answer. + * i64 / f64 / f32 results go through the same slot, proving the `mov x` / + `fmov d` width claims (an f32 carried through the 64-bit FP move must keep + its single-precision bit pattern). + * `block_over_call` / `if_value_over_call` put a `bl` INSIDE a value-carrying + frame. That is the one soundness claim in `reconcile_into` — a call cannot + clobber a live reconciliation slot — that nothing else here executes, and + `bl` really does clobber the caller-saved x9..x15 pool the slot lives in. + Cond nonzero takes the branch (the call never runs, the deposited 7 must + survive); cond zero runs the call (the clobber must be invisible, because + the deposited value is dead on that path). These shapes also force the + HOMED-PARAM path, which no other value-carrying case touches. The harness + APPLIES the `R_AARCH64_CALL26` relocations itself — see `load()` — so the + emitted relocation is part of what is checked rather than a hang. + +Two oracles: unicorn (UC_ARCH_ARM64, FPEN enabled) always, and — on an arm64 +host — NATIVE execution in a forked child, where an expected `brk #0` is +observed by the parent as SIGTRAP. Memory-using functions run under unicorn +only (the `x28` linear-memory base cannot be established through ctypes). + +Run (needs wasmtime + unicorn + pyelftools; native path needs an arm64 host): + SYNTH=/debug/synth python scripts/repro/aarch64_brtable_blockvals_851_differential.py +""" + +import ctypes +import math +import os +import platform +import signal +import struct +import subprocess +import sys +from pathlib import Path + +import wasmtime +from elftools.elf.elffile import ELFFile +from unicorn import UC_ARCH_ARM64, UC_MODE_ARM, Uc, UcError +from unicorn.arm64_const import ( + UC_ARM64_REG_CPACR_EL1, + UC_ARM64_REG_D0, + UC_ARM64_REG_LR, + UC_ARM64_REG_S0, + UC_ARM64_REG_SP, + UC_ARM64_REG_V0, + UC_ARM64_REG_V1, + UC_ARM64_REG_W0, + UC_ARM64_REG_X0, + UC_ARM64_REG_X1, + UC_ARM64_REG_X2, + UC_ARM64_REG_X28, +) + +WAT = Path(__file__).with_name("aarch64_brtable_blockvals_851.wat") +SYNTH = os.environ.get("SYNTH", "./target/debug/synth") +CODE, STK, RET = 0x100000, 0x200000, 0x300000 +LINMEM, LINMEM_SIZE = 0x1000000, 0x20000 +X_ARGS = [UC_ARM64_REG_X0, UC_ARM64_REG_X1, UC_ARM64_REG_X2] +V_ARGS = [UC_ARM64_REG_V0, UC_ARM64_REG_V1] + +M32 = (1 << 32) - 1 +M64 = (1 << 64) - 1 +TRAP = "TRAP" + +# fn -> ([param types], result type). AAPCS64 assigns integer and float args +# from INDEPENDENT counters, which the runners below mirror. +SIGS = { + "switch3": (["i32"], "i32"), + "default_only": (["i32"], "i32"), + "dup_targets": (["i32"], "i32"), + "table_loop_default_back": (["i32"], "i32"), + "table_loop_target0_back": (["i32"], "i32"), + "switch16": (["i32"], "i32"), + "table_trap": (["i32"], "i32"), + "block_two_edges": (["i32", "i32", "i32"], "i32"), + "block_nested_br": (["i32", "i32"], "i32"), + "if_value": (["i32", "i32", "i32"], "i32"), + "loop_value": (["i32"], "i32"), + "nested_value_frames": (["i32"], "i32"), + "block_i64": (["i32", "i64", "i64"], "i64"), + "block_f64": (["i32", "f64", "f64"], "f64"), + "block_f32": (["i32", "f32", "f32"], "f32"), + "block_from_memory": (["i32"], "i32"), + "block_branch_only": (["i32"], "i32"), + "block_over_call": (["i32"], "i32"), + "if_value_over_call": (["i32"], "i32"), +} + +# Functions that read/write linear memory: unicorn only (x28 precondition). +MEM_FNS = {"block_from_memory"} + +# The index lattice every table is walked over. 0..n-1 are the real arms; n is +# exactly AT the bound; n+1 is over it; 0xFFFFFFFF is the unsigned-index case a +# SIGNED compare chain would mis-dispatch. +CASES = [] +for i in [0, 1, 2, 3, 4, 0xFFFFFFFF, 0x80000000, 0x7FFFFFFF]: + CASES.append(("switch3", [i])) + CASES.append(("default_only", [i])) + CASES.append(("dup_targets", [i])) + CASES.append(("table_trap", [i])) +for i in [0, 1, 7, 8, 15, 16, 17, 0xFFFFFFFF, 0x80000000]: + CASES.append(("switch16", [i])) +# Loop-carrying tables: 0 (immediate exit), 1, and multi-iteration counts. +for n in [0, 1, 2, 5, 37, 0xFFFFFFFF]: + CASES.append(("table_loop_default_back", [n])) + CASES.append(("table_loop_target0_back", [n])) +# Value-carrying frames — BOTH edges of every join. +CASES += [ + ("block_two_edges", [1, 7, 9]), # br_if taken -> 7 + 1000 + ("block_two_edges", [0, 7, 9]), # fall-through -> 9 + 1000 + ("block_two_edges", [0xFFFFFFFF, 3, 4]), # any nonzero cond + ("block_nested_br", [0, 55]), # inner br_if taken -> -5 + ("block_nested_br", [1, 55]), # br 1 (depth-1) -> 55 + ("if_value", [1, 5, 100]), # then-arm -> 15 + ("if_value", [0, 5, 100]), # else-arm -> 93 + ("if_value", [0x80000000, 5, 100]), # nonzero high bit -> then + ("loop_value", [0]), # loop body runs once (do-while) + ("loop_value", [1]), + ("loop_value", [5]), + ("loop_value", [100]), + ("nested_value_frames", [0]), + ("nested_value_frames", [1]), + ("nested_value_frames", [2]), + ("nested_value_frames", [9]), + ("block_i64", [1, 0x0123456789ABCDEF, 7]), + ("block_i64", [0, 0x0123456789ABCDEF, 7]), + ("block_i64", [0, 1, 0xFFFFFFFFFFFFFFFF]), + ("block_f64", [1, 1.5, -2.25]), + ("block_f64", [0, 1.5, -2.25]), + ("block_f64", [0, 1.5, float("nan")]), + ("block_f64", [1, -0.0, 3.0]), + ("block_f32", [1, 1.5, -2.25]), + ("block_f32", [0, 1.5, -2.25]), + ("block_f32", [1, -0.0, 3.0]), + ("block_f32", [0, 2.0, float("inf")]), + ("block_from_memory", [1]), + ("block_from_memory", [0]), + ("block_branch_only", [1]), # branch edge -> 77 + ("block_branch_only", [0]), # fall-through is `unreachable` + # A `bl` inside a value-carrying frame clobbers the caller-saved temp pool + # the slot lives in. Cond nonzero -> the branch's 7 must survive (the call + # never runs); cond zero -> the call's 3 must come back (the clobber must + # be invisible, because the deposited value is dead on that path). + ("block_over_call", [1]), + ("block_over_call", [0]), + ("if_value_over_call", [1]), + ("if_value_over_call", [0]), +] + + +# --------------------------------------------------------------------------- # +def as_signed(ty, v): + if ty == "i32": + return struct.unpack("float converts, -;; trapping i64-target truncations). With the SCALAR float surface complete, the -;; test now targets a float construct that DELIBERATELY stays declined: a -;; VALUE-CARRYING (f32-result) `block`. +;; trapping i32 truncations + min/max + copysign, v0.54 L2 (#851) the last four +;; scalar-float classes (rounding, f32/f64 load/store, i64->float converts, +;; trapping i64-target truncations), and v0.55 L6 (VCR-A64-CF-001) the +;; VALUE-CARRYING (f32-result) `block` this fixture used to target — that shape +;; now LOWERS (the reconciliation register carries an f32 through `fmov d`) and +;; is execution-verified in aarch64_brtable_blockvals_851_differential.py. +;; +;; The target therefore moves again, to a float construct that DELIBERATELY +;; stays declined: a NON-LEAF function that reads an f32 PARAMETER. Float params +;; arrive in v0..v7, which a `bl` clobbers, so a non-leaf must HOME them to +;; stack slots — and this encoder has no FP store for the v-register file, so +;; the shape loud-declines rather than read a clobbered register. ;; ;; It is fully DECODED — no upstream drop masks it — so it reaches the aarch64 -;; SELECTOR, which must loud-decline (a value-carrying block needs result- -;; register reconciliation across the branch). That is the strongest form of the -;; honesty check. `i32add` is the control: a supported op that must still -;; compile. +;; SELECTOR, which must loud-decline. That is the strongest form of the honesty +;; check. `i32add` is the control: a supported op that must still compile. (module - (func (export "f32block") (param f32) (result f32) - (block (result f32) (local.get 0))) + (func $twice (param f32) (result f32) + (f32.add (local.get 0) (local.get 0))) + (func (export "f32nonleaf") (param f32) (result f32) + (call $twice (local.get 0))) (func (export "i32add") (param i32 i32) (result i32) (i32.add (local.get 0) (local.get 1)))) diff --git a/scripts/repro/aarch64_m2_decline_538.py b/scripts/repro/aarch64_m2_decline_538.py index bfdde92d..6b3eb0be 100755 --- a/scripts/repro/aarch64_m2_decline_538.py +++ b/scripts/repro/aarch64_m2_decline_538.py @@ -42,16 +42,39 @@ # lanes' pre-merge copies of this list were stale in OPPOSITE # directions — asserting a decline for a capability that now ships is # the same doc-honesty defect as claiming one that does not. - ("br_table", '(func (export "f") (param i32) (result i32) ' - '(block (block (br_table 0 1 (local.get 0))) ' - '(return (i32.const 1))) (i32.const 2))'), + # + # v0.55 L6 (VCR-A64-CF-001) moved `br_table` and the VALUE-CARRYING + # `block (result f32)` off this list. Note what REPLACED them: not + # nothing, but the NARROWER residuals below. A partial lowering that + # deleted its entry outright would be claiming more than it ships. + # v0.55 L6 (VCR-A64-CF-001): `br_table` and the VALUE-CARRYING + # `block`/`loop`/`if` moved OFF this list — both now lower and are + # execution-verified in aarch64_brtable_blockvals_851_differential.py. What + # is LEFT of each is a narrower, named residual, and it stays here: + ("br_table past the compare-chain threshold (>16 targets)", + '(func (export "f") (param i32) (result i32) ' + # 17 TARGETS (+ a trailing default label) — one past BR_TABLE_MAX_TARGETS. + '(block (block (br_table 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 (local.get 0))) ' + '(return (i32.const 1))) (i32.const 2))', + "exceeds the aarch64 compare-chain threshold"), + ("br_table with VALUE-CARRYING targets", + '(func (export "f") (param i32) (result i32) ' + '(block (result i32) (i32.const 7) (local.get 0) ' + '(br_table 0 0 (local.get 0))))', + "VALUE-CARRYING targets"), + ("block with PARAMETERS (multi-value)", + '(func (export "f") (param i32) (result i32) ' + '(local.get 0) (block (param i32) (result i32) (i32.const 1) (i32.add)))', + "PARAMETER-taking block type"), + ("block with MULTI-VALUE results", + '(func (export "f") (param i32) (result i32) ' + '(block (result i32 i32) (i32.const 1) (i32.const 2)) (i32.add))', + "MULTI-VALUE result block type"), ("local.set on a param", '(func (export "f") (param i32) (result i32) ' '(local.set 0 (i32.add (local.get 0) (i32.const 1))) (local.get 0))'), ("memory.fill", '(memory 1)(func (export "f") ' '(memory.fill (i32.const 0) (i32.const 0) (i32.const 4)))'), - ("block (result f32)", '(func (export "f") (param f32) (result f32) ' - '(block (result f32) (local.get 0)))'), ("f32x4.add", '(func (export "f") (param f32) (result f32) ' '(f32x4.extract_lane 0 (f32x4.add ' '(f32x4.splat (local.get 0)) (f32x4.splat (local.get 0)))))'), diff --git a/scripts/templates/feature_matrix.md.tmpl b/scripts/templates/feature_matrix.md.tmpl index a410ca1e..b2a1a4df 100644 --- a/scripts/templates/feature_matrix.md.tmpl +++ b/scripts/templates/feature_matrix.md.tmpl @@ -33,7 +33,7 @@ soundness feature, not an absence. | ARM Thumb-2 (primary) | `synth-backend` | `cortex-m3`, `cortex-m4`, `cortex-m4f`, `cortex-m7`, `cortex-m7dp` (+ `cortex-m55` experimental MVE) | i32 + i64 (register pairs) complete; scalar f32/f64 via VFP on FPU targets; control flow (block/loop/if/br/br_table); memory incl. sub-word; direct calls; `call_indirect` in both relocatable and self-contained `--cortex-m` images (v0.47, #275) | | ARM A32 | `synth-backend` | `cortex-r5` | i32 + i64 integer family (221-variant no-wildcard tripwire, #615); self-contained `call_indirect` declines loudly (no flash-table builder) | | RISC-V RV32IMAC | `synth-backend-riscv` | `rv32imac`, `rv32imc`, `rv32im`, `rv32i`, `rv32gc`, `esp32c3` | i32 + i64 integer ops, control flow, calls incl. `call_indirect`, memory loads/stores; relocatable ELF; import/external calls emit `R_RISCV_CALL_PLT` relocations (`.rela.text`, undefined import symbols — #871) with exact-arity marshalling from the module signature tables; >8-arg / i64-arg / multi-value calls decline loudly; floats decline loudly | -| AArch64 (A64, host-native) | `synth-backend-aarch64` | `cortex-a53` (host-linkable ET_REL, `-b aarch64`) | {{aarch64_selector_ops}} distinct WASM ops handled by the selector: i32 + i64 integer core incl. `div_s/div_u/rem_s/rem_u` (with the ÷0 + INT_MIN/−1 WASM trap guards), `popcnt`, `select` (branchless `CSEL`/`FCSEL`, all four value types), `drop`/`nop`, `i32.wrap_i64`, `i64.extend_i32_{s,u}`, and the five `extend8/16/32_s` sign extensions (#851 v0.53); scalar f32/f64 incl. domain-guarded trapping float→int truncations, IEEE 754-2019 min/max, copysign, and f64↔i64 reinterpret (#538 milestone 4, #851); full control flow — `block`/`loop`/`if`/`else`/`br`/`br_if`/`return` (#538 cf + #851); non-param locals — zero-init stack slots with copy-semantics get/set/tee (#856); linear-memory `i32`/`i64` load/store incl. all sub-word sign/zero forms, **BOUNDS-CHECKED by default** — an out-of-bounds access traps (`brk`) exactly where wasmtime traps, and `--safety-bounds` selects the strategy (`software` = the enforcing default, `none` = explicit opt-out; `mask`/`mpu` hard-error rather than silently degrading) (#851, #865 — execution-verified against the OOB table); fixed-memory `memory.size`/`memory.grow` (declared-min page count; `grow(0)` ≡ size, `grow(n>0)` → −1 — growth failure is spec-permitted and keeps the static bounds limit sound); direct calls (AAPCS64 + `R_AARCH64_CALL26`, #851); **WASM globals** — `global.get`/`global.set` for i32/i64, i.e. every defined global gets an 8-byte slot in a synth-EMITTED `.data` region (`__synth_globals`) carrying its decoded constant initializer (#851 lane L3); **`call_indirect`** — a synth-EMITTED `.text`-resident funcref table (`__synth_func_table`, one `[u32 structural-class-id][b func_N]` record per slot across all tables, null slots `[0][brk #0]`) with all THREE WASM §4.4.8 trap guards emitted inline: out-of-range index (UNSIGNED bounds compare), null slot, and signature mismatch — compared on STRUCTURAL type class, so duplicate-but-identical types stay interchangeable (#851 lane L3, execution-verified against wasmtime incl. every trap); param HOMING for non-leaf functions (incoming argument registers are stored to stack slots at the prologue, so a param survives a call). **PRECONDITIONS — exactly ONE, and it is not new:** memory-using functions expect `x28` = linear-memory base on entry, and synth emits NO startup or prologue that establishes it (no linker script, no data section); the embedder/harness must set it, and a module carrying **active data segments is REFUSED loudly** (v0.53 — previously the segments were silently dropped and initialized regions read zeros). The globals region and the funcref table are explicitly **NOT** preconditions: synth EMITS both into the object with their contents, and code reaches them via an `adrp` + `add :lo12:` pair that the linker resolves — there is no globals base register and no table base register, so no second ambient input and nothing that can collide with the linear-memory base (the #275/#717 class). Loud declines (mechanically enumerated by the VCR-SEL-005 third-backend oracle): import calls, value-carrying blocks/loops, `br_table`, writing a PARAM local in a LEAF function, `memory.copy`/`fill`, v128/SIMD, multi-memory, `>8` args, float-result callees; and — rather than guess — an imported global, a global with no decoded constant initializer (float/v128/non-const init expr), a non-leaf FLOAT param, a growable imported table, an element segment that is not statically verifiable, and a table slot holding an imported function | +| AArch64 (A64, host-native) | `synth-backend-aarch64` | `cortex-a53` (host-linkable ET_REL, `-b aarch64`) | {{aarch64_selector_ops}} distinct WASM ops handled by the selector: i32 + i64 integer core incl. `div_s/div_u/rem_s/rem_u` (with the ÷0 + INT_MIN/−1 WASM trap guards), `popcnt`, `select` (branchless `CSEL`/`FCSEL`, all four value types), `drop`/`nop`, `i32.wrap_i64`, `i64.extend_i32_{s,u}`, and the five `extend8/16/32_s` sign extensions (#851 v0.53); scalar f32/f64 incl. domain-guarded trapping float→int truncations, IEEE 754-2019 min/max, copysign, and f64↔i64 reinterpret (#538 milestone 4, #851); full control flow — `block`/`loop`/`if`/`else`/`br`/`br_if`/`return` (#538 cf + #851), plus **`br_table`** as a compare-and-branch chain (`cbz` / `cmp`+`b.eq` per arm, then the default `b`; the index is compared in the W view, so an out-of-range index — including the "negative" i32s that denote huge unsigned values — reaches the DEFAULT exactly as WASM requires, and one table may MIX a backward loop header with forward block ends) and **VALUE-CARRYING `block`/`loop`/`if`** (a reserved reconciliation register per frame that every incoming edge deposits into — `br`/`br_if` at the branch, the then-arm at `else`, the fall-through at `end` — so the frame's result is in ONE register on every path; i32/i64 through `mov x`, f32/f64 through `fmov d`. A `br` to a LOOP label carries the loop's PARAMETERS, not its results, so a `loop (result T)` back-edge reconciles nothing) (VCR-A64-CF-001, #851 — execution-verified against wasmtime over the index lattice and both join edges); non-param locals — zero-init stack slots with copy-semantics get/set/tee (#856); linear-memory `i32`/`i64` load/store incl. all sub-word sign/zero forms, **BOUNDS-CHECKED by default** — an out-of-bounds access traps (`brk`) exactly where wasmtime traps, and `--safety-bounds` selects the strategy (`software` = the enforcing default, `none` = explicit opt-out; `mask`/`mpu` hard-error rather than silently degrading) (#851, #865 — execution-verified against the OOB table); fixed-memory `memory.size`/`memory.grow` (declared-min page count; `grow(0)` ≡ size, `grow(n>0)` → −1 — growth failure is spec-permitted and keeps the static bounds limit sound); direct calls (AAPCS64 + `R_AARCH64_CALL26`, #851); **WASM globals** — `global.get`/`global.set` for i32/i64, i.e. every defined global gets an 8-byte slot in a synth-EMITTED `.data` region (`__synth_globals`) carrying its decoded constant initializer (#851 lane L3); **`call_indirect`** — a synth-EMITTED `.text`-resident funcref table (`__synth_func_table`, one `[u32 structural-class-id][b func_N]` record per slot across all tables, null slots `[0][brk #0]`) with all THREE WASM §4.4.8 trap guards emitted inline: out-of-range index (UNSIGNED bounds compare), null slot, and signature mismatch — compared on STRUCTURAL type class, so duplicate-but-identical types stay interchangeable (#851 lane L3, execution-verified against wasmtime incl. every trap); param HOMING for non-leaf functions (incoming argument registers are stored to stack slots at the prologue, so a param survives a call). **PRECONDITIONS — exactly ONE, and it is not new:** memory-using functions expect `x28` = linear-memory base on entry, and synth emits NO startup or prologue that establishes it (no linker script, no data section); the embedder/harness must set it, and a module carrying **active data segments is REFUSED loudly** (v0.53 — previously the segments were silently dropped and initialized regions read zeros). The globals region and the funcref table are explicitly **NOT** preconditions: synth EMITS both into the object with their contents, and code reaches them via an `adrp` + `add :lo12:` pair that the linker resolves — there is no globals base register and no table base register, so no second ambient input and nothing that can collide with the linear-memory base (the #275/#717 class). Loud declines (mechanically enumerated by the VCR-SEL-005 third-backend oracle): import calls, writing a PARAM local in a LEAF function, `memory.copy`/`fill`, v128/SIMD, multi-memory, `>8` args, float-result callees; the three NAMED residuals of the v0.55 control-flow increment — a `br_table` past 16 targets (the chain is O(n); PC-relative jump-table dispatch is a follow-up), a `br_table` whose targets are VALUE-CARRYING (the flat chain has no per-path edge to deposit a result on), and a block type with PARAMETERS or MULTI-VALUE results (the reconciliation slot is one register); and — rather than guess — an imported global, a global with no decoded constant initializer (float/v128/non-const init expr), a non-leaf FLOAT param, a growable imported table, an element segment that is not statically verifiable, and a table slot holding an imported function | --- @@ -148,7 +148,7 @@ see [coq/STATUS.md](../../coq/STATUS.md) for the per-file matrix. the newly wired ones; exactly 8 asserted a printed verdict or count. Every `wired` oracle now declares a `# ci-checks:` floor that `scripts/oracle_run.py` enforces per run by counting real emulator entries, - wasmtime executions and compilations: **135 oracles assert 295,333 emulator + wasmtime executions and compilations: **136 oracles assert 295,421 emulator entries**, 7 assert a printed count, 9 assert compilations, and 1 (`aarch64_matrix.sh`, a POSIX shell oracle the in-process driver cannot instrument) is itemized as unbindable in `scripts/repro/ORACLE_WIRING.md`