Skip to content

Commit f8c6826

Browse files
avrabeclaude
andauthored
fix(safety-bounds): #651 — mask bounds the EFFECTIVE address (offset folded before the AND, final byte clamped) (#654)
--safety-bounds mask (direct/thumb-2 path) applied the mask to the OPERAND only and added the static offset AFTER the AND: and.w r0, r0, r10 ; operand & R10 movw/movt r12, #offset add.w r12, r0, r12 ; offset re-added AFTER the mask ldr.w r0, [r11, r12] ; escapes the bound by up to ~4 GiB Two bugs, one lowering: 1. offset ordering — WASM's effective address is `operand + offset` (u33); masking the operand alone lets any non-zero offset escape. 2. mask value — the AND used R10 = memory SIZE in bytes, not `size-1`: for the default 64 KiB memory, `addr & 0x10000` keeps only bit 16, remapping IN-BOUNDS accesses (0xffff -> 0). New lowering (all 8 masking-emission sites funnel through one helper, `mask_effective_address`): [movw/movt r12, #offset ; offsets > 0xFF materialized add addr, addr, r12] ; fold the static offset FIRST sub r12, r10, #1 ; mask = size-1, derived per access and addr, addr, r12 ; ea & (size-1) [sub r12, r12, #(size-1) ; clamp start to size - access_size so cmp addr, r12 ; the access's FINAL byte stays inside it hi; movhi addr, r12] ; the bound (skipped for byte accesses) ldr/str [r11, addr] ; offset 0 — nothing re-added post-mask Soundness of ADD-then-AND (no decline needed for large offsets): the u33 effective address `ea = operand + offset < 2^33`; ARM's ADD gives `ea mod 2^32`, and every set bit of `size-1 < 2^32` lies below bit 32, so `(ea mod 2^32) & (size-1) == ea & (size-1)` exactly. The final-byte clamp mirrors #640's `offset + access_size - 1` software-guard rule and never alters a wasm-defined access: a masked start above `size - access_size` implies the wasm access traps, which the mask profile deliberately replaces with a deterministic in-bounds access (wrap-not-trap, design doc §3.1 path C). Sites audited: the 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 (all now delegate); arm_encoder has no mask emission; bulk-memory memory.copy/fill masking remains the separately-documented #374 gap; the optimized path already declines mask to the direct selector (#640). Also: the ARM backend now declines a non-power-of-two linear-memory size under mask loudly (mirroring the RISC-V backend) — `AND (size-1)` would silently remap in-bounds addresses. Oracles: - tests/issue_651_mask_effective_address.rs — executable differential: mini ARM interpreter runs the selected ops and checks the wasm-side address of the actual access. 8/8 RED on origin/main (huge-offset escape 0xffff0000, small-offset escape, store variant, in-bounds address preservation, word/i64 final-byte clamp, byte-access exactness, halfword boundary); 8/8 green with the fix. - selector unit tests pin the emitted sequence (offset ADD strictly before the AND, MOVW/MOVT materialization, offset-0 access, no clamp for byte accesses). - frozen anchors 10/10 (fixtures don't use --safety-bounds); full workspace suite green; fmt + clippy -D warnings clean. Closes #651 Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
1 parent 9789651 commit f8c6826

3 files changed

Lines changed: 792 additions & 89 deletions

File tree

‎crates/synth-backend/src/arm_backend.rs‎

Lines changed: 19 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -316,7 +316,25 @@ fn compile_wasm_to_arm(
316316
SafetyBounds::None => BoundsCheckConfig::None,
317317
SafetyBounds::Mpu => BoundsCheckConfig::Mpu,
318318
SafetyBounds::Software => BoundsCheckConfig::Software,
319-
SafetyBounds::Mask => BoundsCheckConfig::Masking,
319+
SafetyBounds::Mask => {
320+
// #651 (mirroring the RISC-V backend's compile-time decline):
321+
// index masking wraps `ea & (size-1)` — a modulo only when the
322+
// linear-memory size is a power of two. With a non-power-of-two
323+
// size the AND would silently REMAP in-bounds addresses (e.g.
324+
// 0x18000 & 0x2FFFF = 0x8000 for a 192 KiB memory). Decline
325+
// loudly rather than miscompile. `linear_memory_bytes == 0`
326+
// means "unknown" (plain per-function path, no module context)
327+
// — the startup default of one 64 KiB page is a power of two.
328+
let bytes = config.linear_memory_bytes;
329+
if bytes != 0 && !bytes.is_power_of_two() {
330+
return Err(format!(
331+
"--safety-bounds mask requires a power-of-two linear-memory \
332+
size, got {bytes} bytes — switch to --safety-bounds software \
333+
for the deterministic check (#651)"
334+
));
335+
}
336+
BoundsCheckConfig::Masking
337+
}
320338
};
321339

322340
// The non-optimized (direct) instruction-selection path. Handles f32 via

0 commit comments

Comments
 (0)