fayalite/crates/fayalite/src/testing.rs

// SPDX-License-Identifier: LGPL-3.0-or-later
// See Notices.txt for copyright information
use crate::{
    build::{
        BaseJobArgs, BaseJobKind, JobArgsAndDependencies, JobKindAndArgs, JobParams, NoArgs,
        RunBuild,
        external::{ExternalCommandArgs, ExternalCommandJobKind},
        firrtl::{FirrtlArgs, FirrtlJobKind},
        formal::{Formal, FormalAdditionalArgs, FormalArgs, FormalMode, WriteSbyFileJobKind},
        verilog::{UnadjustedVerilogArgs, VerilogJobArgs, VerilogJobKind},
    },
    bundle::BundleType,
    firrtl::ExportOptions,
    module::Module,
    util::HashMap,
};
use eyre::eyre;
use serde::Deserialize;
use std::{
    fmt::Write,
    path::{Path, PathBuf},
    process::Command,
    sync::{Mutex, OnceLock},
};

#[derive(Deserialize)]
struct CargoMetadata {
    target_directory: String,
}

fn get_cargo_target_dir() -> &'static Path {
    static RETVAL: OnceLock<PathBuf> = OnceLock::new();
    RETVAL.get_or_init(|| {
        let output = Command::new(
            std::env::var_os("CARGO")
                .as_deref()
                .unwrap_or("cargo".as_ref()),
        )
        .arg("metadata")
        .output()
        .expect("can't run `cargo metadata`");
        if !output.status.success() {
            panic!(
                "can't run `cargo metadata`:\n{}\nexited with status: {}",
                String::from_utf8_lossy(&output.stderr),
                output.status
            );
        }
        let CargoMetadata { target_directory } =
            serde_json::from_slice(&output.stdout).expect("can't parse output of `cargo metadata`");
        PathBuf::from(target_directory)
    })
}

#[track_caller]
fn get_assert_formal_target_path(test_name: &dyn std::fmt::Display) -> PathBuf {
    static DIRS: Mutex<Option<HashMap<String, u64>>> = Mutex::new(None);
    let test_name = test_name.to_string();
    // don't use line/column numbers since that constantly changes as you edit tests
    let file = std::panic::Location::caller().file();
    // simple reproducible hash
    let simple_hash = file.bytes().chain(test_name.bytes()).fold(
        ((file.len() as u32) << 16).wrapping_add(test_name.len() as u32),
        |mut h, b| {
            h = h.wrapping_mul(0xaa0d184b);
            h ^= h.rotate_right(5);
            h ^= h.rotate_right(13);
            h.wrapping_add(b as u32)
        },
    );
    let mut dir = String::with_capacity(64);
    for ch in Path::new(file)
        .file_stem()
        .unwrap_or_default()
        .to_str()
        .unwrap()
        .chars()
        .chain(['-'])
        .chain(test_name.chars())
    {
        dir.push(match ch {
            ch if ch.is_alphanumeric() => ch,
            '_' | '-' | '+' | '.' | ',' | ' ' => ch,
            _ => '_',
        });
    }
    write!(dir, "-{simple_hash:08x}").unwrap();
    let index = *DIRS
        .lock()
        .unwrap()
        .get_or_insert_with(HashMap::default)
        .entry_ref(&dir)
        .and_modify(|v| *v += 1)
        .or_insert(0);
    write!(dir, "-{index}").unwrap();
    get_cargo_target_dir()
        .join("fayalite_assert_formal")
        .join(dir)
}

fn make_assert_formal_args(
    test_name: &dyn std::fmt::Display,
    formal_mode: FormalMode,
    formal_depth: u64,
    solver: Option<&str>,
    export_options: ExportOptions,
) -> eyre::Result<JobArgsAndDependencies<ExternalCommandJobKind<Formal>>> {
    let args = JobKindAndArgs {
        kind: BaseJobKind,
        args: BaseJobArgs::from_output_dir_and_env(
            get_assert_formal_target_path(&test_name)
                .into_os_string()
                .into_string()
                .map_err(|_| eyre!("path is not valid UTF-8"))?,
        ),
    };
    let dependencies = JobArgsAndDependencies {
        args,
        dependencies: (),
    };
    let args = JobKindAndArgs {
        kind: FirrtlJobKind,
        args: FirrtlArgs { export_options },
    };
    let dependencies = JobArgsAndDependencies { args, dependencies };
    let args = JobKindAndArgs {
        kind: ExternalCommandJobKind::new(),
        args: ExternalCommandArgs::resolve_program_path(
            None,
            UnadjustedVerilogArgs {
                firtool_extra_args: vec![],
                verilog_dialect: None,
                verilog_debug: true,
            },
        )?,
    };
    let dependencies = JobArgsAndDependencies { args, dependencies };
    let args = JobKindAndArgs {
        kind: VerilogJobKind,
        args: VerilogJobArgs {},
    };
    let dependencies = JobArgsAndDependencies { args, dependencies };
    let args = JobKindAndArgs {
        kind: WriteSbyFileJobKind,
        args: FormalArgs {
            sby_extra_args: vec![],
            formal_mode,
            formal_depth,
            formal_solver: solver.unwrap_or(FormalArgs::DEFAULT_SOLVER).into(),
            smtbmc_extra_args: vec![],
        },
    };
    let dependencies = JobArgsAndDependencies { args, dependencies };
    let args = JobKindAndArgs {
        kind: ExternalCommandJobKind::new(),
        args: ExternalCommandArgs::resolve_program_path(None, FormalAdditionalArgs {})?,
    };
    Ok(JobArgsAndDependencies { args, dependencies })
}

pub fn try_assert_formal<M: AsRef<Module<T>>, T: BundleType>(
    test_name: impl std::fmt::Display,
    module: M,
    formal_mode: FormalMode,
    formal_depth: u64,
    solver: Option<&str>,
    export_options: ExportOptions,
) -> eyre::Result<()> {
    const APP_NAME: &'static str = "fayalite::testing::assert_formal";
    make_assert_formal_args(
        &test_name,
        formal_mode,
        formal_depth,
        solver,
        export_options,
    )?
    .run(
        |NoArgs {}| Ok(JobParams::new(module, APP_NAME)),
        clap::Command::new(APP_NAME), // not actually used, so we can use an arbitrary value
    )
}

#[track_caller]
pub fn assert_formal<M: AsRef<Module<T>>, T: BundleType>(
    test_name: impl std::fmt::Display,
    module: M,
    formal_mode: FormalMode,
    formal_depth: u64,
    solver: Option<&str>,
    export_options: ExportOptions,
) {
    try_assert_formal(
        test_name,
        module,
        formal_mode,
        formal_depth,
        solver,
        export_options,
    )
    .expect("testing::assert_formal() failed");
}