From e3cd8ba48df6e2e98e39d75643618f9eb75a325d Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Wed, 3 Jul 2024 16:25:07 -0700 Subject: [PATCH 1/6] Fix visibility of some kani intrinsics inside `mem.rs` --- library/kani/src/mem.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/library/kani/src/mem.rs b/library/kani/src/mem.rs index 0b390e74288d..4e953020d3b1 100644 --- a/library/kani/src/mem.rs +++ b/library/kani/src/mem.rs @@ -294,21 +294,21 @@ unsafe fn has_valid_value(_ptr: *const T) -> bool { /// Check whether `len * size_of::()` bytes are initialized starting from `ptr`. #[rustc_diagnostic_item = "KaniIsInitialized"] #[inline(never)] -pub fn is_initialized(_ptr: *const T, _len: usize) -> bool { +pub(crate) fn is_initialized(_ptr: *const T, _len: usize) -> bool { kani_intrinsic() } /// Get the object ID of the given pointer. #[rustc_diagnostic_item = "KaniPointerObject"] #[inline(never)] -pub fn pointer_object(_ptr: *const T) -> usize { +pub(crate) fn pointer_object(_ptr: *const T) -> usize { kani_intrinsic() } /// Get the object offset of the given pointer. #[rustc_diagnostic_item = "KaniPointerOffset"] #[inline(never)] -pub fn pointer_offset(_ptr: *const T) -> usize { +pub(crate) fn pointer_offset(_ptr: *const T) -> usize { kani_intrinsic() } From 057aa833aefb57e3f3992b31c14c262e29148482 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Fri, 5 Jul 2024 08:06:02 -0700 Subject: [PATCH 2/6] Fix visibility of intrinsics in `kani_core` --- library/kani_core/src/mem.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs index 3b10856765a5..1d426a733cda 100644 --- a/library/kani_core/src/mem.rs +++ b/library/kani_core/src/mem.rs @@ -302,21 +302,21 @@ macro_rules! kani_mem { /// Check whether `len * size_of::()` bytes are initialized starting from `ptr`. #[rustc_diagnostic_item = "KaniIsInitialized"] #[inline(never)] - pub fn is_initialized(_ptr: *const T, _len: usize) -> bool { + pub(crate) fn is_initialized(_ptr: *const T, _len: usize) -> bool { kani_intrinsic() } /// Get the object ID of the given pointer. #[rustc_diagnostic_item = "KaniPointerObject"] #[inline(never)] - pub fn pointer_object(_ptr: *const T) -> usize { + pub(crate) fn pointer_object(_ptr: *const T) -> usize { kani_intrinsic() } /// Get the object offset of the given pointer. #[rustc_diagnostic_item = "KaniPointerOffset"] #[inline(never)] - pub fn pointer_offset(_ptr: *const T) -> usize { + pub(crate) fn pointer_offset(_ptr: *const T) -> usize { kani_intrinsic() } }; From 71c831323fc36f89b4e25125840ab3c25fac3eb2 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Fri, 5 Jul 2024 15:13:28 -0700 Subject: [PATCH 3/6] Add unstable tag to `pointer_offset` and `pointer_object` --- library/kani/src/mem.rs | 16 ++++++++++++++-- library/kani_core/src/mem.rs | 16 ++++++++++++++-- 2 files changed, 28 insertions(+), 4 deletions(-) diff --git a/library/kani/src/mem.rs b/library/kani/src/mem.rs index 4e953020d3b1..794f7b1223c1 100644 --- a/library/kani/src/mem.rs +++ b/library/kani/src/mem.rs @@ -299,16 +299,28 @@ pub(crate) fn is_initialized(_ptr: *const T, _len: usize) -> bool { } /// Get the object ID of the given pointer. +#[doc(hidden)] +#[crate::unstable( + feature = "ghost-state", + issue = 3184, + reason = "experimental ghost state/shadow memory API" +)] #[rustc_diagnostic_item = "KaniPointerObject"] #[inline(never)] -pub(crate) fn pointer_object(_ptr: *const T) -> usize { +pub fn pointer_object(_ptr: *const T) -> usize { kani_intrinsic() } /// Get the object offset of the given pointer. +#[doc(hidden)] +#[crate::unstable( + feature = "ghost-state", + issue = 3184, + reason = "experimental ghost state/shadow memory API" +)] #[rustc_diagnostic_item = "KaniPointerOffset"] #[inline(never)] -pub(crate) fn pointer_offset(_ptr: *const T) -> usize { +pub fn pointer_offset(_ptr: *const T) -> usize { kani_intrinsic() } diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs index 1d426a733cda..4c8586a2c447 100644 --- a/library/kani_core/src/mem.rs +++ b/library/kani_core/src/mem.rs @@ -307,16 +307,28 @@ macro_rules! kani_mem { } /// Get the object ID of the given pointer. + #[doc(hidden)] + #[crate::unstable( + feature = "ghost-state", + issue = 3184, + reason = "experimental ghost state/shadow memory API" + )] #[rustc_diagnostic_item = "KaniPointerObject"] #[inline(never)] - pub(crate) fn pointer_object(_ptr: *const T) -> usize { + pub fn pointer_object(_ptr: *const T) -> usize { kani_intrinsic() } /// Get the object offset of the given pointer. + #[doc(hidden)] + #[crate::unstable( + feature = "ghost-state", + issue = 3184, + reason = "experimental ghost state/shadow memory API" + )] #[rustc_diagnostic_item = "KaniPointerOffset"] #[inline(never)] - pub(crate) fn pointer_offset(_ptr: *const T) -> usize { + pub fn pointer_offset(_ptr: *const T) -> usize { kani_intrinsic() } }; From ec9c390ff24e90ff7b2d9ddd6722c57e7d30e4e2 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Mon, 8 Jul 2024 08:11:44 -0700 Subject: [PATCH 4/6] Make clippy happy --- library/kani_core/src/mem.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs index 4c8586a2c447..f5fb8b105085 100644 --- a/library/kani_core/src/mem.rs +++ b/library/kani_core/src/mem.rs @@ -308,7 +308,7 @@ macro_rules! kani_mem { /// Get the object ID of the given pointer. #[doc(hidden)] - #[crate::unstable( + #[$crate::unstable( feature = "ghost-state", issue = 3184, reason = "experimental ghost state/shadow memory API" @@ -321,7 +321,7 @@ macro_rules! kani_mem { /// Get the object offset of the given pointer. #[doc(hidden)] - #[crate::unstable( + #[$crate::unstable( feature = "ghost-state", issue = 3184, reason = "experimental ghost state/shadow memory API" From 96b47da3dc24d4b58674d23e542f4794c7e3ef6b Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Wed, 10 Jul 2024 14:50:07 -0700 Subject: [PATCH 5/6] Remove unnecessary `is_initialized` from `slice.rs` --- tests/std-checks/core/src/slice.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/tests/std-checks/core/src/slice.rs b/tests/std-checks/core/src/slice.rs index 044f4bd38586..060b672167a1 100644 --- a/tests/std-checks/core/src/slice.rs +++ b/tests/std-checks/core/src/slice.rs @@ -6,7 +6,6 @@ pub mod contracts { use kani::{mem::*, requires}; #[requires(can_dereference(std::ptr::slice_from_raw_parts(data, len)))] - #[requires(is_initialized(data, len))] pub unsafe fn from_raw_parts<'a, T>(data: *const T, len: usize) -> &'a [T] { std::slice::from_raw_parts(data, len) } From e3ecf8d1788849b1d34f5fe1d6f85a9cb0683c9c Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Wed, 10 Jul 2024 15:11:12 -0700 Subject: [PATCH 6/6] Substitute `unstable` with `pub(crate` in `kani_core` --- library/kani_core/src/mem.rs | 30 ++++++++++++++++-------------- 1 file changed, 16 insertions(+), 14 deletions(-) diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs index f5fb8b105085..f365549316d8 100644 --- a/library/kani_core/src/mem.rs +++ b/library/kani_core/src/mem.rs @@ -307,28 +307,30 @@ macro_rules! kani_mem { } /// Get the object ID of the given pointer. - #[doc(hidden)] - #[$crate::unstable( - feature = "ghost-state", - issue = 3184, - reason = "experimental ghost state/shadow memory API" - )] + // TODO: Add this back later, as there is no unstable attribute here. + // #[doc(hidden)] + // #[crate::unstable( + // feature = "ghost-state", + // issue = 3184, + // reason = "experimental ghost state/shadow memory API" + // )] #[rustc_diagnostic_item = "KaniPointerObject"] #[inline(never)] - pub fn pointer_object(_ptr: *const T) -> usize { + pub(crate) fn pointer_object(_ptr: *const T) -> usize { kani_intrinsic() } /// Get the object offset of the given pointer. - #[doc(hidden)] - #[$crate::unstable( - feature = "ghost-state", - issue = 3184, - reason = "experimental ghost state/shadow memory API" - )] + // TODO: Add this back later, as there is no unstable attribute here. + // #[doc(hidden)] + // #[crate::unstable( + // feature = "ghost-state", + // issue = 3184, + // reason = "experimental ghost state/shadow memory API" + // )] #[rustc_diagnostic_item = "KaniPointerOffset"] #[inline(never)] - pub fn pointer_offset(_ptr: *const T) -> usize { + pub(crate) fn pointer_offset(_ptr: *const T) -> usize { kani_intrinsic() } };