synth-cli 0.6.0

//! Synth CLI - WebAssembly-to-ARM Cortex-M AOT Compiler
//!
//! Command-line interface for the Synth compiler. Compiles WASM/WAT files
//! to bare-metal ARM Cortex-M ELF binaries with optional formal verification.

use anyhow::{Context, Result};
use clap::{Parser, Subcommand};
use std::fs::File;
use std::io::Write;
use std::path::PathBuf;
use synth_backend::{
    ArmBackend, ArmRelocationType, ElfBuilder, ElfSectionType, ElfType, ProgramFlags,
    ProgramHeader, Relocation, Section, SectionFlags, Symbol, SymbolBinding, SymbolType,
    VectorTable, W2C2Backend,
};
use synth_core::HardwareCapabilities;
use synth_core::SafetyManifest;
use synth_core::backend::{Backend, BackendRegistry, CompileConfig, SafetyBounds};
use synth_core::target::TargetSpec;
use synth_core::wasm_decoder::ImportEntry;
use synth_synthesis::{FunctionOps, WasmMemory, WasmOp, decode_wasm_functions, decode_wasm_module};
use tracing::{Level, info};
use wast::parser::{self, ParseBuffer};
use wast::{Wast, WastDirective};

mod sign;

/// Sentinel value clap substitutes when `--sbom` is given without a path.
/// Resolved to `<output>.cdx.json` by [`resolve_sbom_path`]. Unlikely to
/// collide with a real path the user would pass.
const SBOM_DEFAULT_SENTINEL: &str = "\u{0}sbom-default\u{0}";

#[derive(Parser)]
#[command(name = "synth")]
#[command(about = "WebAssembly-to-ARM Cortex-M AOT compiler")]
#[command(
    long_about = "Synth compiles WebAssembly (WASM/WAT) to native ARM Cortex-M machine code,\n\
producing bare-metal ELF binaries for embedded targets.\n\n\
Examples:\n  \
synth compile input.wat -o output.elf\n  \
synth compile input.wat --cortex-m -o firmware.elf\n  \
synth compile input.wat --cortex-m --link -o firmware.elf\n  \
synth disasm firmware.elf\n  \
synth verify input.wat firmware.elf"
)]
#[command(version)]
struct Cli {
    #[command(subcommand)]
    command: Commands,

    /// Enable verbose output
    #[arg(short, long)]
    verbose: bool,
}

#[derive(Subcommand)]
enum Commands {
    /// Parse and analyze a WebAssembly component
    Parse {
        /// Input WebAssembly file
        #[arg(value_name = "INPUT")]
        input: PathBuf,

        /// Output JSON representation
        #[arg(short, long, value_name = "OUTPUT")]
        output: Option<PathBuf>,
    },

    /// Synthesize a component to native code
    Synthesize {
        /// Input WebAssembly file
        #[arg(value_name = "INPUT")]
        input: PathBuf,

        /// Output binary file
        #[arg(short, long, value_name = "OUTPUT")]
        output: PathBuf,

        /// Target architecture
        #[arg(
            short,
            long,
            value_name = "TARGET",
            default_value = "thumbv7em-none-eabihf"
        )]
        target: String,

        /// Hardware config (nrf52840, stm32f407, stm32h743, imxrt1062, or custom)
        #[arg(long, value_name = "HARDWARE", default_value = "nrf52840")]
        hardware: String,

        /// Optimization level (0-3, s, z)
        #[arg(short = 'O', long, value_name = "LEVEL", default_value = "2")]
        opt_level: String,

        /// Enable XIP (execute-in-place)
        #[arg(long)]
        xip: bool,

        /// Enable formal verification
        #[arg(long)]
        verify: bool,
    },

    /// Display information about a target
    TargetInfo {
        /// Target name
        #[arg(value_name = "TARGET")]
        target: String,
    },

    /// Compile WASM/WAT to ARM ELF (e.g., synth compile input.wat --cortex-m -o fw.elf)
    Compile {
        /// Input WASM or WAT file (optional, use --demo for built-in demos)
        #[arg(value_name = "INPUT")]
        input: Option<PathBuf>,

        /// Output ELF file
        #[arg(short, long, value_name = "OUTPUT", default_value = "output.elf")]
        output: PathBuf,

        /// Demo function to compile (add, mul, calc) - used when no input file
        #[arg(short, long, value_name = "DEMO")]
        demo: Option<String>,

        /// Function index to compile (compiles all exports if neither this nor --func-name is set)
        #[arg(short, long, value_name = "INDEX")]
        func_index: Option<u32>,

        /// Function name (export name) to compile - overrides func_index
        #[arg(short = 'n', long, value_name = "NAME")]
        func_name: Option<String>,

        /// Compile ALL exported functions into a multi-function ELF
        #[arg(long)]
        all_exports: bool,

        /// Generate complete Cortex-M binary with vector table (for Renode/QEMU)
        #[arg(long)]
        cortex_m: bool,

        /// Target profile (cortex-m3, cortex-m4, cortex-m4f, cortex-m7, cortex-m7dp)
        /// Implies --cortex-m for Cortex-M targets
        #[arg(short, long, value_name = "TARGET")]
        target: Option<String>,

        /// Disable optimization passes (use direct instruction selection)
        #[arg(long)]
        no_optimize: bool,

        /// Use Loom-compatible optimization (skip passes Loom already handles)
        #[arg(long)]
        loom_compat: bool,

        /// Run Loom WASM optimizer before compilation (requires --features loom)
        /// Pipeline: WASM -> loom optimize -> optimized WASM -> synth compile -> ARM
        /// Implies --loom-compat (skips redundant synth passes)
        #[arg(long)]
        loom: bool,

        /// DEPRECATED: alias for `--safety-bounds software`. Will be removed
        /// in a future release. Prints a deprecation notice when used.
        #[arg(long)]
        bounds_check: bool,

        /// Memory bounds safety profile (Phase 1 of binary-safety design).
        ///
        /// Accepted values:
        /// - `none`     — no inline check, no MPU/PMP setup (fastest, unsafe)
        /// - `mpu`      — rely on ARM MPU / RV32 PMP hardware enforcement
        /// - `software` — emit CMP/BHS (ARM) or BGEU+EBREAK (RV32) per access
        /// - `mask`     — AND addr with `mem_size - 1` (requires power-of-two size)
        #[arg(long, value_name = "MODE")]
        safety_bounds: Option<String>,

        /// Compilation backend (arm, w2c2, awsm, wasker)
        #[arg(short, long, default_value = "arm")]
        backend: String,

        /// Run translation validation after compilation
        #[arg(long)]
        verify: bool,

        /// Link the compiled object into a final firmware ELF using arm-none-eabi-gcc
        #[arg(long)]
        link: bool,

        /// Path to kiln-builtins object file (.o) for linking (used with --link)
        #[arg(long, value_name = "BUILTINS")]
        builtins: Option<PathBuf>,

        /// Force relocatable object (.o, ET_REL) output even when wasm has no imports
        /// — for linking into a host build system.
        #[arg(long)]
        relocatable: bool,

        /// Emit a CycloneDX 1.5 SBOM for the compiled ELF. With a path, writes
        /// there; as a bare flag (`--sbom`) writes `<output>.cdx.json` next to
        /// the ELF. The SBOM documents the synth compiler, the input WASM, the
        /// output ELF (hashes + sizes), and the WASM module's imports. It is
        /// the artifact consumed by `rivet import --format cyclonedx`.
        #[arg(
            long,
            value_name = "PATH",
            num_args = 0..=1,
            default_missing_value = SBOM_DEFAULT_SENTINEL
        )]
        sbom: Option<PathBuf>,

        /// Sign the compiled ELF (in place) via sigil's `wsc sign --keyless
        /// --format elf`. Requires the `wsc` binary from
        /// https://github.com/pulseengine/sigil on PATH, plus an OIDC token
        /// in the environment (e.g. GitHub Actions with `id-token: write`).
        /// Off by default — opt in per-invocation. See
        /// `docs/sigil-integration.md`.
        #[arg(long)]
        sign_output: bool,
    },

    /// Disassemble an ARM ELF file (e.g., synth disasm output.elf)
    Disasm {
        /// Input ELF file
        #[arg(value_name = "INPUT")]
        input: PathBuf,
    },

    /// List available compilation backends and their status
    Backends,

    /// 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")]
        wasm_input: PathBuf,

        /// Input ELF file (compiled output to verify)
        #[arg(value_name = "ELF")]
        elf_input: PathBuf,

        /// Backend that produced the ELF (for verification strategy selection)
        #[arg(short, long, default_value = "arm")]
        backend: String,
    },

    /// Emit RISC-V bare-metal startup code + linker script
    /// (e.g., `synth riscv-runtime -o build/`)
    RiscvRuntime {
        /// Output directory — receives `startup.c` and `linker.ld`
        #[arg(short = 'o', long, value_name = "DIR", default_value = ".")]
        outdir: PathBuf,

        /// Target ISA variant (default: rv32imac)
        #[arg(short, long, default_value = "rv32imac")]
        target: String,

        /// Flash origin address (default: 0x0)
        #[arg(long, default_value = "0x0")]
        flash_origin: String,

        /// RAM origin address (default: 0x80000000)
        #[arg(long, default_value = "0x80000000")]
        ram_origin: String,

        /// Linear-memory size in bytes (default: 65536, one wasm page)
        #[arg(long, default_value = "65536")]
        linear_memory_size: u64,

        /// Stack size in bytes (default: 4096)
        #[arg(long, default_value = "4096")]
        stack_size: u64,

        /// Enable FPU init in the reset vector
        #[arg(long)]
        enable_fpu: bool,
    },
}

fn main() -> Result<()> {
    let cli = Cli::parse();

    // Initialize logging
    let level = if cli.verbose {
        Level::DEBUG
    } else {
        Level::INFO
    };

    tracing_subscriber::fmt()
        .with_max_level(level)
        .with_target(false)
        .init();

    match cli.command {
        Commands::Parse { input, output } => {
            parse_command(input, output)?;
        }
        Commands::Synthesize {
            input,
            output,
            target,
            hardware,
            opt_level,
            xip,
            verify,
        } => {
            synthesize_command(input, output, target, hardware, opt_level, xip, verify)?;
        }
        Commands::TargetInfo { target } => {
            target_info_command(target)?;
        }
        Commands::Compile {
            input,
            output,
            demo,
            func_index,
            func_name,
            all_exports,
            cortex_m,
            target,
            no_optimize,
            loom_compat,
            loom,
            bounds_check,
            safety_bounds,
            backend,
            verify,
            link,
            builtins,
            relocatable,
            sbom,
            sign_output,
        } => {
            // Resolve target spec: --target overrides, --cortex-m is backwards compat
            let target_spec = resolve_target_spec(target.as_deref(), cortex_m)?;
            let is_cortex_m =
                cortex_m || target_spec.family == synth_core::target::ArchFamily::ArmCortexM;

            // --loom implies --loom-compat (skip redundant synth passes)
            let loom_compat = loom_compat || loom;

            // Phase 1 safety-bounds resolution. `--safety-bounds` takes
            // precedence; `--bounds-check` is the legacy alias and emits a
            // single-line deprecation notice when used.
            let resolved_safety_bounds =
                resolve_safety_bounds(safety_bounds.as_deref(), bounds_check)?;

            // Resolve the CycloneDX SBOM destination. `--sbom` with no value
            // means "next to the ELF" (`<output>.cdx.json`); `--sbom PATH`
            // writes there; absent means no SBOM.
            let sbom_path = resolve_sbom_path(sbom, &output);

            compile_command(
                input,
                output.clone(),
                demo,
                func_index,
                func_name,
                all_exports,
                is_cortex_m,
                no_optimize,
                loom_compat,
                loom,
                resolved_safety_bounds,
                &backend,
                verify,
                &target_spec,
                relocatable,
                sbom_path,
                sign_output,
            )?;

            // If --link requested, invoke the cross-linker
            if link {
                link_firmware(&output, builtins.as_deref(), &target_spec)?;
            }
        }
        Commands::Disasm { input } => {
            disasm_command(input)?;
        }
        Commands::Backends => {
            backends_command()?;
        }
        Commands::Verify {
            wasm_input,
            elf_input,
            backend,
        } => {
            verify_command(wasm_input, elf_input, &backend)?;
        }
        Commands::RiscvRuntime {
            outdir,
            target,
            flash_origin,
            ram_origin,
            linear_memory_size,
            stack_size,
            enable_fpu,
        } => {
            riscv_runtime_command(
                outdir,
                target,
                flash_origin,
                ram_origin,
                linear_memory_size,
                stack_size,
                enable_fpu,
            )?;
        }
    }

    Ok(())
}

