Skip to content

Update subtree to 2025-02-11 #259

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 6 commits into from
Mar 3, 2025
Merged

Update subtree to 2025-02-11 #259

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
9c1e515
Squashed 'library/' changes from 78fc550584d..0b9e7db9ccf
Feb 21, 2025
f7d651c
Merge from 124cc92199ffa924f6b4c7cc819a85b65e0c3984 with conflicts
Feb 21, 2025
3238846
Fix merge conflicts
carolynzech Feb 26, 2025
50889e7
rustfmt
carolynzech Feb 26, 2025
4461995
Update toolchain & Kani version to 2025-02-11
carolynzech Feb 26, 2025
c18b612
address comments from review
carolynzech Mar 3, 2025
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
11 changes: 6 additions & 5 deletions library/core/src/ptr/alignment.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -404,11 +404,12 @@ mod verify {
}
}

// pub const fn of<T>() -> Self
#[kani::proof_for_contract(Alignment::of)]
pub fn check_of_i32() {
let _ = Alignment::of::<i32>();
}
/// FIXME, c.f. https://github.com/model-checking/kani/issues/3905
// // pub const fn of<T>() -> Self
// #[kani::proof_for_contract(Alignment::of)]
// pub fn check_of_i32() {
// let _ = Alignment::of::<i32>();
// }

