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-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index ca9e3d04959c..56f5142a1b19 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 `kani-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 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), + }; + 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 1b3b69b93385..c73d2a1bbdd2 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 cargo_metadata::{Message, Metadata, MetadataCommand, Package, Target}; +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::{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,12 +103,13 @@ 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) { + 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 @@ -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.extend(self.run_cargo(cmd, verification_target.target())?.into_iter()); 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 { @@ -165,9 +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, 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)? { let reader = BufReader::new(cargo_process.stdout.take().unwrap()); let mut error_count = 0; @@ -196,9 +190,16 @@ impl KaniSession { } } }, - Message::CompilerArtifact(_) - | Message::BuildScriptExecuted(_) - | Message::BuildFinished(_) => { + Message::CompilerArtifact(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 } Message::TextLine(msg) => { @@ -222,7 +223,11 @@ impl KaniSession { ); } } - Ok(()) + // 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)) } } @@ -236,15 +241,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,20 +272,69 @@ 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<>`. +/// +/// 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")?; + 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); + trace!(rmeta=?path, kani_meta=?meta_path.display(), "map_kani_artifact"); + + // This will check if the file exists and we just skip if it doesn't. + Artifact::try_new(&meta_path, ArtifactType::Metadata).ok() + } else if path.extension() == Some("rlib") { + // We skip `rlib` files since we should also generate a `rmeta`. + trace!(rlib=?path, "map_kani_artifact"); + None + } else { + // For all the other cases we write the path of the metadata into the output file. + // The compiler should always write a valid stub into the artifact file, however the + // kani-metadata file only exists if there were valid targets. + trace!(artifact=?path, "map_kani_artifact"); + let input_file = File::open(path).ok()?; + let stub: CompilerArtifactStub = serde_json::from_reader(input_file).unwrap(); + Artifact::try_new(&stub.metadata_path, ArtifactType::Metadata).ok() + } + }); + debug!(?result, "map_kani_artifact"); + result +} + /// Possible verification targets. enum VerificationTarget { - Bin(String), - Lib, - Test(String), + Bin(Target), + Lib(Target), + Test(Target), } impl VerificationTarget { /// Convert to cargo argument that select the specific target. fn to_args(&self) -> 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, } } } @@ -318,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 => { @@ -331,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()); } @@ -347,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())), (_, _) => {} } } diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index 8e5c31925fe8..39d7ca103f21 100644 --- a/kani-driver/src/main.rs +++ b/kani-driver/src/main.rs @@ -70,6 +70,7 @@ fn cargokani_main(input_args: Vec) -> 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 diff --git a/kani-driver/src/project.rs b/kani-driver/src/project.rs index 043ec2994f55..d0a27136dec6 100644 --- a/kani-driver/src/project.rs +++ b/kani-driver/src/project.rs @@ -98,7 +98,7 @@ impl Project { } /// Information about a build artifact. -#[derive(Debug, Eq, PartialEq, Clone)] +#[derive(Debug, Eq, PartialEq, Clone, Hash)] pub struct Artifact { /// The path for this artifact in the canonical form. path: PathBuf, @@ -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, diff --git a/kani_metadata/src/lib.rs b/kani_metadata/src/lib.rs index 56158599e0f4..7da3cbb94121 100644 --- a/kani_metadata/src/lib.rs +++ b/kani_metadata/src/lib.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -use std::collections::HashSet; +use std::{collections::HashSet, path::PathBuf}; use serde::{Deserialize, Serialize}; @@ -44,3 +44,9 @@ pub struct Location { pub filename: String, pub start_line: u64, } + +/// We stub artifacts with the path to a KaniMetadata file. +#[derive(Debug, Clone, Serialize, Deserialize)] +pub struct CompilerArtifactStub { + pub metadata_path: PathBuf, +}