Report correct package count in assess (rust-lang#2026)

Author: tedinski

kani-driver/src/assess/mod.rs

@@ -2,6 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 use anyhow::Result;
+use kani_metadata::KaniMetadata;
 
 use crate::metadata::merge_kani_metadata;
 use crate::project;
@@ -25,18 +26,28 @@ pub(crate) fn cargokani_assess_main(mut session: KaniSession) -> Result<()> {
     }
 
     let project = project::cargo_project(&session)?;
+    let cargo_metadata = project.cargo_metadata.as_ref().expect("built with cargo");
 
-    let crate_count = project.metadata.len();
+    let packages_metadata = if project.merged_artifacts {
+        // With the legacy linker we can't expect to find the metadata structure we'd expect
+        // so we just use it as-is. This does mean the "package count" will be wrong, but
+        // we will at least continue to see everything.
+        project.metadata.clone()
+    } else {
+        reconstruct_metadata_structure(cargo_metadata, &project.metadata)?
+    };
+
+    // We don't really have a list of crates that went into building our various targets,
+    // so we can't easily count them.
 
-    // An interesting thing to print here would be "number of crates without any warnings"
-    // however this will have to wait until a refactoring of how we aggregate metadata
-    // from multiple crates together here.
-    // tracking for that: https://github.com/model-checking/kani/issues/1758
-    println!("Analyzed {crate_count} crates");
+    // It would also be interesting to classify them by whether they build without warnings or not.
+    // Tracking for the latter: https://github.com/model-checking/kani/issues/1758
 
-    let metadata = merge_kani_metadata(project.metadata.clone());
+    println!("Found {} packages", packages_metadata.len());
+
+    let metadata = merge_kani_metadata(packages_metadata.clone());
     if !metadata.unsupported_features.is_empty() {
-        println!("{}", table_unsupported_features::build(&metadata));
+        println!("{}", table_unsupported_features::build(&packages_metadata));
     } else {
         println!("No crates contained Rust features unsupported by Kani");
     }
@@ -67,3 +78,41 @@ pub(crate) fn cargokani_assess_main(mut session: KaniSession) -> Result<()> {
 
     Ok(())
 }
+
+/// Merges a collection of Kani metadata by figuring out which package each belongs to, from cargo metadata.
+///
+/// This function, properly speaking, should not exist. We should have this information already from `Project`.
+/// This should function should be removable when we fix how driver handles metadata:
+/// <https://github.com/model-checking/kani/issues/1758>
+fn reconstruct_metadata_structure(
+    cargo_metadata: &cargo_metadata::Metadata,
+    kani_metadata: &[KaniMetadata],
+) -> Result<Vec<KaniMetadata>> {
+    let mut search = kani_metadata.to_owned();
+    let mut results = vec![];
+    for package in &cargo_metadata.packages {
+        let mut artifacts = vec![];
+        for target in &package.targets {
+            // cargo_metadata doesn't provide name mangling help here?
+            // we need to know cargo's name changes when it's given to rustc
+            let target_name = target.name.replace('-', "_");
+            if let Some(i) = search.iter().position(|x| x.crate_name == target_name) {
+                let md = search.swap_remove(i);
+                artifacts.push(md);
+            } else {
+                println!(
+                    "Didn't find metadata for target {} in package {}",
+                    target.name, package.name
+                )
+            }
+        }
+        let mut merged = crate::metadata::merge_kani_metadata(artifacts);
+        merged.crate_name = package.name.clone();
+        results.push(merged);
+    }
+    if !search.is_empty() {
+        let search_names: Vec<_> = search.into_iter().map(|x| x.crate_name).collect();
+        println!("Found remaining (unused) metadata after reconstruction: {:?}", search_names);
+    }
+    Ok(results)
+}

kani-driver/src/assess/table_failure_reasons.rs

@@ -68,7 +68,7 @@ impl TableRow for FailureReasonsTableRow {
     }
 
     fn compare(&self, right: &Self) -> Ordering {
-        self.count.cmp(&right.count).reverse()
+        self.count.cmp(&right.count).reverse().then_with(|| self.reason.cmp(&right.reason))
     }
 }
 

kani-driver/src/assess/table_unsupported_features.rs

@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-use std::cmp::Ordering;
+use std::{cmp::Ordering, collections::HashSet};
 
 use comfy_table::Table;
 use kani_metadata::KaniMetadata;
