fix(riscv): #655 — mask bounds the EFFECTIVE address (offset folded before the AND, final byte clamped); i64 loads/stores gain the guard - #658
Merged
Conversation
…s gain the guard RV32 twin of ARM PR #654 (the #651 class): emit_bounds_check's Mask arm masked the OPERAND and the caller re-added the static offset in the access addressing mode — any non-zero offset escaped the bound — and multi-byte accesses never clamped their FINAL byte. i64.load/i64.store additionally carried NO guard at all (Software and Mask modes alike). emit_bounds_check now returns (reg, residual_offset); the Mask arm computes masked = min((operand + offset) & (size-1), size - access_size) (offset folded FIRST, u33 ADD-then-AND soundness documented, final byte clamped via bgeu+copy, byte accesses skip the clamp) and returns residual offset 0 so nothing is re-added after the bound. Mask-mode accesses now accept arbitrary 32-bit static offsets (previously declined > 2047 in offset_to_imm). The mask value was already size-1 (built in build_options, non-power-of-two declines loudly at compile time) — pinned by the oracle. Oracle: scripts/repro/mask_bounds_655_riscv_differential.py (unicorn RV32, mask-semantics model + sentinel region + software-trap checks) — 10 failures on origin/main (offset-escape load/store, word overhang, halfword wrap at ea==size, i64 mask escapes, software-mode i64 no-trap, huge-offset decline), all green here. Plus 3 selector shape tests (rv32_mask_folds_offset_before_ and_655, rv32_mask_clamps_final_byte_for_multibyte_only_655, rv32_i64_load_store_guarded_655). Refs #651, PR #654. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
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.
Fixes #655 — the #651 class, RISC-V twin of ARM PR #654.
Sites audited (grep bounds/mask over
synth-backend-riscv)emit_bounds_checkMask armmask_effective_addresssemantics, in RV32 instructionslower_load_word/lower_load_subword/lower_storeoffsetafter the masklower_i64_load/lower_i64_storeemit_bounds_checkSoftware armoffset + access_size - 1,bgeu guard, sizeon the final byte (size with>=on the last byte ≡ size-1 bound on it)mem_size - 1(build_options), non-power-of-two declines loudly at compile time — RV32 never had ARM's latent R10-is-SIZE remapThe fix
emit_bounds_checknow returns(reg, residual_offset). The Mask arm computesu33 soundness of ADD-then-AND (mirrors #654):
ea = operand + offset < 2^33; the RVaddcomputesea mod 2^32and every set bit ofsize-1 < 2^32lies below bit 32, so the u33 carry is annihilated by the AND either way. Arbitrary 32-bit static offsets are handled exactly — Mask mode now accepts offsets > 2047 thatoffset_to_immpreviously declined.Red → green
scripts/repro/mask_bounds_655_riscv_differential.py(+ 2.wat) — unicorn RV32 execution vs the mask-semantics model, with a deterministic non-periodic pattern in the 64 KiB window and an0xEEsentinel region above it (escapes are detected by value/byte checks, not by an unmapped-page fault); Software mode additionally asserts trap/no-trap.0xeeeeeeeefrom the sentinel) + store (sentinel_intact=False), word final-byte overhang, halfword wrap atea == size, i64 mask escapes (lo and hi), software-mode i64 load and store return instead of trapping, huge-offset compile decline.size-1, word/halfword/i64 in-bounds) and software in-bounds no-trap rows.Selector shape tests:
rv32_mask_folds_offset_before_and_655(access imm must be 0; the offset-add precedes the AND),rv32_mask_clamps_final_byte_for_multibyte_only_655(word clamps, byte doesn't pay),rv32_i64_load_store_guarded_655.Gates
frozen_codegen_bytes, including the RV32 gate — the default RV32 bounds mode isNone, which emits nothing; fixtures don't use--safety-bounds, goldens untouched)cargo test --workspace: 107 suites, 0 failurescargo fmt --check+cargo clippy --workspace --all-targets -- -D warningscleanorigin/main(22517cb, post-v0.34.0)Refs #651, #654.
🤖 Generated with Claude Code