Remove glob to collect all artifacts introduced by cargo kani

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 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,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.extend(self.run_cargo(cmd)?.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) -> 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,10 @@ impl KaniSession {
                             }
                         }
                     },
-                    Message::CompilerArtifact(_)
-                    | Message::BuildScriptExecuted(_)
-                    | Message::BuildFinished(_) => {
+                    Message::CompilerArtifact(rustc_artifact) => {
+                        artifact = Some(rustc_artifact);
+                    }
+                    Message::BuildScriptExecuted(_) | Message::BuildFinished(_) => {
                         // do nothing
                     }
                     Message::TextLine(msg) => {
@@ -222,7 +217,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 +235,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,6 +266,42 @@ 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);
+
+            // 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`.
+            None
+        } else {
+            // For all the other cases we write the path of the metadata into the output file.
+            let input_file = File::open(path).ok()?;
+            let stub: CompilerArtifactStub = serde_json::from_reader(input_file).ok()?;
+            Artifact::try_new(&stub.metadata_path, ArtifactType::Metadata).ok()
+        }
+    });
+    debug!(?result, "map_kani_artifact");
+    result
+}
+
 /// Possible verification targets.
 enum VerificationTarget {
     Bin(String),

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<Self> {
+    pub fn try_new(path: &Path, typ: ArtifactType) -> Result<Self> {
         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<Project> {
         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::<Vec<_>>();
+        session.link_goto_binary(&all_gotos, &goto)?;
         artifacts.push(Artifact::try_new(&goto, Goto)?);
 
         // Merge metadata files.

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,

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,
+}