Issue finding debug_assert in no_std crates when std enabled

[cameron1024]

I tried this code:

#![no_std]

#[cfg(feature = "std")]
extern crate std;

fn foo() {
    std::debug_assert!(true, "text");
}

using the following command line invocation:

cargo kani --features std

with Kani version: 0.20.0

I expected to see this happen: verification should succeed

Instead, this happened:

I get an error:

error: cannot find macro `__kani__workaround_core_assert` in this scope
 --> src/lib.rs:7:5
  |
7 |     std::debug_assert!(true, "text");
  |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  |
  = note: this error originates in the macro `$crate::assert` which comes from the expansion of the macro `std::debug_assert` (in Nightly builds, run with -Z macro-backtrace for more info)

Error: "Failed to compile crate."
error: could not compile `playground` due to previous error
Error: cargo exited with status exit status: 101

Stack backtrace:
   0: anyhow::error::<impl anyhow::Error>::msg
   1: kani_driver::session::KaniSession::run_terminal
   2: kani_driver::call_cargo::<impl kani_driver::session::KaniSession>::cargo_build
   3: kani_driver::project::cargo_project
   4: kani_driver::main
   5: std::sys_common::backtrace::__rust_begin_short_backtrace
   6: std::rt::lang_start::{{closure}}
   7: std::rt::lang_start_internal
   8: main
   9: __libc_start_call_main
  10: __libc_start_main_impl
  11: _start

I initially ran into this while trying to compile a transitive dependency: unicode-bidi, which has a similar snippet (it's found at: https://github.com/servo/unicode-bidi/blob/master/src/implicit.rs#L494).

All of the following make the bug disappear:

• removing #![no_std]
• removing extern crate std
• removing the std:: from std::debug_assert!(...)
• removing the "text" from std::debug_assert!(true, "text")

All of the following have no effect:

• adding #[cfg(feature = "std")] to the debug assert
• adding #[cfg(kani)] to fn foo()
• adding #[kani::proof] to fn foo()
• changing the assert to std::debug_assert!(false, "text");

I've tried to reduce it further, but it's pretty bare at this point.

The key ingredients seem to be:

• extern crate std; gated by a feature flag
• std::debug_assert!
• some actual text in the error message

I can't tell if this is caused by user error, or if there's a workaround I can use to verify my program even in the presence of this. I'm quite new to using kani, and am evaluating it for use at work, so apologies if there's some docs that explains this 😅

Thanks in advance 😁

[danielsn]

Thanks for the bug report @cameron1024. This is likely due to how we re-export the standard library to allow us to override certain macros https://github.com/model-checking/kani/blob/main/library/std/src/lib.rs

We are investigating.

[cameron1024]

Thanks for looking into it, love the project 😊

[zhassan-aws]

Re-opening as the fix has been reverted due to the issues it caused.

[adpaco-aws]

This also affects the harness in lading (DataDog) if one runs cargo kani on the workspace root, but it's possible to work around it for the time being with cargo kani -p lading-throttle