Fix std overrides when crate has extern std (rust-lang#2989)

I tried applying model-checking/kani#2983 fix,
however, this would require user to import
`__kani_workaround_core_assert`. To fix that, I moved the definition to
be under `kani` crate.

I replaced the existing fixme test. Initially I didn't check we had one,
and I created a second one which is simpler (no cargo needed) but that
also includes other cases.

Resolves rust-lang#2187

Author: celinval

library/kani/src/lib.rs

@@ -288,6 +288,13 @@ macro_rules! cover {
     };
 }
 
+// Used to 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 and https://github.com/model-checking/kani/issues/2187
+#[doc(hidden)]
+#[cfg(not(feature = "concrete_playback"))]
+pub use core::assert as __kani__workaround_core_assert;
+
 // Kani proc macros must be in a separate crate
 pub use kani_macros::*;
 

library/std/src/lib.rs

@@ -12,13 +12,6 @@
 // re-export all std symbols
 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;
@@ -64,7 +57,7 @@ macro_rules! assert {
         // strategy, which is tracked in
         // https://github.com/model-checking/kani/issues/692
         if false {
-            __kani__workaround_core_assert!(true, $($arg)+);
+            kani::__kani__workaround_core_assert!(true, $($arg)+);
         }
     }};
 }
@@ -178,7 +171,7 @@ macro_rules! unreachable {
     // handle.
     ($fmt:expr, $($arg:tt)*) => {{
         if false {
-            __kani__workaround_core_assert!(true, $fmt, $($arg)+);
+            kani::__kani__workaround_core_assert!(true, $fmt, $($arg)+);
         }
         kani::panic(concat!("internal error: entered unreachable code: ",
         stringify!($fmt, $($arg)*)))}};
@@ -195,7 +188,7 @@ macro_rules! panic {
     // `panic!("Error message")`
     ($msg:literal $(,)?) => ({
         if false {
-            __kani__workaround_core_assert!(true, $msg);
+            kani::__kani__workaround_core_assert!(true, $msg);
         }
         kani::panic(concat!($msg))
     });
@@ -214,7 +207,7 @@ macro_rules! panic {
     // `panic!("Error: {}", code);`
     ($($arg:tt)+) => {{
         if false {
-            __kani__workaround_core_assert!(true, $($arg)+);
+            kani::__kani__workaround_core_assert!(true, $($arg)+);
         }
         kani::panic(stringify!($($arg)+));
     }};

tests/cargo-kani/no_std/Cargo.toml

@@ -0,0 +1,15 @@
+Checking harness foo...
+
+Status: SUCCESS\
+Description: ""debug_assert""\
+macro_override.rs:
+
+Status: SUCCESS\
+Description: "panic"\
+macro_override.rs:
+
+Status: SUCCESS\
+Description: "internal error: entered unreachable code: unreachable"\
+macro_override.rs:
+
+Complete - 1 successfully verified harnesses, 0 failures, 1 total.

tests/cargo-kani/no_std/foo.expected

@@ -0,0 +1,22 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Test if Kani can correctly identify assertions in a no_std crate that re-exports `std` library.
+//! Issue previously reported here: <https://github.com/model-checking/kani/issues/2187>
+//
+// compile-flags: --cfg=feature="std"
+#![no_std]
+
+#[cfg(feature = "std")]
+extern crate std;
+
+#[kani::proof]
+fn foo() {
+    std::debug_assert!(true, "debug_assert");
+    if kani::any_where(|b| !b) {
+        std::unreachable!("unreachable")
+    }
+    if kani::any_where(|val: &u8| *val > 10) < 10 {
+        std::panic!("panic")
+    }
+}