RV32 br_table lowering + hard-error on target/backend ISA mismatch (#882) - #887
Merged
Conversation
…ckend ISA mismatch (#882) Item A: RV32 br_table lowers as a compare-and-branch chain (entry 0 vs x0, li+beq per entry, jal to default); >16 targets and value-carrying tables (#509 class) LOUD-DECLINE by name. Unit tests cover gale's exact shape, threshold, value-carrying, out-of-range depth, loop head targets. Item B: --target riscv32 with the defaulted arm backend used to silently print 'Using backend: arm' and build Thumb into a RISC-V ELF container. resolve_target_spec now hard-errors on any single-ISA backend/target family mismatch, lists the explicit backend's accepted targets, and from_triple's unknown-target error names the FULL valid set. CLI gate: crates/synth-cli/tests/unknown_target_882.rs. Plus: rv32_br_table_882.wat fixture, unicorn-vs-wasmtime differential (vacuity-guarded), rv32-br-table-oracle CI job, CHANGELOG. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…get-882 # Conflicts: # CHANGELOG.md
…b-shape residual (#882) RV32 now lowers br_table (#882), so the op-level known-divergence entry ("RV32 selector has no BrTable arm") is STALE and the parity gate correctly demanded it be closed. Deleted. But br_table is not ONE shape and the RV32 lowering is deliberately PARTIAL, so deleting the whole-op entry alone would erase a real residual from the gate. Measured 2026-07-29 on the real backends: probed shape (<=16 targets, non-value-carrying) arm=ok rv32=ok 17 targets arm=ok rv32=BrTableTooLarge value-carrying (#509) arm=ok rv32=BrTableValueCarrying Both residuals are now asserted BY NAME in br_table_subshape_asymmetry_882, pinning the DECLINE REASON (not a bare is_err(), which a stack-underflow artifact would satisfy vacuously) and failing in BOTH directions like the ledger: if RV32 later lands the jump table or #509 arity threading, the test goes red and the claim must be deleted. Honest read recorded in the test: arm=ok means "the ARM selector returns Ok", NOT "ARM is verified correct on that shape" — ARM shares the #509 limitation on Br/BrIf and performs no value-carrying check. This is a CAPABILITY asymmetry, not a correctness verdict on ARM. No wildcard added, no op moved to StructurallyExcluded, gate not weakened. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
The refusal read "--target cortex-a53 is a AArch64 target". The family names
are a closed set, so pick the article by lookup rather than a vowel heuristic
("an ARM" is right, "an RISC-V" is not).
Verified by running the built CLI, not just the unit tests:
--target riscv32 -> exit 1, "is a RISC-V target", names `-b riscv`
--target cortex-a53 -> exit 1, "is an AArch64 target", names `-b aarch64`
--target totally-bogus-cpu -> exit 1, names the FULL valid set
--target cortex-m3 -b riscv-> exit 1, lists riscv's accepted targets
None print "Using backend: arm"; all 9 good target/backend pairings still
compile and select the expected backend.
Co-Authored-By: Claude <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
Codecov Report❌ Patch coverage is
📢 Thoughts on this report? Let us know! |
Conflict: #886 changed target_label_for_depth to `&mut self` (it now DEFINES the frame label rather than just naming it — the 'undefined label Lend0' root cause) at the exact point this branch inserted lower_br_table. Kept both: this branch's br_table lowering AND #886's new signature. Not merely compatible — complementary: every br_table target label is handed out by target_label_for_depth, so #886's fix is what guarantees those labels are actually defined when a table branches past a mid-function return. Re-verified the MERGED tree (real exit codes, not `| tail && echo OK`): cargo fmt --all -- --check 0 cargo clippy --workspace --all-targets -D 0 cargo test --workspace --no-fail-fast 0 (130 bins, 2582 passed, 0 failed) scripts/claim_check.py claims.yaml 0 rv32_br_table_882_differential.py PASS (27 vectors, 0 failures) CLI: riscv32 / cortex-a53 / bogus all exit 1, none print "Using backend"; all good target/backend pairings still exit 0 Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
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.
v0.53 lane L3, both halves:
(a)
BrTablecompare-chain lowering — the last gap betweenwdg-thinand a complete RV32 lowering.(b) an unknown
--target(e.g. the invalidriscv32) previously silently selectedUsing backend: armand failed downstream. Now a hard error naming the valid list — silent wrong-backend selection is a soundness papercut.Refs #882. Lane hit the session limit before final self-report; coordinator gating on CI.