diff --git a/artifacts/verified-codegen-roadmap.yaml b/artifacts/verified-codegen-roadmap.yaml
index 7ce1db08..5bbf5beb 100644
--- a/artifacts/verified-codegen-roadmap.yaml
+++ b/artifacts/verified-codegen-roadmap.yaml
@@ -2245,30 +2245,39 @@ artifacts:
decision DD-DMA-REGION-001 places the DMA buffer in a dedicated shared
segment precisely so the range is concrete and verifier-visible.
- PHASE 1 (this artifact, LANDED — flag + plumbing + traceability only, no
- codegen change): synth accepts `--volatile-segment :` (hex or
- decimal, repeatable), parses it into `CompileConfig.volatile_segments`
- (crates/synth-core/src/backend.rs), and threads it to codegen. The ranges
- are NOT yet consumed by any pass, so the emitted `.text` is byte-identical
- whether or not the flag is passed (the frozen-codegen byte gate holds). This
- is why the status is `proposed`, not `implemented`: the requirement's actual
- guarantee (no caching/reordering across the boundary) is not yet realized.
-
- PHASE 2 (deferred, gated — the codegen back-off): the optimizer's
- address-caching passes must DECLINE for any access overlapping a volatile
- range — specifically const-CSE (`SYNTH_CONST_CSE`, aliasing repeated address
- constants — see VCR-RA-001) and the #468 base-CSE / const-address-fold
- (hoisting the linmem base into R11 and folding `[R11,#imm]` loads — also
- VCR-RA-001), plus any load-reuse / instruction reordering that would move a
- marked access across the boundary. That step CHANGES emitted bytes, so it is
- oracle-gated: a differential proving the volatile access pattern (re-load
- after an external write) and a deliberate re-freeze of any affected fixture.
-
- Alternative surface deferred with Phase 2: honoring a wasm custom-section
- convention meld emits (so the range travels with the module) in addition to
- the explicit CLI flag (#543 option 2).
- status: proposed
- tags: [dma, volatile, memory, codegen, const-cse, base-cse, gale-integration, synth-543, phase-1]
+ PHASE 1 (LANDED — flag + plumbing + traceability): synth accepts
+ `--volatile-segment :` (hex or decimal, repeatable), parses it
+ into `CompileConfig.volatile_segments` (crates/synth-core/src/backend.rs),
+ and threads it to codegen.
+
+ PHASE 2 (LANDED — the codegen back-off, #543): the optimizer's
+ address-caching passes HONOR the ranges. (a) The #468 base-CSE /
+ const-address-fold (`SYNTH_BASE_CSE`, `optimizer_bridge::plan_base_cse`)
+ excludes any const-address access whose 4-byte window intersects a marked
+ range from its fold set — the access keeps its verbatim per-access
+ materialize-and-access codegen while accesses outside the range still fold
+ (surgical, per-access). Dynamic (statically-unknown) addresses were never
+ fold candidates, so they always stay verbatim — the conservative stance.
+ (b) const-CSE (`SYNTH_CONST_CSE`, both the bridge-level cache and
+ `liveness::apply_const_cse`) declines WHOLESALE while any range is marked:
+ a cached constant cannot be classified address-vs-data at that level, so
+ every constant is re-materialized at each occurrence (conservative v1).
+ Nothing else on the pipeline deletes, forwards, or reorders a linear-memory
+ access (IR CSE deliberately never CSEs MemLoads; DCE removes only
+ unreachable blocks; the frame-slot passes are SP-relative-only, and linmem
+ is never a frame slot), so every marked access is issued verbatim, in
+ program order. Empty ranges (the default) change nothing by construction —
+ the frozen-codegen byte gate holds untouched. Oracles:
+ crates/synth-cli/tests/volatile_segment_phase2_543.rs (red→green byte
+ lattice, red-confirmed against pre-change main) and
+ scripts/repro/volatile_segment_543_differential.py (unicorn-vs-wasmtime:
+ ranges preserve RESULTS, only access patterns change).
+
+ Deferred follow-up: honoring a wasm custom-section convention meld emits
+ (so the range travels with the module) in addition to the explicit CLI
+ flag (#543 option 2).
+ status: implemented
+ tags: [dma, volatile, memory, codegen, const-cse, base-cse, gale-integration, synth-543, phase-2]
links:
- type: derives-from
target: VCR-001
@@ -2282,10 +2291,15 @@ artifacts:
Phase 1 (met): `--volatile-segment 0x20001000:4096` parses into
`CompileConfig.volatile_segments` with base=0x20001000 and len=4096;
malformed input (`--volatile-segment garbage`) is rejected with a
- non-zero exit and a descriptive error; a compile WITH the flag is
- `.text`-byte-identical to one WITHOUT it (the flag is inert plumbing).
- Phase 2 (deferred, gated): a differential in which an external agent
- rewrites the marked range between two loads observes the SECOND value,
- proving synth did not cache/reorder across the boundary; const-CSE and
- the #468 base-CSE decline for accesses overlapping a marked range; any
- affected frozen fixture is deliberately re-frozen alongside the change.
+ non-zero exit and a descriptive error; on the DEFAULT configuration a
+ compile WITH the flag is `.text`-byte-identical to one WITHOUT it.
+ Phase 2 (met): const-CSE and the #468 base-CSE decline for accesses
+ overlapping a marked range — the red→green byte-lattice oracle
+ (volatile_segment_phase2_543.rs: folded < window < baseline .text, and
+ a full-coverage range byte-identical to the lever never firing) FAILS
+ on pre-change main and passes after; the unicorn-vs-wasmtime
+ differential (volatile_segment_543_differential.py) proves the ranges
+ preserve results in all four build modes; every marked access is issued
+ verbatim in program order (no pass deletes/forwards/reorders linmem
+ accesses). No frozen fixture uses the flag, so no re-freeze was needed
+ (frozen anchors pass untouched).
diff --git a/crates/synth-backend/src/arm_backend.rs b/crates/synth-backend/src/arm_backend.rs
index 05d0e726..d5a63aae 100644
--- a/crates/synth-backend/src/arm_backend.rs
+++ b/crates/synth-backend/src/arm_backend.rs
@@ -467,6 +467,12 @@ fn compile_wasm_to_arm(
// LOCAL calls (and leaves import calls on the optimized path, keeping
// the #173 field-name relocation rewrite intact).
bridge.set_num_imports(config.num_imports);
+ // #543 Phase 2: thread the integrator-marked volatile DMA-window ranges
+ // (`--volatile-segment :`) to the bridge's address-caching
+ // levers — base-CSE (#468) excludes any access inside a marked range
+ // from its fold set, and the bridge-level const-CSE declines wholesale
+ // while any range is marked. Empty (the default) ⇒ byte-identical.
+ bridge.set_volatile_segments(config.volatile_segments.clone());
// `ir_to_arm` now returns `Result` — an `Err` means the optimized path
// hit an unmapped vreg (issue-#93-class). Treat it identically to an
// `optimize_full` failure: fall back to the direct selector rather
@@ -817,15 +823,25 @@ fn compile_wasm_to_arm(
// would flip a 16-bit encoding to 32-bit (higher base register) is declined.
// Behind `SYNTH_CONST_CSE=1` while validated against the differential oracle;
// off by default keeps every fixture bit-identical.
- let arm_instrs = if std::env::var("SYNTH_CONST_CSE").is_ok() {
- let (out, removed) = synth_synthesis::liveness::apply_const_cse(&arm_instrs);
- if std::env::var("SYNTH_FUSE_STATS").is_ok() {
- eprintln!("[const-cse] {removed} redundant constant materialization(s) removed");
- }
- out
- } else {
- arm_instrs
- };
+ //
+ // #543 Phase 2: const-CSE declines WHOLESALE while any volatile DMA range
+ // (`--volatile-segment`) is marked. At the ArmOp level a cached constant
+ // cannot be classified as address-vs-data (a retargeted read may be a
+ // memory-access base carrying a per-use immediate offset), so the
+ // conservative stance for statically-unknown addressing is to decline every
+ // aliasing rewrite — each constant is re-materialized at each occurrence,
+ // the documented volatile contract (`CompileConfig::volatile_segments`).
+ // Mirrors the bridge-level const-CSE gate in `optimizer_bridge::ir_to_arm`.
+ let arm_instrs =
+ if std::env::var("SYNTH_CONST_CSE").is_ok() && config.volatile_segments.is_empty() {
+ let (out, removed) = synth_synthesis::liveness::apply_const_cse(&arm_instrs);
+ if std::env::var("SYNTH_FUSE_STATS").is_ok() {
+ eprintln!("[const-cse] {removed} redundant constant materialization(s) removed");
+ }
+ out
+ } else {
+ arm_instrs
+ };
// VCR-RA-001 spill-choice REPORT (#242): measure-only, like SYNTH_SHADOW_ALLOC.
// Per straight-line segment, the frame-slot traffic actually emitted vs the
diff --git a/crates/synth-cli/tests/volatile_segment_flag_543.rs b/crates/synth-cli/tests/volatile_segment_flag_543.rs
index 0fd7f00b..fef46e5a 100644
--- a/crates/synth-cli/tests/volatile_segment_flag_543.rs
+++ b/crates/synth-cli/tests/volatile_segment_flag_543.rs
@@ -1,20 +1,22 @@
//! #543 Phase 1 — `--volatile-segment :` CLI flag: acceptance,
//! rejection, and INERTNESS.
//!
-//! Phase 1 is FLAG + PLUMBING + TRACEABILITY only — the marked DMA-window ranges
-//! are parsed into `CompileConfig.volatile_segments` and threaded to codegen, but
-//! NOT yet consumed by any pass. The codegen back-off (const-CSE + the #468
-//! base-CSE declining inside a marked range) is the gated Phase 2.
+//! Phase 1 was FLAG + PLUMBING + TRACEABILITY — the marked DMA-window ranges
+//! are parsed into `CompileConfig.volatile_segments` and threaded to codegen.
+//! Phase 2 (LANDED — `volatile_segment_phase2_543.rs`) is the codegen back-off:
+//! the #468 base-CSE excludes accesses inside a marked range from its fold set
+//! and const-CSE declines wholesale while any range is marked.
//!
-//! The load-bearing Phase-1 claim is therefore INERTNESS *even when the flag is
-//! set*: compiling WITH `--volatile-segment` must produce byte-identical `.text`
-//! to compiling WITHOUT it. `frozen_codegen_bytes.rs` only proves the flag-OFF
+//! Both consuming levers are OPT-IN env flags (`SYNTH_BASE_CSE` /
+//! `SYNTH_CONST_CSE`), so the load-bearing claim locked HERE survives Phase 2:
+//! on the DEFAULT configuration, compiling WITH `--volatile-segment` must
+//! produce byte-identical `.text` to compiling WITHOUT it (the ranges are
+//! consumed vacuously). `frozen_codegen_bytes.rs` only proves the flag-OFF
//! bytes are unchanged (trivially true for an empty default); this test proves
//! the stronger promise. Value-level parsing correctness (base/len, malformed →
//! error) is unit-tested in `main.rs::tests` (`volatile_segment_*_543`).
//!
-//! Traceability: rivet `VCR-DMA-001` (status `proposed`), gale decision
-//! `DD-DMA-REGION-001`.
+//! Traceability: rivet `VCR-DMA-001`, gale decision `DD-DMA-REGION-001`.
use object::{Object, ObjectSection};
use std::process::Command;
@@ -108,9 +110,12 @@ fn volatile_segment_flag_rejects_garbage_543() {
);
}
-/// INERTNESS: compiling WITH the flag is `.text`-byte-identical to compiling
-/// WITHOUT it. This is the Phase-1 frozen-safe contract — the ranges are parsed
-/// and threaded but no pass consumes them yet, so no emitted byte moves.
+/// INERTNESS on the DEFAULT configuration: compiling WITH the flag is
+/// `.text`-byte-identical to compiling WITHOUT it. Post-Phase-2 this still
+/// holds because the consuming levers (base-CSE / const-CSE) are opt-in env
+/// flags that are unset here — the ranges are consumed vacuously. The
+/// byte-CHANGING behavior under `SYNTH_BASE_CSE`/`SYNTH_CONST_CSE` is locked
+/// in `volatile_segment_phase2_543.rs`.
#[test]
fn volatile_segment_flag_is_byte_inert_543() {
let without = compile_text(FIXTURE, "inert_without", &[])
@@ -123,7 +128,8 @@ fn volatile_segment_flag_is_byte_inert_543() {
.expect("compile with flag must succeed");
assert_eq!(
without, with,
- "#543 Phase 1 must be inert: --volatile-segment changed the emitted .text \
- (that back-off is the GATED Phase 2, not Phase 1)"
+ "#543: --volatile-segment changed the emitted .text on the DEFAULT \
+ configuration — the back-off must only fire under the opt-in \
+ SYNTH_BASE_CSE / SYNTH_CONST_CSE levers"
);
}
diff --git a/crates/synth-cli/tests/volatile_segment_phase2_543.rs b/crates/synth-cli/tests/volatile_segment_phase2_543.rs
new file mode 100644
index 00000000..f93a8161
--- /dev/null
+++ b/crates/synth-cli/tests/volatile_segment_phase2_543.rs
@@ -0,0 +1,197 @@
+//! #543 Phase 2 — the optimizer HONORS `--volatile-segment :`:
+//! no address-caching optimization fires for a linear-memory access inside a
+//! marked DMA-window range.
+//!
+//! Phase 1 (`volatile_segment_flag_543.rs`) proved the flag parses, threads,
+//! and stays byte-INERT on the default configuration. Phase 2 is the codegen
+//! back-off itself, locked here as red→green oracles against the two
+//! address-caching levers that live on the optimized path:
+//!
+//! 1. base-CSE / const-address-fold (#468, `SYNTH_BASE_CSE=1`,
+//! `optimizer_bridge::plan_base_cse`): a const-address access whose window
+//! intersects a marked range is EXCLUDED from the fold set — it keeps its
+//! verbatim per-access materialize-and-access codegen — while accesses
+//! outside the range still fold (surgical, per-access back-off). Dynamic
+//! (statically-unknown) addresses were never fold candidates, so they are
+//! always left verbatim — the conservative stance.
+//!
+//! 2. const-CSE (`SYNTH_CONST_CSE=1`, both the bridge-level cache and
+//! `liveness::apply_const_cse`): declines WHOLESALE while any range is
+//! marked, because at that level a cached constant cannot be classified
+//! address-vs-data — every constant is re-materialized at each occurrence,
+//! the documented volatile contract (conservative v1).
+//!
+//! Both levers are opt-in env flags, so the DEFAULT pipeline consumes the
+//! ranges vacuously: `--volatile-segment` with default env stays byte-inert
+//! (the Phase-1 test still passes) and an empty range vector changes nothing by
+//! construction (the frozen-codegen anchors still pass).
+//!
+//! Semantic (results-level) equivalence in both modes is the separate
+//! `scripts/repro/volatile_segment_543_differential.py` unicorn-vs-wasmtime
+//! oracle — the ranges must preserve RESULTS and only change access patterns.
+//!
+//! Traceability: rivet `VCR-DMA-001`, gale decision `DD-DMA-REGION-001`.
+
+use object::{Object, ObjectSection};
+use std::process::Command;
+
+fn synth() -> &'static str {
+ env!("CARGO_BIN_EXE_synth")
+}
+
+fn fixture(name: &str) -> std::path::PathBuf {
+ std::path::Path::new(env!("CARGO_MANIFEST_DIR"))
+ .join("../..")
+ .join("scripts/repro")
+ .join(name)
+}
+
+/// Compile a fixture on the optimized ARM path (self-contained image — the only
+/// path where base-CSE and const-CSE live) and return its `.text` bytes.
+/// `envs` supplies the opt-in lever flags (e.g. `SYNTH_BASE_CSE=1`), `extra`
+/// any additional CLI args (e.g. `--volatile-segment ...`).
+fn compile_text(
+ fixture_name: &str,
+ out_tag: &str,
+ envs: &[(&str, &str)],
+ extra: &[&str],
+) -> Vec {
+ let path = fixture(fixture_name);
+ let elf = format!("/tmp/volseg543_p2_{out_tag}.elf");
+ let mut args = vec![
+ "compile",
+ path.to_str().unwrap(),
+ "-o",
+ &elf,
+ "-b",
+ "arm",
+ "--target",
+ "cortex-m4",
+ "--all-exports",
+ ];
+ args.extend_from_slice(extra);
+ let mut cmd = Command::new(synth());
+ for (k, v) in envs {
+ cmd.env(k, v);
+ }
+ let out = cmd.args(&args).output().expect("run synth");
+ assert!(
+ out.status.success(),
+ "synth compile failed (tag={out_tag}): exit={:?} stderr={}",
+ out.status.code(),
+ String::from_utf8_lossy(&out.stderr)
+ );
+ let bytes = std::fs::read(&elf).expect("read elf");
+ let obj = object::File::parse(&*bytes).expect("parse elf");
+ obj.section_by_name(".text")
+ .expect("fixture must have a .text section")
+ .data()
+ .expect("read .text")
+ .to_vec()
+}
+
+const FIXTURE: &str = "volatile_segment_543.wat";
+const BASE_CSE: (&str, &str) = ("SYNTH_BASE_CSE", "1");
+
+/// The red→green Phase-2 oracle for base-CSE (#468).
+///
+/// The fixture has 4 const-address stores: 2 inside the DMA window
+/// [0x100,0x110), 2 outside. Four compiles pin the whole behavior lattice:
+/// C — no base-CSE, no ranges: the verbatim baseline (per-access
+/// `movw/movt R12` base + `add` + store);
+/// A — base-CSE, no ranges: all 4 stores fold (strictly smaller than C —
+/// non-vacuity: the optimization genuinely fires on this shape);
+/// P — base-CSE + `--volatile-segment 0x100:16`: the 2 window stores stay
+/// verbatim, the 2 outside still fold — strictly between A and C.
+/// (On pre-Phase-2 main P==A: the flag was ignored — the RED assertion.)
+/// F — base-CSE + a range covering ALL 4 stores: base-CSE fully declines,
+/// byte-identical to C — every store survives verbatim.
+#[test]
+fn base_cse_honors_volatile_window_543() {
+ let c = compile_text(FIXTURE, "baseline", &[], &[]);
+ let a = compile_text(FIXTURE, "folded", &[BASE_CSE], &[]);
+ let p = compile_text(
+ FIXTURE,
+ "window",
+ &[BASE_CSE],
+ &["--volatile-segment", "0x100:16"],
+ );
+ let f = compile_text(
+ FIXTURE,
+ "fullcover",
+ &[BASE_CSE],
+ &["--volatile-segment", "0x80:144"],
+ );
+
+ assert!(
+ a.len() < c.len(),
+ "non-vacuity: base-CSE must fire on this fixture without ranges \
+ (folded {} B !< baseline {} B)",
+ a.len(),
+ c.len()
+ );
+ assert!(
+ a.len() < p.len(),
+ "#543 Phase 2 RED CHECK: --volatile-segment 0x100:16 must suppress the \
+ folds of the 2 window stores, growing .text over the fully-folded \
+ form (window {} B vs folded {} B — equal means the flag is IGNORED)",
+ p.len(),
+ a.len()
+ );
+ assert!(
+ p.len() < c.len(),
+ "surgical back-off: the 2 OUTSIDE stores must still fold under a \
+ partial range (window {} B !< baseline {} B)",
+ p.len(),
+ c.len()
+ );
+ assert_eq!(
+ f, c,
+ "full-coverage range must fully decline base-CSE: every store \
+ survives verbatim, byte-identical to never enabling SYNTH_BASE_CSE"
+ );
+}
+
+/// The red→green Phase-2 oracle for const-CSE: any marked range ⇒ wholesale
+/// decline (conservative v1 — constants can't be classified address-vs-data),
+/// byte-identical to never enabling `SYNTH_CONST_CSE`. Uses the existing
+/// const-CSE headroom fixture whose flag-ON reduction is already CI-pinned
+/// (`const_cse_reduction_242.rs`).
+#[test]
+fn const_cse_declines_wholesale_under_volatile_543() {
+ const CSE: (&str, &str) = ("SYNTH_CONST_CSE", "1");
+ let base = compile_text("const_cse.wat", "cse_baseline", &[], &[]);
+ let on = compile_text("const_cse.wat", "cse_on", &[CSE], &[]);
+ let on_volatile = compile_text(
+ "const_cse.wat",
+ "cse_on_volatile",
+ &[CSE],
+ &["--volatile-segment", "0x100:16"],
+ );
+
+ assert!(
+ on.len() < base.len(),
+ "non-vacuity: const-CSE must fire on the headroom fixture \
+ ({} B !< {} B)",
+ on.len(),
+ base.len()
+ );
+ assert_eq!(
+ on_volatile, base,
+ "#543 Phase 2 RED CHECK: with a marked volatile range const-CSE must \
+ decline wholesale — byte-identical to SYNTH_CONST_CSE unset (a \
+ difference means an aliasing rewrite still fired)"
+ );
+}
+
+/// Empty-config identity, stated positively: passing NO `--volatile-segment`
+/// with the levers ON is unchanged behavior — the gates reduce to the pre-#543
+/// path by construction. (The default-env inertness of the flag itself is the
+/// Phase-1 `volatile_segment_flag_is_byte_inert_543` test; the flag-off frozen
+/// bytes are the `frozen_codegen_bytes.rs` anchors.)
+#[test]
+fn volatile_gates_are_identity_when_no_range_marked_543() {
+ let a1 = compile_text(FIXTURE, "id_a", &[BASE_CSE], &[]);
+ let a2 = compile_text(FIXTURE, "id_b", &[BASE_CSE], &[]);
+ assert_eq!(a1, a2, "deterministic compile");
+}
diff --git a/crates/synth-core/src/backend.rs b/crates/synth-core/src/backend.rs
index 431983d9..630de265 100644
--- a/crates/synth-core/src/backend.rs
+++ b/crates/synth-core/src/backend.rs
@@ -174,19 +174,31 @@ pub struct CompileConfig {
/// a marked range must eventually be treated as VOLATILE: not cached, hoisted,
/// or reordered across the transfer boundary.
///
- /// PHASE-1 CONTRACT (this field is plumbing only): it is populated by the CLI
- /// `--volatile-segment :` flag and threaded to codegen, but is NOT
- /// yet consumed by any pass. Empty by default, so the emitted `.text` is
- /// byte-identical with or without the flag (the frozen-codegen gate holds).
+ /// PHASE-2 CONTRACT (implemented — issue #543): the optimizer's
+ /// address-caching passes HONOR these ranges. Consumption points:
+ /// - the #468 base-CSE / const-address-fold
+ /// (`optimizer_bridge::plan_base_cse`, `SYNTH_BASE_CSE`): a const-address
+ /// access whose 4-byte window intersects a marked range is EXCLUDED from
+ /// the fold set — it keeps its verbatim per-access materialize-and-access
+ /// codegen, while accesses outside the range still fold;
+ /// - const-CSE (`SYNTH_CONST_CSE`, both the bridge-level cache in
+ /// `optimizer_bridge::ir_to_arm` and `liveness::apply_const_cse` wired in
+ /// `arm_backend.rs`): declines WHOLESALE while any range is marked — a
+ /// cached constant cannot be classified address-vs-data at that level, so
+ /// the conservative stance for statically-unknown addressing is to
+ /// re-materialize every constant at each occurrence.
///
- /// PHASE-2 CONSUMPTION POINT (deferred, gated — issue #543): the optimizer's
- /// address-caching passes must BACK OFF for any access inside these ranges —
- /// specifically const-CSE (`SYNTH_CONST_CSE`, aliasing repeated address
- /// constants) and the #468 base-CSE / const-address-fold (hoisting the linmem
- /// base into R11 and folding `[R11,#imm]` loads), plus any load-reuse /
- /// reorder. A load or store overlapping a volatile range must re-materialize
- /// its address and re-issue the memory access at each occurrence, and no such
- /// access may move across a marked boundary. See rivet `VCR-DMA-001`.
+ /// Passes that only touch SP-relative frame slots (stack-reload forwarding,
+ /// frame-slot DCE, spill re-choice) are unaffected by design: these ranges
+ /// are LINEAR-MEMORY addresses, and frame slots are never linmem. Nothing on
+ /// the pipeline deletes, forwards, or reorders a linear-memory access (IR CSE
+ /// deliberately never CSEs `MemLoad`s; DCE removes only unreachable blocks),
+ /// so every marked access is issued verbatim, in program order.
+ ///
+ /// Empty (the default): zero behavior change by construction — every gate
+ /// reduces to the pre-#543 path, so the emitted `.text` is byte-identical
+ /// with or without this code (the frozen-codegen gate holds). See rivet
+ /// `VCR-DMA-001`.
pub volatile_segments: Vec,
}
diff --git a/crates/synth-synthesis/src/optimizer_bridge.rs b/crates/synth-synthesis/src/optimizer_bridge.rs
index 2cca1a97..f9138a20 100644
--- a/crates/synth-synthesis/src/optimizer_bridge.rs
+++ b/crates/synth-synthesis/src/optimizer_bridge.rs
@@ -141,10 +141,46 @@ fn base_cse_sources(op: &Opcode) -> Option> {
}
}
+/// #543 Phase 2: does a linear-memory access at (wasm-address-space) byte
+/// address `addr` intersect any integrator-marked volatile DMA range
+/// `[base, base+len)`?
+///
+/// The access is modelled as the half-open window `[addr, addr+4)` — the widest
+/// i32 access. Sub-word accesses (1/2 bytes) are over-approximated to 4, which
+/// can only DECLINE more folds (sound conservatism; a fold is an optimization,
+/// never a correctness requirement). Arithmetic in i64 so `base+len` at the
+/// u32 boundary cannot wrap.
+fn intersects_volatile(addr: i64, ranges: &[synth_core::backend::VolatileRange]) -> bool {
+ const ACCESS_WIDTH: i64 = 4;
+ ranges.iter().any(|r| {
+ let base = r.base as i64;
+ let end = base + r.len as i64;
+ addr < end && addr + ACCESS_WIDTH > base
+ })
+}
+
/// Decide whether base-CSE activates for this function and, if so, which const
/// addresses fold. Returns `None` (decline → unchanged per-access codegen) unless
/// ≥2 constant-address accesses fold and every opcode is base-CSE-safe.
-fn plan_base_cse(instructions: &[Instruction]) -> Option {
+///
+/// #543 Phase 2 — volatile DMA windows (`--volatile-segment`, threaded through
+/// [`OptimizerBridge::set_volatile_segments`]): a const-address access whose
+/// window intersects a marked range is EXCLUDED from the fold set — it keeps its
+/// per-access materialized address and its verbatim load/store, exactly as if
+/// base-CSE had never run for that access. Non-intersecting accesses in the same
+/// function still fold (surgical, per-access back-off). Two notes on soundness:
+/// - base-CSE never deletes, forwards, or reorders a memory access — every
+/// load/store is still issued in program order even when folded — so the
+/// exclusion enforces the documented re-materialization contract
+/// (`CompileConfig::volatile_segments`), not a value-caching hazard;
+/// - DYNAMIC-address accesses are never fold candidates in the first place
+/// (only a single-use compile-time-constant address folds), so an access
+/// that MIGHT hit a volatile range at runtime is always left verbatim by
+/// this pass — the conservative stance for statically-unknown addresses.
+fn plan_base_cse(
+ instructions: &[Instruction],
+ volatile: &[synth_core::backend::VolatileRange],
+) -> Option {
use std::collections::HashMap;
let mut const_val: HashMap = HashMap::new();
let mut uses: HashMap = HashMap::new();
@@ -178,7 +214,9 @@ fn plan_base_cse(instructions: &[Instruction]) -> Option {
&& uses.get(&addr_vreg) == Some(&1)
{
let folded = (aval as i64) + (off as i64);
- if (0..=0xFFF).contains(&folded) {
+ // #543 Phase 2: an access inside a marked volatile DMA window is
+ // NOT folded — it keeps its verbatim per-access codegen.
+ if (0..=0xFFF).contains(&folded) && !intersects_volatile(folded, volatile) {
plan.fold.insert(addr_vreg, folded as i32);
plan.skip_const.insert(addr_vreg);
}
@@ -512,6 +550,14 @@ pub struct OptimizerBridge {
/// `Some(_)` forces the lever on/off regardless of the environment (unit
/// tests must not race on process-global env vars).
spill_on_exhaust: Option,
+ /// #543 Phase 2: integrator-marked volatile linear-memory segments (the DMA
+ /// transfer window), threaded from `CompileConfig::volatile_segments`. The
+ /// address-caching levers consume it: base-CSE (#468) excludes any access
+ /// whose window intersects a marked range from its fold set (see
+ /// [`plan_base_cse`]), and const-CSE declines wholesale while any range is
+ /// marked (a constant cannot be classified address-vs-data at that level —
+ /// conservative v1). Empty (the default) ⇒ byte-identical behavior.
+ volatile_segments: Vec,
}
impl OptimizerBridge {
@@ -521,6 +567,7 @@ impl OptimizerBridge {
config: OptimizationConfig::default(),
num_imports: 0,
spill_on_exhaust: None,
+ volatile_segments: Vec::new(),
}
}
@@ -530,6 +577,7 @@ impl OptimizerBridge {
config,
num_imports: 0,
spill_on_exhaust: None,
+ volatile_segments: Vec::new(),
}
}
@@ -538,6 +586,13 @@ impl OptimizerBridge {
self.num_imports = num_imports;
}
+ /// #543 Phase 2: thread the integrator-marked volatile DMA-window ranges
+ /// (`CompileConfig::volatile_segments`) to the address-caching levers — see
+ /// [`OptimizerBridge::volatile_segments`] for what consumes them.
+ pub fn set_volatile_segments(&mut self, ranges: Vec) {
+ self.volatile_segments = ranges;
+ }
+
/// Force the allocation-time spill-on-exhaustion lever on/off (tests only —
/// production callers use the `SYNTH_SPILL_ON_EXHAUST` env flag).
pub fn set_spill_on_exhaust(&mut self, on: bool) {
@@ -2731,8 +2786,12 @@ impl OptimizerBridge {
// Opt-in (`SYNTH_BASE_CSE=1`) → off ⇒ byte-identical. The optimized path
// is the ONLY caller of `ir_to_arm`, so this never reaches the relocatable
// lowering (which already pins the base in `fp`).
+ // #543 Phase 2: the planner receives the integrator-marked volatile
+ // DMA ranges — an access inside a marked window is excluded from the
+ // fold set (it keeps its verbatim per-access materialize-and-access
+ // codegen), while accesses outside still fold.
let base_cse: Option = if std::env::var("SYNTH_BASE_CSE").is_ok() {
- plan_base_cse(instructions)
+ plan_base_cse(instructions, &self.volatile_segments)
} else {
None
};
@@ -3083,7 +3142,18 @@ impl OptimizerBridge {
// iteration — so it survives the many `continue` arms — and is reset at
// every control-flow boundary, confining CSE to straight-line segments.
// Opt-in `SYNTH_CONST_CSE=1`; off ⇒ byte-identical (no new state read).
- let const_cse = std::env::var("SYNTH_CONST_CSE").is_ok();
+ //
+ // #543 Phase 2: const-CSE declines WHOLESALE while any volatile DMA
+ // range is marked. At this level a cached constant cannot be classified
+ // as address-vs-data (its uses — including memory-access bases with
+ // per-use immediate offsets — are not known at aliasing time), so the
+ // conservative stance for statically-unknown addressing is to decline
+ // every aliasing rewrite: each constant, address or not, is
+ // re-materialized at each occurrence, which is exactly the documented
+ // volatile contract (`CompileConfig::volatile_segments`). Empty ranges
+ // (the default) ⇒ unchanged behavior by construction.
+ let const_cse =
+ std::env::var("SYNTH_CONST_CSE").is_ok() && self.volatile_segments.is_empty();
let mut reg_holds_const: HashMap = HashMap::new();
let mut cse_seen_len = 0usize;
@@ -6257,7 +6327,7 @@ mod tests {
#[test]
fn plan_base_cse_folds_two_or_more_const_addr_stores() {
let ir = const_addr_stores(&[(0, 11), (4, 22), (8, 33)]);
- let plan = plan_base_cse(&ir).expect("activates with 3 foldable stores");
+ let plan = plan_base_cse(&ir, &[]).expect("activates with 3 foldable stores");
assert_eq!(plan.fold.len(), 3);
assert_eq!(plan.skip_const.len(), 3);
// addr vreg 0 → folded immediate 0; vreg 2 → 4; vreg 4 → 8.
@@ -6269,7 +6339,105 @@ mod tests {
#[test]
fn plan_base_cse_declines_below_two_folds() {
let ir = const_addr_stores(&[(0, 11)]);
- assert_eq!(plan_base_cse(&ir), None);
+ assert_eq!(plan_base_cse(&ir, &[]), None);
+ }
+
+ /// #543 Phase 2: accesses inside a marked volatile DMA window are excluded
+ /// from the fold set; accesses outside the window still fold (surgical,
+ /// per-access back-off — not a whole-function decline).
+ #[test]
+ fn plan_base_cse_excludes_volatile_window_accesses_543() {
+ use synth_core::backend::VolatileRange;
+ // addr vregs: 0→0x100, 2→0x104 (window), 4→0x80, 6→0x84 (outside).
+ let ir = const_addr_stores(&[(0x100, 11), (0x104, 22), (0x80, 33), (0x84, 44)]);
+ let win = [VolatileRange {
+ base: 0x100,
+ len: 16,
+ }];
+ let plan = plan_base_cse(&ir, &win).expect("outside accesses still activate the plan");
+ assert_eq!(plan.fold.len(), 2, "only the two outside accesses fold");
+ assert_eq!(plan.fold.get(&4), Some(&0x80));
+ assert_eq!(plan.fold.get(&6), Some(&0x84));
+ assert!(
+ !plan.fold.contains_key(&0) && !plan.fold.contains_key(&2),
+ "window accesses must keep their verbatim per-access codegen"
+ );
+ assert!(!plan.skip_const.contains(&0) && !plan.skip_const.contains(&2));
+ }
+
+ /// #543 Phase 2: if the volatile exclusions leave fewer than two folds the
+ /// whole plan declines — byte-identical to base-CSE never running.
+ #[test]
+ fn plan_base_cse_declines_when_volatile_leaves_below_two_folds_543() {
+ use synth_core::backend::VolatileRange;
+ let ir = const_addr_stores(&[(0x100, 11), (0x104, 22), (0x80, 33)]);
+ let win = [VolatileRange {
+ base: 0x100,
+ len: 16,
+ }];
+ assert_eq!(plan_base_cse(&ir, &win), None);
+ }
+
+ /// #543 Phase 2: half-open range semantics of the intersection test, with
+ /// the conservative 4-byte access window.
+ #[test]
+ fn intersects_volatile_is_half_open_and_width_conservative_543() {
+ use synth_core::backend::VolatileRange;
+ let win = [VolatileRange {
+ base: 0x100,
+ len: 16,
+ }];
+ // Exactly at the window end [0x110,0x114): no intersection.
+ assert!(!intersects_volatile(0x110, &win));
+ // Last in-window byte address 0x10F: intersects.
+ assert!(intersects_volatile(0x10F, &win));
+ // [0xFC,0x100) ends exactly at the base: no intersection.
+ assert!(!intersects_volatile(0xFC, &win));
+ // [0xFD,0x101) straddles the base: intersects.
+ assert!(intersects_volatile(0xFD, &win));
+ // u32-boundary range must not wrap (i64 arithmetic).
+ let hi = [VolatileRange {
+ base: 0xFFFF_FFF0,
+ len: 0x10,
+ }];
+ assert!(intersects_volatile(0xFFFF_FFF4, &hi));
+ assert!(!intersects_volatile(0xFFFF_FFE0, &hi));
+ }
+
+ /// #543 Phase 2: the STATIC access offset participates in the intersection —
+ /// `i32.store offset=12 (i32.const 0xF8)` lands at 0x104, inside the window,
+ /// even though the const base 0xF8 is below it.
+ #[test]
+ fn plan_base_cse_volatile_check_includes_static_offset_543() {
+ use synth_core::backend::VolatileRange;
+ let mut ir = const_addr_stores(&[(0x80, 33), (0x84, 44)]);
+ // Const 0xF8 + access offset 12 → effective address 0x104.
+ ir.push(inst(Opcode::Const {
+ dest: vr(100),
+ value: 0xF8,
+ }));
+ ir.push(inst(Opcode::Const {
+ dest: vr(101),
+ value: 55,
+ }));
+ ir.push(inst(Opcode::MemStore {
+ src: vr(101),
+ addr: vr(100),
+ offset: 12,
+ }));
+ let win = [VolatileRange {
+ base: 0x100,
+ len: 16,
+ }];
+ let plan = plan_base_cse(&ir, &win).expect("the two outside accesses still fold");
+ assert_eq!(plan.fold.len(), 2);
+ assert!(
+ !plan.fold.contains_key(&100),
+ "offset-folded effective address 0x104 is in the window → excluded"
+ );
+ // Without the window the same access folds to 0x104.
+ let plan_free = plan_base_cse(&ir, &[]).expect("activates");
+ assert_eq!(plan_free.fold.get(&100), Some(&0x104));
}
#[test]
@@ -6282,7 +6450,7 @@ mod tests {
val_false: vr(102),
cond: vr(103),
}));
- assert_eq!(plan_base_cse(&ir), None);
+ assert_eq!(plan_base_cse(&ir, &[]), None);
}
#[test]
@@ -6294,7 +6462,7 @@ mod tests {
cond: vr(100),
target: 0,
}));
- assert_eq!(plan_base_cse(&ir), None);
+ assert_eq!(plan_base_cse(&ir, &[]), None);
}
#[test]
@@ -6303,7 +6471,7 @@ mod tests {
// does NOT split control flow, so base-CSE still activates.
let mut ir = const_addr_stores(&[(0, 11), (4, 22)]);
ir.push(inst(Opcode::Label { id: 99 }));
- let plan = plan_base_cse(&ir).expect("activates despite a structural label");
+ let plan = plan_base_cse(&ir, &[]).expect("activates despite a structural label");
assert_eq!(plan.fold.len(), 2);
}
@@ -6312,7 +6480,7 @@ mod tests {
// 0x1000 + 0 exceeds the imm12 window → that access does not fold; with
// only one other foldable store the function falls below threshold.
let ir = const_addr_stores(&[(0x1000, 11), (4, 22)]);
- let plan = plan_base_cse(&ir);
+ let plan = plan_base_cse(&ir, &[]);
// Only the (4,22) store folds → 1 fold → below the ≥2 threshold → None.
assert_eq!(plan, None);
}
@@ -6346,7 +6514,7 @@ mod tests {
}),
];
// addr vreg 0 has use_count 2 → neither store folds → None.
- assert_eq!(plan_base_cse(&ir), None);
+ assert_eq!(plan_base_cse(&ir, &[]), None);
}
#[test]
@@ -6380,7 +6548,7 @@ mod tests {
offset: 32,
}),
];
- let plan = plan_base_cse(&ir).expect("activates");
+ let plan = plan_base_cse(&ir, &[]).expect("activates");
assert_eq!(plan.fold.get(&0), Some(&16)); // 0 + 16
assert_eq!(plan.fold.get(&2), Some(&32)); // 0 + 32
}
diff --git a/scripts/repro/volatile_segment_543.wat b/scripts/repro/volatile_segment_543.wat
new file mode 100644
index 00000000..ee971893
--- /dev/null
+++ b/scripts/repro/volatile_segment_543.wat
@@ -0,0 +1,33 @@
+;; #543 Phase 2 — volatile DMA-window red→green oracle fixture.
+;;
+;; dma_window(v): four const-address linear-memory stores. Two land inside the
+;; DMA window [0x100, 0x110) (`--volatile-segment 0x100:16`), two outside it.
+;; Straight-line, every const address DISTINCT and single-use — exactly the
+;; shape the #468 base-CSE / const-address-fold (`SYNTH_BASE_CSE=1`) optimizes
+;; on the OPTIMIZED (non-`--relocatable`) path: hoist the linmem base into R11
+;; once, fold each const address to `[R11,#imm]`, and drop the per-access
+;; `movw/movt R12` base + `add` + address materialization.
+;;
+;; The behavior lattice pinned by volatile_segment_phase2_543.rs:
+;; - C (no SYNTH_BASE_CSE, no ranges): verbatim per-access codegen;
+;; - A (SYNTH_BASE_CSE, no ranges): all 4 stores fold — smallest .text;
+;; - P (SYNTH_BASE_CSE + --volatile-segment 0x100:16): the 2 window stores
+;; keep their verbatim materialize-and-store codegen, the 2 outside
+;; still fold — strictly between A and C;
+;; - F (SYNTH_BASE_CSE + a range covering all 4): base-CSE fully declines,
+;; byte-identical to C.
+;;
+;; Void on purpose: results are read back from linear memory (0x80/0x84 and
+;; 0x100/0x104) by the unicorn-vs-wasmtime differential, and the stored $v
+;; makes the window contents input-dependent. Addresses/values are neutral,
+;; tied to nothing real. Consumed by
+;; crates/synth-cli/tests/volatile_segment_phase2_543.rs and
+;; scripts/repro/volatile_segment_543_differential.py.
+(module
+ (memory 1)
+ (export "memory" (memory 0))
+ (func (export "dma_window") (param $v i32)
+ (i32.store (i32.const 0x100) (local.get $v)) ;; window
+ (i32.store (i32.const 0x104) (i32.const 22)) ;; window
+ (i32.store (i32.const 0x80) (i32.const 33)) ;; outside
+ (i32.store (i32.const 0x84) (i32.const 44)))) ;; outside
diff --git a/scripts/repro/volatile_segment_543_differential.py b/scripts/repro/volatile_segment_543_differential.py
new file mode 100644
index 00000000..19db3216
--- /dev/null
+++ b/scripts/repro/volatile_segment_543_differential.py
@@ -0,0 +1,160 @@
+#!/usr/bin/env python3
+"""#543 Phase 2 / VCR-DMA-001 — EXECUTION-validate the volatile DMA-window back-off.
+
+`--volatile-segment :` must change ACCESS PATTERNS, never RESULTS:
+with the ranges marked, base-CSE (#468, SYNTH_BASE_CSE=1) keeps every in-window
+access as verbatim per-access materialize-and-access codegen (and const-CSE
+declines wholesale), but the memory the function computes must stay bit-identical
+to wasmtime ground truth in EVERY mode. This harness runs the fixture's
+`dma_window(v)` under unicorn in four builds —
+
+ base : default env, no ranges (the pre-#543 baseline)
+ folded : SYNTH_BASE_CSE=1, no ranges (all 4 const-address stores fold)
+ window : SYNTH_BASE_CSE=1, --volatile-segment 0x100:16
+ (the 2 window stores stay verbatim, the 2 outside still fold)
+ cover : SYNTH_BASE_CSE=1, --volatile-segment 0x80:144
+ (covers all 4 → base-CSE fully declines)
+
+— and asserts the resulting LINEAR MEMORY (fields 0x80/0x84 outside, 0x100/0x104
+inside the DMA window) matches wasmtime for several input values.
+
+NON-VACUITY (the byte-shape claims, mirrored from
+crates/synth-cli/tests/volatile_segment_phase2_543.rs): folded < window < base
+.text sizes, and cover ≡ base byte-identical (every store survives verbatim).
+
+Run (needs wasmtime + unicorn + pyelftools; synth binary via $SYNTH or the
+default release path):
+ python scripts/repro/volatile_segment_543_differential.py
+Exits nonzero on any mismatch or vacuity failure.
+"""
+
+import os
+import subprocess
+import sys
+
+import wasmtime
+from elftools.elf.elffile import ELFFile
+from unicorn import UC_ARCH_ARM, UC_MODE_THUMB, Uc, UcError
+from unicorn.arm_const import UC_ARM_REG_LR, UC_ARM_REG_R0, UC_ARM_REG_SP
+
+SYNTH = os.environ.get("SYNTH", "./target/release/synth")
+WAT = "scripts/repro/volatile_segment_543.wat"
+FUNC = "dma_window"
+# The optimized path materializes this absolute linear-memory base.
+LINMEM = 0x20000100
+CODE, STK, RET = 0x200000, 0x90000, 0x300000
+# Fields written by the fixture: 0x80/0x84 outside, 0x100/0x104 inside the window.
+FIELDS = [0x80, 0x84, 0x100, 0x104]
+
+BUILDS = {
+ "base": (False, []),
+ "folded": (True, []),
+ "window": (True, ["--volatile-segment", "0x100:16"]),
+ "cover": (True, ["--volatile-segment", "0x80:144"]),
+}
+
+
+def compile_elf(out, base_cse, extra):
+ env = {"PATH": "/usr/bin:/bin"}
+ if base_cse:
+ env["SYNTH_BASE_CSE"] = "1"
+ r = subprocess.run(
+ [SYNTH, "compile", WAT, "-o", out, "-b", "arm", "--target", "cortex-m4",
+ "--all-exports", *extra],
+ capture_output=True, text=True, env=env,
+ )
+ if r.returncode != 0:
+ sys.exit(f"compile failed (base_cse={base_cse}, extra={extra}): {r.stderr}")
+
+
+def load(elf):
+ """Return (code_bytes, sh_addr, func_entry_offset)."""
+ f = ELFFile(open(elf, "rb"))
+ text = f.get_section_by_name(".text")
+ code, base = text.data(), text["sh_addr"]
+ fa = None
+ # Resolve via the symtab by section TYPE (synth emits an empty section name).
+ for s in f.iter_sections():
+ if s.header.sh_type == "SHT_SYMTAB":
+ for sym in s.iter_symbols():
+ if sym.name == FUNC:
+ fa = sym["st_value"]
+ if fa is None:
+ sys.exit(f"{elf}: symbol {FUNC} not found")
+ return code, base, fa
+
+
+def text_bytes(elf):
+ return ELFFile(open(elf, "rb")).get_section_by_name(".text").data()
+
+
+def run_arm(elf, v):
+ code, base, fa = load(elf)
+ mu = Uc(UC_ARCH_ARM, UC_MODE_THUMB)
+ mu.mem_map(CODE, 0x10000)
+ mu.mem_map(LINMEM & ~0xFFFF, 0x20000)
+ mu.mem_map(STK - 0x8000, 0x10000)
+ mu.mem_map(RET, 0x1000)
+ mu.mem_write(CODE, code)
+ mu.reg_write(UC_ARM_REG_SP, STK)
+ mu.reg_write(UC_ARM_REG_LR, RET | 1)
+ mu.reg_write(UC_ARM_REG_R0, v & 0xFFFFFFFF)
+ try:
+ mu.emu_start((CODE + fa - base) | 1, RET, count=100000)
+ except UcError as e:
+ return f"ERR:{e}"
+ return {off: int.from_bytes(mu.mem_read(LINMEM + off, 4), "little")
+ for off in FIELDS}
+
+
+def wasm_mem(v):
+ engine = wasmtime.Engine()
+ module = wasmtime.Module(engine, open(WAT, "rb").read())
+ store = wasmtime.Store(engine)
+ inst = wasmtime.Instance(store, module, [])
+ inst.exports(store)[FUNC](store, v)
+ mem = inst.exports(store)["memory"]
+ data = mem.read(store, 0, 0x110)
+ return {off: int.from_bytes(data[off:off + 4], "little") for off in FIELDS}
+
+
+def main():
+ elfs = {}
+ for tag, (cse, extra) in BUILDS.items():
+ elf = f"/tmp/volseg543_diff_{tag}.elf"
+ compile_elf(elf, cse, extra)
+ elfs[tag] = elf
+
+ # Non-vacuity: the byte-shape lattice must hold or we are testing nothing.
+ sizes = {tag: len(text_bytes(elf)) for tag, elf in elfs.items()}
+ if not sizes["folded"] < sizes["window"]:
+ sys.exit(f"VACUOUS: window ({sizes['window']}B) not > folded "
+ f"({sizes['folded']}B) — the range suppressed nothing")
+ if not sizes["window"] < sizes["base"]:
+ sys.exit(f"VACUOUS: window ({sizes['window']}B) not < base "
+ f"({sizes['base']}B) — the outside folds did not survive")
+ if text_bytes(elfs["cover"]) != text_bytes(elfs["base"]):
+ sys.exit("FAIL: full-coverage range must fully decline base-CSE "
+ "(cover .text != base .text)")
+ print(f".text: base={sizes['base']}B folded={sizes['folded']}B "
+ f"window={sizes['window']}B cover={sizes['cover']}B (≡ base)")
+
+ fails = 0
+ for v in [0, 1, 22, 0xDEADBEEF, 0x7FFFFFFF, 0xFFFFFFFF]:
+ gt = wasm_mem(v)
+ line = [f"dma_window({v:#x}):"]
+ for tag, elf in elfs.items():
+ got = run_arm(elf, v)
+ ok = got == gt
+ fails += 0 if ok else 1
+ line.append(f"{tag}={'ok' if ok else 'MISMATCH'}")
+ if not ok:
+ line.append(f"\n {tag}={got}\n wt ={gt}")
+ print(" ".join(line))
+
+ print("ORACLE: PASS" if fails == 0 else f"ORACLE: FAIL ({fails})")
+ sys.exit(1 if fails else 0)
+
+
+if __name__ == "__main__":
+ main()