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
76 changes: 45 additions & 31 deletions artifacts/verified-codegen-roadmap.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -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 <base>:<len>` (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 <base>:<len>` (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
Expand All @@ -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).
34 changes: 25 additions & 9 deletions crates/synth-backend/src/arm_backend.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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 <base>:<len>`) 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
Expand Down Expand Up @@ -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
Expand Down
34 changes: 20 additions & 14 deletions crates/synth-cli/tests/volatile_segment_flag_543.rs
Original file line number Diff line number Diff line change
@@ -1,20 +1,22 @@
//! #543 Phase 1 — `--volatile-segment <base>:<len>` 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;
Expand Down Expand Up @@ -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", &[])
Expand All @@ -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"
);
}
197 changes: 197 additions & 0 deletions crates/synth-cli/tests/volatile_segment_phase2_543.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,197 @@
//! #543 Phase 2 — the optimizer HONORS `--volatile-segment <base>:<len>`:
//! 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<u8> {
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");
}
Loading
Loading