#[cfg(feature = "riscv")]
#[allow(clippy::too_many_arguments)]
fn riscv_runtime_command(
    outdir: PathBuf,
    target: String,
    flash_origin: String,
    ram_origin: String,
    linear_memory_size: u64,
    stack_size: u64,
    enable_fpu: bool,
) -> Result<()> {
    use synth_backend_riscv::{
        LinkerScriptConfig, RiscVLinkerScriptGenerator, RiscVStartupGenerator, StartupConfig,
    };
    use synth_core::{HardwareCapabilities, RISCVVariant, TargetArch};

    // Hardware caps from the target name.
    let variant = match target.as_str() {
        "rv32i" => RISCVVariant::RV32I,
        "rv32imac" | "rv32imc" => RISCVVariant::RV32IMAC,
        "rv32gc" => RISCVVariant::RV32GC,
        "rv64i" => RISCVVariant::RV64I,
        "rv64imac" => RISCVVariant::RV64IMAC,
        "rv64gc" => RISCVVariant::RV64GC,
        _ => anyhow::bail!(
            "unknown RISC-V target: {}. Supported: rv32i, rv32imac, rv32gc, rv64i, rv64imac, rv64gc",
            target
        ),
    };

    let parse_addr = |s: &str| -> Result<u64> {
        let s = s.trim_start_matches("0x").trim_start_matches("0X");
        u64::from_str_radix(s, 16).context(format!("invalid hex address: {}", s))
    };
    let flash_origin_v = parse_addr(&flash_origin)?;
    let ram_origin_v = parse_addr(&ram_origin)?;

    let hw_caps = HardwareCapabilities {
        arch: TargetArch::RISCV(variant),
        has_mpu: false,
        mpu_regions: 0,
        has_pmp: true,
        pmp_entries: 16,
        has_fpu: enable_fpu,
        fpu_precision: None,
        has_simd: false,
        simd_level: None,
        xip_capable: true,
        flash_size: 64 * 1024,
        ram_size: 64 * 1024,
    };

    std::fs::create_dir_all(&outdir).context("failed to create output directory")?;

    // Startup
    let startup = RiscVStartupGenerator::new(hw_caps.clone()).with_config(StartupConfig {
        enable_fpu,
        ..Default::default()
    });
    let startup_path = outdir.join("startup.c");
    std::fs::write(&startup_path, startup.generate())
        .context(format!("failed to write {}", startup_path.display()))?;

    // Linker script
    let linker = RiscVLinkerScriptGenerator::new(hw_caps).with_config(LinkerScriptConfig {
        flash_origin: flash_origin_v,
        ram_origin: ram_origin_v,
        linear_memory_size,
        stack_size,
    });
    let linker_path = outdir.join("linker.ld");
    std::fs::write(&linker_path, linker.generate())
        .context(format!("failed to write {}", linker_path.display()))?;

    println!("Wrote {}", startup_path.display());
    println!("Wrote {}", linker_path.display());
    println!();
    let march = if matches!(target.as_str(), "rv32imac" | "rv32imc") {
        "rv32imac"
    } else {
        target.as_str()
    };
    println!("Link your synth-compiled .o with:");
    println!(
        "  riscv64-unknown-elf-gcc -nostartfiles -nostdlib -mabi=ilp32 -march={} \\",
        march
    );
    println!(
        "    -T {} -o firmware.elf {} <synth.o>",
        linker_path.display(),
        startup_path.display()
    );

    Ok(())
}

#[cfg(not(feature = "riscv"))]
#[allow(clippy::too_many_arguments)]
fn riscv_runtime_command(
    _outdir: PathBuf,
    _target: String,
    _flash_origin: String,
    _ram_origin: String,
    _linear_memory_size: u64,
    _stack_size: u64,
    _enable_fpu: bool,
) -> Result<()> {
    anyhow::bail!("RISC-V backend was not compiled in (rebuild with --features riscv)")
}

fn parse_command(input: PathBuf, output: Option<PathBuf>) -> Result<()> {
    info!("Parsing WebAssembly component: {}", input.display());

    // Parse the component
    let component =
        synth_frontend::parse_component_file(&input).context("Failed to parse component")?;

    // Validate the component
    synth_frontend::validate_component(&component).context("Component validation failed")?;

    info!("Component parsed successfully");
    info!("  Name: {}", component.name);
    info!("  Modules: {}", component.modules.len());
    info!("  Total memories: {}", component.total_memories());
    info!(
        "  Total memory size: {} bytes",
        component.total_memory_size()
    );

    // Output JSON if requested
    if let Some(output_path) = output {
        let json =
            serde_json::to_string_pretty(&component).context("Failed to serialize component")?;
        std::fs::write(&output_path, json).context(format!(
            "Failed to write output to {}",
            output_path.display()
        ))?;
        info!("Component JSON written to: {}", output_path.display());
    }

    Ok(())
}

fn synthesize_command(
    input: PathBuf,
    output: PathBuf,
    target: String,
    hardware: String,
    opt_level: String,
    xip: bool,
    verify: bool,
) -> Result<()> {
    info!("Synthesizing WebAssembly component: {}", input.display());
    info!("  Target: {}", target);
    info!("  Hardware: {}", hardware);
    info!("  Optimization level: {}", opt_level);
    info!("  XIP: {}", xip);
    info!("  Verification: {}", verify);

    // Parse the component
    let component =
        synth_frontend::parse_component_file(&input).context("Failed to parse component")?;

    synth_frontend::validate_component(&component).context("Component validation failed")?;

    // Get hardware capabilities
    let hw_caps = match hardware.as_str() {
        "nrf52840" => HardwareCapabilities::nrf52840(),
        "stm32f407" => HardwareCapabilities::stm32f407(),
        "stm32h743" => HardwareCapabilities::stm32h743(),
        "imxrt1062" => HardwareCapabilities::imxrt1062(),
        _ => {
            anyhow::bail!(
                "Unsupported hardware: {}. Use nrf52840, stm32f407, stm32h743, imxrt1062",
                hardware
            );
        }
    };

    info!("Hardware capabilities:");
    info!("  MPU regions: {}", hw_caps.mpu_regions);
    info!("  FPU: {}", hw_caps.has_fpu);
    info!("  Flash: {} KB", hw_caps.flash_size / 1024);
    info!("  RAM: {} KB", hw_caps.ram_size / 1024);

    // For PoC, we'll implement the full synthesis pipeline later
    // For now, just report what would happen
    info!("Synthesis pipeline (PoC - not yet fully implemented):");
    info!("  1. Component parsing: ✓");
    info!("  2. Memory layout analysis: TODO");
    info!("  3. MPU region allocation: TODO");
    info!("  4. Optimization: TODO");
    info!("  5. Code generation: TODO");
    info!("  6. Binary emission: TODO");

    info!("Output would be written to: {}", output.display());

    Ok(())
}

fn target_info_command(target: String) -> Result<()> {
    info!("Target information for: {}", target);

    // Parse target and display info
    match target.as_str() {
        "nrf52840" => {
            let caps = HardwareCapabilities::nrf52840();
            print_hardware_info(&caps);
        }
        "stm32f407" => {
            let caps = HardwareCapabilities::stm32f407();
            print_hardware_info(&caps);
        }
        "stm32h743" => {
            let caps = HardwareCapabilities::stm32h743();
            print_hardware_info(&caps);
        }
        "imxrt1062" => {
            let caps = HardwareCapabilities::imxrt1062();
            print_hardware_info(&caps);
        }
        _ => {
            anyhow::bail!(
                "Unknown target: {}. Supported: nrf52840, stm32f407, stm32h743, imxrt1062",
                target
            );
        }
    }

    Ok(())
}

fn print_hardware_info(caps: &HardwareCapabilities) {
    println!("Hardware Capabilities:");
    println!("  Architecture: {:?}", caps.arch);
    println!("  MPU: {} (regions: {})", caps.has_mpu, caps.mpu_regions);
    println!("  FPU: {}", caps.has_fpu);
    if let Some(precision) = caps.fpu_precision {
        println!("    Precision: {:?}", precision);
    }
    println!("  SIMD: {}", caps.has_simd);
    if let Some(level) = caps.simd_level {
        println!("    Level: {:?}", level);
    }
    println!("  XIP capable: {}", caps.xip_capable);
    println!(
        "  Flash: {} KB ({} MB)",
        caps.flash_size / 1024,
        caps.flash_size / (1024 * 1024)
    );
    println!("  RAM: {} KB", caps.ram_size / 1024);
}

/// Compiled function for ELF building (name + code bytes + relocations)
struct ElfFunction {
    name: String,
    code: Vec<u8>,
    /// Relocations targeting external symbols (from import dispatch stubs)
    relocations: Vec<synth_core::backend::CodeRelocation>,
}

/// Resolve --target / --cortex-m into a TargetSpec
fn resolve_target_spec(target: Option<&str>, cortex_m: bool) -> Result<TargetSpec> {
    match target {
        Some(name) => TargetSpec::from_triple(name).map_err(|e| {
            anyhow::anyhow!(
                "{e}. Supported: cortex-m3, cortex-m4, cortex-m4f, cortex-m7, cortex-m7dp"
            )
        }),
        None if cortex_m => Ok(TargetSpec::cortex_m3()),
        None => {
            // Default: Arm32 ISA (non-Cortex-M, no vector table)
            Ok(TargetSpec {
                isa: synth_core::target::IsaVariant::Arm32,
                ..TargetSpec::cortex_m4()
            })
        }
    }
}

/// Build the backend registry with all available backends
fn build_backend_registry() -> BackendRegistry {
    let mut registry = BackendRegistry::new();

    // Always register the built-in ARM backend
    registry.register(Box::new(ArmBackend::new()));

    // Register w2c2 backend (always available, checks tool at runtime)
    registry.register(Box::new(W2C2Backend::new()));

    // Register aWsm backend if compiled with feature
    #[cfg(feature = "awsm")]
    registry.register(Box::new(synth_backend_awsm::AwsmBackend::new()));

    // Register wasker backend if compiled with feature
    #[cfg(feature = "wasker")]
    registry.register(Box::new(synth_backend_wasker::WaskerBackend::new()));

    // Register RISC-V backend if compiled with feature
    #[cfg(feature = "riscv")]
    registry.register(Box::new(synth_backend_riscv::RiscVBackend::new()));

    registry
}

/// Run the Loom WASM optimizer on a WASM module if enabled.
///
/// Pipeline: raw WASM bytes -> loom optimize -> optimized WASM bytes
///
/// Loom is PulseEngine's WASM-level optimizer (https://github.com/pulseengine/loom).
/// It applies constant folding, strength reduction, and dead code elimination
/// at the WASM level with optional Z3 verification of semantic equivalence.
///
/// ## Integration status
///
/// The `--loom` flag and integration points are wired up. When the `loom` crate
/// is published, enable the dependency in workspace Cargo.toml and synth-cli
/// Cargo.toml (see commented-out lines), then uncomment the `#[cfg(feature = "loom")]`
/// block below.
///
/// ## Expected loom API
///
/// ```ignore
/// // loom-opt crate expected API:
/// pub fn optimize(wasm_bytes: &[u8]) -> Result<Vec<u8>>;
/// ```
fn maybe_run_loom(enabled: bool, wasm_bytes: Vec<u8>) -> Result<Vec<u8>> {
    if !enabled {
        return Ok(wasm_bytes);
    }

    // === Loom integration point ===
    //
    // When the loom crate is available, uncomment the feature-gated block below
    // and the corresponding dependency lines in:
    //   - Cargo.toml (workspace): loom-opt = { git = "..." }
    //   - crates/synth-cli/Cargo.toml: loom = ["dep:loom-opt"], loom-opt = { workspace = true, optional = true }
    //
    // Then compile with: cargo build --features loom
    //
    // #[cfg(feature = "loom")]
    // {
    //     info!("Running Loom WASM optimizer...");
    //     let input_len = wasm_bytes.len();
    //     let optimized = loom_opt::optimize(&wasm_bytes)
    //         .context("Loom optimization failed")?;
    //     let savings = if input_len > 0 {
    //         let reduced = input_len.saturating_sub(optimized.len());
    //         (reduced as f64 / input_len as f64) * 100.0
    //     } else {
    //         0.0
    //     };
    //     info!(
    //         "Loom: {} bytes -> {} bytes ({:.1}% reduction)",
    //         input_len, optimized.len(), savings,
    //     );
    //     return Ok(optimized);
    // }

    anyhow::bail!(
        "--loom is not yet available. The loom WASM optimizer integration is pending.\n\
         See https://github.com/pulseengine/loom for status.\n\n\
         In the meantime, use --loom-compat to skip synth passes that overlap\n\
         with loom's optimizations (constant folding, strength reduction)."
    );
}

/// Reconcile `--safety-bounds` and the legacy `--bounds-check` flag. Prints a
/// one-line deprecation notice when the legacy flag is used. Phase 1 of
/// `docs/binary-safety-design.md` §2 (CLI surface).
fn resolve_safety_bounds(
    safety_bounds: Option<&str>,
    legacy_bounds_check: bool,
) -> Result<SafetyBounds> {
    if let Some(v) = safety_bounds {
        let parsed = SafetyBounds::parse(v).map_err(|e| anyhow::anyhow!(e))?;
        if legacy_bounds_check {
            eprintln!(
                "warning: --bounds-check is deprecated; --safety-bounds={} takes precedence",
                parsed.as_str()
            );
        }
        return Ok(parsed);
    }
    if legacy_bounds_check {
        eprintln!("warning: --bounds-check is deprecated; use --safety-bounds=software instead");
        return Ok(SafetyBounds::Software);
    }
    Ok(SafetyBounds::None)
}

/// Emit the `safety-manifest.json` sidecar when any safety knob is active.
/// Phase 1 only records bounds + division traps; later phases will extend
/// the schema. Silently no-ops when `safety_bounds == None` (the default,
/// for back-compat with callers that don't opt in).
fn maybe_emit_safety_manifest(
    elf_path: &std::path::Path,
    target_spec: &TargetSpec,
    safety_bounds: SafetyBounds,
    linear_memory_bytes: u32,
) -> Result<()> {
    if safety_bounds == SafetyBounds::None {
        return Ok(());
    }
    let manifest = SafetyManifest {
        synth_version: env!("CARGO_PKG_VERSION").to_string(),
        target_triple: target_spec.triple.clone(),
        safety_bounds,
        // Phase 1: div-by-zero and signed-div-overflow are always enabled
        // for WASM-compliant output on both backends. The columns will gain
        // independent knobs in Phase 2 when `--safety-div` / `--safety-div-overflow`
        // CLI flags land.
        safety_div_zero: true,
        safety_div_overflow: true,
        linear_memory_bytes,
    };
    let sidecar = SafetyManifest::sidecar_path(elf_path);
    let json = manifest.to_json();
    std::fs::write(&sidecar, json)
        .with_context(|| format!("Failed to write safety manifest: {}", sidecar.display()))?;
    info!("Wrote safety manifest: {}", sidecar.display());
    Ok(())
}

/// Resolve the `--sbom` flag into a concrete destination path (or `None`).
///
/// clap substitutes [`SBOM_DEFAULT_SENTINEL`] when the flag is given with no
/// value, so:
/// - flag absent            -> `None`              (no SBOM)
/// - bare `--sbom`          -> `Some(<sentinel>)`   -> `<output>.cdx.json`
/// - `--sbom path.cdx.json` -> `Some("path...")`    -> that path verbatim
fn resolve_sbom_path(sbom: Option<PathBuf>, output: &std::path::Path) -> Option<PathBuf> {
    match sbom {
        None => None,
        Some(p) if p.as_os_str() == SBOM_DEFAULT_SENTINEL => {
            Some(synth_core::CycloneDxSbom::sidecar_path(output))
        }
        Some(p) => Some(p),
    }
}

