"cannot call non-const fn `kani::assert` in constant functions"

[tedinski]

Having a poke at building top-100 crates with Kani. Found this one frequently.

Cause is typically an assert! or panic! etc in a constant function. Probably we just need to make kani::assert and friends const?

[zhassan-aws]

Do you have an example?

[tedinski]

Good point. I believe this was the time crate?

[nano-o]

Hello, I'm trying kani and ran into the same issue. The codebase I want to analyze uses panic! in constant functions and this causes cargo kani to fail with "cannot call non-const fn kani::panic in constant functions".
Simple example:

const fn my_const_fn() {
    panic!()
}
#[cfg(kani)]
#[kani::proof]
pub fn check_something() {
    my_const_fn();
}

[zhassan-aws]

Thanks for the example @nano-o! This is due to how Kani defines the panic function:

kani/library/kani/src/lib.rs

Line 137 in 22316d1

pub fn panic(message: &'static str) -> ! {

Adding const to the function seems to fix the issue. I'm running the regressions and will submit a PR if everything looks good.

[tedinski]

Hmm. This is possibly not yet completely solved. It did fix most of the issues I saw but I ran into this:

error: `std::fmt::Arguments::<'a>::new_v1` is not yet stable as a const fn
   --> /home/ubuntu/.cargo/registry/src/github.com-1ecc6299db9ec823/time-0.3.14/src/format_description/well_known/iso8601/adt_hack.rs:148:13
    |
148 |             assert!(bytes[idx] == 0, "invalid configuration");
    |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |
    = help: add `#![feature(const_fmt_arguments_new)]` to the crate attributes to enable
    = note: this error originates in the macro `format_args` which comes from the expansion of the macro `assert` (in Nightly builds, run with -Z macro-backtrace for more info)

Which slightly confuses me. I think it might be triggerable just by building with the time crate.

[tedinski]

Reproduction steps:

$ cargo new time-test
     Created binary (application) `time-test` package
$ cd time-test/
$ cargo add time --features formatting
[..SNIP..]
$ cargo kani
   Compiling itoa v1.0.3
   Compiling time v0.3.14
error: `std::fmt::Arguments::<'a>::new_v1` is not yet stable as a const fn
   --> /home/ubuntu/.cargo/registry/src/github.com-1ecc6299db9ec823/time-0.3.14/src/format_description/well_known/iso8601/adt_hack.rs:148:13
    |
148 |             assert!(bytes[idx] == 0, "invalid configuration");
    |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |
    = help: add `#![feature(const_fmt_arguments_new)]` to the crate attributes to enable
    = note: this error originates in the macro `format_args` which comes from the expansion of the macro `assert` (in Nightly builds, run with -Z macro-backtrace for more info)

Error: "Failed to compile crate."
error: could not compile `time` due to previous error; 2 warnings emitted
Error: cargo exited with status exit status: 101

[zhassan-aws]

The non-const format_args was mentioned in an issue related to the const panic RFC: rust-lang/rust#86998. It seems they implemented a special solution for that, which is currently unstable. I'll dig into this.

[zhassan-aws]

Currently, the format_args! cannot be used in const contexts unless the const_fmt_arguments_new language feature is enabled. So, while this Rust program is accepted by rustc:

const fn const_fn() {
    assert!(1 + 1 == 2, "A message");
}

fn main() {
    const_fn();
}

$ rustc assert.rs && ./assert
$

This one isn't:

const fn const_fn() {
    format_args!("A message");
}

fn main() {
    const_fn();
}

$ rustc assert.rs && ./assert 
error: `Arguments::<'a>::new_v1` is not yet stable as a const fn
 --> assert.rs:2:5
  |
2 |     format_args!("A message");
  |     ^^^^^^^^^^^^^^^^^^^^^^^^^
  |
  = help: add `#![feature(const_fmt_arguments_new)]` to the crate attributes to enable
  = note: this error originates in the macro `format_args` (in Nightly builds, run with -Z macro-backtrace for more info)

error: erroneous constant used
 --> assert.rs:2:18
  |
2 |     format_args!("A message");
  |                  ^^^^^^^^^^^ referenced constant has errors
  |
  = note: `#[deny(const_err)]` on by default
  = warning: this was previously accepted by the compiler but is being phased out; it will become a hard error in a future release!
  = note: for more information, see issue #71800 <https://github.com/rust-lang/rust/issues/71800>

error: erroneous constant used
 --> assert.rs:2:5
  |
2 |     format_args!("A message");
  |     ^^^^^^^^^^^^^^^^^^^^^^^^^ referenced constant has errors
  |
  = warning: this was previously accepted by the compiler but is being phased out; it will become a hard error in a future release!
  = note: for more information, see issue #71800 <https://github.com/rust-lang/rust/issues/71800>
  = note: this error originates in the macro `format_args` (in Nightly builds, run with -Z macro-backtrace for more info)

error: aborting due to 3 previous errors

A workaround is to add:

![feature(const_fmt_arguments_new)]

to the root of the crate in which the assert is used (which may be difficult/impossible to do for dependent crates).

This issue should be resolved if/when const_fmt_arguments_new is stabilized .

[tedinski]

This got hit again: time-rs/time#521

[camshaft]

I think we need to redefine the assert macro

macro_rules! assert {
    ($cond:expr $(,)?) => {
        kani::assert($cond, concat!("assertion failed: ", stringify!($cond)));
    };
    ($cond:expr, $fmt:literal $(,)?) => {{
        kani::assert($cond, concat!(stringify!($fmt)));
        if false {
            let _ = $fmt;
        }
    }};
    ($cond:expr, $fmt:literal, $($arg:tt)+) => {{
        kani::assert($cond, concat!(stringify!($fmt, $($arg)+)));
        if false {
            let _ = format_args!($fmt, $($arg)+);
        }
    }};
}