From 1d7f717fb703196052920109bdf80582e7ebddae Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Wed, 13 Jul 2022 14:51:31 -0700
Subject: [PATCH] Fix `unreachable!()` override macro + new tests (#1372)

My latest change to handling panic messages actually broke `unreachable`
macro. The main issue was the wrong position of a parenthesis and the
fact that we didn't have tests that covered that specific case of the
macro.

One thing I haven't figured out yet is how to trigger an error if the
user code uses edition 2021+ and has the following construct:

```rust
let msg = "blah";
panic!(msg);
```

This is actually an error in 2021+, but the macro override that we
perform accepts that no matter the edition.
---
 library/std/src/lib.rs                    | 37 ++++++++++++++++++++---
 tests/expected/unreachable/expected       |  6 ++++
 tests/expected/unreachable/unreach_msg.rs | 15 +++++++++
 3 files changed, 54 insertions(+), 4 deletions(-)
 create mode 100644 tests/expected/unreachable/expected
 create mode 100644 tests/expected/unreachable/unreach_msg.rs

diff --git a/library/std/src/lib.rs b/library/std/src/lib.rs
index a7b1d81d7be28..aa429d3ffedea 100644
--- a/library/std/src/lib.rs
+++ b/library/std/src/lib.rs
@@ -140,25 +140,54 @@ macro_rules! eprintln {
 
 #[macro_export]
 macro_rules! unreachable {
+    // The argument, if present, is a literal that represents the error message, i.e.:
+    // `unreachable!("Error message")` or `unreachable!()`
     ($($msg:literal)? $(,)?) => (
         kani::panic(concat!("internal error: entered unreachable code: ", $($msg)?))
     );
-    ($fmt:expr, $($arg:tt)*) => (
-        kani::panic(concat!("internal error: entered unreachable code: ", $fmt), stringify!($($arg)*)));
+    // The argument is an expression, such as a variable.
+    // ```
+    // let msg = format!("Error: {}", code);
+    // unreachable!(msg);
+    // ```
+    // This was supported for 2018 and older rust editions.
+    // TODO: Is it possible to trigger an error if 2021 and above?
+    // https://github.com/model-checking/kani/issues/1375
+    ($($msg:expr)? $(,)?) => (
+        kani::panic(concat!("internal error: entered unreachable code: ", stringify!($($msg)?)))
+    );
+    // The first argument is the format and the rest contains tokens to be included in the msg.
+    // `unreachable!("Error: {}", code);`
+    ($fmt:literal, $($arg:tt)*) => (
+        kani::panic(concat!("internal error: entered unreachable code: ",
+        stringify!($fmt, $($arg)*))));
 }
 
 #[macro_export]
 macro_rules! panic {
+    // No argument is given.
     () => (
         kani::panic("explicit panic")
     );
+    // The argument is a literal that represents the error message, i.e.:
+    // `panic!("Error message")`
     ($msg:literal $(,)?) => ({
         kani::panic(concat!($msg));
     });
+    // The argument is an expression, such as a variable.
+    // ```
+    // let msg = format!("Error: {}", code);
+    // panic!(msg);
+    // ```
+    // This was supported for 2018 and older rust editions.
+    // TODO: Is it possible to trigger an error if 2021 and above?
+    // https://github.com/model-checking/kani/issues/1375
     ($msg:expr $(,)?) => ({
         kani::panic(stringify!($msg));
     });
-    ($msg:expr, $($arg:tt)*) => ({
-        kani::panic(stringify!($msg, $($arg)*));
+    // The first argument is the format and the rest contains tokens to be included in the msg.
+    // `panic!("Error: {}", code);`
+    ($msg:literal, $($arg:tt)+) => ({
+        kani::panic(stringify!($msg, $($arg)+));
     });
 }
diff --git a/tests/expected/unreachable/expected b/tests/expected/unreachable/expected
new file mode 100644
index 0000000000000..37eb2240fae59
--- /dev/null
+++ b/tests/expected/unreachable/expected
@@ -0,0 +1,6 @@
+Failed Checks: internal error: entered unreachable code: msg
+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
+
diff --git a/tests/expected/unreachable/unreach_msg.rs b/tests/expected/unreachable/unreach_msg.rs
new file mode 100644
index 0000000000000..14f5755270f66
--- /dev/null
+++ b/tests/expected/unreachable/unreach_msg.rs
@@ -0,0 +1,15 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Checks that our macro override supports different types of messages.
+#[kani::proof]
+fn check_unreachable() {
+    let msg = "Oops.";
+    match kani::any::<u8>() {
+        0 => unreachable!(),
+        1 => unreachable!("Error message"),
+        2 => unreachable!("Unreachable message with arg {}", "str"),
+        3 => unreachable!("{}", msg),
+        _ => unreachable!(msg),
+    }
+}