/// Emit a CycloneDX 1.5 SBOM next to the compiled ELF when `--sbom` was
/// requested. The SBOM documents the synth compiler, the input WASM module
/// (hash + size), the output ELF (hash + size + target + backend), and the
/// WASM module's imports as a CycloneDX dependency graph. It is the artifact
/// consumed by rivet #107's `sbom-record` (`rivet import --format cyclonedx`).
///
/// `input_wasm_bytes` is the post-WAT-decode WASM (the bytes synth actually
/// compiled). When the input was a built-in demo (no file), `input_path` is a
/// synthetic name.
fn emit_sbom(
    sbom_path: &std::path::Path,
    input_path: &std::path::Path,
    input_wasm_bytes: &[u8],
    output_path: &std::path::Path,
    output_elf_bytes: &[u8],
    target_spec: &TargetSpec,
    backend_name: &str,
    imports: &[ImportEntry],
) -> Result<()> {
    let inputs = synth_core::SbomInputs {
        synth_version: env!("CARGO_PKG_VERSION"),
        input_path,
        input_bytes: input_wasm_bytes,
        output_path,
        output_bytes: output_elf_bytes,
        target_triple: &target_spec.triple,
        backend: backend_name,
        imports,
    };
    let sbom = synth_core::CycloneDxSbom::new(&inputs, synth_core::sbom::now_rfc3339());
    std::fs::write(sbom_path, sbom.to_json())
        .with_context(|| format!("Failed to write SBOM: {}", sbom_path.display()))?;
    info!(
        "Wrote CycloneDX SBOM ({} components): {}",
        sbom.components.len(),
        sbom_path.display()
    );
    Ok(())
}

#[allow(clippy::too_many_arguments)]
fn compile_command(
    input: Option<PathBuf>,
    output: PathBuf,
    demo: Option<String>,
    func_index: Option<u32>,
    func_name_arg: Option<String>,
    all_exports: bool,
    cortex_m: bool,
    no_optimize: bool,
    loom_compat: bool,
    loom: bool,
    safety_bounds: SafetyBounds,
    backend_name: &str,
    verify: bool,
    target_spec: &TargetSpec,
    relocatable: bool,
    sbom_path: Option<PathBuf>,
    sign_output: bool,
) -> Result<()> {
    // Validate backend exists
    let registry = build_backend_registry();
    let backend = registry.get(backend_name).ok_or_else(|| {
        let available: Vec<_> = registry
            .list()
            .iter()
            .map(|b| b.name().to_string())
            .collect();
        anyhow::anyhow!(
            "Unknown backend '{}'. Available: {}",
            backend_name,
            available.join(", ")
        )
    })?;

    if !backend.is_available() {
        anyhow::bail!(
            "Backend '{}' is not available (external tool not installed)",
            backend_name
        );
    }

    info!("Using backend: {}", backend.name());

    // Default to multi-function compilation when the user provides a file
    // but doesn't specify --func-index or --func-name.
    let use_all_exports =
        all_exports || (input.is_some() && func_index.is_none() && func_name_arg.is_none());

    if use_all_exports {
        return compile_all_exports(
            input,
            output,
            cortex_m,
            no_optimize,
            loom_compat,
            loom,
            safety_bounds,
            backend,
            verify,
            target_spec,
            relocatable,
            sbom_path,
            sign_output,
        );
    }

    // Single function compilation (when --func-index or --func-name is specified)
    let func_index = func_index.unwrap_or(0);
    // Captured for SBOM emission: the WASM bytes synth actually compiled and
    // the module's imports. `None` for the demo path (no input module).
    let mut sbom_wasm_bytes: Option<Vec<u8>> = None;
    let mut sbom_imports: Vec<ImportEntry> = Vec::new();
    let (wasm_ops, func_name): (Vec<WasmOp>, String) = match (&input, &demo) {
        (Some(path), _) => {
            info!("Compiling WASM file: {}", path.display());

            let file_bytes = std::fs::read(path)
                .context(format!("Failed to read input file: {}", path.display()))?;

            let wasm_bytes = if path.extension().is_some_and(|ext| ext == "wast") {
                info!("Parsing WAST to WASM (extracting module)...");
                let contents =
                    String::from_utf8(file_bytes).context("WAST file is not valid UTF-8")?;
                extract_module_from_wast(&contents)?
            } else if path.extension().is_some_and(|ext| ext == "wat") {
                info!("Parsing WAT to WASM...");
                wat::parse_bytes(&file_bytes)
                    .context("Failed to parse WAT file")?
                    .into_owned()
            } else {
                file_bytes
            };

            // Run Loom WASM optimizer if --loom is enabled
            let wasm_bytes = maybe_run_loom(loom, wasm_bytes)?;

            // Capture the WASM bytes + imports for the SBOM (the bytes synth
            // actually compiles, after WAT decode and any Loom pass).
            if sbom_path.is_some() {
                if let Ok(module) = decode_wasm_module(&wasm_bytes) {
                    sbom_imports = module.imports;
                }
                sbom_wasm_bytes = Some(wasm_bytes.clone());
            }

            let functions =
                decode_wasm_functions(&wasm_bytes).context("Failed to decode WASM functions")?;

            info!("Found {} functions in module", functions.len());

            for f in &functions {
                if let Some(ref name) = f.export_name {
                    info!("  Export '{}' -> function index {}", name, f.index);
                }
            }

            let func = if let Some(ref name) = func_name_arg {
                functions
                    .into_iter()
                    .find(|f| f.export_name.as_deref() == Some(name.as_str()))
                    .context(format!("Function '{}' not found", name))?
            } else {
                functions
                    .into_iter()
                    .find(|f| f.index == func_index)
                    .context(format!("Function index {} not found", func_index))?
            };

            let name = func
                .export_name
                .clone()
                .unwrap_or_else(|| format!("func_{}", func.index));
            info!("Compiling function {} ({} ops)", name, func.ops.len());

            (func.ops, name)
        }
        (None, Some(demo_name)) => {
            info!("Compiling demo function: {}", demo_name);

            match demo_name.as_str() {
                "add" => (
                    vec![WasmOp::LocalGet(0), WasmOp::LocalGet(1), WasmOp::I32Add],
                    "add".to_string(),
                ),
                "mul" => (
                    vec![WasmOp::LocalGet(0), WasmOp::LocalGet(1), WasmOp::I32Mul],
                    "mul".to_string(),
                ),
                "calc" => (
                    vec![
                        WasmOp::I32Const(5),
                        WasmOp::I32Const(3),
                        WasmOp::I32Mul,
                        WasmOp::I32Const(2),
                        WasmOp::I32Add,
                    ],
                    "calc".to_string(),
                ),
                _ => anyhow::bail!("Unknown demo: {}. Available: add, mul, calc", demo_name),
            }
        }
        (None, None) => {
            info!("No input specified, using 'add' demo");
            (
                vec![WasmOp::LocalGet(0), WasmOp::LocalGet(1), WasmOp::I32Add],
                "add".to_string(),
            )
        }
    };

    info!("WASM operations: {:?}", wasm_ops);

    // Build compile config from CLI flags
    let config = CompileConfig {
        no_optimize,
        loom_compat,
        safety_bounds,
        target: target_spec.clone(),
        ..CompileConfig::default()
    };

    // Compile via the selected backend
    let compiled = backend
        .compile_function(&func_name, &wasm_ops, &config)
        .map_err(|e| anyhow::anyhow!("Backend '{}' compilation failed: {}", backend.name(), e))?;
    let code = compiled.code;
    info!("Encoded {} bytes of machine code", code.len());

    let elf_data = if matches!(target_spec.family, synth_core::target::ArchFamily::RiscV) {
        build_riscv_elf(&code, &func_name)?
    } else if cortex_m {
        build_cortex_m_elf(&code, &func_name, target_spec)?
    } else {
        build_simple_elf(&code, &func_name)?
    };

    info!("Generated {} byte ELF file", elf_data.len());

    // Step 4: Write to file
    let mut file = File::create(&output).context(format!(
        "Failed to create output file: {}",
        output.display()
    ))?;
    file.write_all(&elf_data)
        .context("Failed to write ELF data")?;

    // Phase 1: write the safety-manifest sidecar whenever any safety knob
    // is active. Single-function path uses 0 for linear-memory-bytes because
    // the WASM was supplied as a raw function-body slice — `compile_all_exports`
    // has the module context and threads through the real value.
    maybe_emit_safety_manifest(&output, target_spec, safety_bounds, 0)?;

    // Emit a CycloneDX SBOM when requested. Only possible when synth compiled
    // an actual WASM module (not a built-in demo, which has no input file).
    if let Some(ref sbom_dest) = sbom_path {
        match (sbom_wasm_bytes.as_deref(), input.as_deref()) {
            (Some(wasm), Some(in_path)) => {
                emit_sbom(
                    sbom_dest,
                    in_path,
                    wasm,
                    &output,
                    &elf_data,
                    target_spec,
                    backend_name,
                    &sbom_imports,
                )?;
            }
            _ => {
                eprintln!(
                    "warning: --sbom requires a WASM/WAT input file; \
                     skipping SBOM for demo compilation"
                );
            }
        }
    }

    // Phase 5: sign the ELF via sigil's `wsc sign --keyless --format elf`.
    // Done last so the SBOM (if any) records the hash of the unsigned synth
    // output; the on-disk ELF after this step is the signed version. See
    // docs/sigil-integration.md.
    if sign_output {
        sign::sign_elf(&output)?;
    }

    println!("Compiled {} to {}", func_name, output.display());
    println!("  Code size: {} bytes", code.len());
    println!("  ELF size: {} bytes", elf_data.len());
    println!("\nInspect with: synth disasm {}", output.display());

    // Run translation validation if requested
    if verify {
        let caps = backend.capabilities();
        if caps.supports_rule_verification {
            #[cfg(feature = "verify")]
            {
                run_verification(&wasm_ops, &func_name)?;
            }
            #[cfg(not(feature = "verify"))]
            {
                println!("\nVerification requested but z3-solver not available.");
                println!("Rebuild with: cargo build --features verify");
            }
        } else {
            println!(
                "\nBackend '{}' does not support rule verification.",
                backend.name()
            );
            if caps.supports_binary_verification {
                println!("Binary-level translation validation is planned but not yet implemented.");
            }
        }
    }

    Ok(())
}

