`debug_assert` is disabled in the standard library due to poor assertion messages

[celinval]

The custom sysroot build for the MIR Linker introduced by #1717 builds the standard library in debug mode. This enables a bunch of safety checks and debug assertions from the standard library. Some of these checks are for intrinsics safety checks. The issues here are:

1. A lot of these checks make our intrinsics checks redundant.
2. The std checks are added before actually calling the intrinsic and they are not super user friendly.

For example, the following testcase from the expected suite: https://github.com/model-checking/kani/blob/78761bdac057a910a8f23f7622c0a3a9df6953fb/tests/expected/intrinsics/copy-nonoverlapping/copy-overflow/main.rs#L6-L18

Without the MIR Linker, it fails with the following error:

Failed Checks: copy_nonoverlapping: attempt to compute number in bytes which would overflow

With the MIR Linker, the error is:

Failed Checks: called `Option::unwrap()` on a `None` value 

This happens because of the std check is_nonoverlapping which has a call to checked_mul().unwrap(). The checked_mul() is None in the overflow scenario.

[celinval]

Another interesting one is that the checks are not encoded as normal debug_assert!() which panic!(), they call abort instead to optimize the compilation size. So other failures will look like:

Failed Checks: reached intrinsic::abort

[celinval]

The current behavior implemented for MIR Linker keeps the same behavior as before the MIR Linker. Enabling these checks are desirable but they are orthogonal to the MIR Linker work. Hence, I'm removing the link with the MIR Linker milestone.

[cameron1024]

Hi, I've just run into this issue trying to verify a program that depends on unicode-bidi, which has this snippet:

#[cfg(feature = "std")]
std::debug_assert!(
    false,
    "Found broken indices in level run: found indices {}..{} for string of length {}",
    level_run.start,
    level_run.end,
    text.len()
);

This fails with an error:

error: cannot find macro `__kani__workaround_core_assert` in this scope

I'm very new to kani, so I'm not exactly sure if this is actually the same issue, or just user error. I just stumbled upon this issue when googling.

Are there steps a user can take to work around this error? (Apologies if this is the wrong place to ask these sorts of questions :sweat_smile: )

[zhassan-aws]

Thanks for the bug report @cameron1024. Can you please file a separate issue and include information on how to reproduce the error, and the Kani version? Thanks!

[cameron1024]

Opened https://github.com/model-checking/kani/issues/2187

[celinval]

We should revisit this issue. One thing to keep it mind is how to distinguish UB checks and assertion failures.