Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
37 changes: 37 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
34 changes: 17 additions & 17 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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"]
Expand Down
2 changes: 1 addition & 1 deletion MODULE.bazel
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
37 changes: 37 additions & 0 deletions artifacts/gale-integration.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -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).
2 changes: 1 addition & 1 deletion crates/synth-backend-awsm/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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
4 changes: 2 additions & 2 deletions crates/synth-backend-riscv/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion crates/synth-backend-wasker/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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
4 changes: 2 additions & 2 deletions crates/synth-backend/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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
16 changes: 8 additions & 8 deletions crates/synth-cli/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down
35 changes: 35 additions & 0 deletions crates/synth-cli/src/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
2 changes: 1 addition & 1 deletion crates/synth-frontend/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion crates/synth-opt/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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"] }
Expand Down
6 changes: 3 additions & 3 deletions crates/synth-synthesis/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading
Loading