Remove glob to collect all artifacts introduced by cargo kani

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"]
 

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,34 +216,48 @@ 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 <https://github.com/model-checking/kani/issues/2234> for more details.
     fn link(
         &self,
         sess: &Session,
         codegen_results: CodegenResults,
         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: `<crate>.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: `<crate>.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(())
     }
 }

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<PathBuf>,
-    /// The location of vtable restrictions files (a directory of *.restrictions.json)
-    pub restrictions: Option<PathBuf>,
     /// The kani-metadata.json files written by kani-compiler.
-    pub metadata: Vec<PathBuf>,
+    pub metadata: Vec<Artifact>,
     /// Recording the cargo metadata from the build
     pub cargo_metadata: Metadata,
 }
@@ -105,20 +103,21 @@ 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
                     // https://doc.rust-lang.org/cargo/reference/environment-variables.html
                     .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<Metadata> {
@@ -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<Option<Artifact>> {
         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<Vec<PathBuf>> {
-    let results = glob::glob(path.to_str().context("Non-UTF-8 path enountered")?)?;
-    // the logic to turn "Iter<Result<T, E>>" into "Result<Vec<T>, E>" doesn't play well
-    // with anyhow, so a type annotation is required
-    let v: core::result::Result<Vec<PathBuf>, glob::GlobError> = results.collect();
-    Ok(v?)
-}
-
 /// Extract the packages that should be verified.
 /// If `--package <pkg>` 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 <https://github.com/model-checking/kani/issues/2234> for more details.
+fn map_kani_artifact(rustc_artifact: cargo_metadata::Artifact) -> Option<Artifact> {
+    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<String> {
         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<VerificationTarget
             match kind.as_str() {
                 CRATE_TYPE_BIN => {
                     // 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<VerificationTarget
                 CRATE_TYPE_TEST => {
                     // 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<VerificationTarget
                         `proc-macro`.",
                 target.name,
             ),
-            (true, false) => verification_targets.push(VerificationTarget::Lib),
+            (true, false) => verification_targets.push(VerificationTarget::Lib(target.clone())),
             (_, _) => {}
         }
     }

kani-driver/src/main.rs

@@ -70,6 +70,7 @@ fn cargokani_main(input_args: Vec<OsString>) -> 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) }
 }
 

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