From 96e636d737fa48ee0322070f2e6a6cfe8f45f77e Mon Sep 17 00:00:00 2001 From: sintemal Date: Wed, 21 May 2025 23:12:58 +0200 Subject: [PATCH 1/4] Before edition 2021, the `assert!` macro could take a single argument that wasn't a literal. This is not supported in edition 2021 and above. Because we reexport the 2021 edition macro, we need to support this case. This commits adds a special case, if there is only one argument to the assert macro --- library/std/src/lib.rs | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/library/std/src/lib.rs b/library/std/src/lib.rs index 3f8427ffff13..28b61a12282f 100644 --- a/library/std/src/lib.rs +++ b/library/std/src/lib.rs @@ -43,8 +43,13 @@ 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 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 add a default format + // parameter to the macro (see https://github.com/model-checking/kani/issues/1375). + ($cond:expr, $first:expr $(,)?) => {{ + kani::assert(!!$cond, concat!(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 +61,13 @@ 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, $($arg:tt)+) => {{ + kani::assert(!!$cond, concat!(stringify!($($arg)+))); + // See comment above if false { kani::__kani__workaround_core_assert!(true, $($arg)+); } From a2eaa117efae8fbc101cbb3ff1518ab70a2ba1d5 Mon Sep 17 00:00:00 2001 From: sintemal Date: Thu, 22 May 2025 14:25:02 +0200 Subject: [PATCH 2/4] If the string is already a literal, do not add a format specifier but stringify it instead. This helps rustc with coverage information. --- library/std/src/lib.rs | 19 ++++++++++++++----- 1 file changed, 14 insertions(+), 5 deletions(-) diff --git a/library/std/src/lib.rs b/library/std/src/lib.rs index 28b61a12282f..87582ab2399d 100644 --- a/library/std/src/lib.rs +++ b/library/std/src/lib.rs @@ -44,12 +44,14 @@ macro_rules! assert { kani::assert(!!$cond, concat!("assertion failed: ", stringify!($cond))); }; // Before edition 2021, the `assert!` macro could take a single argument - // that wasn't a literal. This is not supported in edition 2021 and above. + // 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 add a default format - // parameter to the macro (see https://github.com/model-checking/kani/issues/1375). - ($cond:expr, $first:expr $(,)?) => {{ - kani::assert(!!$cond, concat!(stringify!($first))); + // 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 @@ -61,6 +63,13 @@ 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, stringify!($first)); + } + }}; + ($cond:expr, $first:expr $(,)?) => {{ + kani::assert(!!$cond, stringify!($first)); + // See comment above if false { kani::__kani__workaround_core_assert!(true, "{}", $first); } From 7019236c36212ac9842c73497cd3fd026b1f5f85 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Tue, 27 May 2025 15:57:10 -0700 Subject: [PATCH 3/4] Tweak macro and update coverage regressions --- library/std/src/lib.rs | 2 +- tests/coverage/abort/expected | 2 +- tests/coverage/debug-assert/expected | 4 ++-- tests/kani/Assert/assert2018.rs | 20 ++++++++++++++++++++ 4 files changed, 24 insertions(+), 4 deletions(-) create mode 100644 tests/kani/Assert/assert2018.rs diff --git a/library/std/src/lib.rs b/library/std/src/lib.rs index 87582ab2399d..59bbadbd4fbc 100644 --- a/library/std/src/lib.rs +++ b/library/std/src/lib.rs @@ -64,7 +64,7 @@ macro_rules! assert { // strategy, which is tracked in // https://github.com/model-checking/kani/issues/692 if false { - kani::__kani__workaround_core_assert!(true, stringify!($first)); + kani::__kani__workaround_core_assert!(true, "{}", $first); } }}; ($cond:expr, $first:expr $(,)?) => {{ diff --git a/tests/coverage/abort/expected b/tests/coverage/abort/expected index ae63575af3bc..c978a8c4e5e8 100644 --- a/tests/coverage/abort/expected +++ b/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| | }\ diff --git a/tests/coverage/debug-assert/expected b/tests/coverage/debug-assert/expected index d36fc11843d0..e246da74022a 100644 --- a/tests/coverage/debug-assert/expected +++ b/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| | }\ diff --git a/tests/kani/Assert/assert2018.rs b/tests/kani/Assert/assert2018.rs new file mode 100644 index 000000000000..62e18eae20d8 --- /dev/null +++ b/tests/kani/Assert/assert2018.rs @@ -0,0 +1,20 @@ +// 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); +} From 919b12f605672bc7409fa6cdd62dfe56698e351b Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Tue, 27 May 2025 16:03:11 -0700 Subject: [PATCH 4/4] Format --- tests/kani/Assert/assert2018.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/tests/kani/Assert/assert2018.rs b/tests/kani/Assert/assert2018.rs index 62e18eae20d8..c28712a6afc8 100644 --- a/tests/kani/Assert/assert2018.rs +++ b/tests/kani/Assert/assert2018.rs @@ -7,7 +7,6 @@ // This was previously failing: // https://github.com/model-checking/kani/issues/3717 - #[kani::proof] fn check_assert_2018() { let s = String::new();