Gracefully exit from kani-driver process (#2168)

When an error that was properly handled ocurrs in `kani-driver` we now gracefully exit and return ExitStatus::FAILURE.

We still print all error context to keep a similar experiece to what it was before. However, this will no longer include the backtrace if users set RUST_BACKTRACE=1.

The backtrace will still be included if you enable the debug logs and also enable the backtrace. I.e.:

```bash
export RUST_BACKTRACE=1
export KANI_LOG=kani_driver=debug
cargo kani
```

Author: celinval

kani-driver/src/main.rs

@@ -4,6 +4,7 @@
 #![feature(array_methods)]
 
 use std::ffi::OsString;
+use std::process::ExitCode;
 
 use anyhow::Result;
 
@@ -39,10 +40,20 @@ mod unsound_experiments;
 /// The main function for the `kani-driver`.
 /// The driver can be invoked via `cargo kani` and `kani` commands, which determines what kind of
 /// project should be verified.
-fn main() -> Result<()> {
-    match determine_invocation_type(Vec::from_iter(std::env::args_os())) {
+fn main() -> ExitCode {
+    let result = match determine_invocation_type(Vec::from_iter(std::env::args_os())) {
         InvocationType::CargoKani(args) => cargokani_main(args),
         InvocationType::Standalone => standalone_main(),
+    };
+
+    if let Err(error) = result {
+        // We are using the debug format for now to print the all the context.
+        // We should consider creating a standard for error reporting.
+        debug!(?error, "main_failure");
+        util::error(&format!("{error:#}"));
+        ExitCode::FAILURE
+    } else {
+        ExitCode::SUCCESS
     }
 }
 

kani-driver/src/util.rs

@@ -88,13 +88,20 @@ pub fn specialized_harness_name(linked_obj: &Path, harness_filename: &str) -> Pa
     alter_extension(linked_obj, &format!("for-{harness_filename}.out"))
 }
 
-/// Print a warning message. This will add a "warning:" tag before the message and style accordinly.
+/// Print a warning message. This will add a "warning:" tag before the message and style accordingly.
 pub fn warning(msg: &str) {
     let warning = console::style("warning:").bold().yellow();
     let msg_fmt = console::style(msg).bold();
     println!("{warning} {msg_fmt}")
 }
 
+/// Print an error message. This will add an "error:" tag before the message and style accordingly.
+pub fn error(msg: &str) {
+    let error = console::style("error:").bold().red();
+    let msg_fmt = console::style(msg).bold();
+    println!("{error} {msg_fmt}")
+}
+
 #[cfg(test)]
 mod tests {
     use super::*;

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

@@ -1,3 +1,3 @@
 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: cargo exited with status exit status: 101

tests/cargo-kani/simple-proof-annotation/main.expected

@@ -1 +1 @@
-Error: A proof harness named main was not found
+error: A proof harness named main was not found

tests/cargo-ui/unsupported-lib-types/proc-macro/expected

@@ -1,2 +1,2 @@
 Skipped the following unsupported targets: 'lib'.
-Error: No supported targets were found.
+error: No supported targets were found.

tests/expected/function-stubbing-no-harness/expected

@@ -1 +1 @@
-Error: A proof harness named foo was not found
+error: A proof harness named foo was not found