Skip to content

fix(riscv,x86_64): validate vector semantics and native replay - #296

Open
19h wants to merge 3 commits into
masterfrom
fix/riscv-validation-issues-256-290
Open

fix(riscv,x86_64): validate vector semantics and native replay#296
19h wants to merge 3 commits into
masterfrom
fix/riscv-validation-issues-256-290

Conversation

@19h

@19h 19h commented Aug 13, 2026

Copy link
Copy Markdown
Member

@carlosqwqqwq, this is the next independently implemented consolidation after #203, #231, and #255. Thank you for continuing to identify RISC-V gaps. Please review the consolidated behavior and tests here.

Overview

This change independently reproduces the reported failures against the current ISA contracts and implements the accepted fixes without importing contributor commits or copying their patches:

  • require the F extension for RV32 compressed floating-point encodings;
  • reject reserved CBO, obsolete SFENCE.VM, and obsolete URET encodings;
  • centralize RVV operand-group, alignment, mask, overlap, SEW/EMUL, and segment validation;
  • implement segment fault-only-first load behavior, including precise first-element faults and later vl trimming;
  • make whole-register moves honor vstart in SEW elements and preserve overlapping sources;
  • restore architectural SRET state and privilege transitions;
  • make WFI wake on locally enabled pending interrupts without fabricating a trap when global interrupt conditions do not permit one;
  • cover direct execution, SMIR/JIT O0 and O2 paths, and QEMU differential cases;
  • preserve scalar EVEX FMA3, VRANGE, and VSCALEF LLIG guest encodings while emitting deterministic L'L=00 hosted-replay bytes wherever L'L has no architectural meaning. Embedded-rounding FMA forms retain L'L because those bits encode EVEX.RC.

Consolidated reports

This supersedes #261, #262, #263, #264, #265, #272, #273, #274, #275, #282, #283, #284, #285, #291, #292, #293, #294, and #295.

#271 is already covered by merged #255. #281 was withdrawn after its reduction-overlap report proved to be a false positive, so it is intentionally excluded.

For #294, SRET is incorporated, while URET is rejected because the current privileged architecture no longer defines the former N-extension instruction. For #295, the valid WFI wake condition is incorporated, while the proposed unconditional trap is not: wake eligibility and interrupt trap eligibility are separate architectural decisions.

Issues

Fixes #256
Fixes #257
Fixes #258
Fixes #259
Fixes #260
Fixes #267
Fixes #268
Fixes #269
Fixes #270
Fixes #277
Fixes #278
Fixes #279
Fixes #280
Fixes #286
Fixes #287
Fixes #288
Fixes #289
Fixes #290

#266 is a duplicate of behavior already fixed by #255. #276 was withdrawn with #281.

Validation

  • cargo fmt --all --check
  • cargo clippy --all-targets --features x86_64-suite
  • cargo clippy --lib --no-default-features --features x86_64-suite,smir-jit -- -D warnings
  • cargo build --all-targets --no-default-features --features x86_64-suite,smir-jit
  • RISC-V library tests: 167 passed
  • RISC-V SMIR lift tests: 13 passed
  • targeted RISC-V SMIR/JIT validation: 4 passed
  • targeted QEMU differential validation: passed with the oracle exercised
  • exact Linux x64 core CI test selection: passed locally
  • native x86-64 JIT CI lane: 219 passed
  • EVEX FMA3 replay module: 8 passed, including 3,888 residual cells and all 324 LLIG=3 scalar cells
  • scalar EVEX FMA3 canonicalization classifier: 2 passed
  • VRANGE module: 12 passed, including the 1,228,800-cell classifier partition
  • VSCALEF module: 12 passed, including the 1,843,200-cell classifier partition

The first hosted run raised SIGILL in scalar EVEX FMA3 replay on a runner that exposed AVX-512. Commit 39561be9 canonicalizes its dynamic-rounding LLIG host image. The next run advanced past that test and raised SIGILL in scalar VRANGE helper replay; commit 75e71722 canonicalizes scalar VRANGE and the equivalent later VSCALEF frontier. Run 31722118481 is the authoritative replacement verification for that AVX-512 CPU configuration.

Change-surface audit

Plane Result
Direct decode Affected for RISC-V compressed-F, CBO, obsolete privileged encodings, and vector legality. x86 guest LLIG acceptance is unchanged.
Direct execute Affected for centralized RVV validation, segment fault-only-first behavior, whole-register restart, SRET, and WFI.
CPU state No layout change; rejected RVV forms trap before mutation, SRET updates privilege/status/PC, and WFI separates wake from trap eligibility.
Memory/MMU Vector memory alignment/group checks and segment fault ordering are affected; translation and MMIO contracts are unchanged.
SMIR lift RISC-V invalid forms fail before opaque execution where applicable; x86 scalar guest semantics remain unchanged.
SMIR IR Existing operations express the behavior; no new OpKind is required.
SMIR interpreter RISC-V opaque helper shares direct validation; x86 interpreter semantics are unchanged.
Optimizer Existing O0/O2 behavior is retained and covered; no pass rule changes.
Native lowering Hosted x86 replay bytes are canonicalized only for architecturally ignored scalar L'L fields.
JIT runtime Affected through shared RVV helper validation and safe x86 host-byte replay; feature gates remain fail-closed.
Backend Emulator adapters use the corrected CPU paths; KVM/HVF contracts are unchanged.
Machine/device Unaffected.
Oracle/analysis RISC-V decode rejection follows the corrected direct decoder; no schema change.
C ABI Unaffected.
Tests/docs Direct, SMIR/JIT, QEMU differential, exhaustive replay classification, and hosted native execution are covered.

