Fast fail feature - Stops verification process as soon as one failure is observed - Use case : CI speed up (#3879)

Resolves #3458 

Added the option `--fail-fast`, which would stop the verification
process whenever any of the harnesses fails, and returns the failed
harness as an error.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Zyad Hassan <[email protected]>

Author: rajath-mk

kani-driver/src/args/mod.rs

@@ -334,6 +334,10 @@ pub struct VerificationArgs {
     #[arg(long)]
     pub harness_timeout: Option<Timeout>,
 
+    /// Stop the verification process as soon as one of the harnesses fails.
+    #[arg(long)]
+    pub fail_fast: bool,
+
     /// Arguments to pass down to Cargo
     #[command(flatten)]
     pub cargo: CargoCommonArgs,

kani-driver/src/harness_runner.rs

@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-use anyhow::{Result, bail};
+use anyhow::{Error, Result, bail};
 use kani_metadata::{ArtifactType, HarnessMetadata};
 use rayon::prelude::*;
 use std::fs::File;
@@ -34,6 +34,20 @@ pub(crate) struct HarnessResult<'pr> {
     pub result: VerificationResult,
 }
 
+#[derive(Debug)]
+struct FailFastHarnessInfo {
+    pub index_to_failing_harness: usize,
+    pub result: VerificationResult,
+}
+
+impl std::error::Error for FailFastHarnessInfo {}
+
+impl std::fmt::Display for FailFastHarnessInfo {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        write!(f, "harness failed")
+    }
+}
+
 impl<'pr> HarnessRunner<'_, 'pr> {
     /// Given a [`HarnessRunner`] (to abstract over how these harnesses were generated), this runs
     /// the proof-checking process for each harness in `harnesses`.
@@ -55,7 +69,8 @@ impl<'pr> HarnessRunner<'_, 'pr> {
         let results = pool.install(|| -> Result<Vec<HarnessResult<'pr>>> {
             sorted_harnesses
                 .par_iter()
-                .map(|harness| -> Result<HarnessResult<'pr>> {
+                .enumerate()
+                .map(|(idx, harness)| -> Result<HarnessResult<'pr>> {
                     let goto_file =
                         self.project.get_harness_artifact(&harness, ArtifactType::Goto).unwrap();
 
@@ -66,12 +81,31 @@ impl<'pr> HarnessRunner<'_, 'pr> {
                     }
 
                     let result = self.sess.check_harness(goto_file, harness)?;
-                    Ok(HarnessResult { harness, result })
+                    if self.sess.args.fail_fast && result.status == VerificationStatus::Failure {
+                        Err(Error::new(FailFastHarnessInfo {
+                            index_to_failing_harness: idx,
+                            result,
+                        }))
+                    } else {
+                        Ok(HarnessResult { harness, result })
+                    }
                 })
                 .collect::<Result<Vec<_>>>()
-        })?;
-
-        Ok(results)
+        });
+        match results {
+            Ok(results) => Ok(results),
+            Err(err) => {
+                if err.is::<FailFastHarnessInfo>() {
+                    let failed = err.downcast::<FailFastHarnessInfo>().unwrap();
+                    Ok(vec![HarnessResult {
+                        harness: sorted_harnesses[failed.index_to_failing_harness],
+                        result: failed.result,
+                    }])
+                } else {
+                    Err(err)
+                }
+            }
+        }
     }
 
     /// Return an error if the user is trying to verify a harness with stubs without enabling the

tests/ui/multiple-harnesses/stop_at_single_fail/fail_fast_test.expected

@@ -0,0 +1 @@
+Complete - 0 successfully verified harnesses, 1 failures, 1 total.

tests/ui/multiple-harnesses/stop_at_single_fail/fail_fast_test.rs

@@ -0,0 +1,26 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: --fail-fast
+//! Ensure that the verification process stops as soon as one of the harnesses fails.
+
+mod tests {
+    #[kani::proof]
+    fn test_01_fail() {
+        assert!(false, "First failure");
+    }
+
+    #[kani::proof]
+    fn test_02_fail() {
+        assert!(false, "Second failure");
+    }
+
+    #[kani::proof]
+    fn test_03_fail() {
+        assert!(false, "Third failure");
+    }
+
+    #[kani::proof]
+    fn test_04_fail() {
+        assert!(false, "Fourth failure");
+    }
+}

tests/ui/multiple-harnesses/stop_at_single_fail/fail_fast_test_parallel.expected

@@ -0,0 +1 @@
+Complete - 0 successfully verified harnesses, 1 failures, 1 total.

tests/ui/multiple-harnesses/stop_at_single_fail/fail_fast_test_parallel.rs

@@ -0,0 +1,57 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: --fail-fast -Z unstable-options --jobs 4 --output-format=terse
+//! Ensure that the verification process stops as soon as one of the harnesses fails.
+//! This test runs on 4 parallel threads. Stops verification as soon as a harness on any of the threads fails.
+
+mod tests {
+    #[kani::proof]
+    fn test_01_fail() {
+        assert!(false, "First failure");
+    }
+
+    #[kani::proof]
+    fn test_02_fail() {
+        assert!(false, "Second failure");
+    }
+
+    #[kani::proof]
+    fn test_03_fail() {
+        assert!(false, "Third failure");
+    }
+
+    #[kani::proof]
+    fn test_04_fail() {
+        assert!(false, "Fourth failure");
+    }
+
+    #[kani::proof]
+    fn test_05_fail() {
+        assert!(false, "Fifth failure");
+    }
+
+    #[kani::proof]
+    fn test_06_fail() {
+        assert!(false, "Sixth failure");
+    }
+
+    #[kani::proof]
+    fn test_07_fail() {
+        assert!(false, "Seventh failure");
+    }
+
+    #[kani::proof]
+    fn test_08_fail() {
+        assert!(false, "Eighth failure");
+    }
+
+    #[kani::proof]
+    fn test_09_fail() {
+        assert!(false, "Ninth failure");
+    }
+
+    #[kani::proof]
+    fn test_10_fail() {
+        assert!(false, "Tenth failure");
+    }
+}