Autoharness: exit code 1 upon harness failure (#4043)

Exit Kani with a failure code if any automatic harnesses fail. This
replicates the behavior of just running manual harnesses.

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

Author: Carolyn Zech

kani-driver/src/autoharness/mod.rs

@@ -200,7 +200,10 @@ impl KaniSession {
     }
 
     /// Prints the results from running the `autoharness` subcommand.
-    pub fn print_autoharness_summary(&self, mut automatic: Vec<&HarnessResult<'_>>) -> Result<()> {
+    pub fn print_autoharness_summary(
+        &self,
+        mut automatic: Vec<&HarnessResult<'_>>,
+    ) -> Result<usize> {
         automatic.sort_by(|a, b| a.harness.pretty_name.cmp(&b.harness.pretty_name));
         let (successes, failures): (Vec<_>, Vec<_>) =
             automatic.into_iter().partition(|r| r.result.status == VerificationStatus::Success);
@@ -258,6 +261,6 @@ impl KaniSession {
             println!("No functions were eligible for automatic verification.");
         }
 
-        Ok(())
+        Ok(failing)
     }
 }

kani-driver/src/harness_runner.rs

@@ -298,11 +298,13 @@ impl KaniSession {
             self.show_coverage_summary()?;
         }
 
-        if self.autoharness_compiler_flags.is_some() {
-            self.print_autoharness_summary(automatic)?;
-        }
+        let autoharness_failing = if self.autoharness_compiler_flags.is_some() {
+            self.print_autoharness_summary(automatic)?
+        } else {
+            0
+        };
 
-        if failing > 0 && self.autoharness_compiler_flags.is_none() {
+        if failing + autoharness_failing > 0 {
             // Failure exit code without additional error message
             drop(self);
             std::process::exit(1);

tests/script-based-pre/cargo_autoharness_contracts/config.yml

@@ -2,3 +2,4 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 script: contracts.sh
 expected: contracts.expected
+exit_code: 1

tests/script-based-pre/cargo_autoharness_contracts/contracts.sh

@@ -3,7 +3,3 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 cargo kani autoharness -Z autoharness
-# We expect verification to fail, so the above command will produce an exit status of 1
-# However, we don't want the test to fail because of that exit status; we only want it to fail if the expected file doesn't match
-# So, exit with a status code of 0 explicitly.
-exit 0;

tests/script-based-pre/cargo_autoharness_dependencies/dependencies.sh

@@ -2,8 +2,4 @@
 # Copyright Kani Contributors
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
-cargo kani autoharness -Z autoharness
-# We expect verification to fail, so the above command will produce an exit status of 1
-# However, we don't want the test to fail because of that exit status; we only want it to fail if the expected file doesn't match
-# So, exit with a status code of 0 explicitly.
-exit 0;
+cargo kani autoharness -Z autoharness

tests/script-based-pre/cargo_autoharness_harnesses_fail/config.yml

@@ -2,3 +2,4 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 script: harnesses_fail.sh
 expected: harnesses_fail.expected
+exit_code: 1

tests/script-based-pre/cargo_autoharness_harnesses_fail/harnesses_fail.sh

@@ -2,8 +2,4 @@
 # Copyright Kani Contributors
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
-cargo kani autoharness -Z autoharness
-# We expect verification to fail, so the above command will produce an exit status of 1
-# However, we don't want the test to fail because of that exit status; we only want it to fail if the expected file doesn't match
-# So, exit with a status code of 0 explicitly.
-exit 0;
+cargo kani autoharness -Z autoharness

tests/script-based-pre/cargo_autoharness_termination_timeout/config.yml

@@ -2,3 +2,4 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 script: termination_timeout.sh
 expected: termination_timeout.expected
+exit_code: 1

tests/script-based-pre/cargo_autoharness_termination_unwind/config.yml

@@ -2,3 +2,4 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 script: termination_unwind.sh
 expected: termination_unwind.expected
+exit_code: 1

tests/script-based-pre/cargo_autoharness_type_invariant/config.yml

@@ -2,3 +2,4 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 script: type-invariant.sh
 expected: type-invariant.expected
+exit_code: 1