/// Run per-rule translation validation using Z3 SMT solver
#[cfg(feature = "verify")]
fn run_verification(wasm_ops: &[WasmOp], func_name: &str) -> Result<()> {
    use std::collections::HashSet;
    use synth_synthesis::{ArmOp, Condition, Operand2, Pattern, Reg, Replacement, SynthesisRule};

    println!("\nRunning translation validation for '{}'...", func_name);

    // Build verification rules for the instruction selection mappings actually used.
    // These correspond to the basic WasmOp → ArmOp translations in the instruction selector.
    let mut rules = Vec::new();
    let mut seen = HashSet::new();

    for op in wasm_ops {
        let disc = std::mem::discriminant(op);
        if !seen.insert(disc) {
            continue; // already added a rule for this op kind
        }

        let rule = match op {
            WasmOp::I32Add => Some(SynthesisRule {
                name: "i32.add → ADD".into(),
                priority: 0,
                pattern: Pattern::WasmInstr(WasmOp::I32Add),
                replacement: Replacement::ArmInstr(ArmOp::Add {
                    rd: Reg::R0,
                    rn: Reg::R0,
                    op2: Operand2::Reg(Reg::R1),
                }),
                cost: synth_synthesis::Cost {
                    cycles: 1,
                    code_size: 2,
                    registers: 2,
                },
            }),
            WasmOp::I32Sub => Some(SynthesisRule {
                name: "i32.sub → SUB".into(),
                priority: 0,
                pattern: Pattern::WasmInstr(WasmOp::I32Sub),
                replacement: Replacement::ArmInstr(ArmOp::Sub {
                    rd: Reg::R0,
                    rn: Reg::R0,
                    op2: Operand2::Reg(Reg::R1),
                }),
                cost: synth_synthesis::Cost {
                    cycles: 1,
                    code_size: 2,
                    registers: 2,
                },
            }),
            WasmOp::I32Mul => Some(SynthesisRule {
                name: "i32.mul → MUL".into(),
                priority: 0,
                pattern: Pattern::WasmInstr(WasmOp::I32Mul),
                replacement: Replacement::ArmInstr(ArmOp::Mul {
                    rd: Reg::R0,
                    rn: Reg::R0,
                    rm: Reg::R1,
                }),
                cost: synth_synthesis::Cost {
                    cycles: 1,
                    code_size: 2,
                    registers: 2,
                },
            }),
            WasmOp::I32And => Some(SynthesisRule {
                name: "i32.and → AND".into(),
                priority: 0,
                pattern: Pattern::WasmInstr(WasmOp::I32And),
                replacement: Replacement::ArmInstr(ArmOp::And {
                    rd: Reg::R0,
                    rn: Reg::R0,
                    op2: Operand2::Reg(Reg::R1),
                }),
                cost: synth_synthesis::Cost {
                    cycles: 1,
                    code_size: 2,
                    registers: 2,
                },
            }),
            WasmOp::I32Or => Some(SynthesisRule {
                name: "i32.or → ORR".into(),
                priority: 0,
                pattern: Pattern::WasmInstr(WasmOp::I32Or),
                replacement: Replacement::ArmInstr(ArmOp::Orr {
                    rd: Reg::R0,
                    rn: Reg::R0,
                    op2: Operand2::Reg(Reg::R1),
                }),
                cost: synth_synthesis::Cost {
                    cycles: 1,
                    code_size: 2,
                    registers: 2,
                },
            }),
            WasmOp::I32Xor => Some(SynthesisRule {
                name: "i32.xor → EOR".into(),
                priority: 0,
                pattern: Pattern::WasmInstr(WasmOp::I32Xor),
                replacement: Replacement::ArmInstr(ArmOp::Eor {
                    rd: Reg::R0,
                    rn: Reg::R0,
                    op2: Operand2::Reg(Reg::R1),
                }),
                cost: synth_synthesis::Cost {
                    cycles: 1,
                    code_size: 2,
                    registers: 2,
                },
            }),
            // Comparison ops: CMP + SetCond sequence (two ARM instructions per WASM op)
            WasmOp::I32Eq => Some(SynthesisRule {
                name: "i32.eq → CMP + SetCond(EQ)".into(),
                priority: 0,
                pattern: Pattern::WasmInstr(WasmOp::I32Eq),
                replacement: Replacement::ArmSequence(vec![
                    ArmOp::Cmp {
                        rn: Reg::R0,
                        op2: Operand2::Reg(Reg::R1),
                    },
                    ArmOp::SetCond {
                        rd: Reg::R0,
                        cond: Condition::EQ,
                    },
                ]),
                cost: synth_synthesis::Cost {
                    cycles: 2,
                    code_size: 4,
                    registers: 2,
                },
            }),
            WasmOp::I32Ne => Some(SynthesisRule {
                name: "i32.ne → CMP + SetCond(NE)".into(),
                priority: 0,
                pattern: Pattern::WasmInstr(WasmOp::I32Ne),
                replacement: Replacement::ArmSequence(vec![
                    ArmOp::Cmp {
                        rn: Reg::R0,
                        op2: Operand2::Reg(Reg::R1),
                    },
                    ArmOp::SetCond {
                        rd: Reg::R0,
                        cond: Condition::NE,
                    },
                ]),
                cost: synth_synthesis::Cost {
                    cycles: 2,
                    code_size: 4,
                    registers: 2,
                },
            }),
            WasmOp::I32LtS => Some(SynthesisRule {
                name: "i32.lt_s → CMP + SetCond(LT)".into(),
                priority: 0,
                pattern: Pattern::WasmInstr(WasmOp::I32LtS),
                replacement: Replacement::ArmSequence(vec![
                    ArmOp::Cmp {
                        rn: Reg::R0,
                        op2: Operand2::Reg(Reg::R1),
                    },
                    ArmOp::SetCond {
                        rd: Reg::R0,
                        cond: Condition::LT,
                    },
                ]),
                cost: synth_synthesis::Cost {
                    cycles: 2,
                    code_size: 4,
                    registers: 2,
                },
            }),
            WasmOp::I32LeS => Some(SynthesisRule {
                name: "i32.le_s → CMP + SetCond(LE)".into(),
                priority: 0,
                pattern: Pattern::WasmInstr(WasmOp::I32LeS),
                replacement: Replacement::ArmSequence(vec![
                    ArmOp::Cmp {
                        rn: Reg::R0,
                        op2: Operand2::Reg(Reg::R1),
                    },
                    ArmOp::SetCond {
                        rd: Reg::R0,
                        cond: Condition::LE,
                    },
                ]),
                cost: synth_synthesis::Cost {
                    cycles: 2,
                    code_size: 4,
                    registers: 2,
                },
            }),
            WasmOp::I32GtS => Some(SynthesisRule {
                name: "i32.gt_s → CMP + SetCond(GT)".into(),
                priority: 0,
                pattern: Pattern::WasmInstr(WasmOp::I32GtS),
                replacement: Replacement::ArmSequence(vec![
                    ArmOp::Cmp {
                        rn: Reg::R0,
                        op2: Operand2::Reg(Reg::R1),
                    },
                    ArmOp::SetCond {
                        rd: Reg::R0,
                        cond: Condition::GT,
                    },
                ]),
                cost: synth_synthesis::Cost {
                    cycles: 2,
                    code_size: 4,
                    registers: 2,
                },
            }),
            WasmOp::I32GeS => Some(SynthesisRule {
                name: "i32.ge_s → CMP + SetCond(GE)".into(),
                priority: 0,
                pattern: Pattern::WasmInstr(WasmOp::I32GeS),
                replacement: Replacement::ArmSequence(vec![
                    ArmOp::Cmp {
                        rn: Reg::R0,
                        op2: Operand2::Reg(Reg::R1),
                    },
                    ArmOp::SetCond {
                        rd: Reg::R0,
                        cond: Condition::GE,
                    },
                ]),
                cost: synth_synthesis::Cost {
                    cycles: 2,
                    code_size: 4,
                    registers: 2,
                },
            }),
            WasmOp::I32LtU => Some(SynthesisRule {
                name: "i32.lt_u → CMP + SetCond(LO)".into(),
                priority: 0,
                pattern: Pattern::WasmInstr(WasmOp::I32LtU),
                replacement: Replacement::ArmSequence(vec![
                    ArmOp::Cmp {
                        rn: Reg::R0,
                        op2: Operand2::Reg(Reg::R1),
                    },
                    ArmOp::SetCond {
                        rd: Reg::R0,
                        cond: Condition::LO,
                    },
                ]),
                cost: synth_synthesis::Cost {
                    cycles: 2,
                    code_size: 4,
                    registers: 2,
                },
            }),
            WasmOp::I32LeU => Some(SynthesisRule {
                name: "i32.le_u → CMP + SetCond(LS)".into(),
                priority: 0,
                pattern: Pattern::WasmInstr(WasmOp::I32LeU),
                replacement: Replacement::ArmSequence(vec![
                    ArmOp::Cmp {
                        rn: Reg::R0,
                        op2: Operand2::Reg(Reg::R1),
                    },
                    ArmOp::SetCond {
                        rd: Reg::R0,
                        cond: Condition::LS,
                    },
                ]),
                cost: synth_synthesis::Cost {
                    cycles: 2,
                    code_size: 4,
                    registers: 2,
                },
            }),
            WasmOp::I32GtU => Some(SynthesisRule {
                name: "i32.gt_u → CMP + SetCond(HI)".into(),
                priority: 0,
                pattern: Pattern::WasmInstr(WasmOp::I32GtU),
                replacement: Replacement::ArmSequence(vec![
                    ArmOp::Cmp {
                        rn: Reg::R0,
                        op2: Operand2::Reg(Reg::R1),
                    },
                    ArmOp::SetCond {
                        rd: Reg::R0,
                        cond: Condition::HI,
                    },
                ]),
                cost: synth_synthesis::Cost {
                    cycles: 2,
                    code_size: 4,
                    registers: 2,
                },
            }),
            WasmOp::I32GeU => Some(SynthesisRule {
                name: "i32.ge_u → CMP + SetCond(HS)".into(),
                priority: 0,
                pattern: Pattern::WasmInstr(WasmOp::I32GeU),
                replacement: Replacement::ArmSequence(vec![
                    ArmOp::Cmp {
                        rn: Reg::R0,
                        op2: Operand2::Reg(Reg::R1),
                    },
                    ArmOp::SetCond {
                        rd: Reg::R0,
                        cond: Condition::HS,
                    },
                ]),
                cost: synth_synthesis::Cost {
                    cycles: 2,
                    code_size: 4,
                    registers: 2,
                },
            }),
            // i32.eqz: unary comparison against zero
            WasmOp::I32Eqz => Some(SynthesisRule {
                name: "i32.eqz → CMP #0 + SetCond(EQ)".into(),
                priority: 0,
                pattern: Pattern::WasmInstr(WasmOp::I32Eqz),
                replacement: Replacement::ArmSequence(vec![
                    ArmOp::Cmp {
                        rn: Reg::R0,
                        op2: Operand2::Imm(0),
                    },
                    ArmOp::SetCond {
                        rd: Reg::R0,
                        cond: Condition::EQ,
                    },
                ]),
                cost: synth_synthesis::Cost {
                    cycles: 2,
                    code_size: 4,
                    registers: 1,
                },
            }),
            // Shift ops use immediate shift values in the instruction selector,
            // so SMT verification of the variable-shift case requires a different
            // ARM op encoding (register-based shift). Skipped for now.
            // LocalGet/LocalSet/Const are register operations, not computational — skip
            _ => None,
        };

        if let Some(r) = rule {
            rules.push(r);
        }
    }

    if rules.is_empty() {
        println!("  No verifiable computational rules for this function.");
        println!("  (LocalGet/Set/Const are register operations, not verified by SMT)");
        return Ok(());
    }

    println!("  Verifying {} instruction selection rules...", rules.len());

    let (verified, failed, unknown) = synth_verify::with_z3_context(|| {
        let validator = synth_verify::TranslationValidator::new();
        let mut verified = 0u32;
        let mut failed = 0u32;
        let mut unknown = 0u32;

        for rule in &rules {
            match validator.verify_rule(rule) {
                Ok(synth_verify::ValidationResult::Verified) => {
                    println!("  ✓ {} verified", rule.name);
                    verified += 1;
                }
                Ok(synth_verify::ValidationResult::Invalid { counterexample }) => {
                    println!("  ✗ {} INVALID: {:?}", rule.name, counterexample);
                    failed += 1;
                }
                Ok(synth_verify::ValidationResult::Unknown { reason }) => {
                    println!("  ? {} unknown: {}", rule.name, reason);
                    unknown += 1;
                }
                Err(e) => {
                    println!("  ! {} error: {}", rule.name, e);
                    unknown += 1;
                }
            }
        }

        (verified, failed, unknown)
    });

    println!(
        "\nVerification summary: {} verified, {} failed, {} unknown",
        verified, failed, unknown
    );

    if failed > 0 {
        anyhow::bail!(
            "Translation validation failed: {} rules produced counterexamples",
            failed
        );
    }

    Ok(())
}

/// Extract module binary from WAST file (handles assert_return, etc.)
/// Extract all modules from a WAST file, returning their binary representations.
///
/// Many spec test files contain multiple modules where exports live in later
/// modules, not the first one.  We collect every valid module so the caller
/// can merge exports across them.
fn extract_all_modules_from_wast(contents: &str) -> Result<Vec<Vec<u8>>> {
    let buf = ParseBuffer::new(contents)
        .map_err(|e| anyhow::anyhow!("Failed to create parse buffer: {}", e))?;

    let wast: Wast =
        parser::parse(&buf).map_err(|e| anyhow::anyhow!("Failed to parse WAST: {}", e))?;

    let mut modules = Vec::new();

    for directive in wast.directives {
        if let WastDirective::Module(mut quote_wat) = directive {
            match quote_wat.encode() {
                Ok(binary) => modules.push(binary),
                Err(e) => {
                    // Some modules in spec tests are intentionally invalid
                    // (e.g. modules used in assert_invalid). Skip them.
                    info!("Skipping unencoded module: {}", e);
                }
            }
        }
    }

    if modules.is_empty() {
        anyhow::bail!("No module found in WAST file");
    }

    Ok(modules)
}

/// Legacy helper: extract a single module from a WAST file.
/// Picks the first module that has exported functions; falls back to the first
/// module if none have exports.
fn extract_module_from_wast(contents: &str) -> Result<Vec<u8>> {
    let modules = extract_all_modules_from_wast(contents)?;

    // Prefer a module with exports
    for module_bytes in &modules {
        if let Ok(decoded) = decode_wasm_module(module_bytes)
            && decoded.functions.iter().any(|f| f.export_name.is_some())
        {
            return Ok(module_bytes.clone());
        }
    }

    // Fall back to first module (non-empty guaranteed by check above)
    modules
        .into_iter()
        .next()
        .ok_or_else(|| anyhow::anyhow!("no modules found in WAST file"))
}

