Add support for edition 2018 crates using assert! (Fixes #3717) (#4096)

We export `core::assert` as `__kani__workaround_core_assert!` to every
crate which uses `assert`. Because kani uses edition 2021, crates which
are built edition 2018 now use the 2021 `assert`.

The behaviour of `assert` changed between both editions (see
https://doc.rust-lang.org/nightly/edition-guide/rust-2021/panic-macro-consistency.html).

This commit adds an extra clause to handle the case, if the first
message parameter isn't of string type and adds a format string
accordingly

This resolves #3717 . 

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Zyad Hassan <zyadh@amazon.com>
Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>

Author: sintemal

library/std/src/lib.rs

@@ -43,8 +43,15 @@ macro_rules! assert {
         // The double negation is to resolve https://github.com/model-checking/kani/issues/2108
         kani::assert(!!$cond, concat!("assertion failed: ", stringify!($cond)));
     };
-    ($cond:expr, $($arg:tt)+) => {{
-        kani::assert(!!$cond, concat!(stringify!($($arg)+)));
+    // Before edition 2021, the `assert!` macro could take a single argument
+    // that wasn't a string literal. This is not supported in edition 2021 and above.
+    // Because we reexport the 2021 edition macro, we need to support this
+    // case. For this, if there is a single argument we do the following:
+    // If it is a literal: Just pass it through and stringify it.
+    // If it isn't a literal: We add a default format
+    // specifier to the macro (see https://github.com/model-checking/kani/issues/1375).
+    ($cond:expr, $first:literal $(,)?) => {{
+        kani::assert(!!$cond, stringify!($first));
         // Process the arguments of the assert inside an unreachable block. This
         // is to make sure errors in the arguments (e.g. an unknown variable or
         // an argument that does not implement the Display or Debug traits) are
@@ -56,6 +63,20 @@ macro_rules! assert {
         // effects). This is fine until we add support for the "unwind" panic
         // strategy, which is tracked in
         // https://github.com/model-checking/kani/issues/692
+        if false {
+            kani::__kani__workaround_core_assert!(true, "{}", $first);
+        }
+    }};
+    ($cond:expr, $first:expr $(,)?) => {{
+        kani::assert(!!$cond, stringify!($first));
+        // See comment above
+        if false {
+            kani::__kani__workaround_core_assert!(true, "{}", $first);
+        }
+    }};
+    ($cond:expr, $($arg:tt)+) => {{
+        kani::assert(!!$cond, concat!(stringify!($($arg)+)));
+        // See comment above
         if false {
             kani::__kani__workaround_core_assert!(true, $($arg)+);
         }

tests/coverage/abort/expected

@@ -17,5 +17,5 @@
   17|    0|             ```process::exit'''(1);\
   18|    1|         } \
   19|     |     }\
-  20|    0|     ```assert!'''(false, ```"This is unreachable"''');\
+  20|    0|     ```assert!'''(false, "This is unreachable");\
   21|     | }\

tests/coverage/debug-assert/expected

@@ -9,7 +9,7 @@
    9|     | #[kani::proof]\
   10|    1| fn main() {\
   11|    1|     for i in 0..4 {\
-  12|    1|         debug_assert!(i > 0, ```"This should fail and stop the execution"''');\
-  13|    0|         ```assert!(i == 0''', ```"This should be unreachable"''');\
+  12|    1|         debug_assert!(i > 0, "This should fail and stop the execution");\
+  13|    0|         ```assert!(i == 0''', "This should be unreachable");\
   14|     |     }\
   15|     | }\

tests/kani/Assert/assert2018.rs

@@ -0,0 +1,19 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// compile-flags: --edition 2018
+// Check that an assert that uses a pre-Rust-2018 style, where a string is
+// directly used without a format string literal is accepted by Kani
+// This was previously failing:
+// https://github.com/model-checking/kani/issues/3717
+
+#[kani::proof]
+fn check_assert_2018() {
+    let s = String::new();
+    // This is deprecated in Rust 2018 and is a hard error starting Rust 2021.
+    // One should instead use:
+    // ```
+    // assert!(true, "{}", s);
+    // ```
+    assert!(true, s);
+}