Do not override std library during playback (#2852)

We override a few std functions to improve verification time or
verification results, however, those functions are quite helpful during
concrete execution. Thus, avoid overriding functions when executing
concrete playback.

Resolves #2850

Co-authored-by: Adrian Palacios <[email protected]>

Author: celinval

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,45 +107,53 @@ 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)*); })
 }
 
 // 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.

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

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

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 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

tests/script-based-pre/playback_print/print_vars.rs

@@ -0,0 +1,19 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Harness used to test that playback do not override assertion and panic functions.
+
+#[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"),
+    }
+}