feat(#815): VCR-RA-003 RV32 register-allocation validator (RV32 analogue of the ARM gate)#821
Merged
Merged
Conversation
…gue of the ARM gate) Port the ARM-only VCR-RA-003 allocation validator to RISC-V as a PARALLEL re-implementation keyed on the RV32 calling convention — not a reuse of the ARM-coupled validate_final_allocation. New: synth_backend_riscv::alloc_validator::validate_final_allocation_rv32 (RaFinalVerdict / RaFinalViolation), wired UNCONDITIONALLY in backend.rs (compile_function_with_opts, on the selector's `selection.ops`) — runs on every RV32 compile in the default --features riscv build, hard-errors on a Violation. Two STRAIGHT-LINE invariants (#815): 1. Callee-saved preservation — a body write (op_dest) of an s-register the pass saves (s1, s2..s10 = is_callee_saved_temp; reserved s0/fp + s11/linmem-base excluded so the checker never false-positives on the pass's own output) must be saved by the prologue `sw s_k, off(sp)` + restored by every epilogue `lw s_k, off(sp)` before a `ret` -> CalleeSavedNotSaved/NotRestored. 2. Spill-slot non-aliasing — a frame slot `off(sp)` overwritten while its value is still reloaded downstream, per straight-line segment (an `addi sp` frame adjust resets the map) -> SpillSlotAliased. A `Call` (the ARM phase-2 across-call/across-join frontier, no RV CFG yet) is a NON-FATAL NotAttempted (decline > guess). DELIBERATELY no ARM-style "unmodeled-op -> force-prologue" fail-safe: on RV every op_dest==None op is CF/system/label/call (writes no s-register), so it would be vacuous AND disagree with the pass -> false-positive. RED-FIRST non-vacuity (8 ra003rv_* unit tests): 3 RED revert a known-fixed clobber and assert the CATCH; 4 GREEN assert SILENT; 1 asserts a Violation before a Call still fires. SILENT-ON-REAL-CODEGEN: frozen RV32 oracle 10/10 (control_step 0x00210A55 byte-identical) + a dedicated repro sweeping 9 fixtures x {relocatable, default} = 18 pairs, 0 false positives. CI-gated: vcr-ra-003-rv32-alloc-validator-gate (red-first + frozen + repro). Roadmap VCR-RA-003 updated (RV32 arm landed). Rivet-clean (0 non-xref errors). Closes #815. Refs #242. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
… boundary Advisor follow-ups on the VCR-RA-003 RV32 lane: - Fix rustdoc broken-intra-doc-link warnings in alloc_validator.rs (private `op_dest` link + stale `op_reads` reference -> plain text). - Document the store-side false-negative boundary: the `saved`-set scan counts any `sw s_k, off(sp)` as a prologue save, so a hypothetical BODY spill of a callee-saved temp would mask a clobber (FN < FP, the checker-safe direction). NOT reachable on current selector output — RV has no Belady/spill-realloc body spilling; `preserve_callee_saved` (the prologue) is the only s-register frame store, and the selector declines rather than body-spills. Named so it is visible if cross-call spilling is wired for RV later. - CI frozen step runs the full `frozen_codegen_bytes` suite (was rv32-filtered), matching the sibling ARM gate. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
Codecov Report❌ Patch coverage is
📢 Thoughts on this report? Let us know! |
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
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
Ports the ARM-only VCR-RA-003 register-allocation validator (#808,
synth_synthesis::liveness::validate_final_allocation) to RISC-V as a parallel re-implementation keyed on the RV32 calling convention. Closes #815. Refs #242 (epic VCR-*).New module
synth_backend_riscv::alloc_validator::validate_final_allocation_rv32(its ownRaFinalVerdict/RaFinalViolationin the riscv crate), wired unconditionally inbackend.rs(compile_function_with_opts, on the selector'sselection.opsimmediately after selection) — runs on every RV32 compile in the default--features riscvbuild (NOT behind--features verify; the #757 dormant-in-shipping lesson) and hard-errors the compile on aViolation.Not a reuse of the ARM validator: RV32 has a different instruction enum (
RiscVOp), a different callee-saved set, a differentaddi sp,sp,-N+sw s_k, off(sp)prologue shape, and noreg_effect— the invariants are ported, not the code.RV32-ABI invariants (the two STRAIGHT-LINE invariants #815 names)
op_dest) of an s-register the pass saves —s1,s2..s10=is_callee_saved_temp, mirroringpreserve_callee_savedexactly; the reserveds0/fp +s11/linmem-base are excluded so the checker never false-positives on the pass's own output — must be saved by a prologuesw s_k, off(sp)and restored by every epiloguelw s_k, off(sp)before aret(jalr x0,0(ra)) →CalleeSavedNotSaved/CalleeSavedNotRestored.off(sp)overwritten by a secondswwhile its value is still reloaded downstream →SpillSlotAliased. Anaddi spframe adjust resets the slot map (the RV analogue of ARM'sldr sp,[sp,#N]clear).What loud-flags NotAttempted (decline > guess)
A
Callis the ARM phase-2 across-call/across-join frontier, which rests oncfg_liveness/check_join_availabilitymachinery that does not exist for RV. Rather than half-implement a second-backend soundness checker, a function containing aCallyields a NON-FATALNotAttempted { reason: "rv32-call-boundary" }— the two straight-line invariants still ran and held. Deliberately no ARM-style "unmodeled-op → force-prologue" fail-safe: on RV everyop_dest==Noneop is CF/system/label/call (writes no s-register), so it would be vacuous AND disagree with the pass → a false-positive; omitting it keeps validator↔pass agreement.Red-first evidence (non-vacuity proven BEFORE trusting)
cargo test -p synth-backend-riscv --lib ra003rv— 8 tests:ra003rv_red_missing_callee_saved_prologue_is_caught(clobber a used s2 with no prologue save →CalleeSavedNotSaved),ra003rv_red_epilogue_drops_saved_register_is_caught(drop thelw s2restore →CalleeSavedNotRestored),ra003rv_red_spill_slot_aliasing_is_caught(alias two live values on slot 4 →SpillSlotAliased).Call→NotAttempted.ra003rv_violation_before_call_still_fires— a straight-line Violation before aCallis not masked by the decline.0 false positives on real RV32 codegen
cargo test -p synth-cli --test frozen_codegen_bytes— 10/10,frozen_fixtures_rv32_text_is_bit_identical_oracle_001compiles control_step (0x00210A55) + signed_div_const through the unconditional validator, byte-identical. The validator emits nothing → RV32.textunchanged.scripts/repro/vcr_ra_003_rv32_alloc_validator.py— 9 fixtures × {relocatable, default} = 18 pairs, 0 false positives (callee-saved-heavy control_step/controller_step, spill-heavy gust_kernel, branchy flight_seam, call-bearing reachable_helper).Documented boundaries (false-negatives, never false-positives)
saved-set scan counts anysw s_k, off(sp)as a prologue save. A hypothetical BODY spill of a callee-saved temp would mask a genuine unsaved clobber (FN < FP, the checker-safe direction — exactly as the ARM validator excludes R0/R1 across a call). NOT reachable on current selector output: RV has no Belady / spill-realloc body spilling (preserve_callee_saved, the prologue, is the only s-register frame store; the selector declines rather than body-spills when it cannot allocate). Named in the module doc so it is re-examined if cross-call spilling is wired for RV later.compile_modulevalidatesselection.opsfromcompile_function_with_opts; the shipped ELF carries the stream from a separatecompile_to_riscv_opscall — both run the identical deterministic selector with the samecfg+opts+ops, so the streams are byte-identical (validating one validates the other).compile_functionreaches the validated path directly.Gate + housekeeping
vcr-ra-003-rv32-alloc-validator-gatejob (red-first unit tests + full frozen suite + the silent-on-real repro).VCR-RA-003updated (the promised RV32 arm landed)..textbyte-identical).cargo test --workspacegreen, clippy-D warningsclean, fmt clean,claim_check25/25, rivet 0 non-xref errors.Cover targets: qemu_riscv32 / ESP32-C3.
🤖 Generated with Claude Code
https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L