Skip to content

Commit eebe612

Browse files
avrabeclaude
andauthored
fix(bulk-memory): #677 operand clobber + #679 silent-unmasked mask — copy/fill (#695)
* fix(bulk-memory): #677 operand-register clobber + #679 silent-unmasked mask profile Two defects in the #374 memory.copy/memory.fill lowering (select_with_stack), one lane: (dst/src as walking loop pointers, len as the byte buffer). LocalGet of a register-homed local (AAPCS param r0-r3, promoted local r4-r8) pushes the HOME register itself, so a local reused AFTER the op read a wild mem_base+cursor pointer or the last byte copied. Fix, mirroring the #193 reservation discipline: `bulk_mutable_operand` copies a popped operand into a fresh scratch before mutation when it is still live (live param/promoted home, duplicate vstack entry, if/block result reg, or aliased to another popped operand of the same op); a provably-dead temp is used in place, keeping the const-operand shapes byte-identical (#374 differential still 16/16). The red differential also exposed the #663-class range-realloc hole the fix then tripped over: `try_reallocate_segment` treated a pool register with NO range in a segment as free, but such a register can be LIVE-THROUGH (a param home the segment never touches — the memcpy backward path recolored its walking-pointer intermediate onto R0, the still-live dst local). Absent pool colours are now blocked with synthetic pinned interference nodes; identity colouring within the segment's present registers always exists, so no recoloring the original bytes had is lost (frozen anchors stay 10/10 bit-identical). Relaxed-exit terminal segments keep the #580 exemptions (only absent R0/R1 blocked past the bx lr). was emitted byte-identical to `none` while safety-manifest.json still attested "mask" (attestation-integrity hole). The lowering now applies the scalar #651/#654 mask_effective_address wrap-not-trap discipline: dst and src effective addresses fold with AND (size-1) and len clamps to size-dst / size-src so the FINAL byte stays in bounds — every loop access lands in [0, size), wasm-in-bounds ops are unchanged, and the manifest's mask claim is now backed by the emission (mask ≢ none proven by the pure-bulk byte-diff gate). Oracles (all run locally, red on v0.37.1 → green here): - scripts/repro/bulk_local_clobber_677_differential.py — 2/8 → 8/8 vs wasmtime under unicorn (dst/src/len reuse + const control). - scripts/repro/bulk_mask_679_differential.py — pure-bulk byte-diff (identical → differs), manifest coherence, escape/fold/clamp vectors with R10=4096 and out-of-bound containment (raw escaped writes → contained). - scripts/repro/bulk_memory_374_differential.py — 16/16 (unchanged shapes byte-identical; script gains SYNTH env override). - frozen_codegen_bytes 10/10; safety_bounds_377 13/13+13/13; unreachable_665, i32_shift_mask_682 PASS; cargo test --workspace green; fmt + clippy -D clean. - 8 new selector unit tests (677 preservation/aliasing/no-copy-when-dead, 679 fold+clamp presence, mask≠none structural). Both oracles are CI-wired in the trap-semantics job (#489 discipline). Closes #677. Closes #679. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * fix: clippy values_mut + harness reads symtab by SHT_SYMTAB type (#489 pattern) - liveness.rs: iter_mut over map → values_mut (rust-1.97 clippy). - The two #677/#679 differential harnesses read .symtab via get_section_by_name, which returns None because synth emits an unnamed SHT_SYMTAB section; switched to iterate by sh_type (the established #489 pattern all other harnesses use). Both oracles PASS locally. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> --------- Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
1 parent 4a3e6bf commit eebe612

8 files changed

Lines changed: 963 additions & 9 deletions

File tree

