Fix compilation of panic!() when the arg is another macro. (#1407)

library/std/src/lib.rs

@@ -158,7 +158,9 @@ macro_rules! unreachable {
     );
     // The first argument is the format and the rest contains tokens to be included in the msg.
     // `unreachable!("Error: {}", code);`
-    ($fmt:literal, $($arg:tt)*) => (
+    // We have the same issue as with panic!() described bellow where we over-approx what we can
+    // handle.
+    ($fmt:expr, $($arg:tt)*) => (
         kani::panic(concat!("internal error: entered unreachable code: ",
         stringify!($fmt, $($arg)*))));
 }
@@ -185,9 +187,19 @@ macro_rules! panic {
     ($msg:expr $(,)?) => ({
         kani::panic(stringify!($msg));
     });
-    // The first argument is the format and the rest contains tokens to be included in the msg.
+    // The first argument is the message and the rest contains tokens to be included in the msg.
     // `panic!("Error: {}", code);`
-    ($msg:literal, $($arg:tt)+) => ({
+    //
+    // 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)+) => ({
         kani::panic(stringify!($msg, $($arg)+));
     });
 }

tests/expected/panic/panic-2018/expected

@@ -1,5 +1,10 @@
+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

tests/expected/panic/panic-2018/messages.rs

@@ -11,3 +11,8 @@ include! {"../test.rs"}
 fn check_panic_2018() {
     check_panic();
 }
+
+#[kani::proof]
+fn check_user_panic_macro() {
+    panic_oob!("try_insert", 5, 3);
+}

tests/expected/panic/panic-2021/expected

@@ -1,5 +1,10 @@
+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

tests/expected/panic/panic-2021/messages.rs

@@ -11,3 +11,8 @@ include! {"../test.rs"}
 fn check_panic_2021() {
     check_panic();
 }
+
+#[kani::proof]
+fn check_user_panic_macro() {
+    panic_oob!("try_insert", 5, 3);
+}

tests/expected/panic/test.rs

@@ -8,6 +8,20 @@ fn check_panic() {
         1 => panic!("Panic message"),
         2 => panic!("Panic message with arg {}", "str"),
         3 => panic!("{}", msg),
-        _ => panic!(msg),
+        4 => panic!(msg),
+        _ => panic!(concat!("Panic: {} code: ", 10), msg),
     }
 }
+
+macro_rules! panic_oob {
+    ($method_name:expr, $index:expr, $len:expr) => {
+        panic!(
+            concat!(
+                "ArrayVec::",
+                $method_name,
+                ": index {} is out of bounds in vector of length {}"
+            ),
+            $index, $len
+        )
+    };
+}

tests/expected/unreachable/expected

@@ -3,4 +3,4 @@ Failed Checks: internal error: entered unreachable code:
 Failed Checks: internal error: entered unreachable code: Error message
 Failed Checks: internal error: entered unreachable code: "Unreachable message with arg {}", "str"
 Failed Checks: internal error: entered unreachable code: "{}", msg
-
+Failed Checks: internal error: entered unreachable code: concat!("My", " error", " message")

tests/expected/unreachable/unreach_msg.rs

@@ -10,6 +10,7 @@ fn check_unreachable() {
         1 => unreachable!("Error message"),
         2 => unreachable!("Unreachable message with arg {}", "str"),
         3 => unreachable!("{}", msg),
+        4 => unreachable!(concat!("My", " error", " message")),
         _ => unreachable!(msg),
     }
 }