From 060af7ec630acbc02fcfafa0c45cd78d92b97b88 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 18 Jun 2026 07:56:55 +0200 Subject: [PATCH 1/3] =?UTF-8?q?track(#359):=20POST-LINK=20oracle=20?= =?UTF-8?q?=E2=80=94=20the=20structural=20fix=20to=20the=20#368=20.o-only?= =?UTF-8?q?=20mistake?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit #368 passed a unicorn-on-.o oracle but failed on silicon (rc=-35) because the #354 link-time retargeting is invisible to a flat-memory .o model. This builds the actual linked image (postlink.ld mimics Zephyr: __synth_wasm_seg_0 in .data, __synth_wasm_data == __bss_start in .bss; zephyr_stubs.s for the 6 kernel undefs) and asserts gale's invariant: no __synth_wasm_data + C literal in the STATIC region (C >= wasm_data_base) may resolve into [__bss_start, __bss_end). Pre-fix (v0.11.47) it FAILS with 4 violations: `__synth_wasm_data + 65552` (the action->ret table accessed at offset 65552 = the EXCLUSIVE END of the 16-byte segment [65536,65552)) resolves into .bss instead of seg_0 (.data) — the #354 retargeting's `c < off+len` check excludes the boundary. So the table lookup reads .bss zero -> "queue full" on an empty queue -> rc=-35. Frame accesses (C < wasm_data_base) correctly stay in .bss and are NOT flagged. Necessary, not sufficient: gale's G474RE re-test stays the final gate (runtime index + Thumb effects). Fix (next block): make #354 retargeting cover the segment-boundary/end offset (and any static-region C) so it lands in seg_K. Co-Authored-By: Claude Opus 4.8 --- scripts/repro/n359/postlink.ld | 13 ++++++ scripts/repro/n359/zephyr_stubs.s | 12 ++++++ scripts/repro/postlink_359_oracle.py | 61 ++++++++++++++++++++++++++++ 3 files changed, 86 insertions(+) create mode 100644 scripts/repro/n359/postlink.ld create mode 100644 scripts/repro/n359/zephyr_stubs.s create mode 100755 scripts/repro/postlink_359_oracle.py diff --git a/scripts/repro/n359/postlink.ld b/scripts/repro/n359/postlink.ld new file mode 100644 index 00000000..0cc6f558 --- /dev/null +++ b/scripts/repro/n359/postlink.ld @@ -0,0 +1,13 @@ +/* #359 post-link oracle: mimic the Zephyr layout that gave rc=-35. + __synth_wasm_seg_0 (.data, real table) at 0x20000000; __synth_wasm_data + (.bss, zero reservation) right after .data — matching gale's objdump + (seg_0=0x20000000, __synth_wasm_data==__bss_start). */ +MEMORY { FLASH (rx) : ORIGIN = 0x08000000, LENGTH = 256K + RAM (rwx) : ORIGIN = 0x20000000, LENGTH = 256K } +SECTIONS { + .text : { *(.text*) } > FLASH + .data : { *(.data*) } > RAM + __bss_start = .; + .bss : { *(.bss*) } > RAM + __bss_end = .; +} diff --git a/scripts/repro/n359/zephyr_stubs.s b/scripts/repro/n359/zephyr_stubs.s new file mode 100644 index 00000000..5a372ec8 --- /dev/null +++ b/scripts/repro/n359/zephyr_stubs.s @@ -0,0 +1,12 @@ +.syntax unified +.thumb +.global k_spin_lock, k_spin_unlock, z_ready_thread, z_reschedule +.global z_thread_return_value_set_with_data, z_unpend_first_thread +.thumb_func +k_spin_lock: +k_spin_unlock: +z_ready_thread: +z_reschedule: +z_thread_return_value_set_with_data: +z_unpend_first_thread: + bx lr diff --git a/scripts/repro/postlink_359_oracle.py b/scripts/repro/postlink_359_oracle.py new file mode 100755 index 00000000..020761e8 --- /dev/null +++ b/scripts/repro/postlink_359_oracle.py @@ -0,0 +1,61 @@ +#!/usr/bin/env python3 +""" +#359 POST-LINK ORACLE — the structural fix to the #368 mistake (a unicorn-on-.o +oracle could not see the #354 link-time retargeting, so #368 passed locally and +failed on silicon with rc=-35). + +Builds the actual linked image for msgq_put_359.wasm (native-pointer + #354 +split) using scripts/repro/n359/postlink.ld (mimics Zephyr: __synth_wasm_seg_0 +in .data, __synth_wasm_data == __bss_start in .bss) + zephyr_stubs.s, then +asserts gale's INVARIANT: + + No `__synth_wasm_*` literal that addresses the relocated `.rodata` table may + resolve into [__bss_start, __bss_end) — every static-data access must land in + the .data/seg_K region that owns its offset. + +PRE-FIX (v0.11.47): FAILS — literals `__synth_wasm_data + 0` (= .bss base) and +`__synth_wasm_data + 65552` (= __bss_end) reach .bss, so the action->ret table +lookup reads zero -> "queue full" on an empty queue -> rc=-35. + +Run: PATH=$PWD/target/release:$PATH python3 scripts/repro/postlink_359_oracle.py +Final silicon gate stays gale's G474RE re-test (this oracle is necessary, not +sufficient — Thumb/runtime-index effects need real hardware). +""" +import subprocess, re, struct, sys, os +HERE=os.path.dirname(os.path.abspath(__file__)) +O="/tmp/n359/msgq.o"; ELF="/tmp/n359/msgq.elf" +os.makedirs("/tmp/n359", exist_ok=True) +def run(c): return subprocess.run(c, capture_output=True, text=True) +run(["synth","compile","scripts/repro/msgq_put_359.wasm","--target","cortex-m4f", + "--native-pointer-abi","--relocatable","--all-exports","-o",O]) +run(["arm-none-eabi-as","-mcpu=cortex-m4","-mthumb",f"{HERE}/n359/zephyr_stubs.s","-o","/tmp/n359/stubs.o"]) +ld=run(["arm-none-eabi-ld","-T",f"{HERE}/n359/postlink.ld",O,"/tmp/n359/stubs.o","-o",ELF]) +if ld.returncode!=0: print("LINK FAILED:",ld.stderr); sys.exit(2) +nm={l.split()[2]:int(l.split()[0],16) for l in run(["arm-none-eabi-nm",ELF]).stdout.splitlines() if len(l.split())==3} +bss_lo,bss_hi=nm["__bss_start"],nm["__bss_end"] +# The SP-global init = the static-data base: linmem [0, WASM_DATA_BASE) is the +# shadow-stack/frame region (legitimately the zero `.bss` reservation), and +# [WASM_DATA_BASE, used_extent) is the static `.rodata`/data that #354 splits +# out to `__synth_wasm_seg_K` (`.data`). A `__synth_wasm_data + C` literal +# addressing the STATIC region (C >= base) that resolves into `.bss` is the bug +# (the table moved to seg_K but the access still points at the zero reservation). +# A literal into the frame region (C < base) is correct and NOT a violation. +WASM_DATA_BASE = 65536 # = $__stack_pointer init in msgq_put_359.wasm +s=run(["arm-none-eabi-objdump","-s","-j",".text",ELF]).stdout +viol=[] +for line in s.splitlines(): + p=line.split() + if len(p)>=2 and re.match(r'^[0-9a-f]{6,8}$', p[0]): + base=int(p[0],16) + for i,w in enumerate(p[1:5]): + if re.match(r'^[0-9a-f]{8}$',w): + v=struct.unpack('= WASM_DATA_BASE: + viol.append((base+i*4, v, v - bss_lo)) +print(f"__bss_start={bss_lo:#x} __bss_end={bss_hi:#x} __synth_wasm_seg_0={nm.get('__synth_wasm_seg_0',0):#x} WASM_DATA_BASE={WASM_DATA_BASE}") +for a,v,off in viol: + print(f" text@{a:#08x}: .word {v:#010x} -> __synth_wasm_data + {off} in STATIC region but lands in .bss — VIOLATION") +ok = len(viol)==0 +print("ORACLE:", "PASS (no static-region __synth_wasm_* literal in .bss)" + if ok else f"FAIL ({len(viol)} static-data literals resolve into .bss — #359 #354x#368)") +sys.exit(0 if ok else 1) From 870920de7efd6522ca3019fe04a1574c8ca02820 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 18 Jun 2026 21:02:44 +0200 Subject: [PATCH 2/3] fix(#359): size .bss for native-pointer Abs32 static accesses (the #354 x #368 root cause) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit gale's msgq rc=-35: the action->ret table lookup reads a ZERO word at linmem offset 65552 (the table tail, just past the 16-byte init segment), but the .bss reservation was sized to exactly 65552 — so the access lands at __bss_end and reads garbage, taking the queue-full branch on an empty queue. Root cause: build_relocatable_elf's `static_top` (the .bss/used_extent sizing) filtered `RelocKind::MovwAbs` relocs, but the native-pointer path relocates static-data accesses as Abs32 LITERAL-POOL words (`S + A`). So static_top saw nothing, used_extent fell back to the init-segment end, and EVERY high-offset native-pointer access past that end read past the reservation. New `static_top_abs32` reads the addend C from each `__synth_wasm_data` Abs32 literal (in-place .text word, pre-retarget) so used_extent spans every offset the code touches. This is a GENERAL native-pointer .bss-undersizing bug, not msgq-specific: native_pointer_bss.wat (`i32.store (i32.const 256) ...`) had .bss=4 while writing at offset 256 — a latent past-reservation write; the fix grows its .bss 4->264 (NOBITS, no binary bloat). .bss is the only delta (code byte-identical). Verified: scripts/repro/postlink_359_oracle.py (links the real image, asserts no __synth_wasm_data literal resolves past __bss_end) FAIL->PASS; native_pointer_ shadow_stack differential PASS; 32 synth-cli tests pass; the three frozen fixtures (control_step 0x00210A55, flight_seam 0x07FDF307, div_const 338/338) byte-identical. NECESSARY-NOT-SUFFICIENT: the post-link oracle can't model the runtime msgq round-trip — gale's G474RE rc=0 stays the final gate. HELD for silicon. Co-Authored-By: Claude Opus 4.8 --- crates/synth-cli/src/main.rs | 35 ++++++++++++++++++++++++++++ scripts/repro/postlink_359_oracle.py | 33 +++++++++++++++----------- 2 files changed, 55 insertions(+), 13 deletions(-) diff --git a/crates/synth-cli/src/main.rs b/crates/synth-cli/src/main.rs index 5219abdc..190325c5 100644 --- a/crates/synth-cli/src/main.rs +++ b/crates/synth-cli/src/main.rs @@ -2438,10 +2438,45 @@ fn build_relocatable_elf( .map(|a: u32| a.saturating_add(8)) .max() .unwrap_or(0); + // #359: the native-pointer path relocates static-data accesses as + // Abs32 LITERAL-POOL words (`S + A`), NOT MovwAbs — so the MovwAbs-only + // `static_top` above sees nothing and under-sizes the `.bss` + // reservation. A legitimate high-offset access (gale's msgq action→ret + // lookup reads a ZERO word at offset 65552 — the tail of the table, + // just past the 16-byte init segment) then lands at/past `__bss_end` + // and reads garbage instead of zero, taking the queue-full branch on + // an empty queue → rc=-35 (the #354 × #368 interaction). Cover the + // Abs32 literal addends too (read C from the in-place `.text` word, + // pre-retarget) so the reservation spans every offset the code reads. + let static_top_abs32 = funcs + .iter() + .flat_map(|f| { + f.relocations.iter().filter_map(move |r| { + if r.symbol != "__synth_wasm_data" + || !matches!(r.kind, synth_core::RelocKind::Abs32) + { + return None; + } + let pos = r.offset as usize; + if pos + 4 > f.code.len() { + return None; + } + Some(u32::from_le_bytes([ + f.code[pos], + f.code[pos + 1], + f.code[pos + 2], + f.code[pos + 3], + ])) + }) + }) + .map(|a: u32| a.saturating_add(8)) + .max() + .unwrap_or(0); data_end .max(sp_top) .max(global_top) .max(static_top) + .max(static_top_abs32) .max(4) .min(linear_memory_bytes) .next_multiple_of(4) diff --git a/scripts/repro/postlink_359_oracle.py b/scripts/repro/postlink_359_oracle.py index 020761e8..845e0146 100755 --- a/scripts/repro/postlink_359_oracle.py +++ b/scripts/repro/postlink_359_oracle.py @@ -33,14 +33,21 @@ def run(c): return subprocess.run(c, capture_output=True, text=True) if ld.returncode!=0: print("LINK FAILED:",ld.stderr); sys.exit(2) nm={l.split()[2]:int(l.split()[0],16) for l in run(["arm-none-eabi-nm",ELF]).stdout.splitlines() if len(l.split())==3} bss_lo,bss_hi=nm["__bss_start"],nm["__bss_end"] -# The SP-global init = the static-data base: linmem [0, WASM_DATA_BASE) is the -# shadow-stack/frame region (legitimately the zero `.bss` reservation), and -# [WASM_DATA_BASE, used_extent) is the static `.rodata`/data that #354 splits -# out to `__synth_wasm_seg_K` (`.data`). A `__synth_wasm_data + C` literal -# addressing the STATIC region (C >= base) that resolves into `.bss` is the bug -# (the table moved to seg_K but the access still points at the zero reservation). -# A literal into the frame region (C < base) is correct and NOT a violation. -WASM_DATA_BASE = 65536 # = $__stack_pointer init in msgq_put_359.wasm +# INVARIANT (precise): a `__synth_wasm_data + C` literal in a synth body must +# resolve to a READABLE location holding linmem[C]'s value: +# - C inside an init segment -> the data moved to seg_K (.data), so the literal +# must be RETARGETED (it must NOT still point at __synth_wasm_data/.bss). +# - C in a zero region -> stays __synth_wasm_data + C in .bss, which is correct +# ONLY IF the .bss reservation covers C (C < used_extent, i.e. the resolved +# address < __bss_end). Reading AT/PAST __bss_end is the #359 bug: gale's msgq +# reads a zero word at offset 65552 (the table tail), but .bss was sized to +# exactly 65552 (the init-seg end) because static_top filtered MovwAbs while +# the real relocs are Abs32 -> the access lands at __bss_end and reads garbage. +# So flag any literal that resolves at/past __bss_end but within the plausible +# linmem window [__bss_start, __bss_start + 128 KiB) — a static access that reads +# past the zero reservation. (The post-link image is NECESSARY-not-sufficient; +# numeric rc=0 stays gale's G474RE round-trip.) +MARGIN = 0x40 # a real boundary over-read lands just past __bss_end; wider hits = code words s=run(["arm-none-eabi-objdump","-s","-j",".text",ELF]).stdout viol=[] for line in s.splitlines(): @@ -50,12 +57,12 @@ def run(c): return subprocess.run(c, capture_output=True, text=True) for i,w in enumerate(p[1:5]): if re.match(r'^[0-9a-f]{8}$',w): v=struct.unpack('= WASM_DATA_BASE: + if bss_hi <= v < bss_hi + MARGIN: viol.append((base+i*4, v, v - bss_lo)) -print(f"__bss_start={bss_lo:#x} __bss_end={bss_hi:#x} __synth_wasm_seg_0={nm.get('__synth_wasm_seg_0',0):#x} WASM_DATA_BASE={WASM_DATA_BASE}") +print(f"__bss_start={bss_lo:#x} __bss_end={bss_hi:#x} __synth_wasm_seg_0={nm.get('__synth_wasm_seg_0',0):#x} .bss size={bss_hi-bss_lo}") for a,v,off in viol: - print(f" text@{a:#08x}: .word {v:#010x} -> __synth_wasm_data + {off} in STATIC region but lands in .bss — VIOLATION") + print(f" text@{a:#08x}: .word {v:#010x} -> __synth_wasm_data + {off} resolves AT/PAST __bss_end (reads past the zero reservation) — VIOLATION") ok = len(viol)==0 -print("ORACLE:", "PASS (no static-region __synth_wasm_* literal in .bss)" - if ok else f"FAIL ({len(viol)} static-data literals resolve into .bss — #359 #354x#368)") +print("ORACLE:", "PASS (no __synth_wasm_* literal reads past __bss_end)" + if ok else f"FAIL ({len(viol)} static-data literals read past .bss — #359 #354x#368)") sys.exit(0 if ok else 1) From 54692b312d82190195f9e0657fb420bb61c37540 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 18 Jun 2026 23:50:09 +0200 Subject: [PATCH 3/3] =?UTF-8?q?chore(release):=20v0.11.48=20=E2=80=94=20#3?= =?UTF-8?q?59=20native-pointer=20.bss=20sizing=20(silicon-confirmed)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Pin sweep 0.11.47 -> 0.11.48 (workspace + 10 path-deps + MODULE.bazel + Cargo.lock). CHANGELOG v0.11.48 with falsification. rivet GI-NPA-005 -> verified (gale G474RE rc=0 + val=0xABCD round-trip). The #359 .bss-undersizing fix is in 870920d; this is the release bump. Co-Authored-By: Claude Opus 4.8 --- CHANGELOG.md | 37 ++++++++++++++++++++++++++ Cargo.lock | 34 +++++++++++------------ Cargo.toml | 2 +- MODULE.bazel | 2 +- artifacts/gale-integration.yaml | 37 ++++++++++++++++++++++++++ crates/synth-backend-awsm/Cargo.toml | 2 +- crates/synth-backend-riscv/Cargo.toml | 4 +-- crates/synth-backend-wasker/Cargo.toml | 2 +- crates/synth-backend/Cargo.toml | 4 +-- crates/synth-cli/Cargo.toml | 16 +++++------ crates/synth-frontend/Cargo.toml | 2 +- crates/synth-opt/Cargo.toml | 2 +- crates/synth-synthesis/Cargo.toml | 6 ++--- crates/synth-verify/Cargo.toml | 8 +++--- 14 files changed, 116 insertions(+), 42 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 6449f761..47099fdd 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,6 +7,43 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ## [Unreleased] +## [0.11.48] - 2026-06-18 + +**ON-TARGET — #359 closed on silicon (G474RE `rc=0`): the dissolved msgq +primitive is functionally correct. Native-pointer `.bss` is now sized for the +Abs32 static accesses it was silently undersizing.** + +- **#359 — `.bss` under-sizing for native-pointer Abs32 static accesses** (the + `#354 × #368` interaction): gale's dissolved `k_msgq_put` returned `rc=-35` + (`-ENOMSG`, queue-full on an empty queue). Root cause: `build_relocatable_elf`'s + `used_extent`/`static_top` computation filtered `RelocKind::MovwAbs`, but the + native-pointer path relocates static-data accesses as **`Abs32` literal-pool** + words (`S + A`). So `static_top` saw nothing, `used_extent` fell back to the + init-segment end, and the decide's action→ret lookup — a **zero word at offset + 65552** (the table tail, just past the 16-byte init segment) — landed at + `__bss_end` and read **garbage** instead of zero, taking the queue-full branch. + New `static_top_abs32` reads the addend from each `__synth_wasm_data` `Abs32` + literal (the in-place `.text` word, pre-retarget) so the `.bss` reservation + spans every offset the code touches (msgq: 65552 → `.bss` 65560). General + native-pointer bug, not msgq-specific: `native_pointer_bss` (`i32.store + (i32.const 256) …`) had `.bss=4` while writing at 256 — fix grows it 4→264 + (`.bss` is NOBITS, so zero binary bloat; `.bss` `sh_size` is the only delta, + code byte-identical). + + Verified: a new **post-link oracle** (`scripts/repro/postlink_359_oracle.py` — + links the real image and asserts no `__synth_wasm_data` literal resolves past + `__bss_end`, the structural fix to the `.o`-only oracle that let #368 pass + locally and fail on silicon) went **FAIL → PASS**; the three frozen fixtures + (control_step `0x00210A55`, flight_seam `0x07FDF307`, div_const 338/338) stay + byte-identical; native-pointer numeric differential PASS; 32 cli tests green. + **Silicon-confirmed by gale on NUCLEO-G474RE: `rc=0`, `val=0xABCD`, correct + round-trip on an empty queue** (was `rc=-35`/`val=0x0`). This clears msgq's + last on-target blocker (#372 was the other, v0.11.47). + + **Falsification:** a native-pointer module whose highest static access lands at + offset `O` now reserves `.bss ≥ O + 8`; a `__synth_wasm_data + O` access reads + within the reservation (correct zero / data) instead of past `__bss_end`. + ## [0.11.47] - 2026-06-18 **CORRECTNESS — #372: `i64.load`/`i64.store` now lower correctly (they were diff --git a/Cargo.lock b/Cargo.lock index b6f474ae..c9b61cdc 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1908,14 +1908,14 @@ dependencies = [ [[package]] name = "synth-abi" -version = "0.11.47" +version = "0.11.48" dependencies = [ "synth-wit", ] [[package]] name = "synth-analysis" -version = "0.11.47" +version = "0.11.48" dependencies = [ "anyhow", "synth-core", @@ -1924,7 +1924,7 @@ dependencies = [ [[package]] name = "synth-backend" -version = "0.11.47" +version = "0.11.48" dependencies = [ "anyhow", "synth-core", @@ -1934,7 +1934,7 @@ dependencies = [ [[package]] name = "synth-backend-awsm" -version = "0.11.47" +version = "0.11.48" dependencies = [ "anyhow", "synth-core", @@ -1943,7 +1943,7 @@ dependencies = [ [[package]] name = "synth-backend-riscv" -version = "0.11.47" +version = "0.11.48" dependencies = [ "anyhow", "proptest", @@ -1955,7 +1955,7 @@ dependencies = [ [[package]] name = "synth-backend-wasker" -version = "0.11.47" +version = "0.11.48" dependencies = [ "anyhow", "synth-core", @@ -1964,11 +1964,11 @@ dependencies = [ [[package]] name = "synth-cfg" -version = "0.11.47" +version = "0.11.48" [[package]] name = "synth-cli" -version = "0.11.47" +version = "0.11.48" dependencies = [ "anyhow", "clap", @@ -1990,7 +1990,7 @@ dependencies = [ [[package]] name = "synth-core" -version = "0.11.47" +version = "0.11.48" dependencies = [ "anyhow", "serde", @@ -2003,7 +2003,7 @@ dependencies = [ [[package]] name = "synth-frontend" -version = "0.11.47" +version = "0.11.48" dependencies = [ "anyhow", "synth-core", @@ -2017,14 +2017,14 @@ dependencies = [ [[package]] name = "synth-memory" -version = "0.11.47" +version = "0.11.48" dependencies = [ "bitflags", ] [[package]] name = "synth-opt" -version = "0.11.47" +version = "0.11.48" dependencies = [ "criterion", "synth-cfg", @@ -2032,11 +2032,11 @@ dependencies = [ [[package]] name = "synth-qemu" -version = "0.11.47" +version = "0.11.48" [[package]] name = "synth-synthesis" -version = "0.11.47" +version = "0.11.48" dependencies = [ "anyhow", "proptest", @@ -2051,7 +2051,7 @@ dependencies = [ [[package]] name = "synth-test" -version = "0.11.47" +version = "0.11.48" dependencies = [ "anyhow", "clap", @@ -2067,7 +2067,7 @@ dependencies = [ [[package]] name = "synth-verify" -version = "0.11.47" +version = "0.11.48" dependencies = [ "anyhow", "chrono", @@ -2085,7 +2085,7 @@ dependencies = [ [[package]] name = "synth-wit" -version = "0.11.47" +version = "0.11.48" [[package]] name = "tempfile" diff --git a/Cargo.toml b/Cargo.toml index 2cf4ce90..33931488 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -27,7 +27,7 @@ resolver = "2" # semver to publish, so the convention now catches up: workspace # version follows the release tag, bumped pre-tag in the release # checklist. See docs/release-process.md. -version = "0.11.47" +version = "0.11.48" edition = "2024" rust-version = "1.88" authors = ["PulseEngine Team"] diff --git a/MODULE.bazel b/MODULE.bazel index 78c38d92..4efed2f8 100644 --- a/MODULE.bazel +++ b/MODULE.bazel @@ -7,7 +7,7 @@ module( name = "synth", # Kept in lockstep with [workspace.package] version in Cargo.toml. # Both are bumped pre-tag — see docs/release-process.md. - version = "0.11.47", + version = "0.11.48", ) # Bazel dependencies diff --git a/artifacts/gale-integration.yaml b/artifacts/gale-integration.yaml index c39e6228..6e6e8143 100644 --- a/artifacts/gale-integration.yaml +++ b/artifacts/gale-integration.yaml @@ -748,3 +748,40 @@ artifacts: pass-criteria: > ld64(16)=0x8877665544332211 on optimized + direct ELFs; frozen oracles + u64_unpack byte-identical; cargo test test_372 green. + + - id: GI-NPA-005 + type: sw-req + title: Native-pointer .bss sized for Abs32 static accesses (#359 — #354 x #368) + description: > + gale's dissolved k_msgq_put returned rc=-35 on G474RE: the action→ret + lookup read a ZERO word at linmem offset 65552 (the table tail, just past + the 16-byte init segment) but the .bss reservation was sized to the + init-segment end (65552), so the access landed at __bss_end and read + garbage -> queue-full on an empty queue. Root cause: + build_relocatable_elf's used_extent/static_top filtered RelocKind::MovwAbs, + but the native-pointer path emits Abs32 LITERAL-POOL relocs (S + A), so + static_top saw nothing and used_extent under-sized .bss. IMPLEMENTED + v0.11.48 (870920d): static_top_abs32 reads the addend from each + __synth_wasm_data Abs32 literal so .bss spans every accessed offset (msgq + 65552 -> .bss 65560). General bug: native_pointer_bss (store@256, .bss was + 4) grows 4->264 (.bss NOBITS, no bloat). NOT the retarget-completeness + first assumed (the naive boundary tweak would mis-point at __synth_globals). + Necessary-not-sufficient post-link oracle (postlink_359_oracle.py) gated the + fix; gale's G474RE round-trip was the sufficient gate. + status: verified + tags: [gale, native-pointer-abi, bss, elf, on-target, silicon-verified, release-v0.11.48] + links: + - type: derives-from + target: GI-NPA-001 + - type: traces-to + target: gale:359 + fields: + req-type: functional + priority: must + verification-criteria: > + scripts/repro/postlink_359_oracle.py (links the real image, asserts no + __synth_wasm_data literal resolves past __bss_end) FAIL->PASS; the three + frozen fixtures (control_step 0x00210A55, flight_seam 0x07FDF307, + div_const 338/338) byte-identical; native_pointer_shadow_stack + differential PASS; 32 cli tests green; gale G474RE silicon rc=0 + + val=0xABCD round-trip on an empty queue (was rc=-35/val=0x0). diff --git a/crates/synth-backend-awsm/Cargo.toml b/crates/synth-backend-awsm/Cargo.toml index bbe479c6..615e2b7c 100644 --- a/crates/synth-backend-awsm/Cargo.toml +++ b/crates/synth-backend-awsm/Cargo.toml @@ -11,6 +11,6 @@ categories.workspace = true description = "aWsm backend integration for the Synth compiler" [dependencies] -synth-core = { path = "../synth-core", version = "0.11.47" } +synth-core = { path = "../synth-core", version = "0.11.48" } anyhow.workspace = true thiserror.workspace = true diff --git a/crates/synth-backend-riscv/Cargo.toml b/crates/synth-backend-riscv/Cargo.toml index d7849217..7faca755 100644 --- a/crates/synth-backend-riscv/Cargo.toml +++ b/crates/synth-backend-riscv/Cargo.toml @@ -11,8 +11,8 @@ categories.workspace = true description = "RISC-V encoder, ELF builder, PMP allocator, and bare-metal startup for synth" [dependencies] -synth-core = { path = "../synth-core", version = "0.11.47" } -synth-synthesis = { path = "../synth-synthesis", version = "0.11.47" } +synth-core = { path = "../synth-core", version = "0.11.48" } +synth-synthesis = { path = "../synth-synthesis", version = "0.11.48" } anyhow.workspace = true thiserror.workspace = true tracing.workspace = true diff --git a/crates/synth-backend-wasker/Cargo.toml b/crates/synth-backend-wasker/Cargo.toml index c84ad056..cc21a151 100644 --- a/crates/synth-backend-wasker/Cargo.toml +++ b/crates/synth-backend-wasker/Cargo.toml @@ -11,6 +11,6 @@ categories.workspace = true description = "Wasker backend integration for the Synth compiler" [dependencies] -synth-core = { path = "../synth-core", version = "0.11.47" } +synth-core = { path = "../synth-core", version = "0.11.48" } anyhow.workspace = true thiserror.workspace = true diff --git a/crates/synth-backend/Cargo.toml b/crates/synth-backend/Cargo.toml index c208a9a9..b1613aed 100644 --- a/crates/synth-backend/Cargo.toml +++ b/crates/synth-backend/Cargo.toml @@ -15,7 +15,7 @@ default = ["arm-cortex-m"] arm-cortex-m = ["synth-synthesis"] [dependencies] -synth-core = { path = "../synth-core", version = "0.11.47" } -synth-synthesis = { path = "../synth-synthesis", version = "0.11.47", optional = true } +synth-core = { path = "../synth-core", version = "0.11.48" } +synth-synthesis = { path = "../synth-synthesis", version = "0.11.48", optional = true } anyhow.workspace = true thiserror.workspace = true diff --git a/crates/synth-cli/Cargo.toml b/crates/synth-cli/Cargo.toml index 938f7548..86cd11ac 100644 --- a/crates/synth-cli/Cargo.toml +++ b/crates/synth-cli/Cargo.toml @@ -27,18 +27,18 @@ verify = ["synth-verify"] # Path deps carry `version` so `cargo publish` rewrites them to the # crates.io coordinate. Bumping the workspace version requires # updating these in lockstep — see docs/release-process.md. -synth-core = { path = "../synth-core", version = "0.11.47" } -synth-frontend = { path = "../synth-frontend", version = "0.11.47" } -synth-synthesis = { path = "../synth-synthesis", version = "0.11.47" } -synth-backend = { path = "../synth-backend", version = "0.11.47" } +synth-core = { path = "../synth-core", version = "0.11.48" } +synth-frontend = { path = "../synth-frontend", version = "0.11.48" } +synth-synthesis = { path = "../synth-synthesis", version = "0.11.48" } +synth-backend = { path = "../synth-backend", version = "0.11.48" } # Optional external backends -synth-backend-awsm = { path = "../synth-backend-awsm", version = "0.11.47", optional = true } -synth-backend-wasker = { path = "../synth-backend-wasker", version = "0.11.47", optional = true } -synth-backend-riscv = { path = "../synth-backend-riscv", version = "0.11.47", optional = true } +synth-backend-awsm = { path = "../synth-backend-awsm", version = "0.11.48", optional = true } +synth-backend-wasker = { path = "../synth-backend-wasker", version = "0.11.48", optional = true } +synth-backend-riscv = { path = "../synth-backend-riscv", version = "0.11.48", optional = true } # Optional verification (requires z3) -synth-verify = { path = "../synth-verify", version = "0.11.47", optional = true, features = ["z3-solver", "arm"] } +synth-verify = { path = "../synth-verify", version = "0.11.48", optional = true, features = ["z3-solver", "arm"] } # Optional PulseEngine WASM optimizer # Uncomment when loom crate is available: diff --git a/crates/synth-frontend/Cargo.toml b/crates/synth-frontend/Cargo.toml index 3b3af28c..0a62a092 100644 --- a/crates/synth-frontend/Cargo.toml +++ b/crates/synth-frontend/Cargo.toml @@ -14,7 +14,7 @@ description = "WASM/WAT parser and module decoder frontend for the Synth compile # Internal path deps carry an explicit version so `cargo publish` # can rewrite to the crates.io coordinate. `path` is used for # in-workspace builds; `version` is what crates.io sees. -synth-core = { path = "../synth-core", version = "0.11.47" } +synth-core = { path = "../synth-core", version = "0.11.48" } wasmparser.workspace = true wasm-encoder.workspace = true diff --git a/crates/synth-opt/Cargo.toml b/crates/synth-opt/Cargo.toml index 700ac69d..e491c2c6 100644 --- a/crates/synth-opt/Cargo.toml +++ b/crates/synth-opt/Cargo.toml @@ -11,7 +11,7 @@ categories.workspace = true description = "Peephole optimization passes for the Synth compiler" [dependencies] -synth-cfg = { path = "../synth-cfg", version = "0.11.47" } +synth-cfg = { path = "../synth-cfg", version = "0.11.48" } [dev-dependencies] criterion = { version = "0.8", features = ["html_reports"] } diff --git a/crates/synth-synthesis/Cargo.toml b/crates/synth-synthesis/Cargo.toml index 48917a68..9b41d431 100644 --- a/crates/synth-synthesis/Cargo.toml +++ b/crates/synth-synthesis/Cargo.toml @@ -11,9 +11,9 @@ categories.workspace = true description = "WASM-to-ARM instruction selection and peephole optimizer" [dependencies] -synth-core = { path = "../synth-core", version = "0.11.47" } -synth-cfg = { path = "../synth-cfg", version = "0.11.47" } -synth-opt = { path = "../synth-opt", version = "0.11.47" } +synth-core = { path = "../synth-core", version = "0.11.48" } +synth-cfg = { path = "../synth-cfg", version = "0.11.48" } +synth-opt = { path = "../synth-opt", version = "0.11.48" } serde.workspace = true anyhow.workspace = true thiserror.workspace = true diff --git a/crates/synth-verify/Cargo.toml b/crates/synth-verify/Cargo.toml index 9a92afc5..d14f719d 100644 --- a/crates/synth-verify/Cargo.toml +++ b/crates/synth-verify/Cargo.toml @@ -17,12 +17,12 @@ arm = ["synth-synthesis"] [dependencies] # Core dependencies (always required) -synth-core = { path = "../synth-core", version = "0.11.47" } -synth-cfg = { path = "../synth-cfg", version = "0.11.47" } -synth-opt = { path = "../synth-opt", version = "0.11.47" } +synth-core = { path = "../synth-core", version = "0.11.48" } +synth-cfg = { path = "../synth-cfg", version = "0.11.48" } +synth-opt = { path = "../synth-opt", version = "0.11.48" } # ARM synthesis (optional, behind 'arm' feature) -synth-synthesis = { path = "../synth-synthesis", version = "0.11.47", optional = true } +synth-synthesis = { path = "../synth-synthesis", version = "0.11.48", optional = true } # SMT solver for formal verification z3 = { version = "0.19", features = ["static-link-z3"], optional = true }