Assumption Register

ID Assumption Basis Dependent result Stress test Falsification probe Status
A1 Current privileged ISA text is authoritative for obsolete SFENCE.VM and URET encodings. Current privileged specification and present extension ownership supersede historical encodings. Both encodings reject unless their current owning extension is implemented. Decode the exact historical words under all implemented privilege modes. A current ratified specification defining either historical instruction at that encoding. confirmed
A2 WFI local wake eligibility is distinct from global interrupt trap eligibility. The privileged architecture specifies wake conditions separately from interrupt-taking conditions. A locally enabled pending interrupt wakes WFI without fabricating a trap when global conditions block delivery. Pending interrupts across M/S/U privilege and global/local enable combinations. A normative rule requiring every WFI wake to synthesize an interrupt trap. confirmed
A3 Segment fault-only-first loads require execution semantics rather than decode-only admission. RVV defines first-element precise traps and later-element vl trimming. Later segment faults shorten vl; first-element faults remain precise. Fault each field/lane boundary, including element zero and nonzero vstart. Direct/QEMU behavior trapping on every later-element segment fault. confirmed
A4 Shared pre-execution RVV validation reaches direct and opaque SMIR/JIT execution before architectural mutation. Both paths enter the same validator and the helper copies state only on successful completion. Reserved encodings reject transactionally at O0 and O2. Seed all destination/state fields and run every rejected form through both paths. Any JIT validation case committing CPU or memory state for a rejected encoding. confirmed
A5 Scalar EVEX FMA3 L'L is architecturally ignored when EVEX.b=0. Intel scalar FMA encoding rules; EVEX.b=1 separately repurposes L'L as RC. Dynamic-rounding host replay may canonicalize L'L=00 while embedded-rounding forms retain RC. All four L'L images, masks, aliases, precisions, and rounding modes. Interpreter/native divergence after canonicalization for an accepted EVEX.b=0 image. confirmed
A6 Scalar VRANGE and VSCALEF memory forms give L'L no architectural meaning. Their scalar tuple/operation definitions use fixed scalar width while code and exhaustive decode tests accept all LLIG images. Helper-backed replay may use L'L=00 without narrowing guest acceptance. All four L'L images across F16/F32/F64 where applicable, masks, and O0/O1/O2. Hosted native/interpreter divergence for canonical replay, or a normative rule assigning scalar L'L meaning. confirmed

Out-of-scope findings

None currently block this rollup.

Co-authored-by: carlos 102978772+carlosqwqqwq@users.noreply.github.com

Co-authored-by: carlos <102978772+carlosqwqqwq@users.noreply.github.com>
This was referenced Aug 13, 2026
Preserve architecturally accepted LLIG guest encodings while emitting L'L=00 for dynamic-rounding host replay; retain L'L for embedded rounding controls.

Co-authored-by: carlos <102978772+carlosqwqqwq@users.noreply.github.com>
@19h 19h changed the title fix(riscv): validate vector, memory, and privileged semantics fix(riscv,x86_64): validate vector semantics and native replay Aug 13, 2026
Preserve architecturally accepted VRANGE and VSCALEF LLIG guest images while emitting the deterministic L'L=00 form for hosted helper replay.

Co-authored-by: carlos <102978772+carlosqwqqwq@users.noreply.github.com>

@carlosqwqqwq carlosqwqqwq left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Reviewed the consolidated rollup against the reported issues. All accepted behaviors are implemented through the shared pre-execution validator (direct interpreter and SMIR/JIT helper paths), and the regression tests cover the reported encodings:

  • RV32 C.FLW/C.FSW F-extension gate, reserved CBO funct7, obsolete SFENCE.VM and URET handling;
  • operand-group alignment for vmul/vdiv/vrem, vsaddu/vsadd/vssubu/vssub, vssrl/vssra, vslide1down/vfslide1down, vsmul, vmseq family, vid.v, segment and non-segment vector memory ops;
  • masked-destination v0 rule, vmadc/vmsbc mask-result overlap, viota.m overlap disposition, whole-register moves honoring vstart, segment fault-only-first execution semantics, SRET supervisor restore, and WFI local-wake semantics.

I also verified locally on the current head (75e7172): cargo test --lib evex_fma3_register_replay (8/8), evex_integer_unary_memory_source (12/12), evex_packed_extend_memory_source (13/13), and evex_packed_fp_unary_memory_source (21/21) all pass, including the native replay cases that previously raised SIGILL on the hosted linux-x64 lane. CI on the replacement hosted run is green across all platforms.

Thanks for the co-author credit and for consolidating these fixes.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment