"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/git.luolix.top-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/git.luolix.top-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)+);
        }
    }};
}

[zhassan-aws]

Thanks @camshaft for the great suggestion! The only downside is that Kani would fail to report errors/warnings in the format literal, e.g.

#[cfg(kani)]
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)+);
        }
    }};
}

#[cfg_attr(kani, kani::proof)]
fn main() {
    assert!(1 + 1 == 2, "Hello world {}");
}

rustc:

$ rustc test_const.rs 
warning: panic message contains an unused formatting placeholder
  --> test_const.rs:22:38
   |
22 |     assert!(1 + 1 == 2, "Hello world {}");
   |                                      ^^
   |
   = note: this message is not used as a format string when given without arguments, but will be in Rust 2021
   = note: `#[warn(non_fmt_panics)]` on by default
help: add the missing argument
   |
22 |     assert!(1 + 1 == 2, "Hello world {}", ...);
   |                                         +++++
help: or add a "{}" format string to use the message literally
   |
22 |     assert!(1 + 1 == 2, "{}", "Hello world {}");
   |                         +++++

warning: 1 warning emitted

rustc 2021:

$ rustc --edition 2021 test_const.rs 
error: 1 positional argument in format string, but no arguments were given
  --> test_const.rs:22:38
   |
22 |     assert!(1 + 1 == 2, "Hello world {}");
   |                                      ^^

error: aborting due to previous error

Kani

$ kani test_const.rs 
Checking harness main...
CBMC 5.67.0 (cbmc-5.67.0)
CBMC version 5.67.0 (cbmc-5.67.0) 64-bit x86_64 linux
Reading GOTO program from file test_const.out.for-main
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 16 object bits, 48 offset bits (user-specified)
Starting Bounded Model Checking
Runtime Symex: 0.000678171s
size of program expression: 45 steps
slicing removed 27 assignments
Generated 2 VCC(s), 1 remaining after simplification
Runtime Postprocess Equation: 1.6311e-05s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 2.8521e-05s
Running propositional reduction
Post-processing
Runtime Post-process: 1.072e-05s
Solving with MiniSAT 2.2.1 with simplifier
0 variables, 0 clauses
SAT checker: instance is SATISFIABLE
Runtime Solver: 3.8802e-05s
Runtime decision procedure: 0.000100895s

RESULTS:
Check 1: main.assertion.1
         - Status: SUCCESS
         - Description: ""Hello world {a}""
         - Location: test_const.rs:22:5 in function main


SUMMARY:
 ** 0 of 1 failed

VERIFICATION:- SUCCESSFUL

Verification Time: 0.015771724s

but perhaps this is OK until format_args is allowed in const contexts?

[camshaft]

Yeah that's a good point. Could you forward the string on to panic instead?

if false {
    ::std::panic!($($arg)+);
}

[zhassan-aws]

That's a great idea! This works if I use core::panic (since Kani overrides std::panic). Both core::panic and ::std::panic work. Will submit a PR shortly.

[zhassan-aws]

D'oh, this still doesn't work with cf017e8 for const panics, e.g.:

const fn my_const_fn(msg: &str) -> ! {
    panic!("{}", msg)
}

#[cfg_attr(kani, kani::proof)]
fn main() {
    my_const_fn("failed");
}

$ rustc const_panic.rs 
$ ./const_panic 
thread 'main' panicked at 'failed', const_panic.rs:2:5
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
$ kani const_panic.rs 
error[E0015]: cannot call non-const formatting macro in constant functions
 --> const_panic.rs:2:18
  |
2 |     panic!("{}", msg)
  |                  ^^^
  |
  = note: calls in constant functions are limited to constant functions, tuple structs and tuple variants
  = note: this error originates in the macro `format_args` which comes from the expansion of the macro `panic` (in Nightly builds, run with -Z macro-backtrace for more info)

error: `std::fmt::Arguments::<'a>::new_v1` is not yet stable as a const fn
 --> const_panic.rs:2:5
  |
2 |     panic!("{}", msg)
  |     ^^^^^^^^^^^^^^^^^
  |
  = 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 `panic` (in Nightly builds, run with -Z macro-backtrace for more info)

error[E0080]: erroneous constant used
 --> const_panic.rs:2:12
  |
2 |     panic!("{}", msg)
  |            ^^^^ referenced constant has errors

error: aborting due to 3 previous errors

Some errors have detailed explanations: E0015, E0080.
For more information about an error, try `rustc --explain E0015`.
Error: "Failed to compile crate."
Error: /home/ubuntu/git/kani/target/kani/bin/kani-compiler exited with status exit status: 1

Re-opening.