// pub const fn new(align: usize) -> Option<Self>
#[kani::proof_for_contract(Alignment::new)]
Expand Down
65 changes: 29 additions & 36 deletions library/core/src/ptr/const_ptr.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -427,12 +427,11 @@ impl<T: ?Sized> *const T {
// Precondition 1: the computed offset `count * size_of::<T>()` does not overflow `isize`.
// Precondition 2: adding the computed offset to `self` does not cause overflow.
// These two preconditions are combined for performance reason, as multiplication is computationally expensive in Kani.
count.checked_mul(core::mem::size_of::<T>() as isize)
.map_or(false, |computed_offset| (self as isize).checked_add(computed_offset).is_some()) &&
count.checked_mul(core::mem::size_of::<T>() as isize).is_some_and(|computed_offset| (self as isize).checked_add(computed_offset).is_some()) &&
// Precondition 3: If `T` is a unit type (`size_of::<T>() == 0`), this check is unnecessary as it has no allocated memory.
// Otherwise, for non-unit types, `self` and `self.wrapping_offset(count)` should point to the same allocated object,
// restricting `count` to prevent crossing allocation boundaries.
((core::mem::size_of::<T>() == 0) || (core::ub_checks::same_allocation(self, self.wrapping_offset(count))))
(core::mem::size_of::<T>() == 0 || core::ub_checks::same_allocation(self, self.wrapping_offset(count)))
)]
// Postcondition: If `T` is a unit type (`size_of::<T>() == 0`), no allocation check is needed.
// Otherwise, for non-unit types, ensure that `self` and `result` point to the same allocated object,
Expand Down Expand Up @@ -492,19 +491,14 @@ impl<T: ?Sized> *const T {
#[rustc_const_stable(feature = "const_pointer_byte_offsets", since = "1.75.0")]
#[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
#[requires(
// If count is zero, any pointer is valid including null pointer.
(count == 0) ||
// Else if count is not zero, then ensure that adding `count` doesn't cause
// overflow and that both pointers `self` and the result are in the same
// allocation
((self.addr() as isize).checked_add(count).is_some() &&
core::ub_checks::same_allocation(self, self.wrapping_byte_offset(count)))
)]
#[ensures(|&result|
// The resulting pointer should either be unchanged or still point to the same allocation
(self.addr() == result.addr()) ||
(core::ub_checks::same_allocation(self, result))
count == 0 ||
(
(core::mem::size_of_val_raw(self) > 0) &&
(self.addr() as isize).checked_add(count).is_some()) &&
(core::ub_checks::same_allocation(self, self.wrapping_byte_offset(count))
)
)]
#[ensures(|result| core::mem::size_of_val_raw(self) == 0 || core::ub_checks::same_allocation(self, *result))]
pub const unsafe fn byte_offset(self, count: isize) -> Self {
// SAFETY: the caller must uphold the safety contract for `offset`.
unsafe { self.cast::<u8>().offset(count).with_metadata_of(self) }
Expand Down Expand Up @@ -990,7 +984,7 @@ impl<T: ?Sized> *const T {
// Precondition 2: adding the computed offset to `self` does not cause overflow.
// These two preconditions are combined for performance reason, as multiplication is computationally expensive in Kani.
count.checked_mul(core::mem::size_of::<T>())
.map_or(false, |computed_offset| {
.is_some_and(|computed_offset| {
computed_offset <= isize::MAX as usize && (self as isize).checked_add(computed_offset as isize).is_some()
}) &&
// Precondition 3: If `T` is a unit type (`size_of::<T>() == 0`), this check is unnecessary as it has no allocated memory.
Expand Down Expand Up @@ -1059,15 +1053,15 @@ impl<T: ?Sized> *const T {
(count == 0) ||
// Else if count is not zero, then ensure that adding `count` doesn't cause
// overflow and that both pointers `self` and the result are in the same
// allocation
((self.addr() as isize).checked_add(count as isize).is_some() &&
core::ub_checks::same_allocation(self, self.wrapping_byte_add(count)))
)]
#[ensures(|&result|
// The resulting pointer should either be unchanged or still point to the same allocation
(self.addr() == result.addr()) ||
(core::ub_checks::same_allocation(self, result))
// allocation
(
(count <= isize::MAX as usize) &&
(core::mem::size_of_val_raw(self) > 0) &&
((self.addr() as isize).checked_add(count as isize).is_some()) &&
(core::ub_checks::same_allocation(self, self.wrapping_byte_add(count)))
)
)]
#[ensures(|result| core::mem::size_of_val_raw(self) == 0 || core::ub_checks::same_allocation(self, *result))]
pub const unsafe fn byte_add(self, count: usize) -> Self {
// SAFETY: the caller must uphold the safety contract for `add`.
unsafe { self.cast::<u8>().add(count).with_metadata_of(self) }
Expand Down Expand Up @@ -1127,7 +1121,7 @@ impl<T: ?Sized> *const T {
// Precondition 2: substracting the computed offset from `self` does not cause overflow.
// These two preconditions are combined for performance reason, as multiplication is computationally expensive in Kani.
count.checked_mul(core::mem::size_of::<T>())
.map_or(false, |computed_offset| {
.is_some_and(|computed_offset| {
computed_offset <= isize::MAX as usize && (self as isize).checked_sub(computed_offset as isize).is_some()
}) &&
// Precondition 3: If `T` is a unit type (`size_of::<T>() == 0`), this check is unnecessary as it has no allocated memory.
Expand Down Expand Up @@ -1202,15 +1196,15 @@ impl<T: ?Sized> *const T {
(count == 0) ||
// Else if count is not zero, then ensure that subtracting `count` doesn't
// cause overflow and that both pointers `self` and the result are in the
// same allocation
((self.addr() as isize).checked_sub(count as isize).is_some() &&
core::ub_checks::same_allocation(self, self.wrapping_byte_sub(count)))
)]
#[ensures(|&result|
// The resulting pointer should either be unchanged or still point to the same allocation
(self.addr() == result.addr()) ||
(core::ub_checks::same_allocation(self, result))
// same allocation.
(
(count <= isize::MAX as usize) &&
(core::mem::size_of_val_raw(self) > 0) &&
((self.addr() as isize).checked_sub(count as isize).is_some()) &&
(core::ub_checks::same_allocation(self, self.wrapping_byte_sub(count)))
)
)]
#[ensures(|result| core::mem::size_of_val_raw(self) == 0 || core::ub_checks::same_allocation(self, *result))]
pub const unsafe fn byte_sub(self, count: usize) -> Self {
// SAFETY: the caller must uphold the safety contract for `sub`.
unsafe { self.cast::<u8>().sub(count).with_metadata_of(self) }
Expand Down Expand Up @@ -2309,7 +2303,6 @@ mod verify {
);

#[kani::proof_for_contract(<*const ()>::byte_offset)]
#[kani::should_panic]
pub fn check_const_byte_offset_unit_invalid_count() {
let val = ();
let ptr: *const () = &val;
Expand Down Expand Up @@ -2340,7 +2333,7 @@ mod verify {
pub fn $proof_name() {
let val = ();
let ptr: *const () = &val;
let count: isize = mem::size_of::<()>() as isize;
let count: isize = kani::any();
unsafe {
ptr.byte_offset(count);
}
Expand All @@ -2353,7 +2346,7 @@ mod verify {
let val = ();
let ptr: *const () = &val;
//byte_add and byte_sub need count to be usize unlike byte_offset
let count: usize = mem::size_of::<()>();
let count: usize = kani::any();
unsafe {
ptr.$fn_name(count);
}
Expand Down
66 changes: 30 additions & 36 deletions library/core/src/ptr/mut_ptr.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -427,7 +427,7 @@ impl<T: ?Sized> *mut T {
// Precondition 2: adding the computed offset to `self` does not cause overflow.
// These two preconditions are combined for performance reason, as multiplication is computationally expensive in Kani.
count.checked_mul(core::mem::size_of::<T>() as isize)
.map_or(false, |computed_offset| (self as isize).checked_add(computed_offset).is_some()) &&
.is_some_and(|computed_offset| (self as isize).checked_add(computed_offset).is_some()) &&
// Precondition 3: If `T` is a unit type (`size_of::<T>() == 0`), this check is unnecessary as it has no allocated memory.
// Otherwise, for non-unit types, `self` and `self.wrapping_offset(count)` should point to the same allocated object,
// restricting `count` to prevent crossing allocation boundaries.
Expand Down Expand Up @@ -493,19 +493,14 @@ impl<T: ?Sized> *mut T {
#[rustc_const_stable(feature = "const_pointer_byte_offsets", since = "1.75.0")]
#[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
#[requires(
// If count is zero, any pointer is valid including null pointer.
(count == 0) ||
// Else if count is not zero, then ensure that subtracting `count` doesn't
// cause overflow and that both pointers `self` and the result are in the
// same allocation.
((self.addr() as isize).checked_add(count).is_some() &&
core::ub_checks::same_allocation(self, self.wrapping_byte_offset(count)))
)]
#[ensures(|&result|
// The resulting pointer should either be unchanged or still point to the same allocation
(self.addr() == result.addr()) ||
(core::ub_checks::same_allocation(self, result))
count == 0 ||
(
(core::mem::size_of_val_raw(self) > 0) &&
(self.addr() as isize).checked_add(count).is_some()) &&
(core::ub_checks::same_allocation(self, self.wrapping_byte_offset(count))
)
)]
#[ensures(|result| core::mem::size_of_val_raw(self) == 0 || core::ub_checks::same_allocation(self, *result))]
pub const unsafe fn byte_offset(self, count: isize) -> Self {
// SAFETY: the caller must uphold the safety contract for `offset`.
unsafe { self.cast::<u8>().offset(count).with_metadata_of(self) }
Expand Down Expand Up @@ -901,7 +896,7 @@ impl<T: ?Sized> *mut T {
// Ensuring that both pointers point to the same address or are in the same allocation
(self as isize == origin as isize || core::ub_checks::same_allocation(self, origin))
)]
#[ensures(|result| *result == (self as isize - origin as isize) / (mem::size_of::<T>() as isize))]
#[ensures(|result| core::mem::size_of::<T>() == 0 || (*result == (self as isize - origin as isize) / (mem::size_of::<T>() as isize)))]
pub const unsafe fn offset_from(self, origin: *const T) -> isize
where
T: Sized,
Expand Down Expand Up @@ -1087,7 +1082,7 @@ impl<T: ?Sized> *mut T {
// Precondition 2: adding the computed offset to `self` does not cause overflow.
// These two preconditions are combined for performance reason, as multiplication is computationally expensive in Kani.
count.checked_mul(core::mem::size_of::<T>())
.map_or(false, |computed_offset| {
.is_some_and(|computed_offset| {
computed_offset <= isize::MAX as usize && (self as isize).checked_add(computed_offset as isize).is_some()
}) &&
// Precondition 3: If `T` is a unit type (`size_of::<T>() == 0`), this check is unnecessary as it has no allocated memory.
Expand Down Expand Up @@ -1154,17 +1149,17 @@ impl<T: ?Sized> *mut T {
#[requires(
// If count is zero, any pointer is valid including null pointer.
(count == 0) ||
// Else if count is not zero, then ensure that subtracting `count` doesn't
// cause overflow and that both pointers `self` and the result are in the
// same allocation.
((self.addr() as isize).checked_add(count as isize).is_some() &&
core::ub_checks::same_allocation(self, self.wrapping_byte_add(count)))
)]
#[ensures(|&result|
// The resulting pointer should either be unchanged or still point to the same allocation
(self.addr() == result.addr()) ||
(core::ub_checks::same_allocation(self, result))
// Else if count is not zero, then ensure that adding `count` doesn't cause
// overflow and that both pointers `self` and the result are in the same
// allocation
(
(count <= isize::MAX as usize) &&
(core::mem::size_of_val_raw(self) > 0) &&
((self.addr() as isize).checked_add(count as isize).is_some()) &&
(core::ub_checks::same_allocation(self, self.wrapping_byte_add(count)))
)
)]
#[ensures(|result| core::mem::size_of_val_raw(self) == 0 || core::ub_checks::same_allocation(self, *result))]
pub const unsafe fn byte_add(self, count: usize) -> Self {
// SAFETY: the caller must uphold the safety contract for `add`.
unsafe { self.cast::<u8>().add(count).with_metadata_of(self) }
Expand Down Expand Up @@ -1227,7 +1222,7 @@ impl<T: ?Sized> *mut T {
// Precondition 2: substracting the computed offset from `self` does not cause overflow.
// These two preconditions are combined for performance reason, as multiplication is computationally expensive in Kani.
count.checked_mul(core::mem::size_of::<T>())
.map_or(false, |computed_offset| {
.is_some_and(|computed_offset| {
computed_offset <= isize::MAX as usize && (self as isize).checked_sub(computed_offset as isize).is_some()
}) &&
// Precondition 3: If `T` is a unit type (`size_of::<T>() == 0`), this check is unnecessary as it has no allocated memory.
Expand Down Expand Up @@ -1303,14 +1298,14 @@ impl<T: ?Sized> *mut T {
// Else if count is not zero, then ensure that subtracting `count` doesn't
// cause overflow and that both pointers `self` and the result are in the
// same allocation.
((self.addr() as isize).checked_sub(count as isize).is_some() &&
core::ub_checks::same_allocation(self, self.wrapping_byte_sub(count)))
)]
#[ensures(|&result|
// The resulting pointer should either be unchanged or still point to the same allocation
(self.addr() == result.addr()) ||
(core::ub_checks::same_allocation(self, result))
(
(count <= isize::MAX as usize) &&
(core::mem::size_of_val_raw(self) > 0) &&
((self.addr() as isize).checked_sub(count as isize).is_some()) &&
(core::ub_checks::same_allocation(self, self.wrapping_byte_sub(count)))
)
)]
#[ensures(|result| core::mem::size_of_val_raw(self) == 0 || core::ub_checks::same_allocation(self, *result))]
pub const unsafe fn byte_sub(self, count: usize) -> Self {
// SAFETY: the caller must uphold the safety contract for `sub`.
unsafe { self.cast::<u8>().sub(count).with_metadata_of(self) }
Expand Down Expand Up @@ -2670,7 +2665,6 @@ mod verify {
);

#[kani::proof_for_contract(<*mut ()>::byte_offset)]
#[kani::should_panic]
pub fn check_mut_byte_offset_unit_invalid_count() {
let mut val = ();
let ptr: *mut () = &mut val;
Expand Down Expand Up @@ -2701,7 +2695,7 @@ mod verify {
pub fn $proof_name() {
let mut val = ();
let ptr: *mut () = &mut val;
let count: isize = mem::size_of::<()>() as isize;
let count: isize = kani::any();
unsafe {
ptr.byte_offset(count);
}
Expand All @@ -2714,7 +2708,7 @@ mod verify {
let mut val = ();
let ptr: *mut () = &mut val;
//byte_add and byte_sub need count to be usize unlike byte_offset
let count: usize = mem::size_of::<()>();
let count: usize = kani::any();
unsafe {
ptr.$fn_name(count);
}
Expand Down
Loading
Loading