@@ -24,24 +24,26 @@ use super::table_builder::{ColumnType, RenderableTableRow, TableBuilder, TableRo
 ///  drop_in_place              |        2 |         2
 /// ===================================================
 /// ```
-pub(crate) fn build(metadata: &KaniMetadata) -> Table {
+pub(crate) fn build(metadata: &[KaniMetadata]) -> Table {
     let mut builder = TableBuilder::new();
 
-    for item in &metadata.unsupported_features {
-        // key is unsupported feature name
-        let mut key = item.feature.clone();
-        // There are several "feature for <instance of use>" unsupported features.
-        // We aggregate those here by reducing it to just "feature".
-        // We should replace this with an enum: https://github.com/model-checking/kani/issues/1765
-        if let Some((prefix, _)) = key.split_once(" for ") {
-            key = prefix.to_string();
+    for package_metadata in metadata {
+        for item in &package_metadata.unsupported_features {
+            // key is unsupported feature name
+            let mut key = item.feature.clone();
+            // There are several "feature for <instance of use>" unsupported features.
+            // We aggregate those here by reducing it to just "feature".
+            // We should replace this with an enum: https://github.com/model-checking/kani/issues/1765
+            if let Some((prefix, _)) = key.split_once(" for ") {
+                key = prefix.to_string();
+            }
+
+            builder.add(UnsupportedFeaturesTableRow {
+                unsupported_feature: key,
+                crates_impacted: HashSet::from([package_metadata.crate_name.to_owned()]),
+                instances_of_use: item.locations.len(),
+            })
         }
-
-        builder.add(UnsupportedFeaturesTableRow {
-            unsupported_feature: key,
-            crates_impacted: 1,
-            instances_of_use: item.locations.len(),
-        })
     }
 
     builder.render()
@@ -50,7 +52,7 @@ pub(crate) fn build(metadata: &KaniMetadata) -> Table {
 #[derive(Default)]
 pub struct UnsupportedFeaturesTableRow {
     pub unsupported_feature: String,
-    pub crates_impacted: usize,
+    pub crates_impacted: HashSet<String>,
     pub instances_of_use: usize,
 }
 
@@ -62,15 +64,17 @@ impl TableRow for UnsupportedFeaturesTableRow {
     }
 
     fn merge(&mut self, new: Self) {
-        self.crates_impacted += new.crates_impacted;
+        self.crates_impacted.extend(new.crates_impacted);
         self.instances_of_use += new.instances_of_use;
     }
 
     fn compare(&self, right: &Self) -> Ordering {
         self.crates_impacted
-            .cmp(&right.crates_impacted)
+            .len()
+            .cmp(&right.crates_impacted.len())
             .reverse()
             .then_with(|| self.instances_of_use.cmp(&right.instances_of_use).reverse())
+            .then_with(|| self.unsupported_feature.cmp(&right.unsupported_feature))
     }
 }
 impl RenderableTableRow for UnsupportedFeaturesTableRow {
@@ -86,7 +90,7 @@ impl RenderableTableRow for UnsupportedFeaturesTableRow {
     fn row(&self) -> Vec<String> {
         vec![
             self.unsupported_feature.clone(),
-            self.crates_impacted.to_string(),
+            self.crates_impacted.len().to_string(),
             self.instances_of_use.to_string(),
         ]
     }

kani-driver/src/call_cargo.rs

@@ -32,6 +32,8 @@ pub struct CargoOutputs {
     pub restrictions: Option<PathBuf>,
     /// The kani-metadata.json files written by kani-compiler.
     pub metadata: Vec<PathBuf>,
+    /// Recording the cargo metadata from the build
+    pub cargo_metadata: Metadata,
 }
 
 impl KaniSession {
@@ -133,6 +135,7 @@ impl KaniSession {
             symtabs: glob(&outdir.join("*.symtab.json"))?,
             metadata: glob(&outdir.join("*.kani-metadata.json"))?,
             restrictions: self.args.restrict_vtable().then_some(outdir),
+            cargo_metadata: metadata,
         })
     }
 }

kani-driver/src/project.rs

@@ -59,7 +59,9 @@ pub struct Project {
     /// When this flag is `true`, there should only be up to one artifact of any given type.
     /// When this flag is `false`, there may be multiple artifacts for any given type. However,
     /// only up to one artifact for each
-    merged_artifacts: bool,
+    pub merged_artifacts: bool,
+    /// Records the cargo metadata from the build, if there was any
+    pub cargo_metadata: Option<cargo_metadata::Metadata>,
 }
 
 impl Project {
@@ -171,7 +173,13 @@ pub fn cargo_project(session: &KaniSession) -> Result<Project> {
         dump_metadata(&metadata, &metadata_file);
         artifacts.push(Artifact::try_new(&metadata_file, Metadata)?);
 
-        Ok(Project { outdir, artifacts, metadata: vec![metadata], merged_artifacts: true })
+        Ok(Project {
+            outdir,
+            artifacts,
+            metadata: vec![metadata],
+            merged_artifacts: true,
+            cargo_metadata: Some(outputs.cargo_metadata),
+        })
     } else {
         // For the MIR Linker we know there is only one artifact per verification target. Use
         // that in our favor.
@@ -192,7 +200,13 @@ pub fn cargo_project(session: &KaniSession) -> Result<Project> {
             debug!(?crate_name, ?crate_metadata, "cargo_project");
             metadata.push(crate_metadata);
         }
-        Ok(Project { outdir, artifacts, metadata, merged_artifacts: false })
+        Ok(Project {
+            outdir,
+            artifacts,
+            metadata,
+            merged_artifacts: false,
+            cargo_metadata: Some(outputs.cargo_metadata),
+        })
     }
 }
 
@@ -283,6 +297,7 @@ impl<'a> StandaloneProjectBuilder<'a> {
                 .filter(|artifact| artifact.path.exists())
                 .collect(),
             merged_artifacts: false,
+            cargo_metadata: None,
         })
     }
 

tests/cargo-kani/assess-works/Cargo.toml renamed to tests/cargo-kani/assess-artifacts/Cargo.toml

@@ -2,12 +2,11 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [package]
-name = "assess-works"
+name = "assess-artifacts"
 version = "0.1.0"
 edition = "2021"
 
-[dependencies]
-anyhow = "1"
+# See src/lib.rs for a comment on this tests's purpose
 
 [package.metadata.kani]
 flags = { assess=true, enable-unstable=true }

tests/cargo-kani/assess-artifacts/expected

@@ -0,0 +1,19 @@
+Found 1 packages
+============================================
+ Unsupported feature |   Crates | Instances
+                     | impacted |    of use
+---------------------+----------+-----------
+ try                 |        1 |         2
+============================================
+=========================================
+ Reason for failure    | Number of tests
+-----------------------+-----------------
+ none (success)        |               2
+ unsupported_construct |               2
+=========================================
+======================================================================================================
+ Candidate for proof harness   | Location
+-------------------------------+----------------------------------------------------------------------
+ a_supported_test_from_tests   |
+ a_supported_test_from_the_lib |
+======================================================================================================

tests/cargo-kani/assess-artifacts/src/lib.rs

@@ -0,0 +1,19 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test ensures:
+//!   1. Assess is able to correctly build and report on a package
+//!   2. Assess is able to correctly count the number of packages (1),
+//!      in the presence of an integration test (which might otherwise
+//!      look like two crates: 'assess-artifact' and 'integ')
+
+#[test]
+fn an_unsupported_test_from_the_lib() {
+    // unsupported feature: try instrinsic
+    assert!(std::panic::catch_unwind(|| panic!("test")).is_err());
+}
+
+#[test]
+fn a_supported_test_from_the_lib() {
+    assert!(1 == 1);
+}

tests/cargo-kani/assess-artifacts/tests/integ.rs

@@ -0,0 +1,13 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#[test]
+fn an_unsupported_test_from_tests() {
+    // unsupported feature: try instrinsic
+    assert!(std::panic::catch_unwind(|| panic!("test")).is_err());
+}
+
+#[test]
+fn a_supported_test_from_tests() {
+    assert!(1 == 1);
+}

tests/cargo-kani/assess-works/expected

@@ -0,0 +1,15 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "assess-artifacts"
+version = "0.1.0"
+edition = "2021"
+
+# See src/lib.rs for a comment on this tests's purpose
+
+[package.metadata.kani]
+flags = { assess=true, enable-unstable=true, workspace=true }
+
+[workspace]
+members = ["subpackage"]

tests/cargo-kani/assess-works/src/main.rs

@@ -0,0 +1,20 @@
+Found 2 packages
+============================================
+ Unsupported feature |   Crates | Instances
+                     | impacted |    of use
+---------------------+----------+-----------
+ try                 |        2 |         3
+============================================
+=========================================
+ Reason for failure    | Number of tests
+-----------------------+-----------------
+ unsupported_construct |               3
+ none (success)        |               3
+=========================================
+=======================================================================================================================
+ Candidate for proof harness          | Location
+--------------------------------------+--------------------------------------------------------------------------------
+ a_supported_test_from_tests          |
+ a_supported_test_from_the_lib        |
+ a_supported_test_from_the_subpackage |
+=======================================================================================================================

tests/cargo-kani/assess-workspace-artifacts/Cargo.toml

@@ -0,0 +1,20 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test ensures:
+//!   1. Assess is able to correctly build and report on a _workspace_
+//!   2. Assess is able to correctly count the number of packages (2),
+//!      in the presence of an integration test (which might otherwise
+//!      look like three crates:
+//!       'assess-artifact', 'subpackage', and 'integ')
+
+#[test]
+fn an_unsupported_test_from_the_lib() {
+    // unsupported feature: try instrinsic
+    assert!(std::panic::catch_unwind(|| panic!("test")).is_err());
+}
+
+#[test]
+fn a_supported_test_from_the_lib() {
+    assert!(1 == 1);
+}