Skip to content

Commit 96eb502

Browse files
authored
Upgrade Rust toolchain to 2025-06-18 (#4166)
Relevant upstream PR: rust-lang/rust#137944 (Sized Hierarchy: Part I). This PR implements a part of [RFC 3729](rust-lang/rfcs#3729), which prescribes a hierarchy of `Sized` traits. Notably, this disallows instantiation of `size_of_val` and `align_of_val` with extern types. Consequently, the code in tests `unsized_foreign.rs` as well as parts of `foreign_type.rs` no longer compile (when previously some of the tests would panic). These test were therefore removed. Resolves: #4165 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
1 parent 9d87281 commit 96eb502

File tree

5 files changed

+29
-95
lines changed

5 files changed

+29
-95
lines changed

library/kani/src/lib.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,7 @@
2121
#![feature(f16)]
2222
#![feature(f128)]
2323
#![feature(convert_float_to_int)]
24+
#![feature(sized_hierarchy)]
2425

2526
// Allow us to use `kani::` to access crate features.
2627
extern crate self as kani;

library/kani_core/src/mem.rs

Lines changed: 19 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@
1212
macro_rules! kani_mem {
1313
($core:tt) => {
1414
use super::kani_intrinsic;
15+
use $core::marker::MetaSized;
1516
use $core::ptr::{DynMetadata, NonNull, Pointee};
1617

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

@@ -49,7 +50,7 @@ macro_rules! kani_mem {
4950
issue = 2690,
5051
reason = "experimental memory predicate API"
5152
)]
52-
pub fn can_write_unaligned<T: ?Sized>(ptr: *const T) -> bool {
53+
pub fn can_write_unaligned<T: MetaSized>(ptr: *const T) -> bool {
5354
let (thin_ptr, metadata) = ptr.to_raw_parts();
5455
is_inbounds(ptr)
5556
}
@@ -72,7 +73,7 @@ macro_rules! kani_mem {
7273
reason = "experimental memory predicate API"
7374
)]
7475
#[allow(clippy::not_unsafe_ptr_arg_deref)]
75-
pub fn can_dereference<T: ?Sized>(ptr: *const T) -> bool {
76+
pub fn can_dereference<T: MetaSized>(ptr: *const T) -> bool {
7677
// Need to assert `is_initialized` because non-determinism is used under the hood, so it
7778
// does not make sense to use it inside assumption context.
7879
is_ptr_aligned(ptr)
@@ -99,7 +100,7 @@ macro_rules! kani_mem {
99100
reason = "experimental memory predicate API"
100101
)]
101102
#[allow(clippy::not_unsafe_ptr_arg_deref)]
102-
pub fn can_read_unaligned<T: ?Sized>(ptr: *const T) -> bool {
103+
pub fn can_read_unaligned<T: MetaSized>(ptr: *const T) -> bool {
103104
let (thin_ptr, metadata) = ptr.to_raw_parts();
104105
// Need to assert `is_initialized` because non-determinism is used under the hood, so it
105106
// does not make sense to use it inside assumption context.
@@ -116,12 +117,15 @@ macro_rules! kani_mem {
116117
reason = "experimental memory predicate API"
117118
)]
118119
#[allow(clippy::not_unsafe_ptr_arg_deref)]
119-
pub fn same_allocation<T: ?Sized>(ptr1: *const T, ptr2: *const T) -> bool {
120+
pub fn same_allocation<T: MetaSized>(ptr1: *const T, ptr2: *const T) -> bool {
120121
same_allocation_internal(ptr1, ptr2)
121122
}
122123

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

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

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

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

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

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

@@ -290,7 +294,7 @@ macro_rules! kani_mem {
290294
)]
291295
#[kanitool::fn_marker = "PointerOffsetHook"]
292296
#[inline(never)]
293-
pub fn pointer_offset<T: ?Sized>(_ptr: *const T) -> usize {
297+
pub fn pointer_offset<T: MetaSized>(_ptr: *const T) -> usize {
294298
kani_intrinsic()
295299
}
296300
};

rust-toolchain.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,5 @@
22
# SPDX-License-Identifier: Apache-2.0 OR MIT
33

44
[toolchain]
5-
channel = "nightly-2025-06-17"
5+
channel = "nightly-2025-06-18"
66
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]
Lines changed: 8 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -1,45 +1,31 @@
11
// Copyright Kani Contributors
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
3-
// kani-flags: -Z mem-predicates -Z c-ffi
4-
//! Check that Kani's memory predicates return that it's not safe to access pointers with foreign
5-
//! types since it cannot compute its size.
3+
// kani-flags: -Z c-ffi
4+
//! We used to check that Kani's memory predicates return that it's not safe to access pointers
5+
//! with foreign types since it cannot compute its size, but with the introduction of
6+
//! sized_hierarchy compilation (expectedly) fails. So all we can check is values through extern
7+
//! types.
68
#![feature(ptr_metadata)]
79
#![feature(extern_types)]
10+
#![feature(sized_hierarchy)]
811

912
extern crate kani;
1013

11-
use kani::mem::{can_dereference, can_read_unaligned, can_write};
1214
use std::ffi::c_void;
13-
use std::ptr;
15+
use std::marker::PointeeSized;
1416

1517
#[derive(Clone, Copy, kani::Arbitrary)]
16-
struct Wrapper<T: ?Sized, U> {
18+
struct Wrapper<T: PointeeSized, U> {
1719
_size: U,
1820
_value: T,
1921
}
2022

2123
extern "C" {
22-
type Foreign;
2324
type __CPROVER_size_t;
2425
fn __CPROVER_havoc_object(p: *mut c_void);
2526

2627
}
2728

28-
#[kani::proof]
29-
pub fn check_write_is_unsafe() {
30-
let mut var: Wrapper<u64, usize> = kani::any();
31-
let ptr: *mut Wrapper<Foreign, usize> = &mut var as *mut _ as *mut _;
32-
assert!(!can_write(ptr));
33-
}
34-
35-
#[kani::proof]
36-
pub fn check_read_is_unsafe() {
37-
let var: usize = kani::any();
38-
let ptr = &var as *const _ as *const __CPROVER_size_t;
39-
assert!(!can_dereference(ptr));
40-
assert!(!can_read_unaligned(ptr));
41-
}
42-
4329
/// Kani APIs cannot tell if that's safe to write to a foreign type.
4430
///
4531
/// However, foreign APIs that have knowledge of the type can still safely set new values.
@@ -66,12 +52,3 @@ pub fn check_write_with_extern_side_effect() {
6652
};
6753
assert!(var == 0);
6854
}
69-
70-
/// Check that Kani can still build the foreign type using from_raw_parts.
71-
#[kani::proof]
72-
pub fn check_from_raw_parts() {
73-
let mut var: Wrapper<u64, usize> = kani::any();
74-
let ptr = &mut var as *mut _ as *mut ();
75-
let fat_ptr: *mut __CPROVER_size_t = ptr::from_raw_parts_mut(ptr, ());
76-
assert!(!can_write(fat_ptr));
77-
}

tests/kani/SizeAndAlignOfDst/unsized_foreign.rs

Lines changed: 0 additions & 48 deletions
This file was deleted.

0 commit comments

Comments
 (0)