fix(arm): optimized path declines br_table to the direct selector (#507, #242)#508
Merged
Merged
Conversation
…, #242) On the optimized (non-`--relocatable`) path, `synth compile` SILENTLY miscompiled `br_table`: the dispatch is dropped during the wasm→IR lowering (`optimize_full`), so `ir_to_arm` emitted the arm bodies in fall-through sequence with no `cmp`/branch on the selector — the selector value isn't even loaded, so every input hits the last arm (exit 0, no warning, violating the #180/#185 Ok-or-Err contract). The `--relocatable` direct path lowered the identical module correctly, so gust and the shipped falcon firmware (both `--relocatable`) were unaffected — this was an optimized-path-only hazard. Because the dispatch is dropped BEFORE `ir_to_arm`, there's no `Err` to fall back on. The fix detects `br_table` on the raw wasm op stream in `arm_backend` and forces the direct selector (`select_with_stack`), which lowers it as a real cmp-chain. Same decline-to-direct shape as #496 / issue-#120: honest degradation, the function compiles correctly without IR-level optimization. The declined output is byte-identical to `--no-optimize`. Frozen-safe by construction: the frozen byte gate compiles `--relocatable` (already direct), and no optimized-path fixture (control_step, flight_algo) contains `br_table`, so they stay on the optimized path bit-identically. Gated by scripts/repro/br_table_507_differential.py (CI: br-table-507-oracle): two table shapes (sequential, shared-tail) × every selector incl. out-of-range, compiled via the DEFAULT optimized path, execute bit-identically to wasmtime; pre-fix every non-last selector mismatched. Unit test test_507_br_table_declines_to_direct asserts the optimized-default bytes equal the direct selector's. Frozen bit-identical; control_step (13/13), r12-spill-496, stack-args-503, block-brif-483 oracles all green. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
avrabe
added a commit
that referenced
this pull request
Jun 26, 2026
… the #509 negative result (#242) (#510) Appends a dated slice to VCR-ORACLE-001's history covering the 2026-06-26 second arc: #496 (R12-exhaustion decline-to-direct, PR #502), #503 (AAPCS stack-arg cap-lift, shipped v0.16.0, PR #504), #507 (optimized-path br_table decline, PR #508), each with its new CI execution oracle (r12-spill-496, stack-args-503, br-table-507). Most importantly it records #509 as a LOAD-BEARING NEGATIVE RESULT so the decline-to-direct shortcut is not re-attempted: the direct selector (the shipped --relocatable path) drops the carried value of a value-returning br/br_if/ br_table-direct, and the shortcut cannot fix it because the IR carries no block-result arity (WasmOp::Block is a unit variant) — a non-empty-vstack decline can't distinguish a carried result from an unwound void-target value, so it over-refuses valid code. This is the sharpest evidence yet for VCR-SEL-001's selector-collapse motivation (the hand-written selectors lack the structured block-arity model a verified DSL carries by construction); the real fix is arity-threading, cross-cutting and silicon-gated. Docs-only, behavior-frozen by construction: frozen byte gate bit-identical; rivet validate non-xref ERROR count 0 (unchanged 49/75/0 baseline). Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
On the optimized (non-
--relocatable) path,synth compilesilently miscompiled voidbr_table: the dispatch is dropped during the wasm→IR lowering (optimize_full), soir_to_armemitted the arm bodies in fall-through sequence with nocmp/branch on the selector — every input hit the last arm. Exit 0, no warning (#180/#185 Ok-or-Err violation).The
--relocatabledirect path lowered the void dispatch correctly, so gust and the shipped falcon firmware were unaffected for that shape (gale #507).Fix
Because the dispatch is dropped before
ir_to_arm, there's noErrto fall back on. The fix detectsbr_tableon the raw wasm op stream inarm_backendand forces the direct selector, which lowers the void dispatch as a real cmp-chain. Same decline-to-direct shape as #496 / issue-#120. The declined output is byte-identical to--no-optimize.Frozen-safe by construction: the frozen gate compiles
--relocatable(already direct), and no optimized-path fixture (control_step, flight_algo) containsbr_table.Scope — important
This fixes the void / dispatch-only
br_tableshape (gale'sseqandshared-tailrepros). While gating it, declining to the direct selector exposed that the direct selector also mishandles value-returningbr_table(abr <label> (value)to a block-with-result drops the carried value) — a separate, deeper bug that affects the shipped--relocatablepath too, filed as #509. My decline does not fix that (it declines to the broken direct selector).So this Addresses #507 (the void/dispatch case) but does not close it — #507 stays open until value-returning br_table is correct on the optimized path, which requires #509 (direct-selector value-carry) first.
Gate
scripts/repro/br_table_507_differential.py(CIbr-table-507-oracle): two void table shapes (sequential, shared-tail) × every selector incl. out-of-range, via the default optimized path, execute bit-identically to wasmtime. Non-vacuity: pre-fix every non-last selector mismatched. Unit testtest_507_br_table_declines_to_directasserts optimized-default bytes == direct selector. (Value-returning is intentionally NOT in this oracle — it's #509, currently red on both paths.)Verification
br-table-507-oracle: 12/12 PASS post-fix; 12/12 FAIL pre-fix.synth-backendsuite (205) green.cargo fmt --check,clippy -D warningsclean.Same family as the closed #483/#496 and open #500. Addresses #507 (void/dispatch); value-returning tracked in #509.
🤖 Generated with Claude Code