diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 7235d36c..1aa8dc34 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -1686,6 +1686,62 @@ jobs: cargo build -p synth-cli python3 scripts/repro/vcr_ra_003_phase2_join_call.py ./target/debug/synth + vcr-ra-003-rv32-alloc-validator-gate: + name: "VCR-RA-003 RV32 register-allocation validator (red-first + frozen)" + # VCR-RA-003 for RISC-V (#815, epic #242): the RV32 analogue of the ARM + # register-allocation validator. A PARALLEL re-implementation + # (synth_backend_riscv::alloc_validator::validate_final_allocation_rv32) keyed + # on the RV32 calling convention — NOT a reuse of the ARM-coupled + # validate_final_allocation. It runs UNCONDITIONALLY on every RV32 compile in + # the default `--features riscv` build (wired in backend.rs + # compile_function_with_opts, on the selector's `selection.ops`) and + # hard-errors on a violation of the two STRAIGHT-LINE invariants #815 names: + # (1) CALLEE-SAVED PRESERVATION — a body write of an s-register the pass + # saves (s1, s2..s10, mirroring `preserve_callee_saved`; the reserved + # s0/fp + s11/linmem-base excluded) must be saved by the prologue + # `sw s_k, off(sp)` + restored by every epilogue `lw s_k, off(sp)` -> + # CalleeSavedNotSaved / CalleeSavedNotRestored. + # (2) SPILL-SLOT NON-ALIASING — a frame slot `off(sp)` overwritten by a + # second `sw` 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). This job pins the gate: + # (a) RED-FIRST non-vacuity: the ra003rv_red_* unit tests synthetically + # revert a known-fixed clobber (drop the prologue save -> CalleeSavedNotSaved; + # drop the epilogue restore -> CalleeSavedNotRestored; alias two live + # values on one slot -> SpillSlotAliased) and assert the validator + # CATCHES it. The ra003rv_green_* tests assert it is SILENT on correct + # code + a Call -> NotAttempted. + # (b) SILENT-ON-REAL-CODEGEN: the frozen RV32 oracle compiles the RV32 + # fixtures THROUGH the unconditional validator; if it false-positived on + # a real function that fixture would fail to compile, so 10/10 green + # (control_step 0x00210A55 byte-identical) is the "Consistent on every + # real RV32 function" proof — PLUS a dedicated repro sweeping 9 fixtures + # × {relocatable, default} = 18 pairs asserting ZERO false positives. + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v7 + - uses: dtolnay/rust-toolchain@stable + - name: Cache Cargo dependencies + uses: actions/cache@v6 + with: + path: | + ~/.cargo/registry + ~/.cargo/git + target/ + key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }} + restore-keys: | + ${{ runner.os }}-cargo- + - name: RED-FIRST non-vacuity + silent-on-correct (RV32 validator unit tests) + run: cargo test -p synth-backend-riscv --lib ra003rv + - name: Silent-on-real-codegen (frozen suite through the unconditional gate) + run: cargo test -p synth-cli --test frozen_codegen_bytes + - name: Silent-on-real-codegen (RV32 fixture sweep, both paths) + run: | + cargo build -p synth-cli + python3 scripts/repro/vcr_ra_003_rv32_alloc_validator.py ./target/debug/synth + vcr-sel-005-cross-backend-op-parity-gate: name: "VCR-SEL-005 cross-backend op-parity (universe-complete + red-first)" # VCR-SEL-005 (#242, #223, #232): the "selector missed an op" class was never diff --git a/artifacts/verified-codegen-roadmap.yaml b/artifacts/verified-codegen-roadmap.yaml index dc0a9c28..b26214df 100644 --- a/artifacts/verified-codegen-roadmap.yaml +++ b/artifacts/verified-codegen-roadmap.yaml @@ -2016,6 +2016,53 @@ artifacts: Frozen-safe (emits nothing; control_step 0x00210A55 / flight_algo 0x07FDF307 byte-identical, 10/10). v2 (Rocq-mechanized soundness of the straight-line fragment) remains the open step. + RV32 ARM LANDED (v0.50, #815) — the per-backend RV32 analogue promised at + "RV32 / AArch64 get their own arms later" now ships: a PARALLEL + re-implementation `synth_backend_riscv::alloc_validator:: + validate_final_allocation_rv32` (RaFinalVerdict / RaFinalViolation in that + crate), keyed on the RV32 calling convention — NOT a reuse of the + ARM-coupled `validate_final_allocation` (different instruction enum + RiscVOp, different callee-saved set, different `addi sp,-N` + `sw s_k` + prologue shape). Wired UNCONDITIONALLY in `backend.rs` + (`compile_function_with_opts`, on `selection.ops` immediately after the + selector) on EVERY RV32 compile in the default `--features riscv` build + (both `compile_module` — the ELF path — and `compile_function` reach it), + hard-erroring on a Violation. Two STRAIGHT-LINE invariants (the two #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 + — the same holder model as the ARM validator, per straight-line segment, + an `addi sp` frame adjust resetting the slot map (the RV analogue of ARM's + `ldr sp,[sp,#N]` clear) -> SpillSlotAliased. A `Call` is the ARM + phase-2 across-call/across-join frontier (no RV `cfg_liveness` yet) -> + NON-FATAL NotAttempted { reason: "rv32-call-boundary" } (decline > guess; + the two straight-line invariants still ran). DELIBERATELY NO + "unmodeled-op → force-prologue" fail-safe (unlike ARM): on RV every + op_dest==None op is CF/system/label/call and writes no s-register, so the + fail-safe would be vacuous AND disagree with the pass -> a false-positive; + omitting it keeps validator↔pass agreement. RED-FIRST non-vacuity (8 + `ra003rv_*` unit tests in alloc_validator.rs): 3 RED synthetically revert a + known-fixed clobber and assert the CATCH (drop the prologue save of a used + s2 -> CalleeSavedNotSaved; drop the epilogue restore -> CalleeSavedNotRestored; + alias two live values on one slot -> SpillSlotAliased) + 4 GREEN assert + SILENT (the balanced save/use/restore leaf; a pure-scratch t0/a0 leaf; + sequential single-slot reuse; a Call -> NotAttempted) + 1 asserting a + straight-line Violation BEFORE a Call still fires (the Call does not mask + it). SILENT-ON-REAL-CODEGEN: the frozen RV32 oracle + (`frozen_fixtures_rv32_text_is_bit_identical_oracle_001`, control_step + 0x00210A55) compiles through the unconditional validator — 0 false + positives, byte-identical — PLUS a dedicated repro + (`scripts/repro/vcr_ra_003_rv32_alloc_validator.py`) sweeps 9 RV32 fixtures + × {relocatable, default} = 18 pairs (callee-saved-heavy control_step / + controller_step, spill-heavy gust_kernel, branchy flight_seam, call-bearing + reachable_helper) with 0 validator false-positives. CI-gated: + `vcr-ra-003-rv32-alloc-validator-gate` in ci.yml (red-first unit tests + + frozen RV32 oracle + the silent-on-real repro). AArch64 arm still open (the + integer subset has minimal spill traffic; a NAMED follow-up). - id: VCR-RA-004 type: sw-req diff --git a/crates/synth-backend-riscv/src/alloc_validator.rs b/crates/synth-backend-riscv/src/alloc_validator.rs new file mode 100644 index 00000000..96844e97 --- /dev/null +++ b/crates/synth-backend-riscv/src/alloc_validator.rs @@ -0,0 +1,631 @@ +//! VCR-RA-003 for RISC-V (#815, epic #242) — the RV32 analogue of the ARM-only +//! `synth_synthesis::liveness::validate_final_allocation` register-allocation +//! validator. +//! +//! # Why a parallel re-implementation, not "also run the ARM one" +//! +//! The ARM validator is deeply ARM-coupled: its signature is +//! `&[ArmInstruction]`, its callee-saved set is `[R4..R8]`, its prologue is an +//! LR-containing `push {…}` reg-list, and its def/use classifier `reg_effect` +//! speaks `ArmOp`. RV32 needs a different instruction enum +//! ([`RiscVOp`]), a different callee-saved set (the RV psABI `s`-registers), a +//! different prologue/epilogue shape (`addi sp,sp,-N` + `sw s_k, off(sp)`), and +//! its own def/use classifier (`op_dest`, already in `selector.rs`, mirroring +//! `reg_effect`'s "bail on unmodeled" contract). So we +//! port the *invariants*, not the code (#815). +//! +//! # Scope — the two STRAIGHT-LINE invariants (ARM phase 1) +//! +//! This validator checks exactly the two invariants the ARM phase-1 validator +//! checks, the two named in #815: +//! +//! 1. **Callee-saved preservation.** A callee-saved register the function body +//! *writes* must be saved by the prologue `sw s_k, off(sp)` and restored by +//! every return epilogue `lw s_k, off(sp)`. Reverting `preserve_callee_saved` +//! (dropping the prologue spill of a written `s`-register) leaves a body def +//! of an `s`-register with no matching save ⇒ +//! [`RaFinalViolation::CalleeSavedNotSaved`]. Whole-function structural check, +//! safe across branches/calls (it is not dataflow). +//! +//! 2. **Spill-slot non-aliasing.** Within one straight-line segment, a frame +//! slot `off(sp)` overwritten by a second `sw` while the first stored value is +//! still reloaded downstream corrupts the reload ⇒ +//! [`RaFinalViolation::SpillSlotAliased`]. Same holder-model the ARM validator +//! and `forward_stack_reloads` use. +//! +//! Everything past straight-line — value flow across a `Call`, availability +//! across a control-flow join — is the ARM *phase-2* 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, those +//! shapes are LOUD-declined: a function containing a `Call` yields +//! [`RaFinalVerdict::NotAttempted`] for the join reasoning (the two straight-line +//! invariants still ran and held). Decline > guess — the checker never claims a +//! coherence it cannot prove. +//! +//! # Callee-saved set — mirror the PASS, not the psABI +//! +//! The set is exactly the registers `preserve_callee_saved` saves: the ones +//! `is_callee_saved_temp` covers — `s1` (x9) and `s2..s10` (x18..x26). This is +//! the ARM validator's core discipline (it uses `[R4..R8]` = the set +//! `body_uses_callee_saved` covers): every function the pass left prologue-less +//! also passes the validator, so there is NO false-positive on real codegen. The +//! runtime-reserved `s0` (x8, frame pointer) and `s11` (x27, +//! `__linear_memory_base`) are DELIBERATELY excluded — the selector never emits a +//! body write to them, and the pass never saves them, so including them could +//! only manufacture a false-positive (a body `s11` read/def with no save the pass +//! was never going to add). Unlike the ARM validator, there is NO "unmodeled op → +//! force prologue" fail-safe: on RV every `op_dest == None` op is control-flow / +//! system / label / call (none write an `s`-register), so the fail-safe is +//! unnecessary AND would disagree with the pass (which has none) → false-positive. +//! +//! # Documented boundaries (false-negatives, never false-positives) +//! +//! The store-side `saved`-set scan counts ANY `sw s_k, off(sp)` as a prologue +//! save. If the RV selector ever spilled a callee-saved temp (s1/s2..s10) to the +//! frame IN THE BODY, that body `sw` would mask a genuine unsaved clobber → a +//! false NEGATIVE (the checker-safe direction, FN < FP, exactly as the ARM +//! validator excludes R0/R1 across a call). This is NOT reachable on current +//! selector output: the RV selector has NO Belady / spill-realloc body spilling +//! (`preserve_callee_saved` is the only site that stores an s-register to the +//! frame, and it is the prologue), and it DECLINES rather than body-spills when +//! it cannot allocate. If cross-call/Belady spilling is wired for RV later, this +//! boundary must be re-examined (anchor the save-set on the prologue window, not +//! any-sw). Named here so the boundary is visible, not silent. + +use crate::register::Reg; +use crate::riscv_op::RiscVOp; +use crate::selector::op_dest; +use std::collections::{BTreeMap, BTreeSet}; + +/// A concrete register-allocation invariant violation on the final RV32 stream. +/// Each variant names a miscompile class the per-compilation checker catches. +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum RaFinalViolation { + /// The body writes callee-saved register `reg` (`s1`/`s2..s10`) but no + /// prologue `sw reg, off(sp)` that saves it precedes the write — a caller's + /// register is silently clobbered (RV psABI violation). Reverting + /// `preserve_callee_saved`'s save of a written `s`-register makes this fire. + CalleeSavedNotSaved { reg: Reg }, + /// Epilogue half: the prologue saved `reg` (there is a `sw reg, off(sp)`) but + /// a return epilogue does not restore it with a matching `lw reg, off(sp)` + /// before the `ret` — the value the callee promised to preserve is not put + /// back. + CalleeSavedNotRestored { reg: Reg }, + /// Within one straight-line segment, spill slot `off(sp)` is overwritten by a + /// second `sw` (`overwriting_store`) while the value from the first `sw` + /// (`first_store`) is still needed by a later `lw` (`stale_reload`) — the + /// reload reads the wrong value. Indices are into the instruction stream. + SpillSlotAliased { + slot: i32, + first_store: usize, + overwriting_store: usize, + stale_reload: usize, + }, +} + +/// Three-valued verdict of the RV32 register-allocation validator, mirroring the +/// ARM validator's Consistent / Violation / NotAttempted. A checker that cannot +/// model a construct says so LOUDLY (`NotAttempted`) rather than return a false +/// `Consistent` (decline > guess — the v0.49 L4 vacuity lesson). +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum RaFinalVerdict { + /// Every checked invariant holds on this function's emitted stream. + Consistent, + /// A checked invariant is violated — the compile must hard-error. + Violation(RaFinalViolation), + /// A construct the whole-function reasoning does not model is present (a + /// `Call` — the ARM phase-2 across-call/across-join frontier, which has no RV + /// CFG machinery yet). The two STRAIGHT-LINE invariants (callee-saved + + /// spill-slot) STILL RAN and held (else this would be a `Violation`); only + /// the past-straight-line reasoning is skipped. NON-FATAL at the call site. + /// `reason` is a static machine-readable tag. + NotAttempted { reason: &'static str }, +} + +/// True for the callee-saved registers `preserve_callee_saved` actually saves: +/// `s1` (x9) and `s2..s10` (x18..x26). MUST mirror `is_callee_saved_temp` in +/// `selector.rs` exactly — see the module doc on why `s0`/`s11` are excluded. +fn is_saved_by_pass(r: Reg) -> bool { + let n = r as u8; + n == 9 || (18..=26).contains(&n) +} + +/// A `sw`/`lw` whose base is `sp` addresses a frame slot at offset `imm`. +/// Returns the slot offset, or `None` if the memory op is not sp-relative (a +/// linear-memory access through the base register, a param home through another +/// pointer, etc. — not a spill slot). +fn sp_slot_store(op: &RiscVOp) -> Option<(i32, Reg)> { + match op { + RiscVOp::Sw { rs1, rs2, imm } if *rs1 == Reg::SP => Some((*imm, *rs2)), + _ => None, + } +} +fn sp_slot_load(op: &RiscVOp) -> Option<(i32, Reg)> { + match op { + RiscVOp::Lw { rd, rs1, imm } if *rs1 == Reg::SP => Some((*imm, *rd)), + _ => None, + } +} + +/// The `ret` terminator: `jalr x0, 0(ra)`. +fn is_ret(op: &RiscVOp) -> bool { + matches!( + op, + RiscVOp::Jalr { + rd: Reg::ZERO, + rs1: Reg::RA, + imm: 0 + } + ) +} + +/// True for ops that do NOT break a straight-line segment: the data ops (arith, +/// load, store, csr). A `Label`, `Jal`, `Branch`, `Call`, `Jalr` return, or any +/// system op breaks the segment (the spill map resets at a join/barrier). +fn is_straight_line(op: &RiscVOp) -> bool { + use RiscVOp::*; + match op { + // Control flow / labels / calls / system — segment barriers. + Label { .. } + | Jal { .. } + | Jalr { .. } + | Branch { .. } + | Call { .. } + | Ecall + | Ebreak + | Mret + | Wfi + | Fence => false, + // Everything else is a data op (arith, load, store, csr) — straight-line. + _ => true, + } +} + +/// VCR-RA-003 (RV32) UNCONDITIONAL single-stream register-allocation validator +/// (#815, epic #242). Runs on every RV32 function compile in the default +/// `--features riscv` build (NOT behind `--features verify` — a verify-gated +/// check would be dormant in the shipping build, the #757 / VCR-VER-003 lesson) +/// and hard-errors the compile on a [`RaFinalViolation`]. Emits nothing, so the +/// RV32 `.text` is byte-identical (the frozen RV32 oracle is unchanged). +/// +/// See the module doc for the invariants, the callee-saved-set discipline, and +/// the phase-2 decline boundary. +pub fn validate_final_allocation_rv32(instrs: &[RiscVOp]) -> RaFinalVerdict { + // ---- Invariant 1: callee-saved preservation, whole-function ---------- + // + // Collect the prologue save-set: every `sw s_k, off(sp)` BEFORE the first + // body op that is not part of the prologue. The pass emits the prologue as a + // leading `addi sp,sp,-frame` followed by the `sw s_k` saves, so the save-set + // is exactly the sp-relative stores of callee-saved regs that appear before + // the first `ret`. We scan the whole stream: any `sw s_k, off(sp)` is a save + // of `s_k` (the pass only stores an s-register to the frame to preserve it). + let mut saved: BTreeSet = BTreeSet::new(); + for ins in instrs { + if let Some((_, rs2)) = sp_slot_store(ins) + && is_saved_by_pass(rs2) + { + saved.insert(rs2); + } + } + // Which callee-saved registers does the body WRITE (op_dest)? A written + // s-register with no matching save is the #490-class clobber. + let mut defined_cs: BTreeSet = BTreeSet::new(); + for ins in instrs { + if let Some(rd) = op_dest(ins) + && is_saved_by_pass(rd) + { + defined_cs.insert(rd); + } + } + for r in &defined_cs { + if !saved.contains(r) { + return RaFinalVerdict::Violation(RaFinalViolation::CalleeSavedNotSaved { reg: *r }); + } + } + // Epilogue half: every saved s-register must be restored by a `lw s_k, + // off(sp)` before each `ret`. We check that between the LAST `lw`/restore + // region and each `ret`, every saved register was reloaded. Simplest sound + // form: for each `ret`, scan backward to the previous segment barrier and + // collect the sp-relative loads of s-registers; every `saved` reg must be + // among them. + if !saved.is_empty() { + for (i, ins) in instrs.iter().enumerate() { + if !is_ret(ins) { + continue; + } + // Collect s-register reloads in the epilogue preceding this ret: + // walk backward until a non-epilogue op (anything that is neither a + // sp-relative `lw` of an s-register nor the `addi sp,sp,frame` frame + // teardown). + let mut restored: BTreeSet = BTreeSet::new(); + let mut j = i; + while j > 0 { + j -= 1; + match &instrs[j] { + RiscVOp::Lw { + rd, rs1: Reg::SP, .. + } if is_saved_by_pass(*rd) => { + restored.insert(*rd); + } + // Frame teardown `addi sp,sp,N` is part of the epilogue. + RiscVOp::Addi { + rd: Reg::SP, + rs1: Reg::SP, + .. + } => {} + // Anything else ends the epilogue window. + _ => break, + } + } + for r in &saved { + if !restored.contains(r) { + return RaFinalVerdict::Violation(RaFinalViolation::CalleeSavedNotRestored { + reg: *r, + }); + } + } + } + } + + // ---- Invariant 2: spill-slot non-aliasing, per straight-line segment -- + // + // Same holder model as the ARM validator: per slot, remember the owning + // store and whether the owner was reloaded (consumed). A second store to a + // slot whose owner has NOT been reloaded shadows a still-live value; a later + // reload of that slot proves the shadow was needed ⇒ aliasing bug. The `addi + // sp,sp,imm` frame adjust rebases every slot offset — it resets the map (the + // RV analogue of the ARM `ldr sp,[sp,#N]` clear). + #[derive(Clone)] + struct SlotState { + owner_store: usize, + owner_reloaded: bool, + shadowed: Option<(usize, usize)>, + } + let mut i = 0usize; + while i < instrs.len() { + if !is_straight_line(&instrs[i]) { + i += 1; + continue; + } + let mut slots: BTreeMap = BTreeMap::new(); + while i < instrs.len() && is_straight_line(&instrs[i]) { + // A frame-pointer / sp adjust invalidates every slot name. + if let RiscVOp::Addi { rd: Reg::SP, .. } = &instrs[i] { + slots.clear(); + i += 1; + continue; + } + if let Some((slot, _)) = sp_slot_store(&instrs[i]) { + let shadowed = match slots.get(&slot) { + Some(prev) if !prev.owner_reloaded => Some((prev.owner_store, i)), + Some(prev) => prev.shadowed, + None => None, + }; + slots.insert( + slot, + SlotState { + owner_store: i, + owner_reloaded: false, + shadowed, + }, + ); + } else if let Some((slot, rd)) = sp_slot_load(&instrs[i]) { + if rd == Reg::SP { + slots.clear(); + } else if let Some(st) = slots.get_mut(&slot) { + if let Some((first_store, overwriting_store)) = st.shadowed { + return RaFinalVerdict::Violation(RaFinalViolation::SpillSlotAliased { + slot, + first_store, + overwriting_store, + stale_reload: i, + }); + } + st.owner_reloaded = true; + } + } + i += 1; + } + } + + // ---- Phase-2 boundary: value flow across a Call (loud decline) -------- + // + // A `Call` is the ARM phase-2 across-call / across-join frontier. RV has no + // `cfg_liveness`/join-availability machinery, so rather than a false pass we + // LOUD-decline the past-straight-line reasoning. The two straight-line + // invariants already ran and held. Decline > guess. + if instrs.iter().any(|op| matches!(op, RiscVOp::Call { .. })) { + return RaFinalVerdict::NotAttempted { + reason: "rv32-call-boundary", + }; + } + + RaFinalVerdict::Consistent +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::register::Reg; + use crate::riscv_op::RiscVOp::*; + + // A minimal correct leaf body that saves+restores s2, uses it, and returns. + fn balanced_callee_saved_body() -> Vec { + vec![ + Addi { + rd: Reg::SP, + rs1: Reg::SP, + imm: -16, + }, // prologue frame + Sw { + rs1: Reg::SP, + rs2: Reg::S2, + imm: 0, + }, // save s2 + Addi { + rd: Reg::S2, + rs1: Reg::ZERO, + imm: 7, + }, // body writes s2 + Add { + rd: Reg::A0, + rs1: Reg::S2, + rs2: Reg::ZERO, + }, + Lw { + rd: Reg::S2, + rs1: Reg::SP, + imm: 0, + }, // restore s2 + Addi { + rd: Reg::SP, + rs1: Reg::SP, + imm: 16, + }, // teardown + Jalr { + rd: Reg::ZERO, + rs1: Reg::RA, + imm: 0, + }, // ret + ] + } + + // ── RED-FIRST: clobber a used s-register with no prologue save ────────── + #[test] + fn ra003rv_red_missing_callee_saved_prologue_is_caught() { + // Body writes s2 but there is NO `sw s2, off(sp)` prologue save. + let clobbering_body = vec![ + Addi { + rd: Reg::SP, + rs1: Reg::SP, + imm: -16, + }, + Addi { + rd: Reg::S2, + rs1: Reg::ZERO, + imm: 7, + }, // clobbers s2, unsaved + Add { + rd: Reg::A0, + rs1: Reg::S2, + rs2: Reg::ZERO, + }, + Addi { + rd: Reg::SP, + rs1: Reg::SP, + imm: 16, + }, + Jalr { + rd: Reg::ZERO, + rs1: Reg::RA, + imm: 0, + }, + ]; + assert_eq!( + validate_final_allocation_rv32(&clobbering_body), + RaFinalVerdict::Violation(RaFinalViolation::CalleeSavedNotSaved { reg: Reg::S2 }), + "a written-but-unsaved callee-saved s-register must be caught" + ); + } + + #[test] + fn ra003rv_green_callee_saved_prologue_present_is_consistent() { + assert_eq!( + validate_final_allocation_rv32(&balanced_callee_saved_body()), + RaFinalVerdict::Consistent, + ); + } + + // ── RED-FIRST: epilogue drops the restore of a saved register ────────── + #[test] + fn ra003rv_red_epilogue_drops_saved_register_is_caught() { + // Prologue saves s2, body writes it, but the epilogue omits the `lw s2`. + let body = vec![ + Addi { + rd: Reg::SP, + rs1: Reg::SP, + imm: -16, + }, + Sw { + rs1: Reg::SP, + rs2: Reg::S2, + imm: 0, + }, + Addi { + rd: Reg::S2, + rs1: Reg::ZERO, + imm: 7, + }, + Add { + rd: Reg::A0, + rs1: Reg::S2, + rs2: Reg::ZERO, + }, + // <-- missing `lw s2, 0(sp)` + Addi { + rd: Reg::SP, + rs1: Reg::SP, + imm: 16, + }, + Jalr { + rd: Reg::ZERO, + rs1: Reg::RA, + imm: 0, + }, + ]; + assert_eq!( + validate_final_allocation_rv32(&body), + RaFinalVerdict::Violation(RaFinalViolation::CalleeSavedNotRestored { reg: Reg::S2 }), + ); + } + + #[test] + fn ra003rv_green_pure_scratch_leaf_needs_no_prologue() { + // Uses only caller-saved temps (t0/a0) — no prologue required. + let body = vec![ + Addi { + rd: Reg::T0, + rs1: Reg::ZERO, + imm: 3, + }, + Add { + rd: Reg::A0, + rs1: Reg::T0, + rs2: Reg::ZERO, + }, + Jalr { + rd: Reg::ZERO, + rs1: Reg::RA, + imm: 0, + }, + ]; + assert_eq!( + validate_final_allocation_rv32(&body), + RaFinalVerdict::Consistent + ); + } + + // ── RED-FIRST: alias two live values on one spill slot ───────────────── + #[test] + fn ra003rv_red_spill_slot_aliasing_is_caught() { + // sw A -> slot 4; sw B -> slot 4 (A not yet reloaded); lw slot 4 -> reads + // B though A was still needed. + let body = vec![ + Sw { + rs1: Reg::SP, + rs2: Reg::T0, + imm: 4, + }, // first_store (A) + Sw { + rs1: Reg::SP, + rs2: Reg::T1, + imm: 4, + }, // overwriting_store (B) + Lw { + rd: Reg::T2, + rs1: Reg::SP, + imm: 4, + }, // stale_reload + Jalr { + rd: Reg::ZERO, + rs1: Reg::RA, + imm: 0, + }, + ]; + assert_eq!( + validate_final_allocation_rv32(&body), + RaFinalVerdict::Violation(RaFinalViolation::SpillSlotAliased { + slot: 4, + first_store: 0, + overwriting_store: 1, + stale_reload: 2, + }), + ); + } + + #[test] + fn ra003rv_green_sequential_slot_reuse_is_consistent() { + // sw A; lw A (consumed); sw B (legal reuse); lw B — no aliasing. + let body = vec![ + Sw { + rs1: Reg::SP, + rs2: Reg::T0, + imm: 4, + }, + Lw { + rd: Reg::T0, + rs1: Reg::SP, + imm: 4, + }, // A consumed + Sw { + rs1: Reg::SP, + rs2: Reg::T1, + imm: 4, + }, // reuse slot 4 + Lw { + rd: Reg::T1, + rs1: Reg::SP, + imm: 4, + }, + Jalr { + rd: Reg::ZERO, + rs1: Reg::RA, + imm: 0, + }, + ]; + assert_eq!( + validate_final_allocation_rv32(&body), + RaFinalVerdict::Consistent + ); + } + + // ── Phase-2 decline: a Call yields NotAttempted (never a false pass) ──── + #[test] + fn ra003rv_call_boundary_is_not_attempted() { + let body = vec![ + Addi { + rd: Reg::A0, + rs1: Reg::ZERO, + imm: 1, + }, + Call { + label: "callee".to_string(), + }, + Jalr { + rd: Reg::ZERO, + rs1: Reg::RA, + imm: 0, + }, + ]; + assert_eq!( + validate_final_allocation_rv32(&body), + RaFinalVerdict::NotAttempted { + reason: "rv32-call-boundary" + }, + ); + } + + // ── A Call does NOT mask a straight-line violation before it ─────────── + #[test] + fn ra003rv_violation_before_call_still_fires() { + let body = vec![ + Addi { + rd: Reg::S2, + rs1: Reg::ZERO, + imm: 7, + }, // unsaved s2 clobber + Call { + label: "callee".to_string(), + }, + Jalr { + rd: Reg::ZERO, + rs1: Reg::RA, + imm: 0, + }, + ]; + assert_eq!( + validate_final_allocation_rv32(&body), + RaFinalVerdict::Violation(RaFinalViolation::CalleeSavedNotSaved { reg: Reg::S2 }), + ); + } +} diff --git a/crates/synth-backend-riscv/src/backend.rs b/crates/synth-backend-riscv/src/backend.rs index 3da5e312..7f5ff251 100644 --- a/crates/synth-backend-riscv/src/backend.rs +++ b/crates/synth-backend-riscv/src/backend.rs @@ -212,6 +212,43 @@ fn compile_function_with_opts( ) .map_err(|e| BackendError::CompilationFailed(format!("RISC-V selector: {e}")))?; + // VCR-RA-003 for RISC-V (#815, epic #242): UNCONDITIONAL per-compilation + // register-allocation validation, the RV32 analogue of the ARM-only + // `synth_synthesis::liveness::validate_final_allocation`. It proves — by + // construction, on the EXACT emitted stream — that the allocation preserves + // the two STRAIGHT-LINE invariants whose reference lives in the stream: (1) + // callee-saved preservation (a written `s`-register saved+restored by the + // prologue/epilogue) and (2) spill-slot non-aliasing (no live frame slot + // overwritten before its reload). Runs on every RV32 compile in the DEFAULT + // `--features riscv` build (NOT behind `--features verify`; a verify-gated + // check would be dormant in the build that ships — the #757 / VCR-VER-003 + // lesson) and hard-errors on a VIOLATION. A `NotAttempted` verdict (a `Call` + // — the ARM phase-2 across-call/across-join frontier, which has no RV CFG + // machinery yet) is NON-FATAL: the two straight-line invariants still ran and + // held; only the past-straight-line reasoning is declined (decline > guess). + // Frozen-safe: it emits nothing, so RV32 `.text` is byte-identical. + match crate::alloc_validator::validate_final_allocation_rv32(&selection.ops) { + crate::alloc_validator::RaFinalVerdict::Violation(v) => { + return Err(BackendError::CompilationFailed(format!( + "VCR-RA-003 (RV32): register-allocation validation FAILED — {v:?}. \ + The emitted stream violates a register-allocation invariant \ + (callee-saved preservation / spill-slot non-aliasing); this is a \ + compiler bug, not a program error. Refusing to emit a miscompiled \ + object." + ))); + } + crate::alloc_validator::RaFinalVerdict::NotAttempted { reason } => { + if std::env::var_os("SYNTH_RA003_VERBOSE").is_some() { + eprintln!( + "VCR-RA-003 (RV32): past-straight-line validation NOT ATTEMPTED \ + ({reason}) — callee-saved / spill-slot invariants held; \ + across-call/across-join reasoning declined on this shape." + ); + } + } + crate::alloc_validator::RaFinalVerdict::Consistent => {} + } + // Encode the function via the ELF builder's per-function pipeline so // we benefit from label resolution. We discard the ELF and keep the // raw bytes — that's what `CompiledFunction` carries. diff --git a/crates/synth-backend-riscv/src/lib.rs b/crates/synth-backend-riscv/src/lib.rs index 195852f9..7df2790a 100644 --- a/crates/synth-backend-riscv/src/lib.rs +++ b/crates/synth-backend-riscv/src/lib.rs @@ -14,6 +14,7 @@ //! The encoder always emits 32-bit instructions in this skeleton. The 16-bit //! C-extension encoding will be a peephole pass in a follow-up. +pub mod alloc_validator; pub mod backend; pub mod elf_builder; pub mod encoder; diff --git a/crates/synth-backend-riscv/src/selector.rs b/crates/synth-backend-riscv/src/selector.rs index cd249b2f..f78d828f 100644 --- a/crates/synth-backend-riscv/src/selector.rs +++ b/crates/synth-backend-riscv/src/selector.rs @@ -471,7 +471,7 @@ fn select_attempt( } /// The destination register an op writes, if any (for the callee-saved scan). -fn op_dest(op: &RiscVOp) -> Option { +pub(crate) fn op_dest(op: &RiscVOp) -> Option { use RiscVOp::*; match *op { Lui { rd, .. } diff --git a/scripts/repro/vcr_ra_003_rv32_alloc_validator.py b/scripts/repro/vcr_ra_003_rv32_alloc_validator.py new file mode 100644 index 00000000..c7a2bf10 --- /dev/null +++ b/scripts/repro/vcr_ra_003_rv32_alloc_validator.py @@ -0,0 +1,135 @@ +#!/usr/bin/env python3 +"""VCR-RA-003 for RISC-V (#815, epic #242) — RV32 register-allocation validator. + +The RV32 analogue of the ARM `validate_final_allocation` gate. The RV32 checker +(`synth_backend_riscv::alloc_validator::validate_final_allocation_rv32`) runs +UNCONDITIONALLY on every RV32 compile in the default `--features riscv` build and +hard-errors on a violation of the two STRAIGHT-LINE invariants #815 names: + + Invariant 1 (callee-saved preservation): a callee-saved `s`-register (s1, + s2..s10 — the set `preserve_callee_saved` saves) written by the body must be + saved by a prologue `sw s_k, off(sp)` and restored by every epilogue + `lw s_k, off(sp)`. Reverting the save/restore makes it fire + (CalleeSavedNotSaved / CalleeSavedNotRestored). + + Invariant 2 (spill-slot non-aliasing): within a straight-line segment a frame + slot `off(sp)` overwritten by a second `sw` while the first value is still + reloaded downstream corrupts the reload (SpillSlotAliased). + +A `Call` — the ARM phase-2 across-call/across-join frontier, which has no RV CFG +machinery yet — yields a NON-FATAL `NotAttempted` (decline > guess): the two +straight-line invariants still run. + +This script is the SILENT-ON-REAL-CODEGEN half of the gate: it compiles the RV32 +repro fixtures (branchy, memory-touching, callee-saved-heavy, call-bearing) +through the UNCONDITIONAL validator on BOTH the default and `--relocatable` +paths and asserts ZERO false positives (no `VCR-RA-003 (RV32) ... FAILED`). If the +validator false-positived on any real function that function would refuse to +compile and this gate would go red — the guard that the callee-saved set mirrors +the pass (s1/s2..s10, NOT the reserved s0/s11) and that the spill-slot map +resets on each `addi sp` frame adjust. + +The RED (non-vacuity) half lives in the `ra003rv_red_*` unit tests +(`cargo test -p synth-backend-riscv --lib ra003rv`), which assert the validator +CATCHES a synthetic unsaved-s-register clobber, a dropped epilogue restore, and a +spill-slot alias. + +Usage: python3 scripts/repro/vcr_ra_003_rv32_alloc_validator.py [path/to/synth] +Exit 0 iff every RV32 fixture compiles clean (validator silent on real code). +""" +import os +import subprocess +import sys +import tempfile +from pathlib import Path + +REPO = Path(__file__).resolve().parents[2] +REPRO = REPO / "scripts" / "repro" + +# RV32-compilable fixtures spanning the shapes the validator reasons about: +# callee-saved-heavy (control_step reads the linmem table via s11, uses +# s-registers), spill/frame traffic, branches, and calls (the NotAttempted +# boundary). A false positive on ANY reds this gate. +RV32_FIXTURES = [ + "control_step.wasm", # callee-saved + linmem base (s11) + branches + "controller_step.wasm", # PID-style step, promoted locals + "filter_axis.wasm", # filter, memory + arithmetic + "signed_div_const.wasm", # signed div-by-const (trap guard shapes) + "reachable_helper.wasm", # call-bearing (NotAttempted boundary) + "msgq_put_359.wasm", # queue put, memory stores + "gust_kernel.wasm", # larger kernel, spill traffic + "flight_seam.wasm", # branchy control flow + "flight_seam_flat.wasm", # flattened branchy control flow +] + + +def synth_bin() -> str: + if len(sys.argv) > 1: + return sys.argv[1] + tgt = os.environ.get("CARGO_TARGET_DIR", str(REPO / "target")) + return str(Path(tgt) / "debug" / "synth") + + +def main() -> int: + binp = synth_bin() + if not Path(binp).exists(): + print(f"error: synth binary not found at {binp}", file=sys.stderr) + print("build first: cargo build -p synth-cli", file=sys.stderr) + return 2 + + failures = [] + checked = 0 + for path_name, extra_args in (("relocatable", ["--relocatable"]), ("default", [])): + for fx in RV32_FIXTURES: + path = REPRO / fx + if not path.exists(): + if path_name == "relocatable": + print(f"warn: fixture missing, skipping: {fx}", file=sys.stderr) + continue + checked += 1 + with tempfile.NamedTemporaryFile(suffix=".o") as out: + proc = subprocess.run( + [ + binp, "compile", str(path), + "-b", "riscv", "-t", "rv32imac", + "--all-exports", "-o", out.name, *extra_args, + ], + capture_output=True, + text=True, + ) + combined = proc.stdout + proc.stderr + if "VCR-RA-003 (RV32)" in combined and "FAILED" in combined: + line = next( + (l for l in combined.splitlines() + if "FAILED" in l and "VCR-RA-003 (RV32)" in l), + "", + ) + failures.append((fx, path_name, line.strip())) + print(f"FAIL [{path_name}] {fx}: RV32 validator false-positived on real codegen") + print(f" {line.strip()}") + elif proc.returncode != 0: + # A non-validator compile error (unsupported op etc.) is not a + # validator false-positive — record but do not fail the gate on it + # (the fixture simply doesn't compile on RV32 for another reason). + print(f"skip [{path_name}] {fx}: compile failed for a non-validator reason " + f"(rc={proc.returncode})") + else: + print(f"ok [{path_name}] {fx}: RV32 validator silent (Consistent / NotAttempted)") + + print(f"\nchecked {checked} (fixture, path) pairs; {len(failures)} validator false-positives") + if failures: + print( + "\nVCR-RA-003 (RV32) validator FALSE-POSITIVED on real codegen — the " + "callee-saved set or the spill-slot segmentation is wrong.", + file=sys.stderr, + ) + return 1 + print( + "VCR-RA-003 (RV32) SILENT on real codegen — the callee-saved-preservation " + "+ spill-slot-non-aliasing checks pass every real RV32 fixture." + ) + return 0 + + +if __name__ == "__main__": + sys.exit(main())