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
44 changes: 44 additions & 0 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -621,6 +621,50 @@ jobs:
SYNTH: ./target/debug/synth
run: python scripts/repro/stack_args_503_differential.py

i64-completeness-503-587-oracle:
name: i64 stack-param + spill-pool-grow oracle
# VCR-ORACLE-001 (#242, #503-i64, #587): EXECUTE the two previously
# loud-skipped direct-selector i64 classes under unicorn and diff vs
# wasmtime, on BOTH paths (--relocatable = falcon's, and the default):
# * #503-i64 — 64-bit params AAPCS-passed on the STACK (past R3 /
# even-align-spilled), incl. the narrow-after-wide shape that was
# silently MIScompiled (p3 of `(i64 i32 i32 i32)` read from R3 = p2),
# a write-back shape, and a has-call shape. Falcon func_58/func_163.
# * #587 — an i64-dense function whose ~16 concurrent pair spills
# exhausted the fixed 8-slot pool; the pool-grow recovery retry (last
# resort, after the #474 promotion-off fallback) sizes the pool from
# the operand-stack-depth bound. Falcon func_60/func_73.
# Isolated job: emulation deps pip-installed here ONLY.
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v7
- uses: dtolnay/rust-toolchain@stable
- name: Cache Cargo dependencies
uses: actions/cache@v6
with:
path: |
~/.cargo/registry
~/.cargo/git
target/
key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
restore-keys: |
${{ runner.os }}-cargo-
- name: Build synth
run: cargo build -p synth-cli
- uses: actions/setup-python@v6
with:
python-version: "3.x"
- name: Install emulation deps
run: pip install wasmtime unicorn pyelftools
- name: Run i64 stack-param oracle (#503-i64)
env:
SYNTH: ./target/debug/synth
run: python scripts/repro/i64_stack_param_503_differential.py
- name: Run i64 spill-pool-grow oracle (#587)
env:
SYNTH: ./target/debug/synth
run: python scripts/repro/i64_spill_pool_587_differential.py

br-table-507-oracle:
name: optimized-path br_table oracle
# VCR-ORACLE-001 (#242, #507): EXECUTE br_table dispatch compiled via the
Expand Down
105 changes: 87 additions & 18 deletions crates/synth-backend/src/arm_backend.rs
Original file line number Diff line number Diff line change
Expand Up @@ -286,7 +286,8 @@ fn compile_wasm_to_arm(
// not behavioural).
let select_direct_attempt = |spill_on_exhaustion: bool,
param_backing_on_exhaustion: bool,
local_promote: bool|
local_promote: bool,
i64_spill_slots: Option<usize>|
-> Result<Vec<ArmInstruction>, synth_core::Error> {
let db = RuleDatabase::with_standard_rules();
let mut selector =
Expand Down Expand Up @@ -327,6 +328,13 @@ fn compile_wasm_to_arm(
}
selector.set_spill_on_exhaustion(spill_on_exhaustion);
selector.set_param_backing_on_exhaustion(param_backing_on_exhaustion);
// #587 pool-grow rung: a larger i64 spill-slot pool, set ONLY on the
// retry after an attempt failed with the slot-pool-exhausted Err —
// functions that compile with the default pool keep their frame
// byte-identical by construction.
if let Some(slots) = i64_spill_slots {
selector.set_i64_spill_slots(slots);
}
// VCR-RA local promotion (#390, #242): keep eligible non-param i32 locals
// in callee-saved registers instead of frame slots — the structural lever
// toward native parity. DEFAULT-ON as of v0.14.0: gale's G474RE DWT gate
Expand All @@ -345,14 +353,17 @@ fn compile_wasm_to_arm(
let select_direct = || -> Result<Vec<ArmInstruction>, String> {
const SINGLE_EXHAUSTION: &str = "all allocatable registers are live on the stack";
const PAIR_EXHAUSTION: &str = "no consecutive pair of free registers for i64";
const SLOT_EXHAUSTION: &str = "i64 spill-slot pool exhausted";
// The full exhaustion-recovery ladder, parameterized on whether local
// promotion is enabled. Each rung is reached only when the previous one
// returned a recoverable register-exhaustion Err, so a function that
// compiles on the first attempt is untouched by the later rungs. Returns
// the result AND which rung produced it (for the #242 measurement below).
let recovery_ladder =
|promote: bool| -> (Result<Vec<ArmInstruction>, synth_core::Error>, &'static str) {
let mut attempt = select_direct_attempt(false, false, promote);
|promote: bool,
i64_spill_slots: Option<usize>|
-> (Result<Vec<ArmInstruction>, synth_core::Error>, &'static str) {
let mut attempt = select_direct_attempt(false, false, promote, i64_spill_slots);
let mut rung = "base";
// VCR-RA-001 step 3b-lite (#242): the i32 register-exhaustion
// hard-fail is recoverable — retry with spill-on-exhaustion, which
Expand All @@ -361,7 +372,7 @@ fn compile_wasm_to_arm(
if let Err(e) = &attempt
&& e.to_string().contains(SINGLE_EXHAUSTION)
{
attempt = select_direct_attempt(true, false, promote);
attempt = select_direct_attempt(true, false, promote, i64_spill_slots);
rung = "spill";
}
// VCR-RA-001 acceptance increment (#242): the i64 consecutive-PAIR
Expand All @@ -371,7 +382,7 @@ fn compile_wasm_to_arm(
if let Err(e) = &attempt
&& e.to_string().contains(PAIR_EXHAUSTION)
{
attempt = select_direct_attempt(true, true, promote);
attempt = select_direct_attempt(true, true, promote, i64_spill_slots);
rung = "param-backing";
}
(attempt, rung)
Expand All @@ -387,19 +398,57 @@ fn compile_wasm_to_arm(
// is reached ONLY by functions that exhaust WITH promotion, so promotion-on
// output is untouched by construction (frozen byte gate stays green).
let promote = std::env::var("SYNTH_NO_LOCAL_PROMOTE").is_err();
let (mut attempt, mut rung) = recovery_ladder(promote);
let mut promotion_dropped = false;
if promote
&& attempt
.as_ref()
.err()
.is_some_and(|e| e.to_string().contains("register exhaustion"))
// The full pre-#587 recovery sequence (promotion-on ladder, then the
// #474 promotion-off fallback), parameterized on the pool size so the
// pool-grow retry below reruns it verbatim.
let full_sequence = |slots: Option<usize>| -> (
Result<Vec<ArmInstruction>, synth_core::Error>,
&'static str,
bool,
) {
let (mut attempt, mut rung) = recovery_ladder(promote, slots);
let mut promotion_dropped = false;
if promote
&& attempt
.as_ref()
.err()
.is_some_and(|e| e.to_string().contains("register exhaustion"))
{
let (rescued, off_rung) = recovery_ladder(false, slots);
if rescued.is_ok() {
attempt = rescued;
rung = off_rung;
promotion_dropped = true;
}
}
(attempt, rung, promotion_dropped)
};
let (mut attempt, mut rung, mut promotion_dropped) = full_sequence(None);
// #587 pool-grow retry (the falcon func_60/func_73 remainder): the fixed
// 8-slot i64 spill pool can exhaust while spilling is otherwise working —
// an i64-dense function simply has more values simultaneously live than
// the pool holds. Rerun the ENTIRE sequence (every rung, both promotion
// modes) with the pool sized from a conservative operand-stack-depth
// bound: the number of simultaneously spilled values can never exceed
// the operand-stack depth, plus a few transient slots (the arg-move
// cycle resolver and call-result parking each borrow one). The selector
// clamps the request to its 12-bit-friendly cap; a function that still
// exhausts stays an honest loud skip. Deliberately LAST — after the #474
// promotion-off fallback — so any function that compiled yesterday
// (through any rung or fallback) is produced by exactly yesterday's
// path, byte-identical; the grown pool only ever fires for functions
// whose every existing escape ended in the slot-pool Err.
if attempt
.as_ref()
.err()
.is_some_and(|e| e.to_string().contains(SLOT_EXHAUSTION))
{
let (rescued, off_rung) = recovery_ladder(false);
if rescued.is_ok() {
attempt = rescued;
rung = off_rung;
promotion_dropped = true;
let depth = synth_core::wasm_stack_check::max_depth_bound(wasm_ops) as usize;
let (grown, _, grown_dropped) = full_sequence(Some(depth.saturating_add(4)));
if grown.is_ok() {
attempt = grown;
rung = "pool-grow";
promotion_dropped = grown_dropped;
}
}
// VCR-RA measurement (#242): log which recovery rung produced the result,
Expand Down Expand Up @@ -452,7 +501,27 @@ fn compile_wasm_to_arm(
// lands the carried value at the join. Never fires for void-block control
// flow (all frozen/optimized fixtures), so those stay byte-identical.
let has_value_carry = has_value_carrying_branch(wasm_ops, &config.current_func_block_arity);
let arm_instrs = if config.no_optimize || config.relocatable || has_br_table || has_value_carry
// #503-i64/#518: route any signature with a 64-bit (i64/f64) param to the
// direct selector. The optimized path's param homing is width-naive — its
// #518 decline covers only functions that READ an i64 param (an `I64Load`
// from a param index), so a function that reads an i32 param whose AAPCS
// home a preceding wide param SHIFTED (e.g. p1 of `(i64 i32)` lives in R2,
// not R1; p3 of `(i64 i32 i32 i32)` lives on the stack, not in R3) was
// silently miscompiled rather than falling back. The direct selector's
// `aapcs_param_layout` homing handles every such shape (i64-param READS
// already fell back to it via the ir_to_arm Err, so those functions emit
// the same bytes as before). `num_params` counts read-first locals, so a
// function that never touches any param keeps the optimized path.
let has_wide_param = config
.current_func_params_i64
.iter()
.take(num_params as usize)
.any(|&w| w);
let arm_instrs = if config.no_optimize
|| config.relocatable
|| has_br_table
|| has_value_carry
|| has_wide_param
{
select_direct()?
} else {
Expand Down
92 changes: 92 additions & 0 deletions crates/synth-cli/tests/i64_completeness_503_587.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,92 @@
//! #503-i64 + #587 — direct-selector i64 completeness guards.
//!
//! Two honest-skip classes closed end-to-end:
//!
//! * **#503-i64**: any 64-bit (i64/f64) param AAPCS-passed on the STACK (past
//! R3, or even-align-spilled) used to loud-skip the whole function
//! ("#518/#503: an i64/f64 param is AAPCS-passed past R3"). The width-aware
//! `aapcs_param_layout` incoming homing now lowers every shape in
//! `scripts/repro/i64_stack_param_503.wat` (falcon func_58/func_163/func_164
//! class).
//! * **#587**: an i64-dense function whose simultaneous pair spills exceed the
//! fixed 8-slot pool used to loud-skip ("i64 spill-slot pool exhausted" —
//! falcon func_60/func_73). The backend's `pool-grow` recovery retry now
//! reruns the full ladder with the pool sized from the operand-stack-depth
//! bound — strictly LAST, after the #474 promotion-off fallback, so every
//! function that compiled before is produced by exactly the old path
//! (`promotion_never_causes_compile_failure_474` + the frozen byte gate
//! prove bit-identity).
//!
//! Execution correctness (vs wasmtime under unicorn) is gated by
//! `scripts/repro/i64_stack_param_503_differential.py` and
//! `scripts/repro/i64_spill_pool_587_differential.py`; these tests pin the
//! compile-side contract: no skips, and #587 lands on the pool-grow rung.

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)
}

fn compile(wat: &str, out: &str, extra_env: &[(&str, &str)]) -> std::process::Output {
let mut cmd = Command::new(synth());
for (k, v) in extra_env {
cmd.env(k, v);
}
cmd.args([
"compile",
fixture(wat).to_str().unwrap(),
"-o",
out,
"-b",
"arm",
"--target",
"cortex-m4",
"--relocatable",
"--all-exports",
])
.output()
.expect("failed to run synth")
}

/// #503-i64: every previously-declined i64-stack-param shape compiles — zero
/// skipped functions in the fixture.
#[test]
fn i64_stack_param_shapes_compile_without_skips_503() {
let out = compile("i64_stack_param_503.wat", "/tmp/cli_503.o", &[]);
let stderr = String::from_utf8_lossy(&out.stderr);
assert!(out.status.success(), "compile failed:\n{stderr}");
assert!(
!stderr.contains("skipping function"),
"an i64-stack-param shape was skipped (the #503-i64 class regressed):\n{stderr}"
);
}

/// #587: the pool-exhausting i64-dense function compiles, and it does so on
/// the `pool-grow` recovery rung (not by accident on an earlier rung — that
/// would make this test vacuous as a pool-grow guard).
#[test]
fn i64_spill_pool_exhaustion_rescued_by_pool_grow_587() {
let out = compile(
"i64_spill_pool_587.wat",
"/tmp/cli_587.o",
&[("SYNTH_RECOVERY_STATS", "1")],
);
let stderr = String::from_utf8_lossy(&out.stderr);
assert!(out.status.success(), "compile failed:\n{stderr}");
assert!(
!stderr.contains("skipping function"),
"the i64-dense function was skipped (the #587 pool-grow rung regressed):\n{stderr}"
);
assert!(
stderr.contains("rung=pool-grow result=ok"),
"expected the pool-grow rung to produce the result (recovery stats):\n{stderr}"
);
}
53 changes: 53 additions & 0 deletions crates/synth-core/src/wasm_stack_check.rs
Original file line number Diff line number Diff line change
Expand Up @@ -77,6 +77,37 @@ pub fn check_no_underflow(wasm_ops: &[WasmOp]) -> crate::Result<()> {
Ok(())
}

/// #587: a conservative UPPER BOUND on the wasm value-stack depth this op
/// sequence can reach. Used by the ARM backend's `pool-grow` exhaustion-
/// recovery rung to size the i64 spill-slot pool: the number of values
/// *simultaneously* spilled by the direct selector can never exceed the
/// number of values simultaneously live on the operand stack, so a pool of
/// `max_depth_bound` slots (plus the resolver/result-parking transients the
/// caller adds) cannot exhaust through the deepest-value spill loop.
///
/// Over-approximation rules (never under-counts in reachable code):
/// * Modeled ops apply their exact pops/pushes; a would-be underflow clamps
/// to 0 (malformed input is someone else's Err, not a panic here).
/// * Unmodeled/`Bail` ops (`call`, terminators, SIMD, …) are treated as net
/// `+1` — every wasm op pushes at most one value net, so this only ever
/// over-counts (a call pops its args; a terminator pushes nothing).
/// * `Block`/`Loop`/`If`/`Else`/`End` are stack-neutral in the effects table,
/// which over-counts (`if` really pops its condition) — same direction.
pub fn max_depth_bound(wasm_ops: &[WasmOp]) -> u32 {
let mut depth: i64 = 0;
let mut max: i64 = 0;
for op in wasm_ops {
match stack_effect_or_bail(op) {
StackEffect::Modeled { pops, pushes } => {
depth = (depth - pops as i64).max(0) + pushes as i64;
}
StackEffect::Bail => depth += 1,
}
max = max.max(depth);
}
u32::try_from(max).unwrap_or(u32::MAX)
}

enum StackEffect {
Modeled { pops: u32, pushes: u32 },
Bail,
Expand Down Expand Up @@ -476,4 +507,26 @@ mod tests {
fn empty_input_is_ok() {
assert!(check_no_underflow(&[]).is_ok());
}

#[test]
fn max_depth_bound_exact_on_modeled_ops() {
// #587: 3 consts (depth 3) folded to 1 — the bound is the peak, 3.
let ops = vec![
WasmOp::I32Const(1),
WasmOp::I32Const(2),
WasmOp::I32Const(3),
WasmOp::I32Add,
WasmOp::I32Add,
];
assert_eq!(max_depth_bound(&ops), 3);
assert_eq!(max_depth_bound(&[]), 0);
}

#[test]
fn max_depth_bound_over_approximates_unmodeled_ops() {
// #587: `call` bails in the underflow checker; the bound treats it as
// net +1 (an over-approximation, never an under-count).
let ops = vec![WasmOp::I32Const(1), WasmOp::Call(0), WasmOp::I32Add];
assert!(max_depth_bound(&ops) >= 2);
}
}
Loading
Loading