From f77805b5efe5537538cec8843896f571174c70c5 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 20 May 2026 19:11:50 +0200 Subject: [PATCH] fix(cli): synth verify exits non-zero when built without verify feature MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `synth verify` is advertised as a subcommand in `synth --help` and in the top-level usage examples, but on a binary built without the `verify` feature (the default — `verify` pulls in z3-sys, which needs network and breaks `cargo install` for many users) it printed a "rebuild" hint and returned `Ok(())`. Exit code 0. A script or CI step gating on `synth verify` — the Z3 translation- validation oracle, the "did the ARM lowering preserve WASM semantics" check — would silently believe the binary was validated when in fact nothing ran. That is a correctness-of-process bug: the verify step is load-bearing on the ASIL-D path, and a success-shaped no-op defeats it. Fix: the `#[cfg(not(feature = "verify"))]` branch now `anyhow::bail!`s with a clear message and a non-zero exit. A consumer that runs `synth verify` and checks the exit code now correctly sees failure when the binary cannot verify. Also marks the `Verify` subcommand's help text as requiring `--features verify`, so `synth --help` is honest about the dependency. Not changed: `verify` stays a non-default feature. Making it default would pull z3-sys into every `cargo install`, which needs network at build time and is the reason it is opt-in. The fix is to fail honestly, not to force the dependency on everyone. Closes #124. --- crates/synth-cli/src/main.rs | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) diff --git a/crates/synth-cli/src/main.rs b/crates/synth-cli/src/main.rs index ac312f9..8b8bbd0 100644 --- a/crates/synth-cli/src/main.rs +++ b/crates/synth-cli/src/main.rs @@ -187,7 +187,8 @@ enum Commands { /// List available compilation backends and their status Backends, - /// Verify compilation correctness via Z3 (e.g., synth verify input.wat output.elf) + /// Verify compilation correctness via Z3 — requires a build with + /// `--features verify` (e.g., synth verify input.wat output.elf) Verify { /// Input WASM or WAT file (source) #[arg(value_name = "WASM")] @@ -2236,8 +2237,19 @@ fn verify_command(wasm_input: PathBuf, elf_input: PathBuf, backend_name: &str) - #[cfg(not(feature = "verify"))] { - println!("\n Rebuild with verification support:"); - println!(" cargo build --features verify"); + // This binary was built without the `verify` feature, so no Z3 + // translation validation can run. Returning Ok here would make + // `synth verify` exit success-shaped while doing nothing — a + // script or CI step gating on `synth verify` would silently + // believe the binary was validated (issue #124). Fail loudly + // with a non-zero exit instead. + anyhow::bail!( + "this `synth` binary was built without the `verify` feature — \ + Z3 translation validation is unavailable.\n \ + Rebuild with verification support:\n \ + cargo build --features verify\n \ + (or `cargo install --path crates/synth-cli --features verify`)" + ); } } else if caps.supports_binary_verification { println!(" Strategy: Binary-level translation validation (ASIL B path)");