Enable concrete playback for satisfiable cover properties (rust-lang#2134)

Author: zhassan-aws

kani-driver/src/call_cbmc.rs

@@ -38,6 +38,8 @@ pub struct VerificationResult {
     pub exit_status: i32,
     /// The runtime duration of this CBMC invocation.
     pub runtime: Duration,
+    /// Whether concrete playback generated a test
+    pub generated_concrete_test: bool,
 }
 
 impl KaniSession {
@@ -51,7 +53,8 @@ impl KaniSession {
 
         let start_time = Instant::now();
 
-        let verification_results = if self.args.output_format == crate::args::OutputFormat::Old {
+        let mut verification_results = if self.args.output_format == crate::args::OutputFormat::Old
+        {
             if self.run_terminal(cmd).is_err() {
                 VerificationResult::mock_failure()
             } else {
@@ -80,7 +83,7 @@ impl KaniSession {
             }
         };
 
-        self.gen_and_add_concrete_playback(harness, &verification_results)?;
+        self.gen_and_add_concrete_playback(harness, &mut verification_results)?;
         Ok(verification_results)
     }
 
@@ -204,6 +207,7 @@ impl VerificationResult {
                 results: Some(results),
                 exit_status: output.process_status,
                 runtime,
+                generated_concrete_test: false,
             }
         } else {
             // We never got results from CBMC - something went wrong (e.g. crash) so it's failure
@@ -213,6 +217,7 @@ impl VerificationResult {
                 results: None,
                 exit_status: output.process_status,
                 runtime,
+                generated_concrete_test: false,
             }
         }
     }
@@ -224,6 +229,7 @@ impl VerificationResult {
             results: None,
             exit_status: 42, // on success, exit code is ignored, so put something weird here
             runtime: Duration::from_secs(0),
+            generated_concrete_test: false,
         }
     }
 
@@ -237,6 +243,7 @@ impl VerificationResult {
             // so again use something weird:
             exit_status: 42,
             runtime: Duration::from_secs(0),
+            generated_concrete_test: false,
         }
     }
 

kani-driver/src/concrete_playback.rs

@@ -5,7 +5,7 @@
 //! generating concrete playback unit tests, and adding them to the user's source code.
 
 use crate::args::ConcretePlaybackMode;
-use crate::call_cbmc::{VerificationResult, VerificationStatus};
+use crate::call_cbmc::VerificationResult;
 use crate::session::KaniSession;
 use anyhow::{Context, Result};
 use concrete_vals_extractor::{extract_harness_values, ConcreteVal};
@@ -23,17 +23,13 @@ impl KaniSession {
     pub fn gen_and_add_concrete_playback(
         &self,
         harness: &HarnessMetadata,
-        verification_result: &VerificationResult,
+        verification_result: &mut VerificationResult,
     ) -> Result<()> {
         let playback_mode = match self.args.concrete_playback {
             Some(playback_mode) => playback_mode,
             None => return Ok(()),
         };
 
-        if verification_result.status == VerificationStatus::Success {
-            return Ok(());
-        }
-
         if let Some(result_items) = &verification_result.results {
             match extract_harness_values(result_items) {
                 None => println!(
@@ -71,6 +67,7 @@ impl KaniSession {
                             .expect("Failed to modify source code");
                         }
                     }
+                    verification_result.generated_concrete_test = true;
                 }
             }
         }
@@ -309,7 +306,8 @@ mod concrete_vals_extractor {
     /// This will return None if the failure is not related to a user assertion.
     pub fn extract_harness_values(result_items: &[Property]) -> Option<Vec<ConcreteVal>> {
         let mut failures = result_items.iter().filter(|prop| {
-            prop.property_class() == "assertion" && prop.status == CheckStatus::Failure
+            (prop.property_class() == "assertion" && prop.status == CheckStatus::Failure)
+                || (prop.property_class() == "cover" && prop.status == CheckStatus::Satisfied)
         });
 
         // Process the first assertion failure.

kani-driver/src/harness_runner.rs

@@ -116,7 +116,10 @@ impl KaniSession {
         let failing = failures.len();
         let total = succeeding + failing;
 
-        if self.args.concrete_playback.is_some() && !self.args.quiet && failures.is_empty() {
+        if self.args.concrete_playback.is_some()
+            && !self.args.quiet
+            && results.iter().all(|r| !r.result.generated_concrete_test)
+        {
             println!(
                 "INFO: The concrete playback feature never generated unit tests because there were no failing harnesses."
             )

tests/ui/concrete-playback/cover/expected

@@ -0,0 +1,14 @@
+1 of 1 cover properties satisfied
+VERIFICATION:- SUCCESSFUL
+
+Concrete playback
+```
+#[test]
+fn kani_concrete_playback_harness
+    let concrete_vals: Vec<Vec<u8>> = vec![
+        // 1
+        vec![1, 0, 0, 0]
+    ];
+    kani::concrete_playback_run(concrete_vals, harness);
+}
+```

tests/ui/concrete-playback/cover/main.rs

@@ -0,0 +1,10 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: --enable-unstable --concrete-playback=print
+
+#[kani::proof]
+pub fn harness() {
+    let x: u32 = kani::any();
+    kani::cover!(x != 0 && x / 2 == 0);
+}