From 54db8506857c1a37fa2aedbd8b3a5ef989a63892 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Wed, 1 Nov 2023 16:39:44 -0700
Subject: [PATCH] Do not override `std` library during playback

---
 library/std/src/lib.rs                        | 14 +++++++
 .../playback_print/config.yml                 |  4 ++
 .../script-based-pre/playback_print/expected  | 13 ++++++
 .../playback_print/playback_print.sh          | 40 +++++++++++++++++++
 .../playback_print/print_vars.rs              | 20 ++++++++++
 5 files changed, 91 insertions(+)
 create mode 100644 tests/script-based-pre/playback_print/config.yml
 create mode 100644 tests/script-based-pre/playback_print/expected
 create mode 100755 tests/script-based-pre/playback_print/playback_print.sh
 create mode 100644 tests/script-based-pre/playback_print/print_vars.rs

diff --git a/library/std/src/lib.rs b/library/std/src/lib.rs
index eae74ebcf055..92ff9216da95 100644
--- a/library/std/src/lib.rs
+++ b/library/std/src/lib.rs
@@ -15,9 +15,11 @@ pub use std::*;
 // Bind `core::assert` to a different name to avoid possible name conflicts if a
 // crate uses `extern crate std as core`. See
 // https://github.com/model-checking/kani/issues/1949
+#[cfg(not(feature = "concrete_playback"))]
 #[allow(unused_imports)]
 use core::assert as __kani__workaround_core_assert;
 
+#[cfg(not(feature = "concrete_playback"))]
 // Override process calls with stubs.
 pub mod process;
 
@@ -41,6 +43,7 @@ pub mod process;
 /// ```
 /// the assert message will be:
 /// "The sum of {} and {} is {}", a, b, c
