Our `std` library cannot properly handle different editions

[celinval]

I tried this code:

#[cfg_attr(kani, kani::proof)]
#[cfg_attr(test, test)]
fn check_panic() {
    let msg = "Oops.";
    panic!(msg);
}

using the following command line invocation:

$ RUSTFLAGS="--edition 2021" kani test.rs --only-codegen

I only get a warning:

warning: unused variable: `msg`
 --> test.rs:5:9
  |
5 |     let msg = "Oops.";
  |         ^^^ help: if this is intentional, prefix it with an underscore: `_msg`
  |
  = note: `#[warn(unused_variables)]` on by default

warning: 1 warning emitted

with Kani version: 0.6.0

When we compile with rustc using 2021 edition:

$ rustc --test test.rs --edition 2021

this code doesn't compile:

error: format argument must be a string literal
 --> test.rs:6:12
  |
6 |     panic!(msg);
  |            ^^^
  |
help: you might be missing a string literal to format with
  |
6 |     panic!("{}", msg);
  |            +++++

error: aborting due to previous error

In the case of panic, unreachable and a few other macros, that have changed across editions, the rust compiler chooses the correct implementation. This mechanism is not available for us when we override macros. We should investigate what's the best way to handle that.

[bennofs]

I am hitting a variant of this issue, where my code doesn't compile since kani's macros use edition 2021. The following code compiles with rustc, if not using edition 2021:

fn main() {
    assert!(false, format!("{}", 42));
}

But kani produces:

Kani Rust Verifier 0.40.0 (standalone)
error: format argument must be a string literal
 --> foo.rs:2:20
  |
2 |     assert!(false, format!("{}", 42));
  |                    ^^^^^^^^^^^^^^^^^
  |
  = note: this error originates in the macro `format` (in Nightly builds, run with -Z macro-backtrace for more info)
help: you might be missing a string literal to format with
  |
2 |     assert!(false, "{}", format!("{}", 42));
  |                    +++++

error: aborting due to previous error

The issue here seems to be that kani's assert macro definition binds to the 2021-edition version, even though the macro is used in a non-2021 code. If I remove the __kani__workaround_core_assert! line from kani's assert definition, then the above code compiles fine.

It seems that macros use the assert! semantics corresponding to the edition of the crate that the macro is defined in, not the crate in which it used. A simple minimal project demonstrating this is here: https://github.com/bennofs/repros/tree/master/kani/%231375

[bennofs]

Do you have any ideas for a possible solution of this issue? I would like to fix this as I have a project where a dependency is using the non-edition-2021 assert, but I don't know much about rust compiler internals to know what the best approach here is.