From ec8f2452bd4e0ae1eb7a7710ed9636d1c9cbff52 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 5 Aug 2026 18:07:52 +0200 Subject: [PATCH 1/4] =?UTF-8?q?docs(#851):=20rivet=20VCR-A64-CF-001=20+=20?= =?UTF-8?q?SWVER-022=20=E2=80=94=20aarch64=20br=5Ftable=20+=20value-carryi?= =?UTF-8?q?ng=20CF?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit STEP 1 of v0.55 lane L6: the traceability artifact BEFORE the code, so the requirement states what must hold and the verification artifact states what proves it — rather than being retrofitted onto a landed diff. VCR-A64-CF-001 (sw-req, derives-from VCR-001, traces-to VCR-SEL-005) names the two largest entries in the mechanically-derived aarch64 decline complement: `br_table` (declined outright) and value-carrying `block`/`loop`/`if` (the #509 result-register-reconciliation class). It pins the SOUNDNESS-CRITICAL distinction up front — a `br` to a `loop` carries the loop's PARAMETER count, not its result count, so a `loop (result i32)` must NOT reconcile on its back-edge — and it names the residuals that stay declined (>16 targets, value-carrying br_table targets, block params, multi-value) rather than promising a coverage the lowering will not have. SWVER-022 (sw-verification, verifies VCR-A64-CF-001) states the both-directions evidence: a wasmtime-vs-unicorn/native execution differential over the br_table index lattice (default arm, at-bound, over-bound, 0xFFFFFFFF, mixed loop/block targets) plus the value-carrying loop back-edge, with a trap case so the harness cannot collapse to all-values; and the decline-honesty half pinned by name in `br_table_subshape_asymmetry_882`. `rivet validate` unchanged at the pre-existing baseline (52 errors, 104 warnings — none of them new); `--explain VCR-A64-CF-001` reports no diagnostics and both traceability rules satisfied. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- artifacts/sw-verification.yaml | 47 ++++++++++++ artifacts/verified-codegen-roadmap.yaml | 96 +++++++++++++++++++++++++ 2 files changed, 143 insertions(+) diff --git a/artifacts/sw-verification.yaml b/artifacts/sw-verification.yaml index 1aa0cf09..06205510 100644 --- a/artifacts/sw-verification.yaml +++ b/artifacts/sw-verification.yaml @@ -533,3 +533,50 @@ artifacts: via pop2_i64 / VI64) + coq/Synth/WASM/WasmCertBridge.v (six i64_*_exec_refines_wasmcert theorems, +6 Qed → 591 total); frozen 10/10 confirms the semantics-model change does not alter compiled bytes + + - id: SWVER-022 + 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 b26214df..a5d47c61 100644 --- a/artifacts/verified-codegen-roadmap.yaml +++ b/artifacts/verified-codegen-roadmap.yaml @@ -613,6 +613,102 @@ artifacts: surfacing the real i32.rotl gap once its ledger entry is removed, and the gate is 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) # --------------------------------------------------------------------------- From c7e26301b181141f23ac4fd69a4e62bd0447943e Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 5 Aug 2026 18:35:33 +0200 Subject: [PATCH 2/4] feat(#851): aarch64 br_table + VALUE-CARRYING block/loop/if (VCR-A64-CF-001) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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`. Selector goes 184 -> 185 ops. BR_TABLE lowers as a compare-and-branch CHAIN — `cbz w_idx, L0` for entry 0, `cmp w_idx, #i` + `b.eq L_i` per further entry, then an unconditional `b L_default`. Deliberately the same construction #882 chose for RV32, so the two backends stay reviewable against each other. The compares are the W view, so the UNSIGNED index rule holds 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 (resolved eagerly to a negative offset) with forward block ends (patched at `End`), because the chain dispatches on the TARGET FRAME's kind exactly as `br`/`br_if` already do. `patch_branch` grows a fourth placeholder kind (`b.`, 0x54…), rebuilt directly so the condition field survives the patch. VALUE-CARRYING FRAMES get a reserved reconciliation register pair (one GP, one FP — the arity side-table carries COUNTS only, so the result's register file is unknown at frame entry) withheld from the temp allocator for the frame's whole extent. Every edge into the join deposits there: `br`/`br_if` at the branch, the then-arm at `else`, the fall-through at `end`. i32/i64 ride `mov x`, f32/f64 ride `fmov d` (the same width argument `epilogue` already relies on). Two things were got right BY CONSTRUCTION rather than by test, and both are silent miscompiles if wrong: * 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 reconciles NOTHING. The frame carries `label_arity` SEPARATELY from `result_arity` and branch reconciliation is driven off the former; treating "the frame has a result" as "reconcile on every branch to it" stamps a garbage value into the result register every iteration. * The reservation is a BITMASK, 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 is out of reach of every whole-stack consumer, and `epilogue(stack.last())` can never return a reservation. The four scratch-allocation sites that bypass `alloc_temp` (copysign, divrem, popcnt, memory.grow) consult it too. `reconcile_into` documents why no clobber window exists: the slot is reserved, so the move never destroys a live operand; and every write is IMMEDIATELY followed by the transfer to the join, so not even a `bl` (which clobbers the caller-saved x9..x15 pool) runs in between. On any other path the written value is dead and is re-written before that path reaches the join. THREE NAMED RESIDUALS replace two blanket declines — partial coverage with named gaps, not a claim that cannot be backed: * `br_table` past BR_TABLE_MAX_TARGETS (16 — the same threshold RV32 uses; the chain is O(n), PC-relative jump-table dispatch is the follow-up); * `br_table` with VALUE-CARRYING targets (the flat chain has no per-path edge to deposit a result on — refused conservatively when any targeted frame, default included, has non-zero label arity or a different entry height); * a block type with PARAMETERS or MULTI-VALUE results (the slot is ONE register). LEDGERS, both directions, same commit as the lowering: * the `br_table` whole-op entry is DELETED from `aarch64_known_divergences()` — the stale-entry check is what forced it — and the ledger's own "leaving the SEVEN below" prose is corrected to FOUR; * `br_table_subshape_asymmetry_882` grows an aarch64 leg pinning all three residuals BY NAME (via a new `aarch64_decline_reason`, so a bare `is_err()` from an unrelated probe artifact cannot satisfy the claim) AND asserting positively that a `(0,1)` value-carrying block now LOWERS, so the claim cannot quietly widen back into "typed blocks decline"; * `aarch64_m2_decline_538.py` swaps its `br_table` and `block (result f32)` entries for the three narrower residuals; * `feature_matrix.md.tmpl` states the capability and the residuals (the generated FEATURE_MATRIX + status.json are regenerated by the script, 185). The #554 float-honesty fixture MOVES again: it targeted a value-carrying f32-result block, which now lowers, so it re-points at a float construct that genuinely still declines — a NON-LEAF function reading an f32 parameter. EVIDENCE. `aarch64_brtable_blockvals_851_differential.py` (new, CI-wired with `set -euo pipefail` + non-zero counts in BOTH outcome classes): 84 checks over 17 exported functions vs 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 — plus a table at exactly 16 targets, a table mixing loop and block targets in both orders, a `br_table` arm falling into a trap, and both join edges of every value-carrying frame. NON-VACUITY BY MUTATION, not assertion: * taking the join position BEFORE the fall-through's reconciliation move (so forward branches land ON it) -> 16 checks red; * an off-by-one in the chain constants -> 22 red, incl. switch16(16); * `result_arity` where `label_arity` belongs -> `loop_value` and `nested_value_frames` fail to compile at all. FROZEN-SAFE: 13 of the 14 aarch64 repro fixtures compile BYTE-IDENTICALLY to a v0.54.0 build; the one that differs is `aarch64_f32_unsupported_554`, and it differs exactly because its declined function now lowers. ARM/RV32 goldens 10/10. All 16 aarch64 CI oracles green; `cargo fmt --check`, `clippy --workspace --all-targets -D warnings` and `cargo test --workspace` all exit 0. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .github/workflows/ci.yml | 27 + CHANGELOG.md | 63 ++ artifacts/status.json | 2 +- crates/synth-backend-aarch64/src/backend.rs | 9 +- crates/synth-backend-aarch64/src/selector.rs | 800 ++++++++++++++++-- .../tests/cross_backend_op_parity.rs | 135 ++- .../tests/aarch64_f32_loudskip_554.rs | 24 +- docs/status/FEATURE_MATRIX.md | 2 +- .../repro/aarch64_brtable_blockvals_851.wat | 202 +++++ ...ch64_brtable_blockvals_851_differential.py | 411 +++++++++ scripts/repro/aarch64_f32_unsupported_554.wat | 29 +- scripts/repro/aarch64_m2_decline_538.py | 33 +- scripts/templates/feature_matrix.md.tmpl | 2 +- 13 files changed, 1612 insertions(+), 127 deletions(-) create mode 100644 scripts/repro/aarch64_brtable_blockvals_851.wat create mode 100644 scripts/repro/aarch64_brtable_blockvals_851_differential.py diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index b6069e16..003b44d9 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -588,6 +588,33 @@ 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. + # + # 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. + run: | + set -euo pipefail + SYNTH=./target/debug/synth \ + python 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 + 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/repro/aarch64_m2_decline_538.py diff --git a/CHANGELOG.md b/CHANGELOG.md index c77dba86..8232888b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,6 +7,69 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ## [Unreleased] +### 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. + +### 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). + +### Verified + +- `scripts/repro/aarch64_brtable_blockvals_851_differential.py` (CI-wired): 84 + checks over 17 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. + 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. + ## [0.54.0] - 2026-08-05 **"Close what we measured."** v0.53 built the instruments; this release acts on 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/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 30b79449..13f3ed30 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.) /// @@ -914,17 +937,25 @@ 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 -/// the SEVEN 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`]. 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 \ @@ -1947,6 +1978,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, @@ -2032,4 +2072,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 dd21747c..9da3908a 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 | --- diff --git a/scripts/repro/aarch64_brtable_blockvals_851.wat b/scripts/repro/aarch64_brtable_blockvals_851.wat new file mode 100644 index 00000000..1976ce68 --- /dev/null +++ b/scripts/repro/aarch64_brtable_blockvals_851.wat @@ -0,0 +1,202 @@ +;; 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)))) 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..8aee9719 --- /dev/null +++ b/scripts/repro/aarch64_brtable_blockvals_851_differential.py @@ -0,0 +1,411 @@ +#!/usr/bin/env python3 +# ci-status: wired +"""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). + +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"), +} + +# 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` +] + + +# --------------------------------------------------------------------------- # +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 c8d8e671..a4494e2b 100755 --- a/scripts/repro/aarch64_m2_decline_538.py +++ b/scripts/repro/aarch64_m2_decline_538.py @@ -41,16 +41,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 a7d99938..c28799cd 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 | --- From 6eb5929d3ff5dfa8fbe97761040d7f14dda9f80d Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 5 Aug 2026 18:52:16 +0200 Subject: [PATCH 3/4] =?UTF-8?q?test(#851):=20put=20a=20`bl`=20inside=20a?= =?UTF-8?q?=20value-carrying=20frame=20=E2=80=94=20the=20one=20unexecuted?= =?UTF-8?q?=20claim?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `reconcile_into` documents that a call cannot clobber a live reconciliation slot, even though `bl` clobbers the caller-saved x9..x15 pool the slot lives in. Nothing in the suite executed that claim: no case had a `call` inside a value-carrying frame. It was the only documented soundness property in this change with no oracle behind it. Two cases close it. `block_over_call` deposits 7 on the `br_if` edge and calls `$three` on the fall-through; `if_value_over_call` does the same across the `else` deposit rather than the `end` one. Cond nonzero -> the branch's 7 must survive (the `bl` 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). Both shapes also force the HOMED-PARAM path (non-leaf + reads a param), which no other value-carrying case here touches. The first attempt HUNG rather than failed, which is worth recording: `bl func_N` is emitted as a placeholder plus an `R_AARCH64_CALL26` a linker would resolve, so executing the object unlinked makes every call branch to ITSELF. `load()` now APPLIES those relocations — which also turns the emitted relocation into part of what this oracle checks — and the count is asserted non-zero in the summary line and in CI, because if the relocations vanished the calls would silently become self-branches and the clobber claim would go untested while the gate stayed green. The native forked child also gets a `signal.alarm(20)` so a runaway branch FAILS instead of hanging the parent: a gate that never reports is worse than a red one. 84 -> 88 checks, 17 -> 19 exported functions, 2 direct-call relocations applied. Verdict unchanged: PASS. Every CI grep assertion in the new step was re-verified locally against the real log. Also ran gale's `aarch64_matrix.sh` acceptance gate (the separate `aarch64-native-matrix` job, which auto-flips declined->verified the day a lowering lands, so this change is exactly such a day): 61 ops, 355 native checks, empty declined frontier, exit 0 — unchanged, no op flipped unexpectedly. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .github/workflows/ci.yml | 11 ++- CHANGELOG.md | 10 ++- .../repro/aarch64_brtable_blockvals_851.wat | 26 ++++++- ...ch64_brtable_blockvals_851_differential.py | 77 ++++++++++++++++++- 4 files changed, 114 insertions(+), 10 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 003b44d9..99a672ba 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -597,14 +597,20 @@ jobs: # 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. + # 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. + # 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 \ @@ -612,6 +618,7 @@ jobs: | 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 ] diff --git a/CHANGELOG.md b/CHANGELOG.md index 8232888b..2b316136 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -52,13 +52,17 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ### Verified -- `scripts/repro/aarch64_brtable_blockvals_851_differential.py` (CI-wired): 84 - checks over 17 exported functions against wasmtime, under unicorn AND +- `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. + 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 diff --git a/scripts/repro/aarch64_brtable_blockvals_851.wat b/scripts/repro/aarch64_brtable_blockvals_851.wat index 1976ce68..771e69aa 100644 --- a/scripts/repro/aarch64_brtable_blockvals_851.wat +++ b/scripts/repro/aarch64_brtable_blockvals_851.wat @@ -199,4 +199,28 @@ (func (export "block_branch_only") (param i32) (result i32) (block (result i32) (br_if 0 (i32.const 77) (local.get 0)) - (unreachable)))) + (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 index 8aee9719..d0d73be3 100644 --- a/scripts/repro/aarch64_brtable_blockvals_851_differential.py +++ b/scripts/repro/aarch64_brtable_blockvals_851_differential.py @@ -35,6 +35,16 @@ * 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 @@ -104,6 +114,8 @@ "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). @@ -157,6 +169,14 @@ ("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]), ] @@ -218,17 +238,51 @@ def compile_aarch64(out): sys.exit(f"aarch64 compile failed/skipped: {r.stderr}") +R_AARCH64_JUMP26 = 282 +R_AARCH64_CALL26 = 283 + + def load(elf): + """Read `.text` + the symtab, and APPLY the direct-call relocations. + + `bl func_N` is emitted as a placeholder word plus an `R_AARCH64_CALL26` + that a linker would normally resolve. Executing the object unlinked would + make every call branch to ITSELF — an infinite loop, which HANGS rather + than fails, so the harness would report nothing at all. Resolving them here + also means the emitted relocation is part of what this oracle checks: a + wrong offset or addend lands the call somewhere else and changes the + result. The displacement is PC-relative, so patching against the section's + own addresses is load-address independent. + """ f = ELFFile(open(elf, "rb")) text = f.get_section_by_name(".text") - code, base = text.data(), text["sh_addr"] + code, base = bytearray(text.data()), text["sh_addr"] + symtab = None syms = {} for sec in f.iter_sections(): if sec.header.sh_type == "SHT_SYMTAB": + symtab = sec for sy in sec.iter_symbols(): if sy.name: syms[sy.name] = sy["st_value"] & ~1 - return code, base, syms + + rela = f.get_section_by_name(".rela.text") + applied = 0 + if rela is not None and symtab is not None: + for r in rela.iter_relocations(): + rtype = r["r_info_type"] + if rtype not in (R_AARCH64_CALL26, R_AARCH64_JUMP26): + sys.exit(f"unhandled .text relocation type {rtype} — this " + f"harness only knows the direct-call forms") + sym = symtab.get_symbol(r["r_info_sym"]) + target = sym["st_value"] + r["r_addend"] + site = base + r["r_offset"] + i = r["r_offset"] - base + w = int.from_bytes(code[i:i + 4], "little") + w = (w & ~0x03FFFFFF) | (((target - site) // 4) & 0x03FFFFFF) + code[i:i + 4] = w.to_bytes(4, "little") + applied += 1 + return bytes(code), base, syms, applied def unicorn_run(code, base, faddr, sig, args): @@ -312,6 +366,11 @@ def native_run(code, faddr, code_base, sig, args): if pid == 0: try: os.close(rd) + # A wrong branch destination can loop forever; without this the + # parent's waitpid would HANG (a gate that never reports is worse + # than a red one). SIGALRM kills the child and surfaces as an + # unexpected signal. + signal.alarm(20) base_addr = native_setup(code) fn = ctypes.CFUNCTYPE(_CTY[ret], *[_CTY[t] for t in types])( base_addr + (faddr - code_base) @@ -337,7 +396,7 @@ def native_run(code, faddr, code_base, sig, args): def main(): out = "/tmp/aarch64_brtable_blockvals_851.o" compile_aarch64(out) - code, base, syms = load(out) + code, base, syms, relocs_applied = load(out) host_native = platform.machine() in ("arm64", "aarch64") fails = 0 @@ -395,9 +454,19 @@ def main(): if total < 60: print(f"VACUOUS: only {total} checks ran; the case lattice shrank") fails += 1 + if relocs_applied < 2: + # The `bl` inside a value-carrying frame is the ONLY thing exercising + # `reconcile_into`'s "a call cannot clobber a live slot" claim. If its + # relocation vanished, the calls would be self-branches and the claim + # would go untested while the gate stayed green. + print(f"VACUOUS: only {relocs_applied} direct-call relocations applied " + f"— the call-inside-a-value-carrying-frame cases stopped " + f"exercising a real `bl`") + fails += 1 print(f"\n{total} checks ({trap_cases} trap, {value_cases} value) across " - f"{len(seen_fns)} exported functions, " + f"{len(seen_fns)} exported functions " + f"[{relocs_applied} direct-call relocations applied], " f"{'arm64 host + unicorn' if host_native else 'unicorn-only host'}") print("RESULT:", "PASS — aarch64 br_table (index lattice incl. default / " "at-bound / over-bound / unsigned 0xFFFFFFFF, mixed loop+block " From e80421a7b754b348640c58253163e7391c6f2fba Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 5 Aug 2026 18:56:01 +0200 Subject: [PATCH 4/4] docs(#851): de-stale the aarch64 CI job comment's decline list MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The `aarch64` job's header comment still described the decline-matrix probe as asserting `br_table`, globals, `call_indirect` and value-carrying blocks — all four of which now SHIP (v0.54 L3 and this lane). A comment is not a gate, but this is the exact doc-honesty defect the v0.54 fan-in hit from the other direction, and it sits directly above the step whose whole purpose is decline honesty. Rewritten to name the narrower residue the probe actually asserts today, with the rule that an entry leaves the list the day its lowering lands. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .github/workflows/ci.yml | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 99a672ba..8bbfe7e9 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -475,9 +475,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