/// Compile all exported functions into a multi-function ELF
#[allow(clippy::too_many_arguments)]
fn compile_all_exports(
    input: Option<PathBuf>,
    output: PathBuf,
    cortex_m: bool,
    no_optimize: bool,
    loom_compat: bool,
    loom: bool,
    safety_bounds: SafetyBounds,
    backend: &dyn Backend,
    verify: bool,
    target_spec: &TargetSpec,
    relocatable: bool,
    sbom_path: Option<PathBuf>,
    sign_output: bool,
) -> Result<()> {
    let path = input.context("--all-exports requires an input file")?;

    info!("Compiling all exports from: {}", path.display());

    let file_bytes =
        std::fs::read(&path).context(format!("Failed to read input file: {}", path.display()))?;

    // WASM bytes captured for the SBOM (the post-decode bytes synth compiles).
    // For a WAST file with multiple modules this holds the representative
    // module (the one whose imports were merged), set inside the match below.
    let mut sbom_wasm_bytes: Option<Vec<u8>> = None;

    // Decode module(s) — for WAST files we merge exports across all modules
    let (all_exports, all_memories, all_imports, max_num_imported_funcs) =
        if path.extension().is_some_and(|ext| ext == "wast") {
            info!("Parsing WAST (extracting all modules)...");
            let contents = String::from_utf8(file_bytes).context("WAST file is not valid UTF-8")?;
            let module_binaries = extract_all_modules_from_wast(&contents)?;
            info!("Found {} modules in WAST file", module_binaries.len());

            // Decode each module and collect exports.
            // Use an IndexMap-style approach: last module with a given export name wins
            // (matching WAST spec semantics where assertions test the most-recent module).
            let mut export_map: std::collections::HashMap<String, FunctionOps> =
                std::collections::HashMap::new();
            let mut merged_memories: Vec<WasmMemory> = Vec::new();
            let mut merged_imports: Vec<ImportEntry> = Vec::new();
            let mut max_imports: u32 = 0;

            for (idx, wasm_bytes) in module_binaries.iter().enumerate() {
                // Run Loom optimizer on each module if --loom is enabled
                let wasm_bytes = maybe_run_loom(loom, wasm_bytes.clone())?;
                // First decoded module is the SBOM default; refined below to
                // the module whose imports get merged.
                if sbom_wasm_bytes.is_none() {
                    sbom_wasm_bytes = Some(wasm_bytes.clone());
                }
                match decode_wasm_module(&wasm_bytes) {
                    Ok(module) => {
                        let export_count = module
                            .functions
                            .iter()
                            .filter(|f| f.export_name.is_some())
                            .count();
                        info!(
                            "  Module {}: {} functions ({} exports), {} memories",
                            idx,
                            module.functions.len(),
                            export_count,
                            module.memories.len()
                        );

                        for func in module.functions {
                            if let Some(name) = func.export_name.clone() {
                                export_map.insert(name, func);
                            }
                        }

                        // Take the largest memory across all modules
                        for mem in &module.memories {
                            if merged_memories.is_empty()
                                || mem.initial_pages
                                    > merged_memories
                                        .first()
                                        .map(|m| m.initial_pages)
                                        .unwrap_or(0)
                            {
                                merged_memories = vec![mem.clone()];
                            }
                        }

                        if module.num_imported_funcs > max_imports {
                            max_imports = module.num_imported_funcs;
                            merged_imports = module.imports.clone();
                            // Keep the SBOM input aligned with the merged
                            // imports (the module the dependency graph reflects).
                            sbom_wasm_bytes = Some(wasm_bytes.clone());
                        }
                    }
                    Err(e) => {
                        info!("  Module {}: decode failed ({}), skipping", idx, e);
                    }
                }
            }

            let exports: Vec<_> = export_map.into_values().collect();
            (exports, merged_memories, merged_imports, max_imports)
        } else {
            let wasm_bytes = if path.extension().is_some_and(|ext| ext == "wat") {
                info!("Parsing WAT to WASM...");
                wat::parse_bytes(&file_bytes)
                    .context("Failed to parse WAT file")?
                    .into_owned()
            } else {
                file_bytes
            };

            // Run Loom optimizer if --loom is enabled
            let wasm_bytes = maybe_run_loom(loom, wasm_bytes)?;

            let module = decode_wasm_module(&wasm_bytes).context("Failed to decode WASM module")?;
            sbom_wasm_bytes = Some(wasm_bytes);

            let exports: Vec<_> = module
                .functions
                .into_iter()
                .filter(|f| f.export_name.is_some())
                .collect();
            let memories = module.memories;
            let imports = module.imports;
            let num_imports = module.num_imported_funcs;
            (exports, memories, imports, num_imports)
        };

    // Log memory information
    if !all_memories.is_empty() {
        info!("Memories ({} total):", all_memories.len());
        for mem in &all_memories {
            let max_str = mem
                .max_pages
                .map(|m| format!("{}", m))
                .unwrap_or_else(|| "unlimited".to_string());
            info!(
                "  memory[{}]: {} initial pages, {} max pages ({}KB initial)",
                mem.index,
                mem.initial_pages,
                max_str,
                mem.initial_pages * 64
            );
        }
    }

    // Log import information
    if max_num_imported_funcs > 0 {
        info!(
            "Module imports {} functions (Meld dispatch enabled):",
            max_num_imported_funcs
        );
        for imp in &all_imports {
            if matches!(imp.kind, synth_core::ImportKind::Function(_)) {
                info!("  import[{}]: {}::{}", imp.index, imp.module, imp.name);
            }
        }
    }

    if all_exports.is_empty() {
        anyhow::bail!("No exported functions found in module");
    }

    info!("Found {} exported functions:", all_exports.len());
    for f in &all_exports {
        let display_name = f
            .export_name
            .as_deref()
            .map_or_else(|| format!("func_{}", f.index), String::from);
        info!("  '{}' (index {})", display_name, f.index);
    }

    // Build compile config from CLI flags
    let config = CompileConfig {
        no_optimize,
        loom_compat,
        safety_bounds,
        num_imports: max_num_imported_funcs,
        target: target_spec.clone(),
        ..CompileConfig::default()
    };

    // Compile each function via the selected backend
    let mut compiled_funcs = Vec::new();
    for func in &all_exports {
        let name = func.export_name.clone().ok_or_else(|| {
            anyhow::anyhow!("function at index {} has no export name", func.index)
        })?;
        info!(
            "Compiling function '{}' via backend '{}'...",
            name,
            backend.name()
        );

        let compiled = backend
            .compile_function(&name, &func.ops, &config)
            .map_err(|e| {
                anyhow::anyhow!("Backend '{}' failed on '{}': {}", backend.name(), name, e)
            })?;
        info!("  {} bytes of machine code", compiled.code.len());

        if !compiled.relocations.is_empty() {
            info!(
                "  {} relocations (external symbol references)",
                compiled.relocations.len()
            );
        }

        compiled_funcs.push(ElfFunction {
            name: name.clone(),
            code: compiled.code,
            relocations: compiled.relocations,
        });

        // Run verification if requested
        if verify {
            #[cfg(feature = "verify")]
            run_verification(&func.ops, &name)?;
            #[cfg(not(feature = "verify"))]
            {
                eprintln!("Warning: --verify requires the 'verify' feature.");
                eprintln!("  Rebuild with: cargo build --features verify");
            }
        }
    }

    // Check if any function has relocations (import calls)
    let has_relocations = compiled_funcs.iter().any(|f| !f.relocations.is_empty());

    // Build multi-function ELF
    // When there are relocations, produce a relocatable object (.o) instead of
    // an executable. This lets the output be linked with the Kiln bridge crate
    // (which provides __meld_dispatch_import and __meld_get_memory_base).
    // The --relocatable flag forces ET_REL output even when the wasm has no
    // imports, for linking into a host build system (e.g. Zephyr).
    let is_riscv = matches!(target_spec.family, synth_core::target::ArchFamily::RiscV);
    let elf_data = if is_riscv {
        info!("Building RISC-V multi-function relocatable object (EM_RISCV)");
        build_multi_func_riscv_elf(&compiled_funcs)?
    } else if has_relocations || relocatable {
        let total_relocs: usize = compiled_funcs.iter().map(|f| f.relocations.len()).sum();
        if has_relocations {
            info!(
                "Producing relocatable object (ET_REL): {} import call relocations",
                total_relocs
            );
        } else {
            info!("Producing relocatable object (ET_REL): forced by --relocatable");
        }
        build_relocatable_elf(&compiled_funcs, &all_imports)?
    } else if cortex_m {
        build_multi_func_cortex_m_elf(&compiled_funcs, &all_memories, target_spec)?
    } else {
        build_multi_func_simple_elf(&compiled_funcs)?
    };

    info!("Generated {} byte ELF file", elf_data.len());

    // Write to file
    let mut file = File::create(&output).context(format!(
        "Failed to create output file: {}",
        output.display()
    ))?;
    file.write_all(&elf_data)
        .context("Failed to write ELF data")?;

    // Phase 1: emit safety-manifest.json next to the ELF when any
    // safety knob is active.
    let linear_mem_bytes = all_memories.first().map(|m| m.initial_bytes()).unwrap_or(0);
    maybe_emit_safety_manifest(&output, target_spec, safety_bounds, linear_mem_bytes)?;

    // Emit a CycloneDX SBOM when requested.
    if let Some(ref sbom_dest) = sbom_path {
        let wasm = sbom_wasm_bytes.as_deref().unwrap_or(&[]);
        emit_sbom(
            sbom_dest,
            &path,
            wasm,
            &output,
            &elf_data,
            target_spec,
            backend.name(),
            &all_imports,
        )?;
    }

    // Phase 5: sign the multi-function ELF via sigil. `--all-exports` produces
    // a single multi-function ELF (all exports linked together), so one signing
    // call covers every exported function. See docs/sigil-integration.md.
    if sign_output {
        sign::sign_elf(&output)?;
    }

    let total_code: usize = compiled_funcs.iter().map(|f| f.code.len()).sum();
    let total_relocs: usize = compiled_funcs.iter().map(|f| f.relocations.len()).sum();
    println!(
        "Compiled {} functions to {}",
        compiled_funcs.len(),
        output.display()
    );
    println!("  Total code size: {} bytes", total_code);
    println!("  ELF size: {} bytes", elf_data.len());
    if has_relocations {
        println!(
            "  Relocations: {} (requires linking with Kiln bridge)",
            total_relocs
        );
        println!("  ELF type: relocatable object (ET_REL)");
        println!(
            "\n  Link with: arm-none-eabi-ld -o firmware.elf {} kiln_bridge.o",
            output.display()
        );
    }
    println!("\nFunction addresses:");

    // Calculate and display addresses (will be printed after ELF building sets them)
    println!(
        "  Use 'synth disasm {}' or 'objdump -t {}' to see symbols",
        output.display(),
        output.display()
    );

    Ok(())
}

/// Build a simple multi-function ELF
fn build_multi_func_simple_elf(funcs: &[ElfFunction]) -> Result<Vec<u8>> {
    let base_addr: u32 = 0x8000;
    let mut elf_builder = ElfBuilder::new_arm32().with_entry(base_addr);

    // Concatenate all function code
    let mut all_code = Vec::new();
    let mut func_offsets = Vec::new();

    for func in funcs {
        // Align each function to 4 bytes
        while all_code.len() % 4 != 0 {
            all_code.push(0);
        }
        func_offsets.push(all_code.len() as u32);
        all_code.extend_from_slice(&func.code);
    }

    let text_section = Section::new(".text", ElfSectionType::ProgBits)
        .with_flags(SectionFlags::ALLOC | SectionFlags::EXEC)
        .with_addr(base_addr)
        .with_align(4)
        .with_data(all_code);

    elf_builder.add_section(text_section);

    // Add symbol for each function
    for (i, func) in funcs.iter().enumerate() {
        let func_sym = Symbol::new(&func.name)
            .with_value(base_addr + func_offsets[i])
            .with_size(func.code.len() as u32)
            .with_binding(SymbolBinding::Global)
            .with_type(SymbolType::Func)
            .with_section(4);

        elf_builder.add_symbol(func_sym);
    }

    elf_builder.build().context("ELF generation failed")
}

/// Build a relocatable ELF object (.o) with undefined symbols and relocations.
///
/// Produced when the WASM module has imports — the resulting .o needs to be linked
/// with the Kiln bridge (which provides `__meld_dispatch_import` etc.) to create
/// a final firmware binary.
fn build_relocatable_elf(funcs: &[ElfFunction], imports: &[ImportEntry]) -> Result<Vec<u8>> {
    use std::collections::HashMap;

    let mut elf_builder = ElfBuilder::new_arm32()
        .with_entry(0)
        .with_type(ElfType::Rel); // ET_REL: relocatable object

    // Concatenate all function code into a single .text blob
    let mut all_code = Vec::new();
    let mut func_offsets = Vec::new();

    for func in funcs {
        // Align each function to 4 bytes
        while all_code.len() % 4 != 0 {
            all_code.push(0);
        }
        func_offsets.push(all_code.len() as u32);
        all_code.extend_from_slice(&func.code);
    }

    let text_section = Section::new(".text", ElfSectionType::ProgBits)
        .with_flags(SectionFlags::ALLOC | SectionFlags::EXEC)
        .with_addr(0) // Relocatable: addresses start at 0
        .with_align(4)
        .with_data(all_code);

    elf_builder.add_section(text_section);

    // Add defined symbols for each compiled function
    for (i, func) in funcs.iter().enumerate() {
        let func_sym = Symbol::new(&func.name)
            .with_value(func_offsets[i])
            .with_size(func.code.len() as u32)
            .with_binding(SymbolBinding::Global)
            .with_type(SymbolType::Func)
            .with_section(4); // .text is section 4 (null=0, shstrtab=1, strtab=2, symtab=3, .text=4)

        elf_builder.add_symbol(func_sym);
    }

    // Collect unique external symbol names from all relocations and add as undefined
    let mut extern_sym_indices: HashMap<String, u32> = HashMap::new();
    for func in funcs {
        for reloc in &func.relocations {
            if !extern_sym_indices.contains_key(&reloc.symbol) {
                let idx = elf_builder.add_undefined_symbol(&reloc.symbol);
                extern_sym_indices.insert(reloc.symbol.clone(), idx);
            }
        }
    }

    // Add R_ARM_CALL relocations for each BL to an external symbol
    for (i, func) in funcs.iter().enumerate() {
        let func_base = func_offsets[i];
        for reloc in &func.relocations {
            let sym_idx = extern_sym_indices[&reloc.symbol];
            elf_builder.add_relocation(Relocation {
                offset: func_base + reloc.offset,
                symbol_index: sym_idx,
                reloc_type: ArmRelocationType::Call, // R_ARM_CALL (28)
            });
        }
    }

    // Add a .meld_import_table section with import metadata
    // This is a custom section that the Kiln bridge can read to understand
    // which module::name each import index corresponds to.
    if !imports.is_empty() {
        let mut import_table_data = Vec::new();
        let mut import_func_count = 0u32;
        for imp in imports {
            if matches!(imp.kind, synth_core::ImportKind::Function(_)) {
                // Format: index(4) | module_len(2) | module | name_len(2) | name
                import_table_data.extend_from_slice(&imp.index.to_le_bytes());
                let mod_bytes = imp.module.as_bytes();
                import_table_data.extend_from_slice(&(mod_bytes.len() as u16).to_le_bytes());
                import_table_data.extend_from_slice(mod_bytes);
                let name_bytes = imp.name.as_bytes();
                import_table_data.extend_from_slice(&(name_bytes.len() as u16).to_le_bytes());
                import_table_data.extend_from_slice(name_bytes);
                import_func_count += 1;
            }
        }

        if !import_table_data.is_empty() {
            // Prepend the count
            let mut header = import_func_count.to_le_bytes().to_vec();
            header.extend_from_slice(&import_table_data);

            let import_section = Section::new(".meld_import_table", ElfSectionType::ProgBits)
                .with_flags(0) // Not ALLOC — metadata only
                .with_align(4)
                .with_data(header);

            elf_builder.add_section(import_section);
        }
    }

    info!(
        "Relocatable ELF: {} functions, {} external symbols, {} relocations",
        funcs.len(),
        extern_sym_indices.len(),
        funcs.iter().map(|f| f.relocations.len()).sum::<usize>()
    );

    elf_builder
        .build()
        .context("Relocatable ELF generation failed")
}

