Skip to content
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.

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

Contract and harness for copy_to, copy_to_nonoverlapping, copy_from, and copy_from_nonoverlapping #149

Open
wants to merge 25 commits into
base: main
Choose a base branch
from
Open
Changes from all commits
Commits
Show all changes
25 commits
Select commit Hold shift + click to select a range
16ecdb9
adding contracts for 4 memory operations
Dhvani-Kapadia Nov 2, 2024
50521ab
Update non_null.rs
Dhvani-Kapadia Nov 2, 2024
5e7ba89
Update non_null.rs
Dhvani-Kapadia Nov 2, 2024
dac703d
Update non_null.rs
Dhvani-Kapadia Nov 8, 2024
a87c214
Merge conflict resolution
Dhvani-Kapadia Nov 8, 2024
90ae95e
Merge branch 'dhvani_mem' of https://github.com/danielhumanmod/verify…
Dhvani-Kapadia Nov 8, 2024
d024fc2
feedback
Dhvani-Kapadia Nov 13, 2024
2da2f74
removing log files
Dhvani-Kapadia Nov 13, 2024
5834365
merge from main
QinyuanWu Dec 4, 2024
6bc91f5
merge from main
QinyuanWu Dec 4, 2024
57cc963
resolve copy_to failed checks, modify contract to refer to entire slice
QinyuanWu Dec 4, 2024
4c9fdfa
updating all contrac ts
Dhvani-Kapadia Dec 5, 2024
73c22f6
updating all contracts
Dhvani-Kapadia Dec 5, 2024
2f0e4b1
changes made
Dhvani-Kapadia Dec 5, 2024
acc33ec
Merge branch 'main' into dhvani_mem
Dhvani-Kapadia Dec 5, 2024
fa037b1
changes
Dhvani-Kapadia Dec 5, 2024
913ebd8
Merge branch 'dhvani_mem' of https://github.com/danielhumanmod/verify…
Dhvani-Kapadia Dec 5, 2024
cb3c0de
Update library/core/src/ptr/non_null.rs
Dhvani-Kapadia Dec 5, 2024
330313c
Merge branch 'main' into dhvani_mem
Dhvani-Kapadia Dec 10, 2024
d2198c9
Merge branch 'main' into dhvani_mem
carolynzech Dec 11, 2024
eccd7da
fix modify clause format
QinyuanWu Dec 11, 2024
2bf9595
Merge branch 'model-checking:main' into dhvani_mem
QinyuanWu Dec 11, 2024
6f0d86f
Merge branch 'main' into dhvani_mem
QinyuanWu Dec 11, 2024
a93a1b0
Update library/core/src/ptr/non_null.rs
Dhvani-Kapadia Dec 11, 2024
146406b
Merge branch 'main' into dhvani_mem
QinyuanWu Dec 12, 2024
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
84 changes: 84 additions & 0 deletions library/core/src/ptr/non_null.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1035,8 +1035,14 @@ impl<T: ?Sized> NonNull<T> {
/// [`ptr::copy`]: crate::ptr::copy()
#[inline(always)]
#[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
#[cfg_attr(kani, kani::modifies(NonNull::slice_from_raw_parts(dest, count).as_ptr()))]
#[stable(feature = "non_null_convenience", since = "1.80.0")]
#[rustc_const_stable(feature = "const_intrinsic_copy", since = "1.83.0")]
#[requires(count.checked_mul(core::mem::size_of::<T>()).map_or_else(|| false, |size| size <= isize::MAX as usize)
&& ub_checks::can_dereference(NonNull::slice_from_raw_parts(self, count).as_ptr())
&& ub_checks::can_write(NonNull::slice_from_raw_parts(dest, count).as_ptr()))]
#[ensures(|result: &()| ub_checks::can_dereference(self.as_ptr() as *const u8)
&& ub_checks::can_dereference(dest.as_ptr() as *const u8))]
pub const unsafe fn copy_to(self, dest: NonNull<T>, count: usize)
where
T: Sized,
Expand All @@ -1055,8 +1061,15 @@ impl<T: ?Sized> NonNull<T> {
/// [`ptr::copy_nonoverlapping`]: crate::ptr::copy_nonoverlapping()
#[inline(always)]
#[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
#[cfg_attr(kani, kani::modifies(NonNull::slice_from_raw_parts(dest, count).as_ptr()))]
#[stable(feature = "non_null_convenience", since = "1.80.0")]
#[rustc_const_stable(feature = "const_intrinsic_copy", since = "1.83.0")]
#[requires(count.checked_mul(core::mem::size_of::<T>()).map_or_else(|| false, |size| size <= isize::MAX as usize)
&& ub_checks::can_dereference(NonNull::slice_from_raw_parts(self, count).as_ptr())
&& ub_checks::can_write(NonNull::slice_from_raw_parts(dest, count).as_ptr())
&& ub_checks::maybe_is_nonoverlapping(self.as_ptr() as *const (), dest.as_ptr() as *const (), count, core::mem::size_of::<T>()))]
#[ensures(|result: &()| ub_checks::can_dereference(self.as_ptr() as *const u8)
&& ub_checks::can_dereference(dest.as_ptr() as *const u8))]
pub const unsafe fn copy_to_nonoverlapping(self, dest: NonNull<T>, count: usize)
where
T: Sized,
Expand All @@ -1075,8 +1088,14 @@ impl<T: ?Sized> NonNull<T> {
/// [`ptr::copy`]: crate::ptr::copy()
#[inline(always)]
#[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
#[cfg_attr(kani, kani::modifies(NonNull::slice_from_raw_parts(self, count).as_ptr()))]
#[stable(feature = "non_null_convenience", since = "1.80.0")]
#[rustc_const_stable(feature = "const_intrinsic_copy", since = "1.83.0")]
#[requires(count.checked_mul(core::mem::size_of::<T>()).map_or_else(|| false, |size| size <= isize::MAX as usize)
&& ub_checks::can_dereference(NonNull::slice_from_raw_parts(src, count).as_ptr())
&& ub_checks::can_write(NonNull::slice_from_raw_parts(self, count).as_ptr()))]
#[ensures(|result: &()| ub_checks::can_dereference(src.as_ptr() as *const u8)
&& ub_checks::can_dereference(self.as_ptr() as *const u8))]
pub const unsafe fn copy_from(self, src: NonNull<T>, count: usize)
where
T: Sized,
Expand All @@ -1095,8 +1114,15 @@ impl<T: ?Sized> NonNull<T> {
/// [`ptr::copy_nonoverlapping`]: crate::ptr::copy_nonoverlapping()
#[inline(always)]
#[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
#[cfg_attr(kani, kani::modifies(NonNull::slice_from_raw_parts(self, count).as_ptr()))]
#[stable(feature = "non_null_convenience", since = "1.80.0")]
#[rustc_const_stable(feature = "const_intrinsic_copy", since = "1.83.0")]
#[requires(count.checked_mul(core::mem::size_of::<T>()).map_or_else(|| false, |size| size <= isize::MAX as usize)
&& ub_checks::can_dereference(NonNull::slice_from_raw_parts(src, count).as_ptr())
&& ub_checks::can_write(NonNull::slice_from_raw_parts(self, count).as_ptr())
&& ub_checks::maybe_is_nonoverlapping(src.as_ptr() as *const (), self.as_ptr() as *const (), count, core::mem::size_of::<T>()))]
#[ensures(|result: &()| ub_checks::can_dereference(src.as_ptr() as *const u8)
&& ub_checks::can_dereference(self.as_ptr() as *const u8))]
pub const unsafe fn copy_from_nonoverlapping(self, src: NonNull<T>, count: usize)
where
T: Sized,
Expand Down Expand Up @@ -2538,4 +2564,62 @@ mod verify {
let _ = ptr.byte_offset_from(origin);
}
}

