diff --git a/CHANGELOG.md b/CHANGELOG.md index 0a23757e..337c50c3 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,6 +7,26 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ## [Unreleased] +## [0.45.2] - 2026-07-16 + +**Soundness patch — #776 closed (aarch64 rotl clobber).** + +### Fixed (soundness) + +- **aarch64 `i32.rotl`/`i64.rotl` clobbered a computed rotate operand (#776).** + Rotate-left lowers to `neg + rorv` (A64 has no native rotate-left). The pre-fix + code reused `dst = alloc_temp()` as the `neg` scratch (`neg(dst,k); + rorv(dst,n,dst)`); when the rotated operand `n` is a **computed** value, + `alloc_temp` can return n's freed register, so `neg(dst,k)` destroyed `n` before + `rorv` read it — a silent wrong result. Param-only rotates escaped it (n sits in + a distinct argument register), which is why it slipped through #769's + param-operand differential. Fix: compute `-k` in `k`'s own now-dead register + (`neg(k,k); rorv(dst,n,k)`) — reads-before-write safe for any `dst` aliasing. + Red-first `i32_rotl_computed`/`i64_rotl_computed` cases added to the aarch64 m2 + differential (n = an add temp): RED on the pre-fix binary (7 cases, e.g. + `A64=-49` vs `wasmtime=1183502082`), GREEN after (182/182). Introduced by #769 + (aarch64 milestone 2, v0.45.0). + ## [0.45.1] - 2026-07-16 **Soundness patch — #757 closed (root-caused + fixed on gale's exact module).** diff --git a/Cargo.lock b/Cargo.lock index a8bc1a73..a1bdb2ce 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1100,14 +1100,14 @@ dependencies = [ [[package]] name = "synth-abi" -version = "0.45.1" +version = "0.45.2" dependencies = [ "synth-wit", ] [[package]] name = "synth-analysis" -version = "0.45.1" +version = "0.45.2" dependencies = [ "anyhow", "synth-core", @@ -1116,7 +1116,7 @@ dependencies = [ [[package]] name = "synth-backend" -version = "0.45.1" +version = "0.45.2" dependencies = [ "anyhow", "synth-core", @@ -1127,7 +1127,7 @@ dependencies = [ [[package]] name = "synth-backend-aarch64" -version = "0.45.1" +version = "0.45.2" dependencies = [ "synth-core", "thiserror", @@ -1136,7 +1136,7 @@ dependencies = [ [[package]] name = "synth-backend-awsm" -version = "0.45.1" +version = "0.45.2" dependencies = [ "anyhow", "synth-core", @@ -1145,7 +1145,7 @@ dependencies = [ [[package]] name = "synth-backend-riscv" -version = "0.45.1" +version = "0.45.2" dependencies = [ "anyhow", "proptest", @@ -1157,7 +1157,7 @@ dependencies = [ [[package]] name = "synth-backend-wasker" -version = "0.45.1" +version = "0.45.2" dependencies = [ "anyhow", "synth-core", @@ -1166,11 +1166,11 @@ dependencies = [ [[package]] name = "synth-cfg" -version = "0.45.1" +version = "0.45.2" [[package]] name = "synth-cli" -version = "0.45.1" +version = "0.45.2" dependencies = [ "anyhow", "clap", @@ -1197,7 +1197,7 @@ dependencies = [ [[package]] name = "synth-core" -version = "0.45.1" +version = "0.45.2" dependencies = [ "anyhow", "gimli", @@ -1211,7 +1211,7 @@ dependencies = [ [[package]] name = "synth-frontend" -version = "0.45.1" +version = "0.45.2" dependencies = [ "anyhow", "synth-core", @@ -1225,14 +1225,14 @@ dependencies = [ [[package]] name = "synth-memory" -version = "0.45.1" +version = "0.45.2" dependencies = [ "bitflags", ] [[package]] name = "synth-opt" -version = "0.45.1" +version = "0.45.2" dependencies = [ "criterion", "synth-cfg", @@ -1240,11 +1240,11 @@ dependencies = [ [[package]] name = "synth-qemu" -version = "0.45.1" +version = "0.45.2" [[package]] name = "synth-synthesis" -version = "0.45.1" +version = "0.45.2" dependencies = [ "anyhow", "proptest", @@ -1259,7 +1259,7 @@ dependencies = [ [[package]] name = "synth-test" -version = "0.45.1" +version = "0.45.2" dependencies = [ "anyhow", "clap", @@ -1275,7 +1275,7 @@ dependencies = [ [[package]] name = "synth-verify" -version = "0.45.1" +version = "0.45.2" dependencies = [ "anyhow", "chrono", @@ -1294,7 +1294,7 @@ dependencies = [ [[package]] name = "synth-wit" -version = "0.45.1" +version = "0.45.2" [[package]] name = "tempfile" diff --git a/Cargo.toml b/Cargo.toml index 7e0a9a7e..2396b036 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -28,7 +28,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.45.1" +version = "0.45.2" edition = "2024" rust-version = "1.88" authors = ["PulseEngine Team"] diff --git a/MODULE.bazel b/MODULE.bazel index bbac26c8..53e5206d 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.45.1", + version = "0.45.2", ) # Bazel dependencies diff --git a/crates/synth-backend-aarch64/Cargo.toml b/crates/synth-backend-aarch64/Cargo.toml index f223c64c..fe73babc 100644 --- a/crates/synth-backend-aarch64/Cargo.toml +++ b/crates/synth-backend-aarch64/Cargo.toml @@ -11,6 +11,6 @@ categories.workspace = true description = "AArch64 (A64) host-native backend for synth — integer subset (milestone 1, #538)" [dependencies] -synth-core = { path = "../synth-core", version = "0.45.1" } +synth-core = { path = "../synth-core", version = "0.45.2" } thiserror.workspace = true tracing.workspace = true diff --git a/crates/synth-backend-awsm/Cargo.toml b/crates/synth-backend-awsm/Cargo.toml index 3e946046..1cc6c964 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.45.1" } +synth-core = { path = "../synth-core", version = "0.45.2" } anyhow.workspace = true thiserror.workspace = true diff --git a/crates/synth-backend-riscv/Cargo.toml b/crates/synth-backend-riscv/Cargo.toml index c9b03ac9..6313cdbf 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.45.1" } -synth-synthesis = { path = "../synth-synthesis", version = "0.45.1" } +synth-core = { path = "../synth-core", version = "0.45.2" } +synth-synthesis = { path = "../synth-synthesis", version = "0.45.2" } 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 443ec344..fc38c71e 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.45.1" } +synth-core = { path = "../synth-core", version = "0.45.2" } anyhow.workspace = true thiserror.workspace = true diff --git a/crates/synth-backend/Cargo.toml b/crates/synth-backend/Cargo.toml index 3050e8a8..e8fecf93 100644 --- a/crates/synth-backend/Cargo.toml +++ b/crates/synth-backend/Cargo.toml @@ -15,8 +15,8 @@ default = ["arm-cortex-m"] arm-cortex-m = ["synth-synthesis"] [dependencies] -synth-core = { path = "../synth-core", version = "0.45.1" } -synth-synthesis = { path = "../synth-synthesis", version = "0.45.1", optional = true } +synth-core = { path = "../synth-core", version = "0.45.2" } +synth-synthesis = { path = "../synth-synthesis", version = "0.45.2", optional = true } anyhow.workspace = true thiserror.workspace = true @@ -24,4 +24,4 @@ thiserror.workspace = true # #667 move 2: the i64 pseudo-op expansion certification oracle # (tests/i64_expansion_certification.rs) feeds THIS crate's emitted encoder # bytes to the synth-verify expansion validator. Dev-only — no prod-dep edge. -synth-verify = { path = "../synth-verify", version = "0.45.1", features = ["arm"] } +synth-verify = { path = "../synth-verify", version = "0.45.2", features = ["arm"] } diff --git a/crates/synth-cli/Cargo.toml b/crates/synth-cli/Cargo.toml index 99b130fb..e4e808f8 100644 --- a/crates/synth-cli/Cargo.toml +++ b/crates/synth-cli/Cargo.toml @@ -52,23 +52,23 @@ 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.45.1" } -synth-frontend = { path = "../synth-frontend", version = "0.45.1" } -synth-synthesis = { path = "../synth-synthesis", version = "0.45.1" } -synth-backend = { path = "../synth-backend", version = "0.45.1" } +synth-core = { path = "../synth-core", version = "0.45.2" } +synth-frontend = { path = "../synth-frontend", version = "0.45.2" } +synth-synthesis = { path = "../synth-synthesis", version = "0.45.2" } +synth-backend = { path = "../synth-backend", version = "0.45.2" } # AArch64 host-native backend (#538) — small pure-Rust crate, always on. -synth-backend-aarch64 = { path = "../synth-backend-aarch64", version = "0.45.1" } +synth-backend-aarch64 = { path = "../synth-backend-aarch64", version = "0.45.2" } # Optional external backends -synth-backend-awsm = { path = "../synth-backend-awsm", version = "0.45.1", optional = true } -synth-backend-wasker = { path = "../synth-backend-wasker", version = "0.45.1", optional = true } -synth-backend-riscv = { path = "../synth-backend-riscv", version = "0.45.1", optional = true } +synth-backend-awsm = { path = "../synth-backend-awsm", version = "0.45.2", optional = true } +synth-backend-wasker = { path = "../synth-backend-wasker", version = "0.45.2", optional = true } +synth-backend-riscv = { path = "../synth-backend-riscv", version = "0.45.2", optional = true } # Optional translation validation — pure-Rust ordeal engine by default (#553), # no C++ toolchain needed. For the Z3 differential oracle build with # `--features verify,synth-verify/z3-solver` (+ SYNTH_SOLVER_DIFF=1 at runtime). -synth-verify = { path = "../synth-verify", version = "0.45.1", optional = true, features = ["arm"] } +synth-verify = { path = "../synth-verify", version = "0.45.2", optional = true, features = ["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 a693da56..1bee71a4 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.45.1" } +synth-core = { path = "../synth-core", version = "0.45.2" } wasmparser.workspace = true wasm-encoder.workspace = true diff --git a/crates/synth-opt/Cargo.toml b/crates/synth-opt/Cargo.toml index 807c3471..db9b2dee 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.45.1" } +synth-cfg = { path = "../synth-cfg", version = "0.45.2" } [dev-dependencies] criterion = { version = "0.8", features = ["html_reports"] } diff --git a/crates/synth-synthesis/Cargo.toml b/crates/synth-synthesis/Cargo.toml index a020f0a9..7657e79f 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.45.1" } -synth-cfg = { path = "../synth-cfg", version = "0.45.1" } -synth-opt = { path = "../synth-opt", version = "0.45.1" } +synth-core = { path = "../synth-core", version = "0.45.2" } +synth-cfg = { path = "../synth-cfg", version = "0.45.2" } +synth-opt = { path = "../synth-opt", version = "0.45.2" } serde.workspace = true anyhow.workspace = true thiserror.workspace = true diff --git a/crates/synth-verify/Cargo.toml b/crates/synth-verify/Cargo.toml index b53e9ecd..355e0118 100644 --- a/crates/synth-verify/Cargo.toml +++ b/crates/synth-verify/Cargo.toml @@ -22,12 +22,12 @@ arm = ["synth-synthesis"] [dependencies] # Core dependencies (always required) -synth-core = { path = "../synth-core", version = "0.45.1" } -synth-cfg = { path = "../synth-cfg", version = "0.45.1" } -synth-opt = { path = "../synth-opt", version = "0.45.1" } +synth-core = { path = "../synth-core", version = "0.45.2" } +synth-cfg = { path = "../synth-cfg", version = "0.45.2" } +synth-opt = { path = "../synth-opt", version = "0.45.2" } # ARM synthesis (optional, behind 'arm' feature) -synth-synthesis = { path = "../synth-synthesis", version = "0.45.1", optional = true } +synth-synthesis = { path = "../synth-synthesis", version = "0.45.2", optional = true } # Default SMT engine: pure-Rust, certificate-checked QF_BV solver (#553). # 0.9 adds the `ordeal::trap` module (trap-preservation VCs, VCR-VER-002 / #166); diff --git a/npm/package.json b/npm/package.json index d7c41840..dc5144db 100644 --- a/npm/package.json +++ b/npm/package.json @@ -1,6 +1,6 @@ { "name": "@pulseengine/synth", - "version": "0.45.1", + "version": "0.45.2", "description": "synth — a WebAssembly-to-ARM/RISC-V/AArch64 compiler with mechanized correctness proofs. Produces bare-metal ELF binaries for embedded targets.", "bin": { "synth": "./run.js"