/// Build a complete Cortex-M multi-function ELF with vector table
fn build_multi_func_cortex_m_elf(
    funcs: &[ElfFunction],
    memories: &[WasmMemory],
    target: &TargetSpec,
) -> Result<Vec<u8>> {
    let flash_base: u32 = 0x0000_0000;
    let ram_base: u32 = 0x2000_0000;

    // Calculate linear memory size from WASM memory declarations
    // Default to 1 page (64KB) if no memory declared (for backwards compatibility)
    let linear_memory_pages = memories.first().map(|m| m.initial_pages).unwrap_or(1);
    let linear_memory_size = linear_memory_pages * 64 * 1024; // 64KB per page

    // RAM layout:
    // 0x2000_0000: Linear memory (R11 points here)
    // 0x2000_0000 + linear_memory_size: Stack base
    // ram_base + ram_size: Stack top (grows down)
    //
    // Auto-scale RAM: linear memory + 8KB stack, rounded up to next 64KB boundary.
    // Minimum 128KB for backwards compatibility.
    let min_stack_size: u32 = 8 * 1024;
    let needed = linear_memory_size + min_stack_size;
    let ram_size: u32 = std::cmp::max(128 * 1024, (needed + 0xFFFF) & !0xFFFF);

    let stack_top = ram_base + ram_size;

    info!(
        "RAM layout: linear memory {}KB at 0x{:08x}, stack at 0x{:08x}",
        linear_memory_size / 1024,
        ram_base,
        stack_top
    );

    // Flash layout:
    // 0x00: Vector table (128 bytes = 32 entries)
    // 0x80: Reset handler (startup code with R10/R11 init)
    // 0xA0: Default handler
    // 0xA4+: User functions (4-byte aligned)

    let vector_table_addr = flash_base;
    let vector_table_size: u32 = 128;

    let startup_addr = flash_base + vector_table_size;
    let startup_code = generate_minimal_startup(linear_memory_size);
    let startup_size = startup_code.len() as u32;

    let default_handler_addr = startup_addr + startup_size;
    let default_handler = generate_default_handler();
    let default_handler_size = default_handler.len() as u32;

    // Trap handler for WASM trap operations (div by zero, integer overflow)
    let trap_handler_addr = default_handler_addr + default_handler_size;
    let trap_handler = generate_trap_handler();
    let trap_handler_size = trap_handler.len() as u32;

    // Functions start after trap handler, aligned to 4 bytes
    let funcs_base = (trap_handler_addr + trap_handler_size + 3) & !3;

    // Concatenate all function code with alignment
    let mut all_func_code = Vec::new();
    let mut func_offsets = Vec::new();

    for func in funcs {
        while all_func_code.len() % 4 != 0 {
            all_func_code.push(0);
        }
        func_offsets.push(all_func_code.len() as u32);
        all_func_code.extend_from_slice(&func.code);
    }

    info!("Cortex-M multi-function layout:");
    info!("  Vector table: 0x{:08x}", vector_table_addr);
    info!("  Startup code: 0x{:08x}", startup_addr);
    info!("  Default handler: 0x{:08x}", default_handler_addr);
    info!("  Trap handler: 0x{:08x}", trap_handler_addr);
    info!("  Functions base: 0x{:08x}", funcs_base);
    for (i, func) in funcs.iter().enumerate() {
        let addr = funcs_base + func_offsets[i];
        info!(
            "    {}: 0x{:08x} ({} bytes)",
            func.name,
            addr,
            func.code.len()
        );
    }
    info!("  Stack top: 0x{:08x}", stack_top);

    // Generate vector table
    let mut vt = VectorTable::new_cortex_m(stack_top);
    vt.reset_handler = startup_addr;

    for handler in &mut vt.handlers {
        if handler.address == 0 {
            // UsageFault and HardFault go to Trap_Handler (for WASM trap detection)
            if handler.name == "UsageFault_Handler" || handler.name == "HardFault_Handler" {
                handler.address = trap_handler_addr;
            } else {
                handler.address = default_handler_addr;
            }
        }
    }

    let vector_table_data = vt
        .generate_binary()
        .context("Vector table generation failed")?;

    // Build flash image
    let mut flash_image = Vec::new();

    // Vector table
    flash_image.extend_from_slice(&vector_table_data);

    // Pad to startup address
    while flash_image.len() < (startup_addr - flash_base) as usize {
        flash_image.push(0);
    }

    // Startup code - patch literal pool to point to FIRST function
    // Literal pool is at offset 24 (after R10/R11 init + LDR/BLX/B/padding)
    let mut patched_startup = startup_code.clone();
    let first_func_addr = funcs_base | 1; // Thumb bit
    patched_startup[24..28].copy_from_slice(&first_func_addr.to_le_bytes());
    flash_image.extend_from_slice(&patched_startup);

    // Default handler
    flash_image.extend_from_slice(&default_handler);

    // Trap handler (for WASM trap operations)
    flash_image.extend_from_slice(&trap_handler);

    // Pad to functions base
    while flash_image.len() < (funcs_base - flash_base) as usize {
        flash_image.push(0);
    }

    // All function code
    flash_image.extend_from_slice(&all_func_code);

    // Build ELF
    let flash_size = flash_image.len() as u32;
    let mut elf_builder = ElfBuilder::new_arm32().with_entry(startup_addr | 1);

    // Set hard-float ABI flag if target has FPU
    if target.has_fpu() {
        elf_builder
            .set_flags(synth_backend::EF_ARM_EABI_VER5 | synth_backend::EF_ARM_ABI_FLOAT_HARD);
    }

    // Calculate proper file offset for .text section
    let shstrtab_size = 1 + ".shstrtab\0.strtab\0.symtab\0.text\0".len();
    let mut strtab_size = 1 + "Reset_Handler\0Default_Handler\0Trap_Handler\0".len();
    for func in funcs {
        strtab_size += func.name.len() + 1;
    }
    let text_file_offset = 52 + 32 + shstrtab_size + strtab_size;

    let text_phdr = ProgramHeader::load(
        flash_base,
        text_file_offset as u32,
        flash_size,
        ProgramFlags::READ | ProgramFlags::EXEC,
    );
    elf_builder.add_program_header(text_phdr);

    let text_section = Section::new(".text", ElfSectionType::ProgBits)
        .with_flags(SectionFlags::ALLOC | SectionFlags::EXEC)
        .with_addr(flash_base)
        .with_align(4)
        .with_data(flash_image);

    elf_builder.add_section(text_section);

    // Add linear memory section (BSS-like, no file data)
    // This section tells the loader about the RAM region for WASM linear memory
    if linear_memory_size > 0 {
        // Program header for linear memory (READ | WRITE, no EXEC)
        // Use load_nobits since there's no file data, just memory allocation
        let ram_phdr = ProgramHeader::load_nobits(
            ram_base,
            linear_memory_size,
            ProgramFlags::READ | ProgramFlags::WRITE,
        );
        elf_builder.add_program_header(ram_phdr);

        // NoBits section (like .bss) - no file data, just reserves address space
        let linear_memory_section = Section::new(".linear_memory", ElfSectionType::NoBits)
            .with_flags(SectionFlags::ALLOC | SectionFlags::WRITE)
            .with_addr(ram_base)
            .with_align(4)
            .with_size(linear_memory_size);

        elf_builder.add_section(linear_memory_section);

        // Add symbol for linear memory base (useful for debugging)
        let mem_sym = Symbol::new("__linear_memory_base")
            .with_value(ram_base)
            .with_size(linear_memory_size)
            .with_binding(SymbolBinding::Global)
            .with_type(SymbolType::Object)
            .with_section(5); // Section 5 will be .linear_memory after .text (section 4)
        elf_builder.add_symbol(mem_sym);

        info!(
            "Added .linear_memory section: 0x{:08x} ({} bytes, {} pages)",
            ram_base, linear_memory_size, linear_memory_pages
        );
    }

    // Add system symbols
    let reset_sym = Symbol::new("Reset_Handler")
        .with_value(startup_addr | 1)
        .with_size(startup_size)
        .with_binding(SymbolBinding::Global)
        .with_type(SymbolType::Func)
        .with_section(4);
    elf_builder.add_symbol(reset_sym);

    let default_sym = Symbol::new("Default_Handler")
        .with_value(default_handler_addr | 1)
        .with_size(default_handler_size)
        .with_binding(SymbolBinding::Global)
        .with_type(SymbolType::Func)
        .with_section(4);
    elf_builder.add_symbol(default_sym);

    let trap_sym = Symbol::new("Trap_Handler")
        .with_value(trap_handler_addr | 1)
        .with_size(trap_handler_size)
        .with_binding(SymbolBinding::Global)
        .with_type(SymbolType::Func)
        .with_section(4);
    elf_builder.add_symbol(trap_sym);

    // Add symbol for each user function
    for (i, func) in funcs.iter().enumerate() {
        let func_addr = funcs_base + func_offsets[i];
        let func_sym = Symbol::new(&func.name)
            .with_value(func_addr | 1) // Thumb bit for Cortex-M
            .with_size(func.code.len() as u32)
            .with_binding(SymbolBinding::Global)
            .with_type(SymbolType::Func)
            .with_section(4);
        elf_builder.add_symbol(func_sym);
    }

    elf_builder.build().context("ELF generation failed")
}

fn disasm_command(input: PathBuf) -> Result<()> {
    use std::process::Command;

    if !input.exists() {
        anyhow::bail!("File not found: {}", input.display());
    }

    info!("Disassembling: {}", input.display());

    // Try objdump with ARM triple (works on macOS with Apple LLVM)
    let output = Command::new("objdump")
        .args(["-d", "--triple=arm-none-eabi"])
        .arg(&input)
        .output()
        .context("Failed to run objdump. Is it installed?")?;

    if output.status.success() {
        print!("{}", String::from_utf8_lossy(&output.stdout));
    } else {
        // Fallback: try without triple
        let output = Command::new("objdump")
            .arg("-d")
            .arg(&input)
            .output()
            .context("Failed to run objdump")?;

        if output.status.success() {
            print!("{}", String::from_utf8_lossy(&output.stdout));
        } else {
            eprintln!("{}", String::from_utf8_lossy(&output.stderr));
            anyhow::bail!("objdump failed");
        }
    }

    Ok(())
}

fn backends_command() -> Result<()> {
    let registry = build_backend_registry();
    let backends = registry.list();

    println!("Available backends:\n");
    println!(
        "  {:<12} {:<12} {:<10} {:<10} {:<10}",
        "NAME", "STATUS", "ELF", "RULE-VERIFY", "BIN-VERIFY"
    );
    println!("  {}", "-".repeat(56));

    for backend in &backends {
        let status = if backend.is_available() {
            "available"
        } else {
            "not found"
        };
        let caps = backend.capabilities();
        println!(
            "  {:<12} {:<12} {:<10} {:<10} {:<10}",
            backend.name(),
            status,
            if caps.produces_elf { "yes" } else { "no" },
            if caps.supports_rule_verification {
                "yes"
            } else {
                "no"
            },
            if caps.supports_binary_verification {
                "yes"
            } else {
                "no"
            },
        );
    }

    println!("\nVerification tiers:");
    println!("  RULE-VERIFY: Per-rule SMT proofs (ASIL D) — only custom ARM backend");
    println!("  BIN-VERIFY:  Binary-level translation validation (ASIL B) — all backends");

    Ok(())
}

fn verify_command(wasm_input: PathBuf, elf_input: PathBuf, backend_name: &str) -> Result<()> {
    if !wasm_input.exists() {
        anyhow::bail!("WASM file not found: {}", wasm_input.display());
    }
    if !elf_input.exists() {
        anyhow::bail!("ELF file not found: {}", elf_input.display());
    }

    let registry = build_backend_registry();
    let backend = registry
        .get(backend_name)
        .ok_or_else(|| anyhow::anyhow!("Unknown backend '{}'", backend_name))?;

    let caps = backend.capabilities();

    println!("Translation validation:");
    println!("  Source: {}", wasm_input.display());
    println!("  Binary: {}", elf_input.display());
    println!("  Backend: {}", backend_name);

    if caps.supports_rule_verification {
        println!("  Strategy: Per-rule SMT verification (ASIL D path)");

        #[cfg(feature = "verify")]
        {
            // Parse WASM to extract function ops
            let file_bytes = std::fs::read(&wasm_input)
                .context(format!("Failed to read: {}", wasm_input.display()))?;

            let wasm_bytes = if wasm_input.extension().map_or(false, |ext| ext == "wat") {
                wat::parse_bytes(&file_bytes)
                    .context("Failed to parse WAT file")?
                    .into_owned()
            } else if wasm_input.extension().map_or(false, |ext| ext == "wast") {
                let contents =
                    String::from_utf8(file_bytes).context("WAST file is not valid UTF-8")?;
                extract_module_from_wast(&contents)?
            } else {
                file_bytes
            };

            let functions =
                decode_wasm_functions(&wasm_bytes).context("Failed to decode WASM functions")?;

            let exports: Vec<_> = functions
                .iter()
                .filter(|f| f.export_name.is_some())
                .collect();

            if exports.is_empty() {
                println!("\n  No exported functions found in WASM module.");
                return Ok(());
            }

            println!("\n  Verifying {} exported functions...", exports.len());

            for func in &exports {
                let name = func.export_name.as_deref().ok_or_else(|| {
                    anyhow::anyhow!("function at index {} has no export name", func.index)
                })?;
                run_verification(&func.ops, name)?;
            }

            println!("\nAll functions verified successfully.");
        }

        #[cfg(not(feature = "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)");
        println!("\n  Binary verification not yet implemented.");
        println!("  Requires: ARM disassembler + SMT equivalence checking on disassembled output.");
    } else {
        println!(
            "  No verification available for backend '{}'.",
            backend_name
        );
    }

    Ok(())
}

/// Build a RISC-V relocatable ELF wrapping the bytes the RV backend produced.
///
/// Re-runs the RISC-V backend's `RiscVElfBuilder` so the output is a real
/// RV32 object file (EM_RISCV, RVC e_flags) rather than the generic ARM
/// ELF that `build_simple_elf` emits.
#[cfg(feature = "riscv")]
fn build_riscv_elf(code: &[u8], func_name: &str) -> Result<Vec<u8>> {
    use synth_backend_riscv::{Reg, RiscVElfBuilder, RiscVElfFunction, RiscVOp};

    // The RISC-V ELF builder operates on `Vec<RiscVOp>` to support label
    // resolution. The CLI path doesn't have ops at this layer (only bytes),
    // so we wrap each 4-byte word as an opaque "raw" instruction by treating
    // the bytes as already encoded. We materialize them as `Addi`-shaped
    // sentinels and then post-process the ELF body to overwrite with our
    // actual code. Cleaner: use a future raw-bytes API on the builder.
    //
    // For the skeleton, the simpler path: wrap as one Addi per word — wrong
    // bits, but the ELF builder writes the section table correctly. We then
    // patch .text bytes back. This avoids leaking the encoder back through
    // the CLI and is fine until we drop ARM-style byte-handoff entirely.
    let n_instrs = code.len().div_ceil(4);
    let placeholder_ops: Vec<RiscVOp> = (0..n_instrs)
        .map(|_| RiscVOp::Addi {
            rd: Reg::ZERO,
            rs1: Reg::ZERO,
            imm: 0,
        })
        .collect();
    let f = RiscVElfFunction {
        name: func_name.to_string(),
        ops: placeholder_ops,
    };

    let builder = RiscVElfBuilder::new_relocatable();
    let mut elf = builder
        .build(&[f])
        .context("RISC-V ELF generation failed")?;

    // .text starts at offset 52 (ELF header). Overwrite the placeholder bytes
    // with the actual code we got from the backend.
    let text_offset = 52;
    if elf.len() < text_offset + code.len() {
        anyhow::bail!("RISC-V ELF is shorter than embedded code");
    }
    elf[text_offset..text_offset + code.len()].copy_from_slice(code);
    Ok(elf)
}

