From d4f0dd0a686575d171fc5af938638be890585d74 Mon Sep 17 00:00:00 2001
From: Yoshiki Takashima <ytakashl@amazon.com>
Date: Sat, 27 May 2023 02:14:21 -0400
Subject: [PATCH] Delay printing playback harness until after verification
 status (#2480)

---
 kani-driver/src/call_cbmc.rs                      |  4 +---
 kani-driver/src/harness_runner.rs                 |  4 ++--
 tests/ui/concrete-playback/message-order/expected | 14 ++++++++++++++
 tests/ui/concrete-playback/message-order/main.rs  |  9 +++++++++
 4 files changed, 26 insertions(+), 5 deletions(-)
 create mode 100644 tests/ui/concrete-playback/message-order/expected
 create mode 100644 tests/ui/concrete-playback/message-order/main.rs

diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs
index 9701efa9c79a..daddfdf62f1c 100644
--- a/kani-driver/src/call_cbmc.rs
+++ b/kani-driver/src/call_cbmc.rs
@@ -66,8 +66,7 @@ impl KaniSession {
 
         let start_time = Instant::now();
 
-        let mut verification_results = if self.args.output_format == crate::args::OutputFormat::Old
-        {
+        let verification_results = if self.args.output_format == crate::args::OutputFormat::Old {
             if self.run_terminal(cmd).is_err() {
                 VerificationResult::mock_failure()
             } else {
@@ -93,7 +92,6 @@ impl KaniSession {
             VerificationResult::from(output, harness.attributes.should_panic, start_time)
         };
 
-        self.gen_and_add_concrete_playback(harness, &mut verification_results)?;
         Ok(verification_results)
     }
 
diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs
index d2885c69429a..f1f0befc4ddd 100644
--- a/kani-driver/src/harness_runner.rs
+++ b/kani-driver/src/harness_runner.rs
@@ -89,7 +89,7 @@ impl KaniSession {
             // Strictly speaking, we're faking success here. This is more "no error"
             Ok(VerificationResult::mock_success())
         } else {
-            let result = self.with_timer(|| self.run_cbmc(binary, harness), "run_cbmc")?;
+            let mut result = self.with_timer(|| self.run_cbmc(binary, harness), "run_cbmc")?;
 
             // When quiet, we don't want to print anything at all.
             // When output is old, we also don't have real results to print.
@@ -99,7 +99,7 @@ impl KaniSession {
                     result.render(&self.args.output_format, harness.attributes.should_panic)
                 );
             }
-
+            self.gen_and_add_concrete_playback(harness, &mut result)?;
             Ok(result)
         }
     }
diff --git a/tests/ui/concrete-playback/message-order/expected b/tests/ui/concrete-playback/message-order/expected
new file mode 100644
index 000000000000..415584e1f2dc
--- /dev/null
+++ b/tests/ui/concrete-playback/message-order/expected
@@ -0,0 +1,14 @@
+VERIFICATION:- SUCCESSFUL
+
+
+Concrete playback unit test for `dummy`:
+```
+#[test]
+fn kani_concrete_playback_dummy
+    let concrete_vals: Vec<Vec<u8>> = vec![
+        // 32778
+        vec![10, 128, 0, 0],
+    ];
+    kani::concrete_playback_run(concrete_vals, dummy);
+}
+```
diff --git a/tests/ui/concrete-playback/message-order/main.rs b/tests/ui/concrete-playback/message-order/main.rs
new file mode 100644
index 000000000000..81aa4c6886db
--- /dev/null
+++ b/tests/ui/concrete-playback/message-order/main.rs
@@ -0,0 +1,9 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: --concrete-playback=print --harness dummy -Z concrete-playback
+
+#[kani::proof]
+fn dummy() {
+    kani::cover!(kani::any::<u32>() != 10);
+}