From bf907c38721ebc804d6aaf0bf5ed6798d8604dab Mon Sep 17 00:00:00 2001 From: Jacob Lifshay Date: Mon, 7 Oct 2024 23:31:24 -0700 Subject: [PATCH] cache results of formal proofs --- Cargo.lock | 48 +++++++++++++ Cargo.toml | 1 + crates/fayalite/Cargo.toml | 1 + crates/fayalite/src/cli.rs | 141 ++++++++++++++++++++++++++++++++----- 4 files changed, 175 insertions(+), 16 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index fa6fb6b..1e6f88c 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -69,6 +69,18 @@ dependencies = [ "windows-sys 0.52.0", ] +[[package]] +name = "arrayref" +version = "0.3.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "76a2e8124351fda1ef8aaaa3bbd7ebbcb486bbcd4225aca0aa0d84bb2db8fecb" + +[[package]] +name = "arrayvec" +version = "0.7.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7c02d123df017efcdfbd739ef81735b36c5ba83ec3c59c80a9d7ecc718f92e50" + [[package]] name = "autocfg" version = "1.1.0" @@ -109,6 +121,20 @@ dependencies = [ "wyz", ] +[[package]] +name = "blake3" +version = "1.5.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d82033247fd8e890df8f740e407ad4d038debb9eb1f40533fffb32e7d17dc6f7" +dependencies = [ + "arrayref", + "arrayvec", + "cc", + "cfg-if", + "constant_time_eq", + "serde", +] + [[package]] name = "block-buffer" version = "0.10.4" @@ -118,6 +144,15 @@ dependencies = [ "generic-array", ] +[[package]] +name = "cc" +version = "1.1.28" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2e80e3b6a3ab07840e1cae9b0666a63970dc28e8ed5ffbcdacbfc760c281bfc1" +dependencies = [ + "shlex", +] + [[package]] name = "cfg-if" version = "1.0.0" @@ -170,6 +205,12 @@ version = "1.0.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0b6a852b24ab71dffc585bcb46eaf7959d175cb865a7152e35b348d1b2960422" +[[package]] +name = "constant_time_eq" +version = "0.3.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7c74b8349d32d297c9134b8c88677813a227df8f779daa29bfc29c183fe3dca6" + [[package]] name = "cpufeatures" version = "0.2.12" @@ -242,6 +283,7 @@ name = "fayalite" version = "0.2.0" dependencies = [ "bitvec", + "blake3", "clap", "eyre", "fayalite-proc-macros", @@ -521,6 +563,12 @@ dependencies = [ "digest", ] +[[package]] +name = "shlex" +version = "1.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0fda2ff0d084019ba4d7c6f371c95d8fd75ce3524c3cb8fb653a3023f6323e64" + [[package]] name = "strsim" version = "0.11.1" diff --git a/Cargo.toml b/Cargo.toml index 15d13b6..699d57f 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -19,6 +19,7 @@ fayalite-proc-macros-impl = { version = "=0.2.0", path = "crates/fayalite-proc-m fayalite-visit-gen = { version = "=0.2.0", path = "crates/fayalite-visit-gen" } base16ct = "0.2.0" bitvec = { version = "1.0.1", features = ["serde"] } +blake3 = { version = "1.5.4", features = ["serde"] } clap = { version = "4.5.9", features = ["derive", "env", "string"] } eyre = "0.6.12" hashbrown = "0.14.3" diff --git a/crates/fayalite/Cargo.toml b/crates/fayalite/Cargo.toml index 21089c0..828d759 100644 --- a/crates/fayalite/Cargo.toml +++ b/crates/fayalite/Cargo.toml @@ -15,6 +15,7 @@ version.workspace = true [dependencies] bitvec.workspace = true +blake3.workspace = true clap.workspace = true eyre.workspace = true fayalite-proc-macros.workspace = true diff --git a/crates/fayalite/src/cli.rs b/crates/fayalite/src/cli.rs index fa1b247..a3649cc 100644 --- a/crates/fayalite/src/cli.rs +++ b/crates/fayalite/src/cli.rs @@ -12,6 +12,7 @@ use clap::{ Parser, Subcommand, ValueEnum, ValueHint, }; use eyre::{eyre, Report}; +use serde::{Deserialize, Serialize}; use std::{ error, ffi::OsString, @@ -197,8 +198,9 @@ impl BaseArgs { &self, _acquired_job: &mut AcquiredJob, mut command: process::Command, + mut captured_output: Option<&mut String>, ) -> io::Result { - if self.redirect_output_for_rust_test { + if self.redirect_output_for_rust_test || captured_output.is_some() { let (reader, writer) = os_pipe::pipe()?; let mut reader = io::BufReader::new(reader); command.stderr(writer.try_clone()?); @@ -209,6 +211,9 @@ impl BaseArgs { Ok(loop { let status = child.try_wait()?; streaming_read_utf8(&mut reader, |s| { + if let Some(captured_output) = captured_output.as_deref_mut() { + captured_output.push_str(s); + } // use print! so output goes to Rust test output capture print!("{s}"); io::Result::Ok(()) @@ -369,6 +374,7 @@ pub struct VerilogArgs { pub struct VerilogOutput { pub firrtl: FirrtlOutput, pub verilog_files: Vec, + pub contents_hash: Option, } impl VerilogOutput { @@ -386,6 +392,7 @@ impl VerilogArgs { let file_separator_prefix = "\n// ----- 8< ----- FILE \""; let file_separator_suffix = "\" ----- 8< -----\n\n"; let mut input = &*input; + output.contents_hash = Some(blake3::hash(input.as_bytes())); let main_verilog_file = output.main_verilog_file(); let mut file_name: Option<&Path> = Some(&main_verilog_file); loop { @@ -428,6 +435,7 @@ impl VerilogArgs { let output = VerilogOutput { firrtl: firrtl_output, verilog_files: vec![], + contents_hash: None, }; let mut cmd = process::Command::new(firtool); cmd.arg(output.firrtl.firrtl_file()); @@ -442,7 +450,7 @@ impl VerilogArgs { } cmd.args(firtool_extra_args); cmd.current_dir(&output.firrtl.output_dir); - let status = firrtl.base.run_external_command(acquired_job, cmd)?; + let status = firrtl.base.run_external_command(acquired_job, cmd, None)?; if status.success() { self.process_unadjusted_verilog_file(output) } else { @@ -541,7 +549,7 @@ pub struct FormalArgs { )] pub sby: PathBuf, #[arg(long)] - pub sby_extra_args: Vec, + pub sby_extra_args: Vec, #[arg(long, default_value_t)] pub mode: FormalMode, #[arg(long, default_value_t = Self::DEFAULT_DEPTH)] @@ -550,6 +558,8 @@ pub struct FormalArgs { pub solver: String, #[arg(long)] pub smtbmc_extra_args: Vec, + #[arg(long, default_value_t = true, env = "FAYALITE_CACHE_RESULTS")] + pub cache_results: bool, #[command(flatten)] _formal_adjust_args: FormalAdjustArgs, } @@ -564,16 +574,18 @@ impl fmt::Debug for FormalArgs { depth, solver, smtbmc_extra_args, + cache_results, _formal_adjust_args: _, } = self; f.debug_struct("FormalArgs") - .field("verilog", &verilog) - .field("sby", &sby) - .field("sby_extra_args", &sby_extra_args) - .field("mode", &mode) - .field("depth", &depth) - .field("solver", &solver) - .field("smtbmc_extra_args", &smtbmc_extra_args) + .field("verilog", verilog) + .field("sby", sby) + .field("sby_extra_args", sby_extra_args) + .field("mode", mode) + .field("depth", depth) + .field("solver", solver) + .field("smtbmc_extra_args", smtbmc_extra_args) + .field("cache_results", cache_results) .finish_non_exhaustive() } } @@ -592,6 +604,48 @@ impl FormalOutput { pub fn sby_file(&self) -> PathBuf { self.verilog.firrtl.file_with_ext("sby") } + pub fn cache_file(&self) -> PathBuf { + self.verilog.firrtl.file_with_ext("cache.json") + } +} + +#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize)] +#[non_exhaustive] +pub struct FormalCacheOutput {} + +#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize)] +#[non_exhaustive] +pub enum FormalCacheVersion { + V1, +} + +impl FormalCacheVersion { + pub const CURRENT: Self = Self::V1; +} + +#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize)] +#[non_exhaustive] +pub struct FormalCache { + pub version: FormalCacheVersion, + pub contents_hash: blake3::Hash, + pub stdout_stderr: String, + pub result: Result, +} + +impl FormalCache { + pub fn new( + version: FormalCacheVersion, + contents_hash: blake3::Hash, + stdout_stderr: String, + result: Result, + ) -> Self { + Self { + version, + contents_hash, + stdout_stderr, + result, + } + } } impl FormalArgs { @@ -604,6 +658,7 @@ impl FormalArgs { depth, smtbmc_extra_args, solver, + cache_results: _, _formal_adjust_args: _, } = self; let smtbmc_options = smtbmc_extra_args.join(" "); @@ -644,7 +699,19 @@ impl FormalArgs { verilog: verilog_output, }; let sby_file = output.sby_file(); - std::fs::write(&sby_file, self.sby_contents(&output)?)?; + let sby_contents = self.sby_contents(&output)?; + let contents_hash = output.verilog.contents_hash.map(|verilog_hash| { + let mut hasher = blake3::Hasher::new(); + hasher.update(verilog_hash.as_bytes()); + hasher.update(sby_contents.as_bytes()); + hasher.update(&(self.sby_extra_args.len() as u64).to_le_bytes()); + for sby_extra_arg in self.sby_extra_args.iter() { + hasher.update(&(sby_extra_arg.len() as u64).to_le_bytes()); + hasher.update(sby_extra_arg.as_bytes()); + } + hasher.finalize() + }); + std::fs::write(&sby_file, sby_contents)?; let mut cmd = process::Command::new(&self.sby); cmd.arg("-f"); cmd.arg(sby_file.file_name().unwrap()); @@ -656,20 +723,62 @@ impl FormalArgs { NonZeroUsize::new(1).unwrap() }; let new_minimum_count = AcquiredJob::max_available_job_count().min(new_minimum_count); + let mut captured_output = String::new(); + let cache_file = output.cache_file(); + let do_cache = if let Some(contents_hash) = contents_hash.filter(|_| self.cache_results) { + if let Some(FormalCache { + version: FormalCacheVersion::CURRENT, + contents_hash: cache_contents_hash, + stdout_stderr, + result, + }) = fs::read(&cache_file) + .ok() + .and_then(|v| serde_json::from_slice(&v).ok()) + { + if cache_contents_hash == contents_hash { + println!("Using cached formal result:\n{stdout_stderr}"); + return match result { + Ok(FormalCacheOutput {}) => Ok(output), + Err(error) => Err(CliError(eyre::Report::msg(error))), + }; + } + } + true + } else { + false + }; + let _ = fs::remove_file(&cache_file); let status = acquired_job.increase_job_count(new_minimum_count, |acquired_job| { - self.verilog - .firrtl - .base - .run_external_command(acquired_job, cmd) + self.verilog.firrtl.base.run_external_command( + acquired_job, + cmd, + do_cache.then_some(&mut captured_output), + ) })?; - if status.success() { + let result = if status.success() { Ok(output) } else { Err(CliError(eyre!( "running {} failed: {status}", self.sby.display() ))) + }; + if do_cache { + fs::write( + cache_file, + serde_json::to_string_pretty(&FormalCache { + version: FormalCacheVersion::CURRENT, + contents_hash: contents_hash.unwrap(), + stdout_stderr: captured_output, + result: match &result { + Ok(FormalOutput { verilog: _ }) => Ok(FormalCacheOutput {}), + Err(error) => Err(error.to_string()), + }, + }) + .expect("serialization shouldn't ever fail"), + )?; } + result } }