#[cfg(not(feature = "riscv"))]
fn build_riscv_elf(_code: &[u8], _func_name: &str) -> Result<Vec<u8>> {
    anyhow::bail!("RISC-V backend was not compiled in (rebuild with --features riscv)")
}

/// Build a multi-function RISC-V relocatable ELF.
#[cfg(feature = "riscv")]
fn build_multi_func_riscv_elf(funcs: &[ElfFunction]) -> Result<Vec<u8>> {
    use synth_backend_riscv::{Reg, RiscVElfBuilder, RiscVElfFunction, RiscVOp};

    // Same placeholder-then-overwrite approach as build_riscv_elf.
    // We accumulate a single .text spanning all functions and patch the
    // bytes back in after the ELF builder finishes layout.
    let mut all_code: Vec<u8> = Vec::new();
    let mut func_byte_ranges: Vec<(usize, usize)> = Vec::new();
    let mut placeholder_funcs: Vec<RiscVElfFunction> = Vec::new();

    for func in funcs {
        // Align each function to 4 bytes (RISC-V requires 4-byte instruction alignment).
        while !all_code.len().is_multiple_of(4) {
            all_code.push(0);
        }
        let start = all_code.len();
        all_code.extend_from_slice(&func.code);
        let end = all_code.len();
        func_byte_ranges.push((start, end));

        let n_instrs = (end - start).div_ceil(4);
        let placeholder_ops: Vec<RiscVOp> = (0..n_instrs)
            .map(|_| RiscVOp::Addi {
                rd: Reg::ZERO,
                rs1: Reg::ZERO,
                imm: 0,
            })
            .collect();
        placeholder_funcs.push(RiscVElfFunction {
            name: func.name.clone(),
            ops: placeholder_ops,
        });
    }

    let builder = RiscVElfBuilder::new_relocatable();
    let mut elf = builder
        .build(&placeholder_funcs)
        .context("RISC-V multi-function ELF generation failed")?;

    // .text starts immediately after the 52-byte ELF header.
    let text_offset = 52usize;
    if elf.len() < text_offset + all_code.len() {
        anyhow::bail!("RISC-V ELF too small to embed code");
    }
    elf[text_offset..text_offset + all_code.len()].copy_from_slice(&all_code);
    Ok(elf)
}

#[cfg(not(feature = "riscv"))]
fn build_multi_func_riscv_elf(_funcs: &[ElfFunction]) -> Result<Vec<u8>> {
    anyhow::bail!("RISC-V backend was not compiled in (rebuild with --features riscv)")
}

/// Build a simple ELF with just the code section (for quick testing)
fn build_simple_elf(code: &[u8], func_name: &str) -> Result<Vec<u8>> {
    let mut elf_builder = ElfBuilder::new_arm32().with_entry(0x8000);

    let text_section = Section::new(".text", ElfSectionType::ProgBits)
        .with_flags(SectionFlags::ALLOC | SectionFlags::EXEC)
        .with_addr(0x8000)
        .with_align(4)
        .with_data(code.to_vec());

    elf_builder.add_section(text_section);

    let func_sym = Symbol::new(func_name)
        .with_value(0x8000)
        .with_size(code.len() as u32)
        .with_binding(SymbolBinding::Global)
        .with_type(SymbolType::Func)
        .with_section(4);

    elf_builder.add_symbol(func_sym);

    elf_builder.build().context("ELF generation failed")
}

/// Build a complete Cortex-M ELF with vector table and startup code
fn build_cortex_m_elf(code: &[u8], func_name: &str, target: &TargetSpec) -> Result<Vec<u8>> {
    // Memory layout for generic Cortex-M (works with QEMU/Renode)
    let flash_base: u32 = 0x0000_0000;
    let ram_base: u32 = 0x2000_0000;
    let ram_size: u32 = 128 * 1024; // 128KB to accommodate linear memory + stack
    let stack_top = ram_base + ram_size;

    // Default linear memory size (1 WASM page = 64KB) for single-function mode
    let linear_memory_size: u32 = 64 * 1024;

    // Calculate addresses
    let vector_table_addr = flash_base;
    let vector_table_size: u32 = 128; // 32 entries * 4 bytes

    let startup_addr = flash_base + vector_table_size;
    let startup_code = generate_minimal_startup(linear_memory_size);
    let startup_size = startup_code.len() as u32;

    let default_handler_addr = startup_addr + startup_size;
    let default_handler = generate_default_handler();
    let default_handler_size = default_handler.len() as u32;

    // Trap handler for WASM trap operations
    let trap_handler_addr = default_handler_addr + default_handler_size;
    let trap_handler = generate_trap_handler();
    let trap_handler_size = trap_handler.len() as u32;

    // Align code to 4 bytes
    let code_addr = (trap_handler_addr + trap_handler_size + 3) & !3;

    info!("Cortex-M layout:");
    info!("  Vector table: 0x{:08x}", vector_table_addr);
    info!("  Startup code: 0x{:08x}", startup_addr);
    info!("  Default handler: 0x{:08x}", default_handler_addr);
    info!("  Trap handler: 0x{:08x}", trap_handler_addr);
    info!("  User code: 0x{:08x}", code_addr);
    info!("  Stack top: 0x{:08x}", stack_top);

    // Generate vector table
    let mut vt = VectorTable::new_cortex_m(stack_top);
    vt.reset_handler = startup_addr;

    // Set handlers - UsageFault/HardFault go to Trap_Handler for WASM trap detection
    for handler in &mut vt.handlers {
        if handler.address == 0 {
            if handler.name == "UsageFault_Handler" || handler.name == "HardFault_Handler" {
                handler.address = trap_handler_addr;
            } else {
                handler.address = default_handler_addr;
            }
        }
    }

    let vector_table_data = vt
        .generate_binary()
        .context("Vector table generation failed")?;

    // Build complete flash image
    let mut flash_image = Vec::new();

    // Vector table
    flash_image.extend_from_slice(&vector_table_data);

    // Pad to startup address
    while flash_image.len() < (startup_addr - flash_base) as usize {
        flash_image.push(0);
    }

    // Startup code (patch the literal pool with actual function address)
    // Literal pool is at offset 24 (after R10/R11 init + LDR/BLX/B/padding)
    let mut patched_startup = startup_code.clone();
    let func_addr_thumb = code_addr | 1; // Thumb bit
    patched_startup[24..28].copy_from_slice(&func_addr_thumb.to_le_bytes());
    flash_image.extend_from_slice(&patched_startup);

    // Default handler
    flash_image.extend_from_slice(&default_handler);

    // Trap handler
    flash_image.extend_from_slice(&trap_handler);

    // Pad to code address
    while flash_image.len() < (code_addr - flash_base) as usize {
        flash_image.push(0);
    }

    // User code
    flash_image.extend_from_slice(code);

    // Build ELF
    let flash_size = flash_image.len() as u32;
    let mut elf_builder = ElfBuilder::new_arm32().with_entry(startup_addr | 1); // Thumb bit

    // Set hard-float ABI flag if target has FPU
    if target.has_fpu() {
        elf_builder
            .set_flags(synth_backend::EF_ARM_EABI_VER5 | synth_backend::EF_ARM_ABI_FLOAT_HARD);
    }

    // Add LOAD program header for the .text section
    // The offset is calculated as: ELF header (52) + program headers (32 * 1) + string tables
    // String tables: .shstrtab (~33 bytes) + .strtab (~50 bytes)
    // This puts .text data at approximately offset 167, but we need exact calculation
    // For now, we'll compute based on the section name string table size
    let shstrtab_size = 1 + ".shstrtab\0.strtab\0.symtab\0.text\0".len(); // ~34 bytes
    let strtab_size =
        1 + "Reset_Handler\0Default_Handler\0Trap_Handler\0".len() + func_name.len() + 1;
    let text_file_offset = 52 + 32 + shstrtab_size + strtab_size;

    let text_phdr = ProgramHeader::load(
        flash_base,                              // vaddr
        text_file_offset as u32,                 // offset in file
        flash_size,                              // size
        ProgramFlags::READ | ProgramFlags::EXEC, // flags: R-X
    );
    elf_builder.add_program_header(text_phdr);

    let text_section = Section::new(".text", ElfSectionType::ProgBits)
        .with_flags(SectionFlags::ALLOC | SectionFlags::EXEC)
        .with_addr(flash_base)
        .with_align(4)
        .with_data(flash_image);

    elf_builder.add_section(text_section);

    // Add symbols
    let reset_sym = Symbol::new("Reset_Handler")
        .with_value(startup_addr | 1)
        .with_size(startup_size)
        .with_binding(SymbolBinding::Global)
        .with_type(SymbolType::Func)
        .with_section(4);
    elf_builder.add_symbol(reset_sym);

    let default_sym = Symbol::new("Default_Handler")
        .with_value(default_handler_addr | 1)
        .with_size(default_handler_size)
        .with_binding(SymbolBinding::Global)
        .with_type(SymbolType::Func)
        .with_section(4);
    elf_builder.add_symbol(default_sym);

    let trap_sym = Symbol::new("Trap_Handler")
        .with_value(trap_handler_addr | 1)
        .with_size(trap_handler_size)
        .with_binding(SymbolBinding::Global)
        .with_type(SymbolType::Func)
        .with_section(4);
    elf_builder.add_symbol(trap_sym);

    let func_sym = Symbol::new(func_name)
        .with_value(code_addr | 1)
        .with_size(code.len() as u32)
        .with_binding(SymbolBinding::Global)
        .with_type(SymbolType::Func)
        .with_section(4);
    elf_builder.add_symbol(func_sym);

    elf_builder.build().context("ELF generation failed")
}

/// Generate minimal Thumb startup code that calls the user function and loops
///
/// # Arguments
/// * `memory_size` - Size of linear memory in bytes (for R10 bounds checking)
///
/// # Memory Register Setup
/// * R10 = memory_size (for bounds checking)
/// * R11 = 0x20000000 (linear memory base)
fn generate_minimal_startup(memory_size: u32) -> Vec<u8> {
    // This startup code:
    // 1. Initializes R10 with memory size (for bounds checking)
    // 2. Initializes R11 with linear memory base (0x20000000) for WASM memory access
    // 3. Loads the address of the user function
    // 4. Calls it with BLX
    // 5. Loops forever
    //
    // In Thumb assembly:
    //   MOVW R10, #(memory_size & 0xFFFF)
    //   MOVT R10, #(memory_size >> 16)
    //   MOVW R11, #0x0000  ; Low 16 bits of memory base
    //   MOVT R11, #0x2000  ; High 16 bits of memory base
    //   LDR r0, [pc, #4]   ; Load function address from literal pool
    //   BLX r0             ; Call function
    //   B .                ; Infinite loop
    //   .word func_addr    ; Literal pool

    // Encode MOVW/MOVT for R10 with memory_size
    let r10_movw = encode_thumb2_movw(10, (memory_size & 0xFFFF) as u16);
    let r10_movt = encode_thumb2_movt(10, (memory_size >> 16) as u16);

    vec![
        // MOVW R10, #(memory_size & 0xFFFF)
        r10_movw[0],
        r10_movw[1],
        r10_movw[2],
        r10_movw[3],
        // MOVT R10, #(memory_size >> 16)
        r10_movt[0],
        r10_movt[1],
        r10_movt[2],
        r10_movt[3],
        // MOVW R11, #0x0000 - Thumb-2 32-bit encoding
        0x40,
        0xF2,
        0x00,
        0x0B,
        // MOVT R11, #0x2000 - Thumb-2 32-bit encoding
        0xC2,
        0xF2,
        0x00,
        0x0B,
        // LDR r0, [pc, #4] - Thumb 16-bit encoding: 0x4801
        // PC = current_addr + 4, literal at PC+4
        0x01,
        0x48,
        // BLX r0 - Thumb encoding: 0x4780
        0x80,
        0x47,
        // B . (branch to self) - Thumb encoding: 0xe7fe
        0xfe,
        0xe7,
        // Padding for alignment (to make literal pool 4-byte aligned)
        0x00,
        0x00,
        // Literal pool placeholder at offset 24 (will be patched with func_addr | 1)
        0x91,
        0x00,
        0x00,
        0x00,
    ]
}

/// Encode Thumb-2 MOVW instruction (move 16-bit immediate to low half of register)
fn encode_thumb2_movw(rd: u8, imm16: u16) -> [u8; 4] {
    // Thumb-2 MOVW encoding:
    // First halfword:  1111 0 i 10 0 1 0 0 imm4
    // Second halfword: 0 imm3 Rd imm8
    let imm4 = ((imm16 >> 12) & 0xF) as u8;
    let i = ((imm16 >> 11) & 0x1) as u8;
    let imm3 = ((imm16 >> 8) & 0x7) as u8;
    let imm8 = (imm16 & 0xFF) as u8;

    let hw1: u16 = 0xF240 | ((i as u16) << 10) | (imm4 as u16);
    let hw2: u16 = ((imm3 as u16) << 12) | ((rd as u16) << 8) | (imm8 as u16);

    let hw1_bytes = hw1.to_le_bytes();
    let hw2_bytes = hw2.to_le_bytes();
    [hw1_bytes[0], hw1_bytes[1], hw2_bytes[0], hw2_bytes[1]]
}

