Store failure reason into assess metadata (#2166)

We now store Kani's version and the failure reason (if there's one) into the assess metadata. For now, we still need to manually parse this information, but this moves us closer to #2058 and #2165.

In order to collect more details about the compilation errors, we now inspect the cargo diagnostic messages.

Author: celinval

kani-driver/src/assess/args.rs

@@ -28,6 +28,9 @@ pub enum AssessSubcommand {
 /// `cargo kani assess scan` subcommand arguments
 #[derive(Debug, Parser)]
 pub struct ScanArgs {
+    // TODO: When assess scan is invoked using `--existing-only`, it should check if the Kani version
+    // from the existing metadata files matches the current version. Otherwise, the results may no
+    // longer hold.
     /// Don't run assess on found packages, just re-analyze the results from a previous run
     #[arg(long, hide = true)]
     pub existing_only: bool,

kani-driver/src/assess/metadata.rs

@@ -27,6 +27,11 @@ use super::AssessArgs;
 /// This is not a stable interface.
 #[derive(Serialize, Deserialize)]
 pub struct AssessMetadata {
+    /// Kani version that was used to generate the metadata.
+    #[serde(rename = "kani_version")]
+    pub version: String,
+    /// Contains an error message in cases where it failed the execution.
+    pub error: Option<SessionError>,
     /// Report on the presence of `codegen_unimplemented` in the analyzed packages
     pub unsupported_features: TableBuilder<UnsupportedFeaturesTableRow>,
     /// Report of the reasons why tests could not be analyzed by Kani
@@ -35,32 +40,62 @@ pub struct AssessMetadata {
     pub promising_tests: TableBuilder<PromisingTestsTableRow>,
 }
 
+impl AssessMetadata {
+    pub fn new(
+        unsupported_features: TableBuilder<UnsupportedFeaturesTableRow>,
+        failure_reasons: TableBuilder<FailureReasonsTableRow>,
+        promising_tests: TableBuilder<PromisingTestsTableRow>,
+    ) -> AssessMetadata {
+        AssessMetadata {
+            version: env!("CARGO_PKG_VERSION").to_string(),
+            error: None,
+            unsupported_features,
+            failure_reasons,
+            promising_tests,
+        }
+    }
+
+    pub fn from_error(err: &dyn std::error::Error) -> AssessMetadata {
+        let error = Some(SessionError {
+            root_cause: err.source().map(|e| format!("{e:#}")),
+            msg: err.to_string(),
+        });
+        AssessMetadata {
+            version: env!("CARGO_PKG_VERSION").to_string(),
+            error,
+            unsupported_features: TableBuilder::new(),
+            failure_reasons: TableBuilder::new(),
+            promising_tests: TableBuilder::new(),
+        }
+    }
+    pub fn empty() -> AssessMetadata {
+        AssessMetadata {
+            version: env!("CARGO_PKG_VERSION").to_string(),
+            error: None,
+            unsupported_features: TableBuilder::new(),
+            failure_reasons: TableBuilder::new(),
+            promising_tests: TableBuilder::new(),
+        }
+    }
+}
+
+#[derive(Serialize, Deserialize, Debug)]
+pub struct SessionError {
+    pub root_cause: Option<String>,
+    pub msg: String,
+}
+
 /// If given the argument to so do, write the assess metadata to the target file.
-pub(crate) fn write_metadata(args: &AssessArgs, build: AssessMetadata) -> Result<()> {
+pub(crate) fn write_metadata(args: &AssessArgs, metadata: AssessMetadata) -> Result<()> {
     if let Some(path) = &args.emit_metadata {
         let out_file = File::create(&path)?;
         let writer = BufWriter::new(out_file);
         // use pretty for now to keep things readable and debuggable, but this should change eventually
-        serde_json::to_writer_pretty(writer, &build)?;
+        serde_json::to_writer_pretty(writer, &metadata)?;
     }
     Ok(())
 }
 
-/// Write metadata with unsupported features only, supporting the `--only-codegen` option.
-pub(crate) fn write_partial_metadata(
-    args: &AssessArgs,
-    unsupported_features: TableBuilder<UnsupportedFeaturesTableRow>,
-) -> Result<()> {
-    write_metadata(
-        args,
-        AssessMetadata {
-            unsupported_features,
-            failure_reasons: TableBuilder::new(),
-            promising_tests: TableBuilder::new(),
-        },
-    )
-}
-
 /// Read assess metadata from a file.
 pub(crate) fn read_metadata(path: &Path) -> Result<AssessMetadata> {
     // this function already exists, but a proxy here helps find it :)
@@ -72,11 +107,7 @@ pub(crate) fn read_metadata(path: &Path) -> Result<AssessMetadata> {
 /// This is not a complicated operation, because the assess metadata structure is meant
 /// to accomodate multiple packages already, so we're just "putting it together".
 pub(crate) fn aggregate_metadata(metas: Vec<AssessMetadata>) -> AssessMetadata {
-    let mut result = AssessMetadata {
-        unsupported_features: TableBuilder::new(),
-        failure_reasons: TableBuilder::new(),
-        promising_tests: TableBuilder::new(),
-    };
+    let mut result = AssessMetadata::empty();
     for meta in metas {
         for item in meta.unsupported_features.build() {
             result.unsupported_features.add(item.clone());

kani-driver/src/assess/mod.rs

@@ -1,9 +1,11 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
+use self::metadata::{write_metadata, AssessMetadata};
 use anyhow::Result;
 use kani_metadata::KaniMetadata;
 
+use crate::assess::table_builder::TableBuilder;
 use crate::metadata::merge_kani_metadata;
 use crate::project;
 use crate::session::KaniSession;
@@ -21,11 +23,23 @@ mod table_unsupported_features;
 /// `cargo kani assess` main entry point.
 ///
 /// See <https://model-checking.github.io/kani/dev-assess.html>
-pub(crate) fn cargokani_assess_main(mut session: KaniSession, args: AssessArgs) -> Result<()> {
+pub(crate) fn run_assess(session: KaniSession, args: AssessArgs) -> Result<()> {
     if let Some(args::AssessSubcommand::Scan(args)) = &args.command {
         return scan::assess_scan_main(session, args);
     }
 
+    let result = assess_project(session);
+    match result {
+        Ok(metadata) => write_metadata(&args, metadata),
+        Err(err) => {
+            let metadata = AssessMetadata::from_error(err.as_ref());
+            write_metadata(&args, metadata)?;
+            Err(err.context("Failed to assess project"))
+        }
+    }
+}
+
+fn assess_project(mut session: KaniSession) -> Result<AssessMetadata> {
     // Fix (as in "make unchanging/unchangable") some settings.
     // 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,
@@ -69,8 +83,11 @@ pub(crate) fn cargokani_assess_main(mut session: KaniSession, args: AssessArgs)
     }
 
     if session.args.only_codegen {
-        metadata::write_partial_metadata(&args, unsupported_features)?;
-        return Ok(());
+        return Ok(AssessMetadata::new(
+            unsupported_features,
+            TableBuilder::new(),
+            TableBuilder::new(),
+        ));
     }
 
     // Done with the 'cargo-kani' part, now we're going to run *test* harnesses instead of proof:
@@ -95,12 +112,7 @@ pub(crate) fn cargokani_assess_main(mut session: KaniSession, args: AssessArgs)
     let promising_tests = table_promising_tests::build(&results);
     println!("{}", promising_tests.render());
 
-    metadata::write_metadata(
-        &args,
-        metadata::AssessMetadata { unsupported_features, failure_reasons, promising_tests },
-    )?;
-
-    Ok(())
+    Ok(AssessMetadata::new(unsupported_features, failure_reasons, promising_tests))
 }
 
 /// Merges a collection of Kani metadata by figuring out which package each belongs to, from cargo metadata.

kani-driver/src/call_cargo.rs

@@ -4,9 +4,11 @@
 use crate::args::KaniArgs;
 use crate::session::{KaniSession, ReachabilityMode};
 use anyhow::{bail, Context, Result};
-use cargo_metadata::{Metadata, MetadataCommand, Package};
+use cargo_metadata::diagnostic::{Diagnostic, DiagnosticLevel};
+use cargo_metadata::{Message, Metadata, MetadataCommand, Package};
 use std::ffi::OsString;
 use std::fs;
+use std::io::BufReader;
 use std::path::{Path, PathBuf};
 use std::process::Command;
 use tracing::{debug, trace};
@@ -81,6 +83,10 @@ impl KaniSession {
         cargo_args.push("--target-dir".into());
         cargo_args.push(target_dir.into());
 
+        // Configuration needed to parse cargo compilation status.
+        cargo_args.push("--message-format".into());
+        cargo_args.push("json-diagnostic-rendered-ansi".into());
+
         if self.args.tests {
             // Use test profile in order to pull dev-dependencies and compile using `--test`.
             // Initially the plan was to use `--tests` but that brings in multiple targets.
@@ -120,9 +126,10 @@ impl KaniSession {
                     .args(&pkg_args)
                     .env("RUSTC", &self.kani_compiler)
                     .env("RUSTFLAGS", "--kani-flags")
-                    .env("KANIFLAGS", &crate::util::join_osstring(&kani_args, " "));
+                    .env("KANIFLAGS", &crate::util::join_osstring(&kani_args, " "))
+                    .env("CARGO_TERM_PROGRESS_WHEN", "never");
 
-                self.run_terminal(cmd)?;
+                self.run_cargo(cmd)?;
                 found_target = true;
             }
         }
@@ -167,6 +174,67 @@ impl KaniSession {
 
         cmd.exec().context("Failed to get cargo metadata.")
     }
+
+    /// 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<()> {
+        let support_color = atty::is(atty::Stream::Stdout);
+        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;
+            for message in Message::parse_stream(reader) {
+                let message = message.unwrap();
+                match message {
+                    Message::CompilerMessage(msg) => match msg.message.level {
+                        DiagnosticLevel::FailureNote => {
+                            print_msg(&msg.message, support_color)?;
+                        }
+                        DiagnosticLevel::Error => {
+                            error_count += 1;
+                            print_msg(&msg.message, support_color)?;
+                        }
+                        DiagnosticLevel::Ice => {
+                            print_msg(&msg.message, support_color)?;
+                            let _ = cargo_process.wait();
+                            return Err(anyhow::Error::msg(msg.message).context(format!(
+                                "Failed to compile `{}` due to an internal compiler error.",
+                                msg.target.name
+                            )));
+                        }
+                        _ => {
+                            if !self.args.quiet {
+                                print_msg(&msg.message, support_color)?;
+                            }
+                        }
+                    },
+                    Message::CompilerArtifact(_)
+                    | Message::BuildScriptExecuted(_)
+                    | Message::BuildFinished(_) => {
+                        // do nothing
+                    }
+                    // Non-exhaustive enum.
+                    _ => {}
+                }
+            }
+            let status = cargo_process.wait()?;
+            if !status.success() {
+                bail!(
+                    "Failed to execute cargo ({status}). Found {error_count} compilation errors."
+                );
+            }
+        }
+        Ok(())
+    }
+}
+
+/// Print the compiler message following the coloring schema.
+fn print_msg(diagnostic: &Diagnostic, use_rendered: bool) -> Result<()> {
+    if use_rendered {
+        print!("{diagnostic}");
+    } else {
+        print!("{}", console::strip_ansi_codes(diagnostic.rendered.as_ref().unwrap()));
+    }
+    Ok(())
 }
 
 /// Given a `path` with glob characters in it (e.g. `*.json`), return a vector of matching files

kani-driver/src/main.rs

@@ -65,9 +65,9 @@ fn cargokani_main(input_args: Vec<OsString>) -> Result<()> {
     let session = session::KaniSession::new(args.common_opts)?;
 
     if let Some(CargoKaniSubcommand::Assess(args)) = args.command {
-        return assess::cargokani_assess_main(session, args);
+        return assess::run_assess(session, args);
     } else if session.args.assess {
-        return assess::cargokani_assess_main(session, assess::AssessArgs::default());
+        return assess::run_assess(session, assess::AssessArgs::default());
     }
 
     let project = project::cargo_project(&session)?;

tests/cargo-kani/asm/global_error/doesnt_call_crate_with_global_asm.expected

@@ -1,3 +1,2 @@
 error: Crate crate_with_global_asm contains global ASM, which is not supported by Kani. Rerun with `--enable-unstable --ignore-global-asm` to suppress this error (**Verification results may be impacted**).
-error: could not compile `crate_with_global_asm` due to previous error
-error: cargo exited with status exit status: 101
+error: could not compile `crate_with_global_asm` due to 2 previous errors

tests/cargo-kani/stubbing-do-not-resolve/harness.expected

@@ -2,4 +2,3 @@ error: unable to resolve function/method: crate::other_crate2::mock
 error: unable to resolve function/method: super::other_crate2::mock
 error: unable to resolve function/method: self::other_crate2::mock
 error: unable to resolve function/method: other_crate1::mock
-error: could not compile `stubbing-do-not-resolve` due to 4 previous errors

tests/cargo-ui/assess-error/Cargo.toml

@@ -0,0 +1,12 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "compilation-error"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[package.metadata.kani]
+flags = { assess=true, enable-unstable=true }

tests/cargo-ui/assess-error/expected

@@ -0,0 +1 @@
+error: Failed to assess project: Failed to execute cargo (exit status: 101). Found 3 compilation errors.

tests/cargo-ui/assess-error/src/lib.rs

@@ -0,0 +1,19 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! Check that the compilation error detection works as expected
+use std::option;
+
+pub fn add(left: usize, right: u32) -> usize {
+    left + right
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn it_works() {
+        let result = add(2, 2);
+        assert_eq!(result, 4);
+    }
+}