Assess improvements: build tolerance, detect CBMC crashes, allow set default unwind (rust-lang#2267)

I made a few improvements while trying to use assess:

- Allow assess to keep building packages even when one or more targets failed to build. Instead, just report how many failed and how many succeeded.
- Fix test result reporting for cases where CBMC crashes. We were counting them as success. Now we report the error code.
- Allow users to set the default unwind value using --default-unwind. By default, we still use value 1.
- Only report as analyzed crates that have any kani-metadata.json file.

Author: celinval

kani-driver/src/assess/mod.rs

@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 use self::metadata::{write_metadata, AssessMetadata};
-use anyhow::Result;
+use anyhow::{bail, Result};
 use kani_metadata::KaniMetadata;
 
 use crate::assess::table_builder::TableBuilder;
@@ -44,7 +44,7 @@ fn assess_project(mut session: KaniSession) -> Result<AssessMetadata> {
     // This is a temporary hack to make things work, until we get around to refactoring how arguments
     // work generally in kani-driver. These arguments, for instance, are all prepended to the subcommand,
     // which is not a nice way of taking arguments.
-    session.args.unwind = Some(1);
+    session.args.unwind = Some(session.args.default_unwind.unwrap_or(1));
     session.args.tests = true;
     session.args.output_format = crate::args::OutputFormat::Terse;
     session.codegen_tests = true;
@@ -54,7 +54,7 @@ fn assess_project(mut session: KaniSession) -> Result<AssessMetadata> {
         session.args.jobs = Some(None); // -j, num_cpu
     }
 
-    let project = project::cargo_project(&session)?;
+    let project = project::cargo_project(&session, true)?;
     let cargo_metadata = project.cargo_metadata.as_ref().expect("built with cargo");
 
     let packages_metadata = if project.merged_artifacts {
@@ -72,7 +72,15 @@ fn assess_project(mut session: KaniSession) -> Result<AssessMetadata> {
     // 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
 
-    println!("Found {} packages", packages_metadata.len());
+    let build_fail = project.failed_targets.as_ref().unwrap();
+    match (build_fail.len(), packages_metadata.len()) {
+        (0, 0) => println!("No relevant data was found."),
+        (0, succeeded) => println!("Analyzed {succeeded} packages"),
+        (_failed, 0) => bail!("Failed to build all targets"),
+        (failed, succeeded) => {
+            println!("Analyzed {succeeded} packages. Failed to build {failed} targets",)
+        }
+    }
 
     let metadata = merge_kani_metadata(packages_metadata.clone());
     let unsupported_features = table_unsupported_features::build(&packages_metadata);
@@ -161,9 +169,11 @@ fn reconstruct_metadata_structure(
                 )
             }
         }
-        let mut merged = crate::metadata::merge_kani_metadata(package_artifacts);
-        merged.crate_name = package.name.clone();
-        package_metas.push(merged);
+        if !package_artifacts.is_empty() {
+            let mut merged = crate::metadata::merge_kani_metadata(package_artifacts);
+            merged.crate_name = package.name.clone();
+            package_metas.push(merged);
+        }
     }
     if !remaining_metas.is_empty() {
         let remaining_names: Vec<_> = remaining_metas.into_iter().map(|x| x.crate_name).collect();

kani-driver/src/assess/table_failure_reasons.rs

@@ -35,14 +35,19 @@ pub(crate) fn build(results: &[HarnessResult]) -> TableBuilder<FailureReasonsTab
     let mut builder = TableBuilder::new();
 
     for r in results {
-        let failures = r.result.failed_properties();
-        let classification = if failures.is_empty() {
-            "none (success)".to_string()
+        let classification = if let Err(exit_code) = r.result.results {
+            format!("CBMC failed with status {exit_code}")
         } else {
-            let mut classes: Vec<_> = failures.into_iter().map(|p| p.property_class()).collect();
-            classes.sort();
-            classes.dedup();
-            classes.join(" + ")
+            let failures = r.result.failed_properties();
+            if failures.is_empty() {
+                "none (success)".to_string()
+            } else {
+                let mut classes: Vec<_> =
+                    failures.into_iter().map(|p| p.property_class()).collect();
+                classes.sort();
+                classes.dedup();
+                classes.join(" + ")
+            }
         };
 
         let name = r.harness.pretty_name.trim_end_matches("::{closure#0}").to_string();

kani-driver/src/assess/table_promising_tests.rs

@@ -29,7 +29,7 @@ use super::table_builder::{ColumnType, RenderableTableRow, TableBuilder, TableRo
 pub(crate) fn build(results: &[HarnessResult]) -> TableBuilder<PromisingTestsTableRow> {
     let mut builder = TableBuilder::new();
 
-    for r in results {
+    for r in results.iter().filter(|res| res.result.results.is_ok()) {
         // For now we're just reporting "successful" harnesses as candidates.
         // In the future this heuristic should be expanded. More data is required to do this, however.
         if r.result.failed_properties().is_empty() {

kani-driver/src/call_cargo.rs

@@ -5,11 +5,13 @@ use crate::args::KaniArgs;
 use crate::call_single_file::to_rustc_arg;
 use crate::project::Artifact;
 use crate::session::KaniSession;
+use crate::util;
 use anyhow::{bail, Context, Result};
 use cargo_metadata::diagnostic::{Diagnostic, DiagnosticLevel};
 use cargo_metadata::{Message, Metadata, MetadataCommand, Package, Target};
 use kani_metadata::{ArtifactType, CompilerArtifactStub};
 use std::ffi::{OsStr, OsString};
+use std::fmt::{self, Display};
 use std::fs::{self, File};
 use std::io::BufReader;
 use std::path::PathBuf;
@@ -35,11 +37,13 @@ pub struct CargoOutputs {
     pub metadata: Vec<Artifact>,
     /// Recording the cargo metadata from the build
     pub cargo_metadata: Metadata,
+    /// For build `keep_going` mode, we collect the targets that we failed to compile.
+    pub failed_targets: Option<Vec<String>>,
 }
 
 impl KaniSession {
     /// Calls `cargo_build` to generate `*.symtab.json` files in `target_dir`
-    pub fn cargo_build(&self) -> Result<CargoOutputs> {
+    pub fn cargo_build(&self, keep_going: bool) -> Result<CargoOutputs> {
         let build_target = env!("TARGET"); // see build.rs
         let metadata = self.cargo_metadata(build_target)?;
         let target_dir = self
@@ -102,6 +106,7 @@ impl KaniSession {
         let mut found_target = false;
         let packages = packages_to_verify(&self.args, &metadata);
         let mut artifacts = vec![];
+        let mut failed_targets = vec![];
         for package in packages {
             for verification_target in package_targets(&self.args, package) {
                 let mut cmd = Command::new("cargo");
@@ -115,7 +120,19 @@ impl KaniSession {
                     .env("CARGO_ENCODED_RUSTFLAGS", rustc_args.join(OsStr::new("\x1f")))
                     .env("CARGO_TERM_PROGRESS_WHEN", "never");
 
-                artifacts.extend(self.run_cargo(cmd, verification_target.target())?.into_iter());
+                match self.run_cargo(cmd, verification_target.target()) {
+                    Err(err) => {
+                        if keep_going {
+                            let target_str = format!("{verification_target}");
+                            util::error(&format!("Failed to compile {target_str}"));
+                            failed_targets.push(target_str);
+                        } else {
+                            return Err(err);
+                        }
+                    }
+                    Ok(Some(artifact)) => artifacts.push(artifact),
+                    Ok(None) => {}
+                }
                 found_target = true;
             }
         }
@@ -124,7 +141,12 @@ impl KaniSession {
             bail!("No supported targets were found.");
         }
 
-        Ok(CargoOutputs { outdir, metadata: artifacts, cargo_metadata: metadata })
+        Ok(CargoOutputs {
+            outdir,
+            metadata: artifacts,
+            cargo_metadata: metadata,
+            failed_targets: keep_going.then_some(failed_targets),
+        })
     }
 
     fn cargo_metadata(&self, build_target: &str) -> Result<Metadata> {
@@ -312,6 +334,7 @@ fn map_kani_artifact(rustc_artifact: cargo_metadata::Artifact) -> Option<Artifac
 }
 
 /// Possible verification targets.
+#[derive(Debug)]
 enum VerificationTarget {
     Bin(Target),
     Lib(Target),
@@ -337,6 +360,16 @@ impl VerificationTarget {
     }
 }
 
+impl Display for VerificationTarget {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        match self {
+            VerificationTarget::Test(target) => write!(f, "test `{}`", target.name),
+            VerificationTarget::Bin(target) => write!(f, "binary `{}`", target.name),
+            VerificationTarget::Lib(target) => write!(f, "lib `{}`", target.name),
+        }
+    }
+}
+
 /// Extract the targets inside a package.
 ///
 /// If `--tests` is given, the list of targets will include any integration tests.

kani-driver/src/call_cbmc.rs

@@ -30,12 +30,11 @@ pub struct VerificationResult {
     /// The parsed output, message by message, of CBMC. However, the `Result` message has been
     /// removed and is available in `results` instead.
     pub messages: Option<Vec<ParserItem>>,
-    /// The `Result` properties in detail.
-    pub results: Option<Vec<Property>>,
-    /// CBMC process exit status. NOTE: Only potentially useful if `status` is `Failure`.
+    /// The `Result` properties in detail or the exit_status of CBMC.
+    /// Note: CBMC process exit status is only potentially useful if `status` is `Failure`.
     /// Kani will see CBMC report "failure" that's actually success (interpreting "failed"
     /// checks like coverage as expected and desirable.)
-    pub exit_status: i32,
+    pub results: Result<Vec<Property>, i32>,
     /// The runtime duration of this CBMC invocation.
     pub runtime: Duration,
     /// Whether concrete playback generated a test
@@ -67,21 +66,17 @@ impl KaniSession {
 
             // Spawn the CBMC process and process its output below
             let cbmc_process_opt = self.run_piped(cmd)?;
-            if let Some(cbmc_process) = cbmc_process_opt {
-                let output = process_cbmc_output(cbmc_process, |i| {
-                    kani_cbmc_output_filter(
-                        i,
-                        self.args.extra_pointer_checks,
-                        self.args.quiet,
-                        &self.args.output_format,
-                    )
-                })?;
-
-                VerificationResult::from(output, start_time)
-            } else {
-                // None is only ever returned when it's a dry run
-                VerificationResult::mock_success()
-            }
+            let cbmc_process = cbmc_process_opt.ok_or(anyhow::Error::msg("Failed to run cbmc"))?;
+            let output = process_cbmc_output(cbmc_process, |i| {
+                kani_cbmc_output_filter(
+                    i,
+                    self.args.extra_pointer_checks,
+                    self.args.quiet,
+                    &self.args.output_format,
+                )
+            })?;
+
+            VerificationResult::from(output, start_time)
         };
 
         self.gen_and_add_concrete_playback(harness, &mut verification_results)?;
@@ -247,8 +242,7 @@ impl VerificationResult {
             VerificationResult {
                 status: determine_status_from_properties(&results),
                 messages: Some(items),
-                results: Some(results),
-                exit_status: output.process_status,
+                results: Ok(results),
                 runtime,
                 generated_concrete_test: false,
             }
@@ -257,8 +251,7 @@ impl VerificationResult {
             VerificationResult {
                 status: VerificationStatus::Failure,
                 messages: Some(items),
-                results: None,
-                exit_status: output.process_status,
+                results: Err(output.process_status),
                 runtime,
                 generated_concrete_test: false,
             }
@@ -269,8 +262,7 @@ impl VerificationResult {
         VerificationResult {
             status: VerificationStatus::Success,
             messages: None,
-            results: None,
-            exit_status: 42, // on success, exit code is ignored, so put something weird here
+            results: Ok(vec![]),
             runtime: Duration::from_secs(0),
             generated_concrete_test: false,
         }
@@ -280,36 +272,38 @@ impl VerificationResult {
         VerificationResult {
             status: VerificationStatus::Failure,
             messages: None,
-            results: None,
             // on failure, exit codes in theory might be used,
             // but `mock_failure` should never be used in a context where they will,
             // so again use something weird:
-            exit_status: 42,
+            results: Err(42),
             runtime: Duration::from_secs(0),
             generated_concrete_test: false,
         }
     }
 
     pub fn render(&self, output_format: &OutputFormat) -> String {
-        if let Some(results) = &self.results {
-            let show_checks = matches!(output_format, OutputFormat::Regular);
-            let mut result = format_result(results, show_checks);
-            writeln!(result, "Verification Time: {}s", self.runtime.as_secs_f32()).unwrap();
-            result
-        } else {
-            let verification_result = console::style("FAILED").red();
-            format!(
-                "\nCBMC failed with status {}\nVERIFICATION:- {verification_result}\n",
-                self.exit_status
-            )
+        match &self.results {
+            Ok(results) => {
+                let show_checks = matches!(output_format, OutputFormat::Regular);
+                let mut result = format_result(results, show_checks);
+                writeln!(result, "Verification Time: {}s", self.runtime.as_secs_f32()).unwrap();
+                result
+            }
+            Err(exit_status) => {
+                let verification_result = console::style("FAILED").red();
+                format!(
+                    "\nCBMC failed with status {exit_status}\nVERIFICATION:- {verification_result}\n",
+                )
+            }
         }
     }
 
     /// Find the failed properties from this verification run
     pub fn failed_properties(&self) -> Vec<&Property> {
-        if let Some(properties) = &self.results {
+        if let Ok(properties) = &self.results {
             properties.iter().filter(|prop| prop.status == CheckStatus::Failure).collect()
         } else {
+            debug_assert!(false, "expected error to be handled before invoking this function");
             vec![]
         }
     }

kani-driver/src/concrete_playback.rs

@@ -31,7 +31,7 @@ impl KaniSession {
             None => return Ok(()),
         };
 
-        if let Some(result_items) = &verification_result.results {
+        if let Ok(result_items) = &verification_result.results {
             match extract_harness_values(result_items) {
                 None => println!(
                     "WARNING: Kani could not produce a concrete playback for `{}` because there \

kani-driver/src/main.rs

@@ -70,8 +70,7 @@ fn cargokani_main(input_args: Vec<OsString>) -> Result<()> {
         return assess::run_assess(session, assess::AssessArgs::default());
     }
 
-    let project = project::cargo_project(&session)?;
-    debug!(?project, "cargokani_main");
+    let project = project::cargo_project(&session, false)?;
     if session.args.only_codegen { Ok(()) } else { verify_project(project, session) }
 }
 
@@ -82,7 +81,6 @@ 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/project.rs

@@ -59,6 +59,8 @@ pub struct Project {
     pub merged_artifacts: bool,
     /// Records the cargo metadata from the build, if there was any
     pub cargo_metadata: Option<cargo_metadata::Metadata>,
+    /// For build `keep_going` mode, we collect the targets that we failed to compile.
+    pub failed_targets: Option<Vec<String>>,
 }
 
 impl Project {
@@ -145,8 +147,10 @@ fn dump_metadata(metadata: &KaniMetadata, path: &Path) {
 }
 
 /// Generate a project using `cargo`.
-pub fn cargo_project(session: &KaniSession) -> Result<Project> {
-    let outputs = session.cargo_build()?;
+/// Accept a boolean to build as many targets as possible. The number of failures in that case can
+/// be collected from the project.
+pub fn cargo_project(session: &KaniSession, keep_going: bool) -> Result<Project> {
+    let outputs = session.cargo_build(keep_going)?;
     let mut artifacts = vec![];
     let outdir = outputs.outdir.canonicalize()?;
     if session.args.function.is_some() {
@@ -181,6 +185,7 @@ pub fn cargo_project(session: &KaniSession) -> Result<Project> {
             metadata: vec![metadata],
             merged_artifacts: true,
             cargo_metadata: Some(outputs.cargo_metadata),
+            failed_targets: outputs.failed_targets,
         })
     } else {
         // For the MIR Linker we know there is only one artifact per verification target. Use
@@ -208,6 +213,7 @@ pub fn cargo_project(session: &KaniSession) -> Result<Project> {
             metadata,
             merged_artifacts: false,
             cargo_metadata: Some(outputs.cargo_metadata),
+            failed_targets: outputs.failed_targets,
         })
     }
 }
@@ -300,6 +306,7 @@ impl<'a> StandaloneProjectBuilder<'a> {
                 .collect(),
             merged_artifacts: false,
             cargo_metadata: None,
+            failed_targets: None,
         })
     }