/// Encode Thumb-2 MOVT instruction (move 16-bit immediate to high half of register)
fn encode_thumb2_movt(rd: u8, imm16: u16) -> [u8; 4] {
    // Thumb-2 MOVT encoding:
    // First halfword:  1111 0 i 10 1 1 0 0 imm4
    // Second halfword: 0 imm3 Rd imm8
    let imm4 = ((imm16 >> 12) & 0xF) as u8;
    let i = ((imm16 >> 11) & 0x1) as u8;
    let imm3 = ((imm16 >> 8) & 0x7) as u8;
    let imm8 = (imm16 & 0xFF) as u8;

    let hw1: u16 = 0xF2C0 | ((i as u16) << 10) | (imm4 as u16);
    let hw2: u16 = ((imm3 as u16) << 12) | ((rd as u16) << 8) | (imm8 as u16);

    let hw1_bytes = hw1.to_le_bytes();
    let hw2_bytes = hw2.to_le_bytes();
    [hw1_bytes[0], hw1_bytes[1], hw2_bytes[0], hw2_bytes[1]]
}

/// Generate default exception handler (infinite loop)
fn generate_default_handler() -> Vec<u8> {
    // B . (branch to self) - Thumb encoding
    vec![0xfe, 0xe7]
}

fn generate_trap_handler() -> Vec<u8> {
    // Trap handler for WASM trap operations (div by zero, integer overflow)
    // Same as Default_Handler - infinite loop (B .)
    // The difference is the address, which allows tests to distinguish
    // between normal return (PC at Default_Handler) and trap (PC at Trap_Handler)
    // B . (branch to self) - Thumb encoding
    vec![0xfe, 0xe7]
}

/// Link a compiled .o into a final firmware.elf using arm-none-eabi-gcc.
///
/// Steps:
/// 1. Generate a linker script from the .o file
/// 2. Find arm-none-eabi-gcc in PATH
/// 3. Invoke the linker with the generated script
/// 4. Replace the .o output with the linked .elf
fn link_firmware(
    object_path: &std::path::Path,
    builtins: Option<&std::path::Path>,
    _target_spec: &TargetSpec,
) -> Result<()> {
    use std::process::Command;

    // Find cross-compiler
    let gcc = ["arm-none-eabi-gcc", "arm-none-eabi-ld"]
        .iter()
        .find(|cmd| {
            Command::new(cmd)
                .arg("--version")
                .output()
                .map(|o| o.status.success())
                .unwrap_or(false)
        })
        .copied();

    let gcc = match gcc {
        Some(g) => g,
        None => {
            anyhow::bail!(
                "arm-none-eabi-gcc not found in PATH. Install the ARM embedded toolchain:\n  \
                 brew install arm-none-eabi-gcc  (macOS)\n  \
                 apt install gcc-arm-none-eabi   (Linux)"
            );
        }
    };

    info!("Using cross-linker: {}", gcc);

    // Generate linker script
    let mut ls_gen = synth_backend::LinkerScriptGenerator::new();
    ls_gen.add_region(synth_backend::MemoryRegion {
        name: "FLASH".to_string(),
        origin: 0x0000_0000,
        length: 256 * 1024,
        attributes: "rx".to_string(),
    });
    ls_gen.add_region(synth_backend::MemoryRegion {
        name: "RAM".to_string(),
        origin: 0x2000_0000,
        length: 128 * 1024,
        attributes: "rwx".to_string(),
    });
    let ls_gen = ls_gen.with_stack_size(4096).with_meld_integration();
    let linker_script = ls_gen
        .generate()
        .context("Failed to generate linker script")?;

    let ld_script_path = object_path.with_extension("ld");
    std::fs::write(&ld_script_path, &linker_script).context("Failed to write linker script")?;

    info!("Generated linker script: {}", ld_script_path.display());

    // Build linker command
    let firmware_path = object_path.with_extension("firmware.elf");
    let mut cmd = Command::new(gcc);

    if gcc == "arm-none-eabi-gcc" {
        cmd.args(["-nostartfiles", "-nostdlib", "-mcpu=cortex-m4", "-mthumb"]);
    }

    cmd.arg("-T").arg(&ld_script_path);
    cmd.arg(object_path);

    if let Some(builtins_path) = builtins {
        cmd.arg(builtins_path);
    }

    cmd.arg("-o").arg(&firmware_path);

    info!("Linking: {:?}", cmd);

    let output = cmd.output().context("Failed to invoke cross-linker")?;

    if !output.status.success() {
        let stderr = String::from_utf8_lossy(&output.stderr);
        anyhow::bail!("Linker failed:\n{}", stderr);
    }

    // Clean up linker script
    let _ = std::fs::remove_file(&ld_script_path);

    println!(
        "Linked firmware: {} ({} bytes)",
        firmware_path.display(),
        std::fs::metadata(&firmware_path)
            .map(|m| m.len())
            .unwrap_or(0)
    );

    Ok(())
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn test_cortex_m_binary_structure() {
        // Simple add function: ADD r0, r0, r1; BX lr
        let code = vec![
            0x00, 0x80, 0x80, 0xe0, // ADD r0, r0, r1 (ARM encoding)
            0x1e, 0xff, 0x2f, 0xe1, // BX lr (ARM encoding)
        ];

        let elf_data = build_cortex_m_elf(&code, "test_func", &TargetSpec::cortex_m3()).unwrap();

        // Verify ELF magic
        assert_eq!(&elf_data[0..4], b"\x7fELF", "Invalid ELF magic");

        // Verify 32-bit little-endian ARM
        assert_eq!(elf_data[4], 1, "Should be 32-bit ELF");
        assert_eq!(elf_data[5], 1, "Should be little-endian");

        // Verify it's an executable
        assert_eq!(elf_data[16], 2, "Should be ET_EXEC");

        // Verify ARM architecture (0x28 = ARM)
        assert_eq!(elf_data[18], 0x28, "Should be ARM architecture");
    }

    #[test]
    fn test_vector_table_structure() {
        let code = vec![0x00, 0x80, 0x80, 0xe0]; // ADD r0, r0, r1

        let elf_data = build_cortex_m_elf(&code, "test", &TargetSpec::cortex_m3()).unwrap();

        // Find .text section (it starts after ELF headers)
        // For simplicity, look for the vector table pattern
        // Stack pointer at offset 0 should be 0x20020000 (128KB RAM)
        // This is little-endian, so bytes are: 00 00 02 20

        // The vector table is in the .text section data
        // Find where vector table data starts (after ELF headers)
        let mut found_sp = false;
        for i in 0..elf_data.len().saturating_sub(4) {
            let word = u32::from_le_bytes([
                elf_data[i],
                elf_data[i + 1],
                elf_data[i + 2],
                elf_data[i + 3],
            ]);
            if word == 0x20020000 {
                found_sp = true;
                // Next word should be reset handler with Thumb bit (0x81)
                let reset = u32::from_le_bytes([
                    elf_data[i + 4],
                    elf_data[i + 5],
                    elf_data[i + 6],
                    elf_data[i + 7],
                ]);
                assert_eq!(reset, 0x81, "Reset handler should be 0x81 (0x80 | 1)");
                break;
            }
        }
        assert!(found_sp, "Stack pointer (0x20020000) not found in ELF");
    }

    #[test]
    fn test_simple_elf_generation() {
        let code = vec![0x00, 0x80, 0x80, 0xe0]; // ADD r0, r0, r1

        let elf_data = build_simple_elf(&code, "simple_func").unwrap();

        // Verify ELF magic
        assert_eq!(&elf_data[0..4], b"\x7fELF", "Invalid ELF magic");

        // Verify entry point is 0x8000
        let entry = u32::from_le_bytes([elf_data[24], elf_data[25], elf_data[26], elf_data[27]]);
        assert_eq!(
            entry, 0x8001,
            "Entry point should be 0x8001 (0x8000 | Thumb bit)"
        );
    }

    #[test]
    fn test_startup_code_patching() {
        let code = vec![0x00, 0x80, 0x80, 0xe0];

        let elf_data = build_cortex_m_elf(&code, "patched", &TargetSpec::cortex_m3()).unwrap();

        // With the new startup code layout (28 bytes with R10/R11 init):
        // - Startup: 0x80 (28 bytes)
        // - Default handler: 0x9C (2 bytes)
        // - Trap handler: 0x9E (2 bytes)
        // - User function: 0xA0 (aligned to 4)
        // So literal pool should contain 0xA1 (0xA0 | 1 for Thumb bit)
        let mut found_literal = false;
        for i in 0..elf_data.len().saturating_sub(4) {
            let word = u32::from_le_bytes([
                elf_data[i],
                elf_data[i + 1],
                elf_data[i + 2],
                elf_data[i + 3],
            ]);
            if word == 0xA1 {
                found_literal = true;
                break;
            }
        }
        assert!(
            found_literal,
            "Literal pool should contain 0xA1 (0xA0 | 1 for Thumb)"
        );
    }

    #[test]
    fn test_minimal_startup_generation() {
        // Test with 64KB memory size (0x10000)
        let memory_size: u32 = 64 * 1024;
        let startup = generate_minimal_startup(memory_size);

        // Should be 28 bytes:
        // MOVW R10 + MOVT R10 + MOVW R11 + MOVT R11 + LDR + BLX + B + padding + literal
        assert_eq!(startup.len(), 28, "Startup code should be 28 bytes");

        // Bytes 8-11: MOVW R11, #0
        assert_eq!(startup[8], 0x40);
        assert_eq!(startup[9], 0xF2);
        assert_eq!(startup[10], 0x00);
        assert_eq!(startup[11], 0x0B);

        // Bytes 12-15: MOVT R11, #0x2000
        assert_eq!(startup[12], 0xC2);
        assert_eq!(startup[13], 0xF2);
        assert_eq!(startup[14], 0x00);
        assert_eq!(startup[15], 0x0B);

        // Bytes 16-17: LDR r0, [pc, #4] = 0x4801
        assert_eq!(startup[16], 0x01);
        assert_eq!(startup[17], 0x48);

        // Bytes 18-19: BLX r0 = 0x4780
        assert_eq!(startup[18], 0x80);
        assert_eq!(startup[19], 0x47);

        // Bytes 20-21: B . = 0xe7fe
        assert_eq!(startup[20], 0xfe);
        assert_eq!(startup[21], 0xe7);
    }

    #[test]
    fn test_default_handler_generation() {
        let handler = generate_default_handler();

        // Should be 2 bytes: B . = 0xe7fe
        assert_eq!(handler.len(), 2);
        assert_eq!(handler[0], 0xfe);
        assert_eq!(handler[1], 0xe7);
    }

    // =========================================================================
    // PR #86 patch coverage: --hardware dispatch and target_info_command
    // =========================================================================

    #[test]
    fn test_target_info_command_imxrt1062() {
        // The new "imxrt1062" hardware string must dispatch successfully.
        let result = target_info_command("imxrt1062".to_string());
        assert!(result.is_ok(), "imxrt1062 target_info should succeed");
    }

    #[test]
    fn test_target_info_command_stm32h743() {
        let result = target_info_command("stm32h743".to_string());
        assert!(result.is_ok(), "stm32h743 target_info should succeed");
    }

    #[test]
    fn test_target_info_command_existing_targets_still_work() {
        // Sanity: nrf52840 + stm32f407 should still dispatch successfully
        // alongside the new M7 entries.
        assert!(target_info_command("nrf52840".to_string()).is_ok());
        assert!(target_info_command("stm32f407".to_string()).is_ok());
    }

    #[test]
    fn test_target_info_command_unknown_target_errors() {
        // Unknown target errors with a message that lists ALL supported names,
        // including the new M7 hardware.
        let err = target_info_command("not-a-real-mcu".to_string()).unwrap_err();
        let msg = err.to_string();
        assert!(msg.contains("not-a-real-mcu"));
        assert!(msg.contains("nrf52840"));
        assert!(msg.contains("stm32f407"));
        assert!(
            msg.contains("stm32h743"),
            "error message should advertise stm32h743"
        );
        assert!(
            msg.contains("imxrt1062"),
            "error message should advertise imxrt1062"
        );
    }

    #[test]
    fn test_synthesize_command_unsupported_hardware_message() {
        // synthesize_command's --hardware error must list all four supported
        // names. We can't easily test the success path (it parses a wasm
        // component) but the unsupported branch is reachable with a dummy
        // input file path.
        let bad_path = std::path::PathBuf::from("/tmp/__non_existent_wasm__");
        let out_path = std::path::PathBuf::from("/tmp/__non_existent_out__");
        // synthesize_command tries to parse the component first — that fails
        // before the hardware check. Use the hardware match directly via the
        // public re-exposed HardwareCapabilities surface to validate the
        // string→ctor dispatch.
        let names = ["nrf52840", "stm32f407", "stm32h743", "imxrt1062"];
        for n in names {
            // Each name must produce a HardwareCapabilities with a non-zero
            // MPU region count (every supported part has an MPU).
            let caps = match n {
                "nrf52840" => HardwareCapabilities::nrf52840(),
                "stm32f407" => HardwareCapabilities::stm32f407(),
                "stm32h743" => HardwareCapabilities::stm32h743(),
                "imxrt1062" => HardwareCapabilities::imxrt1062(),
                _ => unreachable!(),
            };
            assert!(caps.mpu_regions > 0, "{} should have MPU regions", n);
        }
        // And confirm the synthesize_command pathway exists with the new
        // signature. We deliberately don't run it here (would require a
        // valid wasm file); the unit test above covers the hardware dispatch.
        let _ = (bad_path, out_path);
    }

    #[test]
    fn test_resolve_target_spec_default_no_cortex_m() {
        // When neither --target nor --cortex-m is given, the default is an
        // Arm32-ISA cortex_m4 spec (used by the non-Cortex-M flow).
        let spec = resolve_target_spec(None, false).unwrap();
        assert_eq!(spec.isa, synth_core::target::IsaVariant::Arm32);
    }

    #[test]
    fn test_resolve_target_spec_cortex_m_flag() {
        // --cortex-m without --target maps to cortex-m3.
        let spec = resolve_target_spec(None, true).unwrap();
        assert_eq!(spec.triple, "thumbv7m-none-eabi");
    }

    #[test]
    fn test_resolve_target_spec_explicit_target_wins_over_cortex_m() {
        // --target overrides --cortex-m.
        let spec = resolve_target_spec(Some("cortex-m7"), true).unwrap();
        assert_eq!(spec.triple, "thumbv7em-none-eabihf");
    }

    #[test]
    fn test_resolve_target_spec_unknown_triple_errors() {
        let err = resolve_target_spec(Some("totally-bogus-triple"), false).unwrap_err();
        let msg = err.to_string();
        assert!(msg.contains("totally-bogus-triple"));
        assert!(msg.contains("Supported"));
    }
}