From ceefdba42a64113d0b21d53300e30fefa465dd89 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 18 Oct 2024 13:52:23 -0700 Subject: [PATCH] Breaking change: Make `kani::check` private In the previous release, we added a deprecation warning to `kani::check` which was incorrectly exposed in our crate interface. Make this private and remove the deprecation tag. --- library/kani/src/lib.rs | 2 - library/kani_core/src/lib.rs | 75 +++++++------------ library/kani_core/src/mem.rs | 2 +- .../deprecated_warning.expected | 1 - .../ui/check_deprecated/deprecated_warning.rs | 10 --- 5 files changed, 28 insertions(+), 62 deletions(-) delete mode 100644 tests/ui/check_deprecated/deprecated_warning.expected delete mode 100644 tests/ui/check_deprecated/deprecated_warning.rs diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index ce1eeb992121..053af760067b 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -19,8 +19,6 @@ #![feature(ptr_metadata)] #![feature(f16)] #![feature(f128)] -// Need to add this since we are deprecating `kani::check`. Remove this when we remove that API. -#![allow(deprecated)] // Allow us to use `kani::` to access crate features. extern crate self as kani; diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index ee0092554e56..4919473bf0f1 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -42,7 +42,6 @@ macro_rules! kani_lib { pub use kani_core::*; kani_core::kani_intrinsics!(core); kani_core::generate_arbitrary!(core); - kani_core::check_intrinsic!(); pub mod mem { kani_core::kani_mem!(core); @@ -59,10 +58,6 @@ macro_rules! kani_lib { kani_core::kani_intrinsics!(std); kani_core::generate_arbitrary!(std); - kani_core::check_intrinsic! { - msg="This API will be made private in future releases.", vis=pub - } - pub mod mem { kani_core::kani_mem!(std); } @@ -462,51 +457,35 @@ macro_rules! kani_intrinsics { /// Stub the body with its contract. pub const REPLACE: Mode = 3; - } - }; -} -#[macro_export] -macro_rules! check_intrinsic { - ($(msg=$msg:literal, vis=$vis:vis)?) => { - /// Creates a non-fatal property with the specified condition and message. - /// - /// This check will not impact the program control flow even when it fails. - /// - /// # Example: - /// - /// ```no_run - /// let x: bool = kani::any(); - /// let y = !x; - /// kani::check(x || y, "ORing a boolean variable with its negation must be true"); - /// kani::check(x == y, "A boolean variable is always different than its negation"); - /// kani::cover!(true, "This should still be reachable"); - /// ``` - /// - /// # Deprecated - /// - /// This function was meant to be internal only, and it was added to Kani's public interface - /// by mistake. Thus, it will be made private in future releases. - /// Instead, we recommend users to either use `assert` or `cover` to create properties they - /// would like to verify. - /// - /// See for more details. - #[cfg(not(feature = "concrete_playback"))] - #[inline(never)] - #[rustc_diagnostic_item = "KaniCheck"] - // TODO: Remove the `#![allow(deprecated)]` inside kani's crate once this is made private. - $(#[deprecated(since="0.55.0", note=$msg)])? - $($vis)? const fn check(cond: bool, msg: &'static str) { - let _ = cond; - let _ = msg; - } + /// Creates a non-fatal property with the specified condition and message. + /// + /// This check will not impact the program control flow even when it fails. + /// + /// # Example: + /// + /// ```no_run + /// let x: bool = kani::any(); + /// let y = !x; + /// kani::check(x || y, "ORing a boolean variable with its negation must be true"); + /// kani::check(x == y, "A boolean variable is always different than its negation"); + /// kani::cover!(true, "This should still be reachable"); + /// ``` + /// + #[cfg(not(feature = "concrete_playback"))] + #[inline(never)] + #[rustc_diagnostic_item = "KaniCheck"] + pub(crate) const fn check(cond: bool, msg: &'static str) { + let _ = cond; + let _ = msg; + } - #[cfg(feature = "concrete_playback")] - #[inline(never)] - #[rustc_diagnostic_item = "KaniCheck"] - $(#[deprecated(since="0.55.0", note=$msg)])? - $($vis)? const fn check(cond: bool, msg: &'static str) { - assert!(cond, "{}", msg); + #[cfg(feature = "concrete_playback")] + #[inline(never)] + #[rustc_diagnostic_item = "KaniCheck"] + pub(crate) const fn check(cond: bool, msg: &'static str) { + assert!(cond, "{}", msg); + } } }; } diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs index c8501e977096..2a2676c61db3 100644 --- a/library/kani_core/src/mem.rs +++ b/library/kani_core/src/mem.rs @@ -327,7 +327,7 @@ macro_rules! kani_mem { /// A helper to assert `is_initialized` to use it as a part of other predicates. fn assert_is_initialized(ptr: *const T) -> bool { - super::check( + super::internal::check( is_initialized(ptr), "Undefined Behavior: Reading from an uninitialized pointer", ); diff --git a/tests/ui/check_deprecated/deprecated_warning.expected b/tests/ui/check_deprecated/deprecated_warning.expected deleted file mode 100644 index 3a0760035f8b..000000000000 --- a/tests/ui/check_deprecated/deprecated_warning.expected +++ /dev/null @@ -1 +0,0 @@ -warning: use of deprecated function `kani::check`: This API will be made private in future releases. diff --git a/tests/ui/check_deprecated/deprecated_warning.rs b/tests/ui/check_deprecated/deprecated_warning.rs deleted file mode 100644 index f3d791256081..000000000000 --- a/tests/ui/check_deprecated/deprecated_warning.rs +++ /dev/null @@ -1,10 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT -// -// kani-flags: --only-codegen - -/// Ensure that Kani prints a deprecation warning if users invoke `kani::check`. -#[kani::proof] -fn internal_api() { - kani::check(kani::any(), "oops"); -}