fix(safety-bounds): #651 — mask bounds the EFFECTIVE address (offset folded before the AND, final byte clamped)

[avrabe]

Fixes #651.

The bug (two, in one lowering)

--safety-bounds mask (direct selector, thumb-2) emitted, for (i32.load offset=0xffff0000 (local.get 0)):

and.w  r0, r0, r10        ; operand & R10   — mask applied to the OPERAND
movw   r12, #0x0
movt   r12, #0xffff
add.w  r12, r0, r12       ; offset re-added AFTER the mask
ldr.w  r0, [r11, r12]     ; escapes the bound by up to ~4 GiB

1. Offset ordering (the filed issue): WASM's effective address is operand + offset (u33). Masking the operand only lets any non-zero static offset escape the bound — the entire point of the masking profile (bounded, trap-free access) defeated.
2. Mask value (latent, surfaced by the oracle): the AND used R10 = memory SIZE in bytes, not size-1. For the default 64 KiB memory, addr & 0x10000 keeps only bit 16 — in-bounds accesses were remapped too (0xffff → 0).

The fix

All 8 masking-emission sites now delegate to one helper, mask_effective_address (crates/synth-synthesis/src/instruction_selector.rs), which computes

masked = min((operand + offset) & (size - 1), size - access_size)

[movw/movt r12, #offset]   ; offsets > 0xFF materialized via the R12 scratch
[add  addr, addr, r12]     ; fold the static offset FIRST
 sub  r12, r10, #1         ; mask = size-1, derived per access (R10 keeps its
 and  addr, addr, r12      ;   memory.size contract)
[sub  r12, r12, #(s-1)     ; clamp the start to size - access_size so the
 cmp  addr, r12            ;   access's FINAL byte stays inside the bound
 it hi; movhi addr, r12]   ;   (skipped for byte accesses — cannot overhang)
 ldr/str [r11, addr]       ; offset 0 — nothing is re-added after the mask

Soundness argument for ADD-then-AND (large offsets do NOT decline)

ea = operand + offset < 2^33 (both u32). The ARM ADD computes ea mod 2^32; every set bit of the mask size-1 < 2^32 lies below bit 32, so (ea mod 2^32) & (size-1) == ea & (size-1) — the u33 carry is annihilated by the AND either way. Arbitrary 32-bit offsets are therefore handled exactly (materialized via MOVW/MOVT when > 0xFF), no decline needed.

Final byte (mirroring #640's offset + access_size - 1 software-guard rule): the AND bounds only the first byte; a multi-byte access starting in the last access_size-1 bytes would overhang, so the CMP/IT-HI clamp caps the start at size - access_size, giving start + access_size - 1 ≤ size - 1 unconditionally. The clamp never alters a wasm-defined access: a masked start above size - access_size for an in-range ea implies ea + access_size - 1 ≥ size, which wasm traps — the mask profile deliberately replaces that trap with a deterministic in-bounds access (wrap-not-trap, design doc §3.1 path C). In-bounds accesses are executed at their exact address; the profile's power-of-two contract is now enforced loudly by the ARM backend (mirroring the RISC-V backend's compile-time decline) since AND (size-1) on a non-power-of-two size would silently remap in-bounds addresses.

Sites audited (no wildcard survives)

• instruction_selector.rs: all 8 generate_{load,store,i64_load,i64_store,i64_load_into_regs,i64_store_from_regs,subword_load,subword_store}_with_bounds_check Masking arms — every one had the identical operand-first AND; all now delegate to the single helper, and the memory op itself uses offset 0 under Masking.
• arm_encoder.rs: no mask emission (grep-verified).
• Bulk memory (memory.copy/fill): masking remains the separately-documented arm backend cannot lower memory.copy/memory.fill — 19 sites, falcon's largest remaining on-target gap #374 gap (Software is the guarded mode there) — unchanged.
• Optimized path: already declines mask to the direct selector (fix(safety-bounds): #377 — software bounds enforced on the optimized path; inline UDF trap fixes the direct path's fallthrough no-op #640) — its census test (optimized ≡ direct bytes) still passes.
• RISC-V's Mask lowering masks the operand before the offset too (emit_bounds_check returns the masked operand, callers fold the offset into the addressing) — same class, separate backend, not touched here; will file follow-up.

Red → green

crates/synth-synthesis/tests/issue_651_mask_effective_address.rs — executable differential: a mini ARM interpreter (the semantic_correctness.rs pattern) runs the selected ops with R10 = 64 KiB and checks the wasm-side address of the actual R11-based access against the mask-semantics model.

• origin/main (5f8c24c): 8/8 FAILED — e.g. access [0xffff0000, 0xffff0003] escapes the 0x10000-byte bound (the filed escape) and masked access at 0x0, mask semantics require 0xffff (the latent R10-is-size bug remapping an in-bounds byte load).
• this branch: 8/8 ok — huge-offset escape, small-offset escape, store variant, in-bounds address preservation (exact), word/i64 final-byte clamp, byte-access exactness at size-1, halfword boundary.

End-to-end (CLI, -t cortex-m3 --safety-bounds mask, force-thumb objdump): peek/poke emit exactly the sequence above; a 3-page (non-power-of-two) memory now declines with an actionable error.

Gates

• frozen anchors 10/10 (frozen_codegen_bytes; fixtures don't use --safety-bounds)
• full cargo test --workspace green (107 suites, 0 failures)
• cargo fmt --check + cargo clippy --workspace --all-targets -- -D warnings clean
• rebased onto origin/main (b471c38, post-fix(decoder): float-typed global accesses loud-skip — the last silent float path (GI-FPU-001, #369) #648)

🤖 Generated with Claude Code

[codecov]

Codecov Report

❌ Patch coverage is 84.94624% with 28 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
crates/synth-synthesis/src/instruction_selector.rs	87.00%	23 Missing ⚠️
crates/synth-backend/src/arm_backend.rs	44.44%	5 Missing ⚠️

📢 Thoughts on this report? Let us know!