#[kani::proof_for_contract(NonNull::<T>::copy_to)]
pub fn non_null_check_copy_to() {
// PointerGenerator instance
let mut generator = PointerGenerator::<16>::new();
Dhvani-Kapadia marked this conversation as resolved.
Show resolved Hide resolved
// Generate arbitrary pointers for src and dest
let src_ptr = generator.any_in_bounds::<i32>().ptr;
let dest_ptr = generator.any_in_bounds::<i32>().ptr;
// Wrap the raw pointers in NonNull
let src = NonNull::new(src_ptr).unwrap();
let dest = NonNull::new(dest_ptr).unwrap();
// Generate an arbitrary count using kani::any
let count: usize = kani::any();
unsafe { src.copy_to(dest, count);}
}

#[kani::proof_for_contract(NonNull::<T>::copy_from)]
pub fn non_null_check_copy_from() {
// PointerGenerator instance
let mut generator = PointerGenerator::<16>::new();
// Generate arbitrary pointers for src and dest
let src_ptr = generator.any_in_bounds::<i32>().ptr;
let dest_ptr = generator.any_in_bounds::<i32>().ptr;
// Wrap the raw pointers in NonNull
let src = NonNull::new(src_ptr).unwrap();
let dest = NonNull::new(dest_ptr).unwrap();
// Generate an arbitrary count using kani::any
let count: usize = kani::any();
unsafe { src.copy_from(dest, count);}
}
#[kani::proof_for_contract(NonNull::<T>::copy_to_nonoverlapping)]
pub fn non_null_check_copy_to_nonoverlapping() {
// PointerGenerator instance
let mut generator = PointerGenerator::<16>::new();
// Generate arbitrary pointers for src and dest
let src_ptr = generator.any_in_bounds::<i32>().ptr;
let dest_ptr = generator.any_in_bounds::<i32>().ptr;
// Wrap the raw pointers in NonNull
let src = NonNull::new(src_ptr).unwrap();
let dest = NonNull::new(dest_ptr).unwrap();
// Generate an arbitrary count using kani::any
let count: usize = kani::any();
unsafe { src.copy_to_nonoverlapping(dest, count);}
}
#[kani::proof_for_contract(NonNull::<T>::copy_from_nonoverlapping)]
pub fn non_null_check_copy_from_nonoverlapping() {
// PointerGenerator instance
let mut generator = PointerGenerator::<16>::new();
// Generate arbitrary pointers for src and dest
let src_ptr = generator.any_in_bounds::<i32>().ptr;
let dest_ptr = generator.any_in_bounds::<i32>().ptr;
// Wrap the raw pointers in NonNull
let src = NonNull::new(src_ptr).unwrap();
let dest = NonNull::new(dest_ptr).unwrap();
// Generate an arbitrary count using kani::any
let count: usize = kani::any();
unsafe { src.copy_from_nonoverlapping(dest, count);}
}
}
Loading