Skip to content
Merged
Show file tree
Hide file tree
Changes from 3 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions library/kani/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,7 @@
#![feature(f16)]
#![feature(f128)]
#![feature(convert_float_to_int)]
#![feature(sized_hierarchy)]

// Allow us to use `kani::` to access crate features.
extern crate self as kani;
Expand Down
34 changes: 19 additions & 15 deletions library/kani_core/src/mem.rs
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@
macro_rules! kani_mem {
($core:tt) => {
use super::kani_intrinsic;
use $core::marker::MetaSized;
use $core::ptr::{DynMetadata, NonNull, Pointee};

/// Check if the pointer is valid for write access according to [crate::mem] conditions 1, 2
Expand All @@ -31,7 +32,7 @@ macro_rules! kani_mem {
issue = 2690,
reason = "experimental memory predicate API"
)]
pub fn can_write<T: ?Sized>(ptr: *mut T) -> bool {
pub fn can_write<T: MetaSized>(ptr: *mut T) -> bool {
is_ptr_aligned(ptr) && is_inbounds(ptr)
}

Expand All @@ -49,7 +50,7 @@ macro_rules! kani_mem {
issue = 2690,
reason = "experimental memory predicate API"
)]
pub fn can_write_unaligned<T: ?Sized>(ptr: *const T) -> bool {
pub fn can_write_unaligned<T: MetaSized>(ptr: *const T) -> bool {
let (thin_ptr, metadata) = ptr.to_raw_parts();
is_inbounds(ptr)
}
Expand All @@ -72,7 +73,7 @@ macro_rules! kani_mem {
reason = "experimental memory predicate API"
)]
#[allow(clippy::not_unsafe_ptr_arg_deref)]
pub fn can_dereference<T: ?Sized>(ptr: *const T) -> bool {
pub fn can_dereference<T: MetaSized>(ptr: *const T) -> bool {
// Need to assert `is_initialized` because non-determinism is used under the hood, so it
// does not make sense to use it inside assumption context.
is_ptr_aligned(ptr)
Expand All @@ -99,7 +100,7 @@ macro_rules! kani_mem {
reason = "experimental memory predicate API"
)]
#[allow(clippy::not_unsafe_ptr_arg_deref)]
pub fn can_read_unaligned<T: ?Sized>(ptr: *const T) -> bool {
pub fn can_read_unaligned<T: MetaSized>(ptr: *const T) -> bool {
let (thin_ptr, metadata) = ptr.to_raw_parts();
// Need to assert `is_initialized` because non-determinism is used under the hood, so it
// does not make sense to use it inside assumption context.
Expand All @@ -116,12 +117,15 @@ macro_rules! kani_mem {
reason = "experimental memory predicate API"
)]
#[allow(clippy::not_unsafe_ptr_arg_deref)]
pub fn same_allocation<T: ?Sized>(ptr1: *const T, ptr2: *const T) -> bool {
pub fn same_allocation<T: MetaSized>(ptr1: *const T, ptr2: *const T) -> bool {
same_allocation_internal(ptr1, ptr2)
}

#[allow(clippy::not_unsafe_ptr_arg_deref)]
pub(super) fn same_allocation_internal<T: ?Sized>(ptr1: *const T, ptr2: *const T) -> bool {
pub(super) fn same_allocation_internal<T: MetaSized>(
ptr1: *const T,
ptr2: *const T,
) -> bool {
let addr1 = ptr1 as *const ();
let addr2 = ptr2 as *const ();
cbmc::same_allocation(addr1, addr2)
Expand All @@ -135,7 +139,7 @@ macro_rules! kani_mem {
/// - The computed size exceeds `isize::MAX` (the maximum safe Rust allocation size).
/// TODO: Optimize this if T is sized.
#[kanitool::fn_marker = "CheckedSizeOfIntrinsic"]
pub fn checked_size_of_raw<T: ?Sized>(ptr: *const T) -> Option<usize> {
pub fn checked_size_of_raw<T: MetaSized>(ptr: *const T) -> Option<usize> {
#[cfg(not(feature = "concrete_playback"))]
return kani_intrinsic();

Expand All @@ -153,7 +157,7 @@ macro_rules! kani_mem {
/// Return `None` if alignment information cannot be retrieved (foreign types), or if value
/// is not power-of-two.
#[kanitool::fn_marker = "CheckedAlignOfIntrinsic"]
pub fn checked_align_of_raw<T: ?Sized>(ptr: *const T) -> Option<usize> {
pub fn checked_align_of_raw<T: MetaSized>(ptr: *const T) -> Option<usize> {
#[cfg(not(feature = "concrete_playback"))]
return kani_intrinsic();

Expand All @@ -180,7 +184,7 @@ macro_rules! kani_mem {
issue = 3946,
reason = "experimental memory predicate API"
)]
pub fn is_inbounds<T: ?Sized>(ptr: *const T) -> bool {
pub fn is_inbounds<T: MetaSized>(ptr: *const T) -> bool {
// If size overflows, then pointer cannot be inbounds.
let Some(sz) = checked_size_of_raw(ptr) else { return false };
if sz == 0 {
Expand All @@ -203,7 +207,7 @@ macro_rules! kani_mem {

// Return whether the pointer is aligned
#[allow(clippy::manual_is_power_of_two)]
fn is_ptr_aligned<T: ?Sized>(ptr: *const T) -> bool {
fn is_ptr_aligned<T: MetaSized>(ptr: *const T) -> bool {
// Cannot be aligned if pointer alignment cannot be computed.
let Some(align) = checked_align_of_raw(ptr) else { return false };
if align > 0 && (align & (align - 1)) == 0 {
Expand Down Expand Up @@ -237,19 +241,19 @@ macro_rules! kani_mem {
/// - Users have to ensure that the pointed to memory is allocated.
#[kanitool::fn_marker = "ValidValueIntrinsic"]
#[inline(never)]
unsafe fn has_valid_value<T: ?Sized>(_ptr: *const T) -> bool {
unsafe fn has_valid_value<T: MetaSized>(_ptr: *const T) -> bool {
kani_intrinsic()
}

/// Check whether `len * size_of::<T>()` bytes are initialized starting from `ptr`.
#[kanitool::fn_marker = "IsInitializedIntrinsic"]
#[inline(never)]
pub(crate) fn is_initialized<T: ?Sized>(_ptr: *const T) -> bool {
pub(crate) fn is_initialized<T: MetaSized>(_ptr: *const T) -> bool {
kani_intrinsic()
}

/// A helper to assert `is_initialized` to use it as a part of other predicates.
fn assert_is_initialized<T: ?Sized>(ptr: *const T) -> bool {
fn assert_is_initialized<T: MetaSized>(ptr: *const T) -> bool {
super::internal::check(
is_initialized(ptr),
"Undefined Behavior: Reading from an uninitialized pointer",
Expand Down Expand Up @@ -277,7 +281,7 @@ macro_rules! kani_mem {
#[doc(hidden)]
#[kanitool::fn_marker = "PointerObjectHook"]
#[inline(never)]
pub(crate) fn pointer_object<T: ?Sized>(_ptr: *const T) -> usize {
pub(crate) fn pointer_object<T: MetaSized>(_ptr: *const T) -> usize {
kani_intrinsic()
}

Expand All @@ -290,7 +294,7 @@ macro_rules! kani_mem {
)]
#[kanitool::fn_marker = "PointerOffsetHook"]
#[inline(never)]
pub fn pointer_offset<T: ?Sized>(_ptr: *const T) -> usize {
pub fn pointer_offset<T: MetaSized>(_ptr: *const T) -> usize {
kani_intrinsic()
}
};
Expand Down
2 changes: 1 addition & 1 deletion rust-toolchain.toml
Original file line number Diff line number Diff line change
Expand Up @@ -2,5 +2,5 @@
# SPDX-License-Identifier: Apache-2.0 OR MIT

[toolchain]
channel = "nightly-2025-06-17"
channel = "nightly-2025-06-18"
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]
77 changes: 0 additions & 77 deletions tests/kani/MemPredicates/foreign_type.rs

This file was deleted.

48 changes: 0 additions & 48 deletions tests/kani/SizeAndAlignOfDst/unsized_foreign.rs

This file was deleted.

Loading