Store failure reason into assess metadata

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);
+    }
+}

tests/cargo-ui/function-stubbing-trait-mismatch/main.expected

@@ -1,3 +1,2 @@
 error: `&str` doesn't implement `DoIt`. The function `foo` cannot be stubbed by `bar` due to generic bounds not being met.
 error: `&str` doesn't implement `std::cmp::PartialEq`. The function `foo` cannot be stubbed by `bar` due to generic bounds not being met.
-error: could not compile `function-stubbing-trait-mismatch` due to 2 previous errors