From b8206449a13e79895096646132e08bb50a8162a1 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 24 Feb 2023 12:42:35 -0800 Subject: [PATCH 1/5] Remove glob from cargo call Looking at the artifacts doesn't always work since Kani doesn't produce any artifact for binary, tests, static / shared library. Need to find a better solution. --- kani-driver/src/call_cargo.rs | 66 ++++++++++++++++++++--------------- kani-driver/src/project.rs | 13 +++++-- kani_metadata/src/artifact.rs | 2 +- 3 files changed, 49 insertions(+), 32 deletions(-) diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index 1b3b69b93385..a98b0f1d37d7 100644 --- a/kani-driver/src/call_cargo.rs +++ b/kani-driver/src/call_cargo.rs @@ -3,14 +3,16 @@ use crate::args::KaniArgs; use crate::call_single_file::to_rustc_arg; +use crate::project::Artifact; use crate::session::KaniSession; use anyhow::{bail, Context, Result}; use cargo_metadata::diagnostic::{Diagnostic, DiagnosticLevel}; use cargo_metadata::{Message, Metadata, MetadataCommand, Package}; +use kani_metadata::ArtifactType; use std::ffi::{OsStr, OsString}; use std::fs; use std::io::BufReader; -use std::path::{Path, PathBuf}; +use std::path::PathBuf; use std::process::Command; use tracing::{debug, trace}; @@ -29,12 +31,8 @@ pub struct CargoOutputs { /// The directory where compiler outputs should be directed. /// Usually 'target/BUILD_TRIPLE/debug/deps/' pub outdir: PathBuf, - /// The collection of *.symtab.out goto binary files written. - pub symtab_gotos: Vec, - /// The location of vtable restrictions files (a directory of *.restrictions.json) - pub restrictions: Option, /// The kani-metadata.json files written by kani-compiler. - pub metadata: Vec, + pub metadata: Vec, /// Recording the cargo metadata from the build pub cargo_metadata: Metadata, } @@ -105,6 +103,7 @@ impl KaniSession { let mut found_target = false; let packages = packages_to_verify(&self.args, &metadata); + let mut artifacts = vec![]; for package in packages { for target in package_targets(&self.args, package) { let mut cmd = Command::new("cargo"); @@ -118,7 +117,7 @@ impl KaniSession { .env("CARGO_ENCODED_RUSTFLAGS", rustc_args.join(OsStr::new("\x1f"))) .env("CARGO_TERM_PROGRESS_WHEN", "never"); - self.run_cargo(cmd)?; + artifacts.append(&mut self.run_cargo(cmd)?); found_target = true; } } @@ -127,13 +126,7 @@ impl KaniSession { bail!("No supported targets were found."); } - Ok(CargoOutputs { - outdir: outdir.clone(), - symtab_gotos: glob(&outdir.join("*.symtab.out"))?, - metadata: glob(&outdir.join("*.kani-metadata.json"))?, - restrictions: self.args.restrict_vtable().then_some(outdir), - cargo_metadata: metadata, - }) + Ok(CargoOutputs { outdir, metadata: artifacts, cargo_metadata: metadata }) } fn cargo_metadata(&self, build_target: &str) -> Result { @@ -166,8 +159,9 @@ impl KaniSession { /// Run cargo and collect any error found. /// TODO: We should also use this to collect the artifacts generated by cargo. - fn run_cargo(&self, cargo_cmd: Command) -> Result<()> { + fn run_cargo(&self, cargo_cmd: Command) -> Result> { let support_color = atty::is(atty::Stream::Stdout); + let mut artifacts = vec![]; if let Some(mut cargo_process) = self.run_piped(cargo_cmd)? { let reader = BufReader::new(cargo_process.stdout.take().unwrap()); let mut error_count = 0; @@ -196,9 +190,10 @@ impl KaniSession { } } }, - Message::CompilerArtifact(_) - | Message::BuildScriptExecuted(_) - | Message::BuildFinished(_) => { + Message::CompilerArtifact(rustc_artifact) => { + artifacts.extend(map_kani_artifact(rustc_artifact).into_iter()); + } + Message::BuildScriptExecuted(_) | Message::BuildFinished(_) => { // do nothing } Message::TextLine(msg) => { @@ -222,7 +217,7 @@ impl KaniSession { ); } } - Ok(()) + Ok(artifacts) } } @@ -236,15 +231,6 @@ fn print_msg(diagnostic: &Diagnostic, use_rendered: bool) -> Result<()> { Ok(()) } -/// Given a `path` with glob characters in it (e.g. `*.json`), return a vector of matching files -fn glob(path: &Path) -> Result> { - let results = glob::glob(path.to_str().context("Non-UTF-8 path enountered")?)?; - // the logic to turn "Iter>" into "Result, E>" doesn't play well - // with anyhow, so a type annotation is required - let v: core::result::Result, glob::GlobError> = results.collect(); - Ok(v?) -} - /// Extract the packages that should be verified. /// If `--package ` is given, return the list of packages selected. /// If `--workspace` is given, return the list of workspace members. @@ -276,6 +262,30 @@ fn packages_to_verify<'b>(args: &KaniArgs, metadata: &'b Metadata) -> Vec<&'b Pa packages } +/// Extract Kani artifact that might've been generated from a given rustc artifact. +/// Not every rustc artifact will map to a kani artifact, hence the `Option<>`. +fn map_kani_artifact(rustc_artifact: cargo_metadata::Artifact) -> Option { + debug!(?rustc_artifact, "map_kani_artifact"); + let result = rustc_artifact.filenames.iter().find_map(|path| { + if path.extension() == Some("rmeta") { + let file_stem = path.file_stem()?.strip_prefix("lib")?; + let parent = + path.parent().map(|p| p.as_std_path().to_path_buf()).unwrap_or(PathBuf::new()); + let mut meta_path = parent.join(file_stem); + meta_path.set_extension(ArtifactType::Metadata); + + println!("{} Match: {}", path.extension().unwrap(), meta_path.display()); + // This will check if the file exists and we just skip if it doesn't. + Artifact::try_new(&meta_path, ArtifactType::Metadata).ok() + } else { + None + } + }); + debug!(?result, "map_kani_artifact"); + println!("Artifact: {rustc_artifact:?} Result: {result:?}"); + result +} + /// Possible verification targets. enum VerificationTarget { Bin(String), diff --git a/kani-driver/src/project.rs b/kani-driver/src/project.rs index 043ec2994f55..4222dbbbce13 100644 --- a/kani-driver/src/project.rs +++ b/kani-driver/src/project.rs @@ -121,12 +121,12 @@ impl Deref for Artifact { impl Artifact { /// Create a new artifact if the given path exists. - fn try_new(path: &Path, typ: ArtifactType) -> Result { + pub fn try_new(path: &Path, typ: ArtifactType) -> Result { Ok(Artifact { path: path.canonicalize()?, typ }) } /// Check if this artifact has the given type. - fn has_type(&self, typ: ArtifactType) -> bool { + pub fn has_type(&self, typ: ArtifactType) -> bool { self.typ == typ } } @@ -156,7 +156,14 @@ pub fn cargo_project(session: &KaniSession) -> Result { let joined_name = "cbmc-linked"; let base_name = outdir.join(joined_name); let goto = base_name.with_extension(Goto); - session.link_goto_binary(&outputs.symtab_gotos, &goto)?; + let all_gotos = outputs + .metadata + .iter() + .map(|artifact| { + convert_type(&artifact, ArtifactType::Metadata, ArtifactType::SymTabGoto) + }) + .collect::>(); + session.link_goto_binary(&all_gotos, &goto)?; artifacts.push(Artifact::try_new(&goto, Goto)?); // Merge metadata files. diff --git a/kani_metadata/src/artifact.rs b/kani_metadata/src/artifact.rs index 55db234e51c3..54ff7a025e19 100644 --- a/kani_metadata/src/artifact.rs +++ b/kani_metadata/src/artifact.rs @@ -11,7 +11,7 @@ use std::path::{Path, PathBuf}; pub enum ArtifactType { /// A complete goto model generated after linking. Goto, - /// The metadata generated by the compiler. + /// The metadata generated by the kani compiler. Metadata, /// The `json` file that represents the symbol table generated by the compiler. SymTab, From 3638801fa53defb3eae8caa643020308ccd3f913 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 27 Feb 2023 17:06:10 -0800 Subject: [PATCH 2/5] Replace glob by hacky file stub --- .../compiler_interface.rs | 57 ++++++++++++------- kani-driver/src/call_cargo.rs | 34 +++++++---- kani-driver/src/project.rs | 2 +- kani_metadata/src/lib.rs | 8 ++- 4 files changed, 67 insertions(+), 34 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index ca9e3d04959c..a13bfdef2cb3 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -15,6 +15,7 @@ use crate::kani_middle::reachability::{ use bitflags::_core::any::Any; use cbmc::goto_program::Location; use cbmc::{InternedString, MachineModel}; +use kani_metadata::CompilerArtifactStub; use kani_metadata::{ArtifactType, HarnessMetadata, KaniMetadata}; use kani_queries::{QueryDb, ReachabilityType, UserInput}; use rustc_codegen_ssa::back::metadata::create_wrapper_file; @@ -205,7 +206,7 @@ impl CodegenBackend for GotocCodegenBackend { .unwrap()) } - /// Emit `rlib` files during the link stage if it was requested. + /// Emit output files during the link stage if it was requested. /// /// We need to emit `rlib` files normally if requested. Cargo expects these in some /// circumstances and sends them to subsequent builds with `-L`. @@ -215,6 +216,10 @@ impl CodegenBackend for GotocCodegenBackend { /// Types such as `bin`, `cdylib`, `dylib` will trigger the native linker. /// /// Thus, we manually build the rlib file including only the `rmeta` file. + /// + /// For cases where no metadata file was requested, we stub the file requested by writing the + /// path of the `metadata.json` file so `kani-driver` can safely find the latest metadata. + /// See for more details. fn link( &self, sess: &Session, @@ -222,27 +227,37 @@ impl CodegenBackend for GotocCodegenBackend { outputs: &OutputFilenames, ) -> Result<(), ErrorGuaranteed> { let requested_crate_types = sess.crate_types(); - if !requested_crate_types.contains(&CrateType::Rlib) { - // Quit successfully if we don't need an `rlib`: - return Ok(()); + for crate_type in requested_crate_types { + let out_path = out_filename( + sess, + *crate_type, + outputs, + codegen_results.crate_info.local_crate_name, + ); + debug!(?crate_type, ?out_path, "link"); + if *crate_type == CrateType::Rlib { + // Emit the `rlib` that contains just one file: `.rmeta` + let mut builder = ArchiveBuilder::new(sess); + let tmp_dir = TempFileBuilder::new().prefix("kani").tempdir().unwrap(); + let path = MaybeTempDir::new(tmp_dir, sess.opts.cg.save_temps); + let (metadata, _metadata_position) = create_wrapper_file( + sess, + b".rmeta".to_vec(), + codegen_results.metadata.raw_data(), + ); + let metadata = emit_wrapper_file(sess, &metadata, &path, METADATA_FILENAME); + builder.add_file(&metadata); + builder.build(&out_path); + } else { + // Write the location of the metadata file to the requested type. + let base_filename = outputs.output_path(OutputType::Object); + let content_stub = CompilerArtifactStub { + metadata_path: base_filename.with_extension(ArtifactType::Metadata), + }; + let out_file = File::create(out_path).unwrap(); + serde_json::to_writer(out_file, &content_stub).unwrap(); + } } - - // Emit the `rlib` that contains just one file: `.rmeta` - let mut builder = ArchiveBuilder::new(sess); - let tmp_dir = TempFileBuilder::new().prefix("kani").tempdir().unwrap(); - let path = MaybeTempDir::new(tmp_dir, sess.opts.cg.save_temps); - let (metadata, _metadata_position) = - create_wrapper_file(sess, b".rmeta".to_vec(), codegen_results.metadata.raw_data()); - let metadata = emit_wrapper_file(sess, &metadata, &path, METADATA_FILENAME); - builder.add_file(&metadata); - - let rlib = out_filename( - sess, - CrateType::Rlib, - outputs, - codegen_results.crate_info.local_crate_name, - ); - builder.build(&rlib); Ok(()) } } diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index a98b0f1d37d7..b39e567df477 100644 --- a/kani-driver/src/call_cargo.rs +++ b/kani-driver/src/call_cargo.rs @@ -8,9 +8,9 @@ use crate::session::KaniSession; use anyhow::{bail, Context, Result}; use cargo_metadata::diagnostic::{Diagnostic, DiagnosticLevel}; use cargo_metadata::{Message, Metadata, MetadataCommand, Package}; -use kani_metadata::ArtifactType; +use kani_metadata::{ArtifactType, CompilerArtifactStub}; use std::ffi::{OsStr, OsString}; -use std::fs; +use std::fs::{self, File}; use std::io::BufReader; use std::path::PathBuf; use std::process::Command; @@ -117,7 +117,7 @@ impl KaniSession { .env("CARGO_ENCODED_RUSTFLAGS", rustc_args.join(OsStr::new("\x1f"))) .env("CARGO_TERM_PROGRESS_WHEN", "never"); - artifacts.append(&mut self.run_cargo(cmd)?); + artifacts.extend(self.run_cargo(cmd)?.into_iter()); found_target = true; } } @@ -158,10 +158,10 @@ impl KaniSession { } /// Run cargo and collect any error found. - /// TODO: We should also use this to collect the artifacts generated by cargo. - fn run_cargo(&self, cargo_cmd: Command) -> Result> { + /// We also collect the metadata file generated during compilation if any. + fn run_cargo(&self, cargo_cmd: Command) -> Result> { let support_color = atty::is(atty::Stream::Stdout); - let mut artifacts = vec![]; + let mut artifact = None; if let Some(mut cargo_process) = self.run_piped(cargo_cmd)? { let reader = BufReader::new(cargo_process.stdout.take().unwrap()); let mut error_count = 0; @@ -191,7 +191,7 @@ impl KaniSession { } }, Message::CompilerArtifact(rustc_artifact) => { - artifacts.extend(map_kani_artifact(rustc_artifact).into_iter()); + artifact = Some(rustc_artifact); } Message::BuildScriptExecuted(_) | Message::BuildFinished(_) => { // do nothing @@ -217,7 +217,7 @@ impl KaniSession { ); } } - Ok(artifacts) + Ok(artifact.and_then(map_kani_artifact)) } } @@ -264,8 +264,16 @@ fn packages_to_verify<'b>(args: &KaniArgs, metadata: &'b Metadata) -> Vec<&'b Pa /// Extract Kani artifact that might've been generated from a given rustc artifact. /// Not every rustc artifact will map to a kani artifact, hence the `Option<>`. +/// +/// Unfortunately, we cannot always rely on the messages to get the path for the original artifact +/// that `rustc` produces. So we hack the content of the output path to point to the original +/// metadata file. See for more details. fn map_kani_artifact(rustc_artifact: cargo_metadata::Artifact) -> Option { debug!(?rustc_artifact, "map_kani_artifact"); + if rustc_artifact.target.is_custom_build() { + // We don't verify custom builds. + return None; + } let result = rustc_artifact.filenames.iter().find_map(|path| { if path.extension() == Some("rmeta") { let file_stem = path.file_stem()?.strip_prefix("lib")?; @@ -274,15 +282,19 @@ fn map_kani_artifact(rustc_artifact: cargo_metadata::Artifact) -> Option Date: Wed, 1 Mar 2023 21:23:02 -0800 Subject: [PATCH 3/5] Address PR comments --- kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs | 4 ++-- kani-driver/src/call_cargo.rs | 4 ++++ 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index a13bfdef2cb3..56f5142a1b19 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -218,7 +218,7 @@ impl CodegenBackend for GotocCodegenBackend { /// Thus, we manually build the rlib file including only the `rmeta` file. /// /// For cases where no metadata file was requested, we stub the file requested by writing the - /// path of the `metadata.json` file so `kani-driver` can safely find the latest metadata. + /// path of the `kani-metadata.json` file so `kani-driver` can safely find the latest metadata. /// See for more details. fn link( &self, @@ -249,7 +249,7 @@ impl CodegenBackend for GotocCodegenBackend { builder.add_file(&metadata); builder.build(&out_path); } else { - // Write the location of the metadata file to the requested type. + // Write the location of the kani metadata file in the requested compiler output file. let base_filename = outputs.output_path(OutputType::Object); let content_stub = CompilerArtifactStub { metadata_path: base_filename.with_extension(ArtifactType::Metadata), diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index b39e567df477..bcf659665707 100644 --- a/kani-driver/src/call_cargo.rs +++ b/kani-driver/src/call_cargo.rs @@ -217,6 +217,10 @@ impl KaniSession { ); } } + // We generate kani specific artifacts only for the build target. The build target is + // always the last artifact generated in a build, and all the other artifacts are related + // to dependencies or build scripts. Hence, we need to invoke `map_kani_artifact` only + // for the last compiler artifact. Ok(artifact.and_then(map_kani_artifact)) } } From 789dc19e791d7eb4f3312b95a5acc0ba1fbdb5d0 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 2 Mar 2023 10:09:39 -0800 Subject: [PATCH 4/5] Add more logs + improve error handling --- kani-driver/src/call_cargo.rs | 7 ++++++- kani-driver/src/main.rs | 2 ++ kani-driver/src/metadata.rs | 4 +++- 3 files changed, 11 insertions(+), 2 deletions(-) diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index bcf659665707..57514c3af17c 100644 --- a/kani-driver/src/call_cargo.rs +++ b/kani-driver/src/call_cargo.rs @@ -285,16 +285,21 @@ fn map_kani_artifact(rustc_artifact: cargo_metadata::Artifact) -> Option) -> Result<()> { } let project = project::cargo_project(&session)?; + debug!(?project, "cargokani_main"); if session.args.only_codegen { Ok(()) } else { verify_project(project, session) } } @@ -80,6 +81,7 @@ fn standalone_main() -> Result<()> { let session = session::KaniSession::new(args.common_opts)?; let project = project::standalone_project(&args.input, &session)?; + debug!(?project, "standalone_main"); if session.args.only_codegen { Ok(()) } else { verify_project(project, session) } } diff --git a/kani-driver/src/metadata.rs b/kani-driver/src/metadata.rs index 13c200f6f90f..0e10a3077880 100644 --- a/kani-driver/src/metadata.rs +++ b/kani-driver/src/metadata.rs @@ -3,7 +3,7 @@ use anyhow::Result; use std::path::Path; -use tracing::debug; +use tracing::{debug, trace}; use kani_metadata::{ HarnessAttributes, HarnessMetadata, InternedString, KaniMetadata, TraitDefinedMethod, @@ -178,6 +178,8 @@ fn find_proof_harnesses<'a>( || targets.iter().any(|target| md.pretty_name.contains(*target)) { result.push(*md); + } else { + trace!(skip = md.pretty_name, "find_proof_harnesses"); } } result From c920caa1f90e1303add8fe66707304f40b419d54 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 2 Mar 2023 20:19:33 -0800 Subject: [PATCH 5/5] Fix flaky behavior when artifact is reported out of order --- kani-compiler/Cargo.toml | 4 ++-- kani-driver/src/call_cargo.rs | 44 +++++++++++++++++++++++------------ 2 files changed, 31 insertions(+), 17 deletions(-) diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index f1d57948c3a0..f8770975702c 100644 --- a/kani-compiler/Cargo.toml +++ b/kani-compiler/Cargo.toml @@ -17,7 +17,7 @@ clap = { version = "4.1.3", features = ["cargo"] } home = "0.5" itertools = "0.10" kani_queries = {path = "kani_queries"} -kani_metadata = { path = "../kani_metadata", optional = true } +kani_metadata = {path = "../kani_metadata"} lazy_static = "1.4.0" libc = { version = "0.2", optional = true } num = { version = "0.4.0", optional = true } @@ -36,7 +36,7 @@ tracing-tree = "0.2.2" # Future proofing: enable backend dependencies using feature. [features] default = ['cprover'] -cprover = ['ar', 'bitflags', 'cbmc', 'kani_metadata', 'libc', 'num', 'object', 'rustc-demangle', 'serde', +cprover = ['ar', 'bitflags', 'cbmc', 'libc', 'num', 'object', 'rustc-demangle', 'serde', 'serde_json', "strum", "strum_macros"] unsound_experiments = ["kani_queries/unsound_experiments"] diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index 57514c3af17c..c73d2a1bbdd2 100644 --- a/kani-driver/src/call_cargo.rs +++ b/kani-driver/src/call_cargo.rs @@ -7,7 +7,7 @@ use crate::project::Artifact; use crate::session::KaniSession; use anyhow::{bail, Context, Result}; use cargo_metadata::diagnostic::{Diagnostic, DiagnosticLevel}; -use cargo_metadata::{Message, Metadata, MetadataCommand, Package}; +use cargo_metadata::{Message, Metadata, MetadataCommand, Package, Target}; use kani_metadata::{ArtifactType, CompilerArtifactStub}; use std::ffi::{OsStr, OsString}; use std::fs::{self, File}; @@ -105,11 +105,11 @@ impl KaniSession { let packages = packages_to_verify(&self.args, &metadata); let mut artifacts = vec![]; for package in packages { - for target in package_targets(&self.args, package) { + for verification_target in package_targets(&self.args, package) { let mut cmd = Command::new("cargo"); cmd.args(&cargo_args) .args(vec!["-p", &package.name]) - .args(&target.to_args()) + .args(&verification_target.to_args()) .args(&pkg_args) .env("RUSTC", &self.kani_compiler) // Use CARGO_ENCODED_RUSTFLAGS instead of RUSTFLAGS is preferred. See @@ -117,7 +117,7 @@ impl KaniSession { .env("CARGO_ENCODED_RUSTFLAGS", rustc_args.join(OsStr::new("\x1f"))) .env("CARGO_TERM_PROGRESS_WHEN", "never"); - artifacts.extend(self.run_cargo(cmd)?.into_iter()); + artifacts.extend(self.run_cargo(cmd, verification_target.target())?.into_iter()); found_target = true; } } @@ -159,7 +159,7 @@ impl KaniSession { /// Run cargo and collect any error found. /// We also collect the metadata file generated during compilation if any. - fn run_cargo(&self, cargo_cmd: Command) -> Result> { + fn run_cargo(&self, cargo_cmd: Command, target: &Target) -> Result> { let support_color = atty::is(atty::Stream::Stdout); let mut artifact = None; if let Some(mut cargo_process) = self.run_piped(cargo_cmd)? { @@ -191,7 +191,13 @@ impl KaniSession { } }, Message::CompilerArtifact(rustc_artifact) => { - artifact = Some(rustc_artifact); + if rustc_artifact.target == *target { + debug_assert!( + artifact.is_none(), + "expected only one artifact for `{target:?}`", + ); + artifact = Some(rustc_artifact); + } } Message::BuildScriptExecuted(_) | Message::BuildFinished(_) => { // do nothing @@ -309,18 +315,26 @@ fn map_kani_artifact(rustc_artifact: cargo_metadata::Artifact) -> Option Vec { match self { - VerificationTarget::Test(name) => vec![String::from("--test"), name.clone()], - VerificationTarget::Bin(name) => vec![String::from("--bin"), name.clone()], - VerificationTarget::Lib => vec![String::from("--lib")], + VerificationTarget::Test(target) => vec![String::from("--test"), target.name.clone()], + VerificationTarget::Bin(target) => vec![String::from("--bin"), target.name.clone()], + VerificationTarget::Lib(_) => vec![String::from("--lib")], + } + } + + fn target(&self) -> &Target { + match self { + VerificationTarget::Test(target) + | VerificationTarget::Bin(target) + | VerificationTarget::Lib(target) => target, } } } @@ -349,7 +363,7 @@ fn package_targets(args: &KaniArgs, package: &Package) -> Vec { // Binary targets. - verification_targets.push(VerificationTarget::Bin(target.name.clone())); + verification_targets.push(VerificationTarget::Bin(target.clone())); } CRATE_TYPE_LIB | CRATE_TYPE_RLIB | CRATE_TYPE_CDYLIB | CRATE_TYPE_DYLIB | CRATE_TYPE_STATICLIB => { @@ -362,7 +376,7 @@ fn package_targets(args: &KaniArgs, package: &Package) -> Vec { // Test target. if args.tests { - verification_targets.push(VerificationTarget::Test(target.name.clone())); + verification_targets.push(VerificationTarget::Test(target.clone())); } else { ignored_tests.push(target.name.as_str()); } @@ -378,7 +392,7 @@ fn package_targets(args: &KaniArgs, package: &Package) -> Vec verification_targets.push(VerificationTarget::Lib), + (true, false) => verification_targets.push(VerificationTarget::Lib(target.clone())), (_, _) => {} } }