+#[cfg(not(feature = "concrete_playback"))]
 #[macro_export]
 macro_rules! assert {
     ($cond:expr $(,)?) => {
@@ -77,6 +80,7 @@ macro_rules! assert {
 //    (see https://github.com/model-checking/kani/issues/13)
 // 3. Call kani::assert so that any instrumentation that it does (e.g. injecting
 //    reachability checks) is done for assert_eq and assert_ne
+#[cfg(not(feature = "concrete_playback"))]
 #[macro_export]
 macro_rules! assert_eq {
     ($left:expr, $right:expr $(,)?) => ({
@@ -89,6 +93,7 @@ macro_rules! assert_eq {
     });
 }
 
+#[cfg(not(feature = "concrete_playback"))]
 #[macro_export]
 macro_rules! assert_ne {
     ($left:expr, $right:expr $(,)?) => ({
@@ -102,16 +107,19 @@ macro_rules! assert_ne {
 }
 
 // Treat the debug assert macros same as non-debug ones
+#[cfg(not(feature = "concrete_playback"))]
 #[macro_export]
 macro_rules! debug_assert {
     ($($x:tt)*) => ({ $crate::assert!($($x)*); })
 }
 
+#[cfg(not(feature = "concrete_playback"))]
 #[macro_export]
 macro_rules! debug_assert_eq {
     ($($x:tt)*) => ({ $crate::assert_eq!($($x)*); })
 }
 
+#[cfg(not(feature = "concrete_playback"))]
 #[macro_export]
 macro_rules! debug_assert_ne {
     ($($x:tt)*) => ({ $crate::assert_ne!($($x)*); })
@@ -119,28 +127,33 @@ macro_rules! debug_assert_ne {
 
 // Override the print macros to skip all the printing functionality (which
 // is not relevant for verification)
+#[cfg(not(feature = "concrete_playback"))]
 #[macro_export]
 macro_rules! print {
     ($($x:tt)*) => {{ let _ = format_args!($($x)*); }};
 }
 
+#[cfg(not(feature = "concrete_playback"))]
 #[macro_export]
 macro_rules! eprint {
     ($($x:tt)*) => {{ let _ = format_args!($($x)*); }};
 }
 
+#[cfg(not(feature = "concrete_playback"))]
 #[macro_export]
 macro_rules! println {
     () => { };
     ($($x:tt)*) => {{ let _ = format_args!($($x)*); }};
 }
 
+#[cfg(not(feature = "concrete_playback"))]
 #[macro_export]
 macro_rules! eprintln {
     () => { };
     ($($x:tt)*) => {{ let _ = format_args!($($x)*); }};
 }
 
+#[cfg(not(feature = "concrete_playback"))]
 #[macro_export]
 macro_rules! unreachable {
     // The argument, if present, is a literal that represents the error message, i.e.:
@@ -171,6 +184,7 @@ macro_rules! unreachable {
         stringify!($fmt, $($arg)*)))}};
 }
 
+#[cfg(not(feature = "concrete_playback"))]
 #[macro_export]
 macro_rules! panic {
     // No argument is given.
diff --git a/tests/script-based-pre/playback_print/config.yml b/tests/script-based-pre/playback_print/config.yml
new file mode 100644
index 000000000000..abda4b73edb7
--- /dev/null
+++ b/tests/script-based-pre/playback_print/config.yml
@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: playback_print.sh
+expected: expected
diff --git a/tests/script-based-pre/playback_print/expected b/tests/script-based-pre/playback_print/expected
new file mode 100644
index 000000000000..b9a04bb58988
--- /dev/null
+++ b/tests/script-based-pre/playback_print/expected
@@ -0,0 +1,13 @@
+internal error: entered unreachable code: oops
+
+assertion `left == right` failed: Found 1 != 0
+left: 1
+right: 0
+
+assertion `left == right` failed
+left: 0
+right: 1
+
+Found value 2
+
+test result: FAILED. 0 passed; 4 failed
diff --git a/tests/script-based-pre/playback_print/playback_print.sh b/tests/script-based-pre/playback_print/playback_print.sh
new file mode 100755
index 000000000000..abcade64a218
--- /dev/null
+++ b/tests/script-based-pre/playback_print/playback_print.sh
@@ -0,0 +1,40 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+# Test that concrete playback -Z concrete-playback does not override std print
+# functions
+
+set -o nounset
+
+function error() {
+    echo $@
+    # Cleanup
+    rm ${RS_FILE}
+    rm output.log
+    exit 1
+}
+
+RS_FILE="modified.rs"
+cp print_vars.rs ${RS_FILE}
+export RUSTFLAGS="--edition 2021"
+
+echo "[TEST] Generate test..."
+kani ${RS_FILE} -Z concrete-playback --concrete-playback=inplace
+
+echo "[TEST] Run test..."
+kani playback -Z concrete-playback ${RS_FILE} 2>&1 | tee output.log
+
+echo "------ Check output ----------"
+
+set -e
+while read -r line; do
+    grep "${line}" output.log || error "Failed to find: \"${line}\""
+done < expected
+
+echo
+echo "------ Output OK ----------"
+echo
+
+# Cleanup
+rm ${RS_FILE}
+rm output.log
diff --git a/tests/script-based-pre/playback_print/print_vars.rs b/tests/script-based-pre/playback_print/print_vars.rs
new file mode 100644
index 000000000000..07457cbe9957
--- /dev/null
+++ b/tests/script-based-pre/playback_print/print_vars.rs
@@ -0,0 +1,20 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// compile-flags: --edition 2021
+// kani-flags: playback
+
+#[kani::proof]
+pub fn harness() {
+    let v1: u32 = kani::any();
+    let v2: u32 = kani::any();
+    // avoid direct assignments to v1 to block constant propagation.
+    kani::assume(v1 == v2);
+
+    match v2 {
+        0 => assert_eq!(v1, 1),
+        1 => assert_eq!(v1, 0, "Found {v1} != 0"),
+        2 => panic!("Found value {v1}"),
+        _ => unreachable!("oops"),
+    }
+}