diff --git a/Cargo.lock b/Cargo.lock index 37839d4..d03ef6d 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -102,18 +102,6 @@ dependencies = [ "rustversion", ] -[[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 = "askama" version = "0.13.1" @@ -177,20 +165,6 @@ version = "2.11.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "c4512299f36f043ab09a583e57bceb5a5aab7a73db1805848e8fef3c9e8c78b3" -[[package]] -name = "blake3" -version = "1.8.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0aa83c34e62843d924f905e0f5c866eb1dd6545fc4d719e803d9ba6030371fce" -dependencies = [ - "arrayref", - "arrayvec", - "cc", - "cfg-if", - "constant_time_eq", - "cpufeatures", -] - [[package]] name = "bumpalo" version = "3.20.2" @@ -314,27 +288,12 @@ dependencies = [ "windows-sys", ] -[[package]] -name = "constant_time_eq" -version = "0.4.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3d52eff69cd5e647efe296129160853a42795992097e8af39800e1060caeea9b" - [[package]] name = "core-foundation-sys" version = "0.8.7" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "773648b94d0e5d620f64f280777445740e61fe701025087ec8b57f45c791888b" -[[package]] -name = "cpufeatures" -version = "0.3.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8b2a41393f66f16b0823bb79094d54ac5fbd34ab292ddafb9a0456ac9f87d201" -dependencies = [ - "libc", -] - [[package]] name = "crc32fast" version = "1.5.0" @@ -584,12 +543,6 @@ version = "0.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "2304e00983f87ffb38b55b444b5e3b60a884b5d30c0fca7d82fe33449bbe55ea" -[[package]] -name = "hex" -version = "0.4.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7f24254aa9a54b5c858eaee2f5bccdb46aaf0e486a595ed5fd8f86ba55232a70" - [[package]] name = "humantime" version = "2.3.0" @@ -1199,13 +1152,11 @@ version = "0.0.0" dependencies = [ "anyhow", "askama", - "blake3", "cargo_metadata", "clap", "colored", "dotenv", "git2", - "hex", "indexmap", "log", "log4rs", diff --git a/Cargo.toml b/Cargo.toml index 98dd320..f465bd8 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -45,8 +45,6 @@ log = { version = "*" } log4rs = { version = "*", features = ["gzip"] } walkdir = { version = "*" } rayon = { version = "*" } -blake3 = { version = "*" } -hex = { version = "*" } toml_edit = { version = "*" } syn = { version = "2", features = ["full", "extra-traits"] } diff --git a/src/fingerprint.rs b/src/fingerprint.rs deleted file mode 100644 index e38c128..0000000 --- a/src/fingerprint.rs +++ /dev/null @@ -1,45 +0,0 @@ -use blake3::Hasher; -use rayon::prelude::*; -use std::{fs::File, io::Read, path::PathBuf}; -use walkdir::WalkDir; - -type Hash = [u8; 32]; - -pub fn fingerprint_file(path: &PathBuf) -> Hash { - let mut hasher = Hasher::new(); - let mut file = File::open(path).unwrap(); - let mut buffer = Vec::new(); - file.read_to_end(&mut buffer).unwrap(); - hasher.update(&buffer); - *hasher.finalize().as_bytes() -} - -pub fn fingerprint_dir(root: &PathBuf) -> Hash { - let mut paths: Vec = WalkDir::new(root) - .into_iter() - .filter_map(|e| e.ok()) - .filter(|e| e.file_type().is_file()) - .map(|e| e.path().to_path_buf()) - .collect::>(); - paths.sort(); - - let file_hashes: Vec<(PathBuf, Hash)> = paths - .into_par_iter() - .map(|path| { - let rel = path.strip_prefix(root).unwrap().to_path_buf(); - let h = fingerprint_file(&path); - (rel, h) - }) - .collect::>(); - - let mut dir_hasher = Hasher::new(); - for (rel, h) in file_hashes.iter() { - dir_hasher.update(rel.to_string_lossy().as_bytes()); - dir_hasher.update(h); - } - *dir_hasher.finalize().as_bytes() -} - -pub fn fingerprint_as_str(hash: &Hash) -> String { - hex::encode(hash) -} diff --git a/src/lib.rs b/src/lib.rs index 5d5b739..f55f3cb 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -8,7 +8,6 @@ pub mod commands; pub mod config; pub mod dep_tree; pub mod doc; -pub mod fingerprint; pub mod format; pub mod generator; pub mod metadata; diff --git a/src/main.rs b/src/main.rs index 4be583d..326ccbe 100644 --- a/src/main.rs +++ b/src/main.rs @@ -47,13 +47,6 @@ enum Commands { )] Clean(CleanArgs), - #[command( - name = "fingerprint", - about = "Print the fingerprint of the verification targets", - alias = "fp" - )] - Fingerprint(FingerprintArgs), - #[command( name = "list", about = "List all available verification targets", @@ -307,18 +300,6 @@ struct BuildArgs { #[derive(Parser, Debug)] struct CleanArgs {} -#[derive(Parser, Debug)] -struct FingerprintArgs { - #[arg( - short = 't', - long = "targets", - value_parser = verus::find_target, - help = "The targets to fingerprint", - num_args = 0.., - action = ArgAction::Append)] - targets: Vec, -} - #[derive(Parser, Debug)] struct ListTargetsArgs {} @@ -424,13 +405,6 @@ struct FmtArgs { fn verify(args: &VerifyArgs) -> Result<(), DynError> { let targets = args.targets.clone(); - // verify-only-module should only apply to the main target - // Conditions: exactly one target AND pass_through contains "--verify-only-module" - let verify_only_module_main_only = targets.len() == 1 - && args - .pass_through - .iter() - .any(|arg| arg == "--verify-only-module" || arg.starts_with("--verify-only-module=")); let options = verus::ExtraOptions { max_errors: args.max_errors, log: args.log, @@ -440,7 +414,6 @@ fn verify(args: &VerifyArgs) -> Result<(), DynError> { pass_through: args.pass_through.clone(), count_line: args.count_line, focus: args.focus, - verify_only_module_main_only, }; verus::exec_verify(&targets, &options) @@ -482,20 +455,11 @@ fn build(args: &BuildArgs) -> Result<(), DynError> { pass_through: args.pass_through.clone(), count_line: false, focus: false, - verify_only_module_main_only: false, }; verus::exec_build(&targets, &options) } -fn fingerprint(args: &FingerprintArgs) -> Result<(), DynError> { - let targets = args.targets.clone(); - for target in targets { - println!("{}: {}", target.name, target.fingerprint()); - } - Ok(()) -} - fn clean(_args: &CleanArgs) -> Result<(), DynError> { verus::exec_clean() } @@ -567,7 +531,6 @@ fn main() { Commands::Doc(args) => doc(args), Commands::Bootstrap(args) => bootstrap(args), Commands::Build(args) => build(args), - Commands::Fingerprint(args) => fingerprint(args), Commands::ListTargets(args) => list_targets(args), Commands::NewTarget(args) => new_target(args), Commands::ShowItem(args) => show_item(args), diff --git a/src/verus.rs b/src/verus.rs index f2bb590..5635212 100644 --- a/src/verus.rs +++ b/src/verus.rs @@ -3,7 +3,6 @@ use indexmap::IndexMap; use memoize::memoize; use std::collections::{HashMap, HashSet}; use std::fs::{self, File}; -use std::hash::Hash; use std::io::{Read, Write}; use std::path::{Path, PathBuf}; use std::process::{Command, Stdio}; @@ -13,7 +12,7 @@ use cargo_metadata; use cargo_metadata::CrateType; use crate::commands::CargoBuildExterns; -use crate::{commands, dep_tree, executable, files, fingerprint, projects, serialization}; +use crate::{commands, dep_tree, executable, files, projects, serialization}; pub type DynError = Box; @@ -191,51 +190,6 @@ pub struct ExtraOptions { pub count_line: bool, /// use cargo-verus focus instead of cargo-verus verify pub focus: bool, - /// verify-only-module should only apply to the main target, not its dependencies - pub verify_only_module_main_only: bool, -} - -impl ExtraOptions { - /// Create a modified version of options for dependency builds - /// If verify_only_module_main_only is true, removes the verify-only-module parameter - /// since it should only apply to the main target - pub fn for_dependency(&self) -> Self { - let pass_through = if self.verify_only_module_main_only { - let mut filtered = Vec::new(); - let mut skip_next = false; - - for arg in self.pass_through.iter() { - if skip_next { - skip_next = false; - continue; - } - - if arg == "--verify-only-module" { - // Skip this argument and the next one (the module name) - skip_next = true; - } else if arg.starts_with("--verify-only-module=") { - // Skip inline form: --verify-only-module= - } else { - filtered.push(arg.clone()); - } - } - filtered - } else { - self.pass_through.clone() - }; - - ExtraOptions { - log: self.log, - trace: self.trace, - release: self.release, - max_errors: self.max_errors, - disasm: self.disasm, - pass_through, - count_line: self.count_line, - focus: self.focus, - verify_only_module_main_only: self.verify_only_module_main_only, - } - } } #[derive(Clone, Debug, PartialEq, Eq, Hash)] @@ -250,70 +204,6 @@ impl VerusTarget { self.crate_type.clone() } - pub fn fingerprint(&self) -> String { - let content = fingerprint::fingerprint_dir(&self.dir); - fingerprint::fingerprint_as_str(&content) - } - - pub fn fingerprint_recursive(&self, all_targets: &HashMap) -> String { - use std::collections::hash_map::DefaultHasher; - use std::hash::{Hash, Hasher}; - - let mut hasher = DefaultHasher::new(); - let content = fingerprint::fingerprint_dir(&self.dir); - fingerprint::fingerprint_as_str(&content).hash(&mut hasher); - for dep in &self.dependencies { - if let Some(dep_target) = all_targets.get(&dep.name) { - dep_target - .fingerprint_recursive(all_targets) - .hash(&mut hasher); - } - } - hasher.finish().to_string() - } - - pub fn is_fresh(&self, all_targets: &HashMap) -> bool { - let ts = self.library_proof_timestamp(); - if !ts.exists() { - return false; - } - - // Check if our own verification file exists - if !self.library_proof().exists() { - return false; - } - - // Get our own timestamp - let self_timestamp = match std::fs::metadata(&self.library_proof()) { - Ok(metadata) => metadata.modified().unwrap_or(std::time::UNIX_EPOCH), - Err(_) => return false, - }; - - // Check if all recursive dependencies have their verification files and are not newer than us - let deps = get_local_dependency(self); - for dep in deps.values() { - if !dep.library_proof().exists() { - return false; - } - - // Check if dependency is newer than us - if let Ok(dep_metadata) = std::fs::metadata(&dep.library_proof()) { - if let Ok(dep_timestamp) = dep_metadata.modified() { - if dep_timestamp > self_timestamp { - return false; // Dependency is newer, we need to rebuild - } - } - } - } - - let ts_hash = self.load_library_proof_timestamp(); - let cur_hash = self.fingerprint_recursive(all_targets); - if cur_hash == ts_hash { - return true; - } - false - } - pub fn library_prefix(&self) -> String { match self.crate_type { CrateType::Bin => "", @@ -342,40 +232,6 @@ impl VerusTarget { .to_path_buf() } - pub fn library_proof_timestamp(&self) -> PathBuf { - get_target_dir() - .join(format!("{}.verusdata.timestamp", self.name)) - .to_path_buf() - } - - pub fn load_library_proof_timestamp(&self) -> String { - let content = File::open(self.library_proof_timestamp()) - .map(|mut f| { - let mut content = Vec::::new(); - f.read_to_end(&mut content).unwrap_or_else(|e| { - warn!("Failed to read library proof timestamp: {}", e); - 0 - }); - content - }) - .unwrap_or_else(|e| { - warn!("Failed to open library proof timestamp: {}", e); - vec![] - }); - String::from_utf8_lossy(&content).to_string() - } - - pub fn save_library_proof_timestamp(&self, all_targets: &HashMap) { - let content = self.fingerprint_recursive(all_targets); - files::touch(self.library_proof_timestamp().to_string_lossy().as_ref()); - let mut file = File::create(self.library_proof_timestamp()).unwrap_or_else(|e| { - error!("Failed to create library proof timestamp: {}", e); - }); - file.write_all(content.as_bytes()).unwrap_or_else(|e| { - error!("Failed to write library proof timestamp: {}", e); - }); - } - pub fn library_path(&self) -> PathBuf { let lib = format!( "{}{}.{}", @@ -757,6 +613,9 @@ pub fn exec_verify(targets: &[VerusTarget], options: &ExtraOptions) -> Result<() let ts_start = Instant::now(); let cmd = &mut Command::new(get_cargo_verus(options.release)); cmd.arg(if options.focus { "focus" } else { "verify" }); + if !options.focus && verus_args_should_apply_to_roots_only(&options.pass_through) { + cmd.arg("--fwd-verus-args-to").arg("roots"); + } if let Some(target) = target { cmd.arg("-p").arg(&target.name); } @@ -853,6 +712,17 @@ pub fn exec_verify(targets: &[VerusTarget], options: &ExtraOptions) -> Result<() Ok(()) } +fn verus_args_should_apply_to_roots_only(args: &[String]) -> bool { + args.iter().any(|arg| { + matches!( + arg.as_str(), + "--verify-root" | "--verify-module" | "--verify-only-module" | "--verify-function" + ) || arg.starts_with("--verify-module=") + || arg.starts_with("--verify-only-module=") + || arg.starts_with("--verify-function=") + }) +} + pub fn disassemble(target: &VerusTarget) -> Result<(), DynError> { let objdump = commands::get_objdump(); let cmd = &mut Command::new(&objdump);