.github/workflows/ci.yml

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -346,6 +346,10 @@ jobs:
346346
# elision never fires unsoundly (red-tested at land time).
347347
- name: Run i32 shift-mask oracle with mask elision ON (#686)
348348
run: SYNTH_SHIFT_MASK_ELIDE=1 SYNTH=./target/debug/synth python scripts/repro/i32_shift_mask_682_differential.py
349+
- name: Run bulk-memory operand-clobber oracle (#677, thumb2)
350+
run: SYNTH=./target/debug/synth python scripts/repro/bulk_local_clobber_677_differential.py
351+
- name: Run bulk-memory mask-coverage oracle (#679, thumb2)
352+
run: SYNTH=./target/debug/synth python scripts/repro/bulk_mask_679_differential.py
349353

350354
fact-spec-oracle:
351355
name: fact-spec elision oracle (#494 phases 2 + 2b)

crates/synth-synthesis/src/instruction_selector.rs

Lines changed: 489 additions & 7 deletions
Large diffs are not rendered by default.

crates/synth-synthesis/src/liveness.rs

Lines changed: 35 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3612,12 +3612,46 @@ fn try_reallocate_segment(
36123612

36133613
// Colouring input: pool ranges only (reserved registers cannot collide
36143614
// with pool colours, so their edges are irrelevant to the colouring).
3615-
let pool_adj: BTreeMap<usize, BTreeSet<usize>> = adj
3615+
let mut pool_adj: BTreeMap<usize, BTreeSet<usize>> = adj
36163616
.iter()
36173617
.filter(|(n, _)| pool_nodes.contains(n))
36183618
.map(|(n, nbrs)| (*n, nbrs.intersection(&pool_nodes).copied().collect()))
36193619
.collect();
36203620

3621+
// #677 (the #663 defect class): a pool register with NO range in this
3622+
// segment is not thereby FREE — it may be live-through (defined before the
3623+
// segment, read after it: a param home the segment never touches, a value
3624+
// live across a loop back-edge). Segment-local analysis cannot prove it
3625+
// dead, so introducing it as a rename target silently clobbers the live
3626+
// value — the memory.copy backward path recolored its walking-pointer
3627+
// intermediate onto R0, the still-live dst local (#677). Block every
3628+
// ABSENT pool colour with a synthetic pinned node that interferes with all
3629+
// real pool nodes. This never costs a recoloring the original bytes did
3630+
// not have: simultaneously-live ranges carry distinct ORIGINAL registers
3631+
// (a register holds one value at a time), all of which are present, so an
3632+
// identity-shaped colouring within the present registers always exists.
3633+
// Relaxed-exit terminal segments (VCR-VER-001 #580) keep their exemptions:
3634+
// past the `bx lr` only R0/R1 are observable, so only absent R0/R1 are
3635+
// blocked there — R2-R8/R12 stay introducible, preserving the push-shrink
3636+
// the post-exhaust pass exists for.
3637+
let present: BTreeSet<Reg> = ranges.iter().map(|r| r.reg).collect();
3638+
let mut next_blocker = ranges.len();
3639+
for (idx, reg) in pool.iter().enumerate() {
3640+
if present.contains(reg) {
3641+
continue;
3642+
}
3643+
if relaxed_exit && !matches!(reg, Reg::R0 | Reg::R1) {
3644+
continue;
3645+
}
3646+
let blocker = next_blocker;
3647+
next_blocker += 1;
3648+
pins.insert(blocker, idx);
3649+
for nbrs in pool_adj.values_mut() {
3650+
nbrs.insert(blocker);
3651+
}
3652+
pool_adj.insert(blocker, pool_nodes.iter().copied().collect());
3653+
}
3654+
36213655
// Spill cost: occurrence count per range (1 per def + 1 per use event),
36223656
// replayed with the same numbering.
36233657
let mut costs: BTreeMap<usize, usize> = BTreeMap::new();
Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
(module
2+
;; #677 — memory.copy/memory.fill clobber a local dest/src/len operand that is
3+
;; reused AFTER the op (the lowering mutated the popped register in place as
4+
;; the loop pointer / byte buffer, with no scratch copy).
5+
(memory 1)
6+
(export "memory" (memory 0))
7+
8+
;; dst is a local, read back after the copy (issue reproducer 1).
9+
;; wasmtime: i32.load([dst]) = the copied word. pre-fix synth: wild pointer.
10+
(func (export "cpy_dst") (param i32 i32) (result i32)
11+
(i32.store (i32.const 16) (i32.const 67305985)) ;; 0x04030201 at [16]
12+
(memory.copy (local.get 0) (i32.const 16) (local.get 1))
13+
(i32.load (local.get 0)))
14+
15+
;; memory.fill, dst is a local read back after (issue reproducer 2).
16+
(func (export "fil_dst") (param i32 i32) (result i32)
17+
(memory.fill (local.get 0) (i32.const 66) (local.get 1))
18+
(i32.load8_u (local.get 0)))
19+
20+
;; len operand reused after the copy (issue reproducer 3).
21+
;; pre-fix synth returned the last byte copied (len recycled as byte buffer).
22+
(func (export "cpy_len") (param i32 i32) (result i32)
23+
(i32.store (i32.const 16) (i32.const 99))
24+
(memory.copy (i32.const 32) (i32.const 16) (local.get 1))
25+
(local.get 1))
26+
27+
;; src operand reused after the copy.
28+
(func (export "cpy_src") (param i32 i32) (result i32)
29+
(i32.store (i32.const 16) (i32.const 168496141)) ;; 0x0A0B0C0D at [16]
30+
(memory.copy (i32.const 64) (local.get 0) (local.get 1))
31+
(local.get 0))
32+
33+
;; control: const dest — unaffected pre-fix, isolates the local-operand bug.
34+
(func (export "cpy_const") (param i32 i32) (result i32)
35+
(i32.store (i32.const 16) (i32.const 67305985))
36+
(memory.copy (i32.const 32) (i32.const 16) (local.get 1))
37+
(i32.load (i32.const 32))))
Lines changed: 148 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,148 @@
1+
#!/usr/bin/env python3
2+
"""#677 — bulk-memory operand-register clobber differential (thumb-2).
3+
4+
The #374 memory.copy/memory.fill lowering mutated its popped operand registers
5+
in place (dst/src as walking loop pointers, len as the byte buffer). A popped
6+
register is NOT always a dead temp: `local.get` of a register-homed local
7+
(AAPCS param r0-r3, promoted local r4-r8) pushes the HOME register itself, so
8+
a local reused AFTER the op read a wild `mem_base + <loop cursor>` pointer (for
9+
a dest/src) or the last byte copied (for a len). Const operands were unaffected.
10+
The fix copies any still-live popped operand into a scratch register before the
11+
loop mutates it (#193 reservation discipline, `bulk_mutable_operand`).
12+
13+
**wasmtime is ground truth**; **unicorn** runs synth's Thumb-2 output. All
14+
vectors are in-bounds — this gate is about the RETURN VALUE (the reused local)
15+
and the memory image, not traps. Symbols are read from the ELF symtab
16+
(pyelftools), not `synth disasm` text (host-dependent — see PR #489).
17+
18+
Run:
19+
SYNTH=./target/release/synth python scripts/repro/bulk_local_clobber_677_differential.py
20+
Exits nonzero on any mismatch. RED on pre-fix main, GREEN post-#677.
21+
"""
22+
23+
import os
24+
import subprocess
25+
import sys
26+
import tempfile
27+
from pathlib import Path
28+
29+
import wasmtime
30+
from elftools.elf.elffile import ELFFile
31+
from unicorn import UC_ARCH_ARM, UC_ERR_INSN_INVALID, UC_MODE_THUMB, Uc, UcError
32+
from unicorn.arm_const import (
33+
UC_ARM_REG_LR,
34+
UC_ARM_REG_R0,
35+
UC_ARM_REG_R1,
36+
UC_ARM_REG_R10,
37+
UC_ARM_REG_R11,
38+
UC_ARM_REG_SP,
39+
)
40+
41+
WAT = Path(__file__).with_name("bulk_local_clobber_677.wat")
42+
SYNTH = os.environ.get("SYNTH", "./target/release/synth")
43+
44+
MEM_BYTES = 0x10000 # 1 page = 64 KiB (matches the wat `(memory 1)`)
45+
CODE, LIN, STK, RET = 0x200000, 0x400000, 0x90000, 0x300000
46+
47+
# (fn, arg0, arg1) — arg0 = the local under test (dst/src), arg1 = len.
48+
VECTORS = [
49+
("cpy_dst", 32, 4), # dst local read back: expect 67305985
50+
("cpy_dst", 4096, 8), # different dst, len
51+
("fil_dst", 32, 4), # fill dst local read back: expect 66
52+
("fil_dst", 100, 1),
53+
("cpy_len", 0, 4), # len local reused: expect 4
54+
("cpy_len", 0, 0), # len 0: no-op copy, local must still read 0
55+
("cpy_src", 16, 4), # src local reused: expect 16
56+
("cpy_const", 0, 4), # control (const dest): green pre-fix too
57+
]
58+
59+
60+
def load_text_and_syms(elf_path):
61+
with open(elf_path, "rb") as f:
62+
ef = ELFFile(f)
63+
text = ef.get_section_by_name(".text")
64+
code, base = text.data(), text["sh_addr"]
65+
syms = {}
66+
# synth emits .symtab as an unnamed SHT_SYMTAB section, so match by
67+
# TYPE not name (#489 pattern — get_section_by_name returns None here).
68+
for sec in ef.iter_sections():
69+
if sec.header.sh_type == "SHT_SYMTAB":
70+
for s in sec.iter_symbols():
71+
if s.name:
72+
syms[s.name] = s["st_value"]
73+
if not syms:
74+
# Self-contained images carry no symtab — fall back to `synth disasm`
75+
# labels (same-arch decode, the established #374-harness pattern).
76+
import re
77+
dis = subprocess.run([SYNTH, "disasm", elf_path],
78+
capture_output=True, text=True).stdout
79+
syms = {m.group(2): int(m.group(1), 16)
80+
for m in re.finditer(r"^([0-9a-f]{8}) <(\w+)>:", dis, re.M)}
81+
return code, base, syms
82+
83+
84+
def main():
85+
elf = tempfile.NamedTemporaryFile(suffix=".elf", delete=False).name
86+
subprocess.run(
87+
[SYNTH, "compile", str(WAT), "-o", elf, "--target", "cortex-m4",
88+
"--all-exports", "--safety-bounds", "software"],
89+
check=True,
90+
)
91+
code, base, syms = load_text_and_syms(elf)
92+
93+
eng = wasmtime.Engine()
94+
mod = wasmtime.Module(eng, WAT.read_bytes())
95+
96+
def wasmtime_run(fn, a, b):
97+
store = wasmtime.Store(eng)
98+
inst = wasmtime.Instance(store, mod, [])
99+
ret = inst.exports(store)[fn](store, a, b)
100+
mem = inst.exports(store)["memory"]
101+
img = bytes(mem.read(store, 0, MEM_BYTES))
102+
return ret & 0xFFFFFFFF, img
103+
104+
def unicorn_run(fn, a, b):
105+
fa = syms[fn] & ~1 # thumb bit
106+
mu = Uc(UC_ARCH_ARM, UC_MODE_THUMB)
107+
mu.mem_map(CODE, 0x10000)
108+
mu.mem_map(LIN, MEM_BYTES)
109+
mu.mem_map(STK - 0x8000, 0x10000)
110+
mu.mem_map(RET, 0x1000)
111+
mu.mem_write(CODE, code)
112+
mu.mem_write(LIN, b"\x00" * MEM_BYTES)
113+
mu.reg_write(UC_ARM_REG_SP, STK)
114+
mu.reg_write(UC_ARM_REG_R11, LIN) # linear-memory base
115+
mu.reg_write(UC_ARM_REG_R10, MEM_BYTES) # memory size (bytes)
116+
mu.reg_write(UC_ARM_REG_R0, a & 0xFFFFFFFF)
117+
mu.reg_write(UC_ARM_REG_R1, b & 0xFFFFFFFF)
118+
mu.reg_write(UC_ARM_REG_LR, RET | 1)
119+
try:
120+
mu.emu_start((CODE + fa - base) | 1, RET, count=500000)
121+
except UcError as e:
122+
# No vector here should trap; UDF or an unmapped access both mean
123+
# a wild pointer escaped — report as ERR, never a match.
124+
return f"ERR:{e}", b""
125+
return mu.reg_read(UC_ARM_REG_R0), bytes(mu.mem_read(LIN, MEM_BYTES))
126+
127+
fails = 0
128+
for fn, a, b in VECTORS:
129+
gt_ret, gt_img = wasmtime_run(fn, a, b)
130+
sy_ret, sy_img = unicorn_run(fn, a, b)
131+
if isinstance(sy_ret, str):
132+
ok, detail = False, sy_ret
133+
else:
134+
ok = sy_ret == gt_ret and sy_img == gt_img
135+
detail = f"ret synth={sy_ret} wasmtime={gt_ret}"
136+
if sy_img != gt_img:
137+
diff = next(i for i in range(MEM_BYTES) if sy_img[i] != gt_img[i])
138+
detail += (f"; mem differs @{diff}: synth=0x{sy_img[diff]:02x} "
139+
f"wasmtime=0x{gt_img[diff]:02x}")
140+
fails += 0 if ok else 1
141+
print(f"{fn}({a},{b}): {'OK' if ok else 'MISMATCH'} [{detail}]")
142+
print(f"\n{len(VECTORS) - fails}/{len(VECTORS)} match")
143+
print("ORACLE: PASS" if fails == 0 else f"ORACLE: FAIL ({fails})")
144+
sys.exit(1 if fails else 0)
145+
146+
147+
if __name__ == "__main__":
148+
main()

scripts/repro/bulk_mask_679.wat

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
(module
2+
;; #679 — `--safety-bounds mask` was a silent no-op for memory.copy /
3+
;; memory.fill: the bulk lowering was emitted byte-identical to `none`
4+
;; (no fold, no clamp) while the safety manifest still attested `mask`.
5+
(memory 1)
6+
(export "memory" (memory 0))
7+
8+
;; issue reproducer: copy 1 byte [100] -> dst=local0, read back [16].
9+
;; With mem_size=4096 and dst=4112: masked dst folds 4112&4095=16 -> 171.
10+
;; Escaped (pre-fix): raw write at 4112, [16] untouched -> 0.
11+
(func (export "cpy_esc") (param i32 i32) (result i32)
12+
(i32.store8 (i32.const 100) (i32.const 171))
13+
(i32.store8 (i32.const 16) (i32.const 0))
14+
(memory.copy (local.get 0) (i32.const 100) (i32.const 1))
15+
(i32.load8_u (i32.const 16)))
16+
17+
;; fill escape: fill 1 byte 238 at dst=local0, read back [24].
18+
(func (export "fil_esc") (param i32 i32) (result i32)
19+
(i32.store8 (i32.const 24) (i32.const 0))
20+
(memory.fill (local.get 0) (i32.const 238) (i32.const 1))
21+
(i32.load8_u (i32.const 24)))
22+
23+
;; src escape: stage 205 at [40]; copy 1 byte src=local0 -> [8]; read [8].
24+
;; With src=4136: masked src folds 4136&4095=40 -> 205.
25+
(func (export "cpy_src_esc") (param i32 i32) (result i32)
26+
(i32.store8 (i32.const 40) (i32.const 205))
27+
(i32.store8 (i32.const 8) (i32.const 0))
28+
(memory.copy (i32.const 8) (local.get 0) (i32.const 1))
29+
(i32.load8_u (i32.const 8)))
30+
31+
;; len clamp: stage 119 at [3]; copy len=local1 bytes [0..) -> [4092..).
32+
;; With len=400 and mem_size=4096: len clamps to 4096-4092=4 — the copy
33+
;; ends exactly at the bound; read back [4095] (= staged byte [3]).
34+
(func (export "cpy_clamp") (param i32 i32) (result i32)
35+
(i32.store8 (i32.const 3) (i32.const 119))
36+
(memory.copy (i32.const 4092) (i32.const 0) (local.get 1))
37+
(i32.load8_u (i32.const 4095))))

0 commit comments

Comments
 (0)