Skip to content
Merged
Show file tree
Hide file tree
Changes from all 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"]
39 changes: 8 additions & 31 deletions tests/kani/MemPredicates/foreign_type.rs
Original file line number Diff line number Diff line change
@@ -1,45 +1,31 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
// kani-flags: -Z mem-predicates -Z c-ffi
//! Check that Kani's memory predicates return that it's not safe to access pointers with foreign
//! types since it cannot compute its size.
// kani-flags: -Z c-ffi
//! We used to check that Kani's memory predicates return that it's not safe to access pointers
//! with foreign types since it cannot compute its size, but with the introduction of
//! sized_hierarchy compilation (expectedly) fails. So all we can check is values through extern
//! types.
#![feature(ptr_metadata)]
#![feature(extern_types)]
#![feature(sized_hierarchy)]

extern crate kani;

use kani::mem::{can_dereference, can_read_unaligned, can_write};
use std::ffi::c_void;
use std::ptr;
use std::marker::PointeeSized;

#[derive(Clone, Copy, kani::Arbitrary)]
struct Wrapper<T: ?Sized, U> {
struct Wrapper<T: PointeeSized, U> {
_size: U,
_value: T,
}

extern "C" {
type Foreign;
type __CPROVER_size_t;
fn __CPROVER_havoc_object(p: *mut c_void);

}

#[kani::proof]
pub fn check_write_is_unsafe() {
let mut var: Wrapper<u64, usize> = kani::any();
let ptr: *mut Wrapper<Foreign, usize> = &mut var as *mut _ as *mut _;
assert!(!can_write(ptr));
}

#[kani::proof]
pub fn check_read_is_unsafe() {
let var: usize = kani::any();
let ptr = &var as *const _ as *const __CPROVER_size_t;
assert!(!can_dereference(ptr));
assert!(!can_read_unaligned(ptr));
}

/// Kani APIs cannot tell if that's safe to write to a foreign type.
///
/// However, foreign APIs that have knowledge of the type can still safely set new values.
Expand All @@ -66,12 +52,3 @@ pub fn check_write_with_extern_side_effect() {
};
assert!(var == 0);
}

/// Check that Kani can still build the foreign type using from_raw_parts.
#[kani::proof]
pub fn check_from_raw_parts() {
let mut var: Wrapper<u64, usize> = kani::any();
let ptr = &mut var as *mut _ as *mut ();
let fat_ptr: *mut __CPROVER_size_t = ptr::from_raw_parts_mut(ptr, ());
assert!(!can_write(fat_ptr));
}
48 changes: 0 additions & 48 deletions tests/kani/SizeAndAlignOfDst/unsized_foreign.rs

This file was deleted.

Loading