Skip to content

Commit

Permalink
Fix visibility of some Kani intrinsics (rust-lang#3323)
Browse files Browse the repository at this point in the history
This PR fixes inadvertently exposing some of the unstable Kani
intrinsics.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
  • Loading branch information
artemagvanian authored Jul 16, 2024
1 parent 441451c commit 398729c
Show file tree
Hide file tree
Showing 2 changed files with 30 additions and 4 deletions.
14 changes: 13 additions & 1 deletion library/kani/src/mem.rs
Original file line number Diff line number Diff line change
Expand Up @@ -300,7 +300,7 @@ unsafe fn has_valid_value<T: ?Sized>(_ptr: *const T) -> bool {
/// Check whether `len * size_of::<T>()` bytes are initialized starting from `ptr`.
#[rustc_diagnostic_item = "KaniIsInitialized"]
#[inline(never)]
pub fn is_initialized<T: ?Sized>(_ptr: *const T) -> bool {
pub(crate) fn is_initialized<T: ?Sized>(_ptr: *const T) -> bool {
kani_intrinsic()
}

Expand All @@ -311,13 +311,25 @@ fn assert_is_initialized<T: ?Sized>(ptr: *const T) -> 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 fn pointer_object<T: ?Sized>(_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 fn pointer_offset<T: ?Sized>(_ptr: *const T) -> usize {
Expand Down
20 changes: 17 additions & 3 deletions library/kani_core/src/mem.rs
Original file line number Diff line number Diff line change
Expand Up @@ -306,7 +306,7 @@ macro_rules! kani_mem {
/// Check whether `len * size_of::<T>()` bytes are initialized starting from `ptr`.
#[rustc_diagnostic_item = "KaniIsInitialized"]
#[inline(never)]
pub fn is_initialized<T: ?Sized>(_ptr: *const T) -> bool {
pub(crate) fn is_initialized<T: ?Sized>(_ptr: *const T) -> bool {
kani_intrinsic()
}

Expand All @@ -320,16 +320,30 @@ macro_rules! kani_mem {
}

/// Get the object ID of the given pointer.
// 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<T: ?Sized>(_ptr: *const T) -> usize {
pub(crate) fn pointer_object<T: ?Sized>(_ptr: *const T) -> usize {
kani_intrinsic()
}

/// Get the object offset of the given pointer.
// 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<T: ?Sized>(_ptr: *const T) -> usize {
pub(crate) fn pointer_offset<T: ?Sized>(_ptr: *const T) -> usize {
kani_intrinsic()
}
};
Expand Down

0 comments on commit 398729c

Please sign in to comment.