From 1308efb60cf172d8055dff1d22fa770b4f29f7d5 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Thu, 20 Apr 2023 00:13:04 -0700
Subject: [PATCH 1/2] Define different function for concrete playback

It looks like the `if cfg!()` is no longer being propagated and the
concrete playback code is increasing the logic that the compiler detects
as reachable.
---
 library/kani/src/lib.rs | 41 ++++++++++++++++++++++++++++-------------
 1 file changed, 28 insertions(+), 13 deletions(-)

diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs
index e82b57d35457..7807a4068beb 100644
--- a/library/kani/src/lib.rs
+++ b/library/kani/src/lib.rs
@@ -48,10 +48,16 @@ pub use futures::block_on;
 /// ```
 #[inline(never)]
 #[rustc_diagnostic_item = "KaniAssume"]
-pub fn assume(_cond: bool) {
-    if cfg!(feature = "concrete_playback") {
-        assert!(_cond, "kani::assume should always hold");
-    }
+#[cfg(not(feature = "concrete_playback"))]
+pub fn assume(cond: bool) {
+    let _ = cond;
+}
+
+#[inline(never)]
+#[rustc_diagnostic_item = "KaniAssume"]
+#[cfg(feature = "concrete_playback")]
+pub fn assume(cond: bool) {
+    assert!(cond, "kani::assume should always hold");
 }
 
 /// Creates an assertion of the specified condition and message.
@@ -63,12 +69,19 @@ pub fn assume(_cond: bool) {
 /// let y = !x;
 /// kani::assert(x || y, "ORing a boolean variable with its negation must be true")
 /// ```
+#[cfg(not(feature = "concrete_playback"))]
+#[inline(never)]
+#[rustc_diagnostic_item = "KaniAssert"]
+pub const fn assert(cond: bool, msg: &'static str) {
+    let _ = cond;
+    let _ = msg;
+}
+
+#[cfg(feature = "concrete_playback")]
 #[inline(never)]
 #[rustc_diagnostic_item = "KaniAssert"]
-pub const fn assert(_cond: bool, _msg: &'static str) {
-    if cfg!(feature = "concrete_playback") {
-        assert!(_cond, "{}", _msg);
-    }
+pub const fn assert(cond: bool, msg: &'static str) {
+    assert!(cond, "{}", msg);
 }
 
 /// Creates a cover property with the specified condition and message.
@@ -153,15 +166,17 @@ pub fn any_where<T: Arbitrary, F: FnOnce(&T) -> bool>(f: F) -> T {
 ///
 /// Note that SIZE_T must be equal the size of type T in bytes.
 #[inline(never)]
+#[cfg(not(feature = "concrete_playback"))]
 pub(crate) unsafe fn any_raw_internal<T, const SIZE_T: usize>() -> T {
-    #[cfg(feature = "concrete_playback")]
-    return concrete_playback::any_raw_internal::<T, SIZE_T>();
-
-    #[cfg(not(feature = "concrete_playback"))]
-    #[allow(unreachable_code)]
     any_raw_inner::<T>()
 }
 
+#[inline(never)]
+#[cfg(feature = "concrete_playback")]
+pub(crate) unsafe fn any_raw_internal<T, const SIZE_T: usize>() -> T {
+    return concrete_playback::any_raw_internal::<T, SIZE_T>();
+}
+
 /// This low-level function returns nondet bytes of size T.
 #[rustc_diagnostic_item = "KaniAnyRaw"]
 #[inline(never)]

From 6ea2a52988d6ad0416fe459371374b617b123341 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Wed, 26 Apr 2023 13:51:10 -0700
Subject: [PATCH 2/2] Apply suggestions from code review

Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
---
 library/kani/src/lib.rs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs
index 7807a4068beb..8dd1c68a06e3 100644
--- a/library/kani/src/lib.rs
+++ b/library/kani/src/lib.rs
@@ -57,7 +57,7 @@ pub fn assume(cond: bool) {
 #[rustc_diagnostic_item = "KaniAssume"]
 #[cfg(feature = "concrete_playback")]
 pub fn assume(cond: bool) {
-    assert!(cond, "kani::assume should always hold");
+    assert!(cond, "`kani::assume` should always hold");
 }
 
 /// Creates an assertion of the specified condition and message.
@@ -174,7 +174,7 @@ pub(crate) unsafe fn any_raw_internal<T, const SIZE_T: usize>() -> T {
 #[inline(never)]
 #[cfg(feature = "concrete_playback")]
 pub(crate) unsafe fn any_raw_internal<T, const SIZE_T: usize>() -> T {
-    return concrete_playback::any_raw_internal::<T, SIZE_T>();
+    concrete_playback::any_raw_internal::<T, SIZE_T>()
 }
 
 /// This low-level function returns nondet bytes of size T.