Skip to content

feat(#815): VCR-RA-003 RV32 register-allocation validator (RV32 analogue of the ARM gate)#821

Merged
avrabe merged 2 commits into
mainfrom
feat/50-rv32-alloc-validator
Jul 18, 2026
Merged

feat(#815): VCR-RA-003 RV32 register-allocation validator (RV32 analogue of the ARM gate)#821
avrabe merged 2 commits into
mainfrom
feat/50-rv32-alloc-validator

Conversation

@avrabe

@avrabe avrabe commented Jul 17, 2026

Copy link
Copy Markdown
Contributor

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 own RaFinalVerdict / RaFinalViolation in the riscv crate), wired unconditionally in backend.rs (compile_function_with_opts, on the selector's selection.ops immediately after selection) — runs on every RV32 compile in the default --features riscv build (NOT behind --features verify; the #757 dormant-in-shipping lesson) and hard-errors the compile on a Violation.

Not a reuse of the ARM validator: RV32 has a different instruction enum (RiscVOp), a different callee-saved set, a different addi sp,sp,-N + sw s_k, off(sp) prologue shape, and no reg_effect — the invariants are ported, not the code.

RV32-ABI invariants (the two STRAIGHT-LINE invariants #815 names)

  1. Callee-saved preservation. A body write (op_dest) of an s-register the pass saves — s1, s2..s10 = is_callee_saved_temp, mirroring preserve_callee_saved exactly; the reserved s0/fp + s11/linmem-base are excluded so the checker never false-positives on the pass's own output — must be saved by a prologue sw s_k, off(sp) and restored by every epilogue lw s_k, off(sp) before a ret (jalr x0,0(ra)) → CalleeSavedNotSaved / CalleeSavedNotRestored.
  2. Spill-slot non-aliasing. Per straight-line segment (same holder model as the ARM validator), a frame slot off(sp) overwritten by a second sw while its value is still reloaded downstream → SpillSlotAliased. An addi sp frame adjust resets the slot map (the RV analogue of ARM's ldr sp,[sp,#N] clear).

What loud-flags NotAttempted (decline > guess)

A Call is the ARM phase-2 across-call/across-join frontier, which rests on cfg_liveness/check_join_availability machinery that does not exist for RV. Rather than half-implement a second-backend soundness checker, a function containing a Call yields a NON-FATAL NotAttempted { 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 every op_dest==None op 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:

  • RED (catches the bug): 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 the lw s2 restore → CalleeSavedNotRestored), ra003rv_red_spill_slot_aliasing_is_caught (alias two live values on slot 4 → SpillSlotAliased).
  • GREEN (silent on correct): balanced save/use/restore leaf; pure-scratch t0/a0 leaf; sequential single-slot reuse; a CallNotAttempted.
  • Guard: ra003rv_violation_before_call_still_fires — a straight-line Violation before a Call is not masked by the decline.

0 false positives on real RV32 codegen

  • Frozen RV32 oracle: cargo test -p synth-cli --test frozen_codegen_bytes — 10/10, frozen_fixtures_rv32_text_is_bit_identical_oracle_001 compiles control_step (0x00210A55) + signed_div_const through the unconditional validator, byte-identical. The validator emits nothing → RV32 .text unchanged.
  • Dedicated sweep: 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)

  • Store-side saved-set scan counts any sw 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.
  • Re-derived stream. compile_module validates selection.ops from compile_function_with_opts; the shipped ELF carries the stream from a separate compile_to_riscv_ops call — both run the identical deterministic selector with the same cfg+opts+ops, so the streams are byte-identical (validating one validates the other). compile_function reaches the validated path directly.

Gate + housekeeping

  • CI: new vcr-ra-003-rv32-alloc-validator-gate job (red-first unit tests + full frozen suite + the silent-on-real repro).
  • Roadmap VCR-RA-003 updated (the promised RV32 arm landed).
  • Frozen-safe (RV32 .text byte-identical). cargo test --workspace green, clippy -D warnings clean, fmt clean, claim_check 25/25, rivet 0 non-xref errors.

Cover targets: qemu_riscv32 / ESP32-C3.

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

avrabe and others added 2 commits July 17, 2026 17:53
…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

codecov Bot commented Jul 17, 2026

Copy link
Copy Markdown

Codecov Report

❌ Patch coverage is 96.00000% with 14 lines in your changes missing coverage. Please review.

Files with missing lines Patch % Lines
crates/synth-backend-riscv/src/backend.rs 27.77% 13 Missing ⚠️
crates/synth-backend-riscv/src/alloc_validator.rs 99.69% 1 Missing ⚠️

📢 Thoughts on this report? Let us know!

@avrabe
avrabe merged commit 7b04efd into main Jul 18, 2026
44 checks passed
@avrabe
avrabe deleted the feat/50-rv32-alloc-validator branch July 18, 2026 11:16
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

VCR-RA-003: RV32 callee-saved / spill-slot allocation validator (RV32 analogue of the ARM-only liveness gate)

1 participant