Allow panic with args to be called in a const context

library/std/src/lib.rs

@@ -54,7 +54,7 @@ macro_rules! assert {
         // strategy, which is tracked in
         // https://github.com/model-checking/kani/issues/692
         if false {
-            ::std::panic!($($arg)+);
+            core::assert!(true, $($arg)+);
         }
     }};
 }
@@ -158,7 +158,7 @@ macro_rules! unreachable {
     // handle.
     ($fmt:expr, $($arg:tt)*) => {{
         if false {
-            let _ = format_args!($fmt, $($arg)+);
+            core::assert!(true, $fmt, $($arg)+);
         }
         kani::panic(concat!("internal error: entered unreachable code: ",
         stringify!($fmt, $($arg)*)))}};
@@ -186,22 +186,12 @@ macro_rules! panic {
     ($msg:expr $(,)?) => ({
         kani::panic(stringify!($msg));
     });
-    // The first argument is the message and the rest contains tokens to be included in the msg.
+    // All other cases, e.g.:
     // `panic!("Error: {}", code);`
-    //
-    // Note: This macro may match things that wouldn't be accepted by the panic!() macro. we have
-    // decided to over-approximate the matching so we can deal with things like macro inside a macro
-    // E.g.:
-    // ```
-    // panic!(concat!("Message {}", " split in two"), argument);
-    // ```
-    // The std implementation of `panic!()` macro is implemented in the compiler and it seems to
-    // be able to do things that we cannot do here.
-    // https://github.com/rust-lang/rust/blob/dc2d232c7485c60dd856f8b9aee83426492d4661/compiler/rustc_expand/src/base.rs#L1197
-    ($msg:expr, $($arg:tt)+) => {{
+    ($($arg:tt)+) => {{
         if false {
-            let _ = format_args!($msg, $($arg)+);
+            core::assert!(true, $($arg)+);
         }
-        kani::panic(stringify!($msg, $($arg)+));
+        kani::panic(stringify!($($arg)+));
     }};
 }

tests/expected/panic/arg-error/expected

@@ -0,0 +1,2 @@
+error: 1 positional argument in format string, but no arguments were given
+error: aborting due to previous error

tests/expected/panic/arg-error/test.rs

@@ -0,0 +1,15 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// compile-flags: --edition 2021
+
+//! This test checks that Kani processes arguments of panic macros and produces
+//! a compile error for invalid arguments (e.g. missing argument)
+
+const fn my_const_fn(msg: &str) -> ! {
+    core::panic!("{}")
+}
+
+#[kani::proof]
+fn check_panic_arg_error() {
+    my_const_fn("failed");
+}

tests/expected/panic/panic-2018/expected

@@ -1,10 +1,10 @@
-Failed Checks: concat!("Panic: {} code: ", 10), msg
+Failed Checks: concat! ("Panic: {} code: ", 10), msg
 Failed Checks: msg
 Failed Checks: explicit panic
 Failed Checks: Panic message
 Failed Checks: "Panic message with arg {}", "str"
 Failed Checks: "{}", msg
 
-Failed Checks: concat!("ArrayVec::", "try_insert",\
-": index {} is out of bounds in vector of length {}"),\
-5, 3
+Failed Checks: concat!\
+("ArrayVec::", "try_insert",\
+": index {} is out of bounds in vector of length {}"), 5, 3

tests/expected/panic/panic-2021/expected

@@ -1,10 +1,10 @@
-Failed Checks: concat!("Panic: {} code: ", 10), msg
+Failed Checks: concat! ("Panic: {} code: ", 10), msg
 Failed Checks: msg
 Failed Checks: explicit panic
 Failed Checks: Panic message
 Failed Checks: "Panic message with arg {}", "str"
 Failed Checks: "{}", msg
 
-Failed Checks: concat!("ArrayVec::", "try_insert",\
-": index {} is out of bounds in vector of length {}"),\
-5, 3
+Failed Checks: concat!\
+("ArrayVec::", "try_insert",\
+": index {} is out of bounds in vector of length {}"), 5, 3

tests/kani/Panic/compile_panic.rs

@@ -0,0 +1,15 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-check-fail
+
+//! This test checks that Kani fails in compilation due to a panic evaluated at
+//! compile time
+
+const fn my_const_fn(x: i32) -> i32 {
+    if x > 0 { x - 1 } else { panic!("x is negative") }
+}
+
+#[kani::proof]
+pub fn check_something() {
+    const _X: i32 = my_const_fn(-3);
+}

tests/kani/Panic/const_args.rs

@@ -0,0 +1,16 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test checks that `panic!` with args can be used in a const fn
+
+const fn my_const_fn(msg: &str) -> ! {
+    panic!("{}", msg)
+}
+
+#[kani::proof]
+pub fn check_something() {
+    let x: u8 = if kani::any() { 3 } else { 95 };
+    if x > 100 {
+        my_const_fn("x is greater than 100");
+    }
+}