Skip to content

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

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 25 commits into from
Dec 12, 2024
Merged

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

Changes from 3 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
133 changes: 132 additions & 1 deletion library/core/src/ptr/non_null.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ use crate::slice::{self, SliceIndex};
use crate::ub_checks::assert_unsafe_precondition;
use crate::{fmt, hash, intrinsics, ptr};
use safety::{ensures, requires};

use crate::{ub_checks};

#[cfg(kani)]
use crate::kani;
Expand Down Expand Up @@ -934,6 +934,12 @@ impl<T: ?Sized> NonNull<T> {
#[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
#[stable(feature = "non_null_convenience", since = "1.80.0")]
#[rustc_const_unstable(feature = "const_intrinsic_copy", issue = "80697")]
#[kani::requires(count * core::mem::size_of::<T>() <= isize::MAX as usize)]
#[requires(ub_checks::can_dereference(self.as_ptr()))] //The pointer is valid
#[requires(ub_checks::can_dereference(dest.as_ptr()))]
#[ensures(|result: &()| ub_checks::can_dereference(self.as_ptr() as *const T))]
#[ensures(|result: &()| ub_checks::can_dereference(dest.as_ptr() as *const T))]
#[kani::modifies(dest.as_ptr())]
pub const unsafe fn copy_to(self, dest: NonNull<T>, count: usize)
where
T: Sized,
Expand All @@ -954,6 +960,14 @@ impl<T: ?Sized> NonNull<T> {
#[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
#[stable(feature = "non_null_convenience", since = "1.80.0")]
#[rustc_const_unstable(feature = "const_intrinsic_copy", issue = "80697")]
#[kani::requires(count * core::mem::size_of::<T>() <= isize::MAX as usize)]
#[requires(ub_checks::can_dereference(self.as_ptr()))]
#[requires(ub_checks::can_dereference(dest.as_ptr()))]
#[requires((self.as_ptr() as usize).abs_diff(dest.as_ptr() as usize) >= count * core::mem::size_of::<T>())]
#[ensures(|result: &()| ub_checks::can_dereference(self.as_ptr()))]
#[ensures(|result: &()| ub_checks::can_dereference(dest.as_ptr()))]
#[kani::modifies(dest.as_ptr())]
#[kani::modifies(self.as_ptr())]
pub const unsafe fn copy_to_nonoverlapping(self, dest: NonNull<T>, count: usize)
where
T: Sized,
Expand All @@ -974,6 +988,13 @@ impl<T: ?Sized> NonNull<T> {
#[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
#[stable(feature = "non_null_convenience", since = "1.80.0")]
#[rustc_const_unstable(feature = "const_intrinsic_copy", issue = "80697")]
#[kani::requires(count * core::mem::size_of::<T>() <= isize::MAX as usize)]
#[requires(ub_checks::can_dereference(src.as_ptr()) )]//The pointer is valid
#[requires( ub_checks::can_dereference(self.as_ptr()))]//The pointer is valid
#[requires((src.as_ptr() as usize).abs_diff(self.as_ptr() as usize) >= count * core::mem::size_of::<T>())]
#[ensures(|result: &()| ub_checks::can_dereference(src.as_ptr()))]
#[ensures(|result: &()| ub_checks::can_dereference(self.as_ptr()))]
#[kani::modifies(self.as_ptr())]
pub const unsafe fn copy_from(self, src: NonNull<T>, count: usize)
where
T: Sized,
Expand All @@ -994,6 +1015,14 @@ impl<T: ?Sized> NonNull<T> {
#[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
#[stable(feature = "non_null_convenience", since = "1.80.0")]
#[rustc_const_unstable(feature = "const_intrinsic_copy", issue = "80697")]
#[kani::requires(count * core::mem::size_of::<T>() <= isize::MAX as usize)]//count check
#[requires(ub_checks::can_dereference(self.as_ptr()))]
#[requires(ub_checks::can_dereference(src.as_ptr()))]
#[requires((self.as_ptr() as usize).abs_diff(src.as_ptr() as usize) >= count * core::mem::size_of::<T>())]//The source and destination regions do not overlap.
#[ensures(|result: &()| ub_checks::can_dereference(self.as_ptr()))]
#[ensures(|result: &()| ub_checks::can_dereference(src.as_ptr()))]
#[kani::modifies(self.as_ptr())]
#[kani::modifies(src.as_ptr())]
pub const unsafe fn copy_from_nonoverlapping(self, src: NonNull<T>, count: usize)
where
T: Sized,
Expand Down Expand Up @@ -1803,4 +1832,106 @@ mod verify {
let maybe_null_ptr = if kani::any() { xptr as *mut i32 } else { null_mut() };
let _ = NonNull::new(maybe_null_ptr);
}

#[kani::proof_for_contract(NonNull::<T>::copy_to)]
pub fn non_null_check_copy_to() {
// Create source and destination values
let mut src_value: i32 = kani::any();
let mut dest_value: i32 = 0;

// Create NonNull pointers
let src = NonNull::new(&mut src_value as *mut i32).unwrap();
let dest = NonNull::new(&mut dest_value as *mut i32).unwrap();
//casting the pointer
let src_u8 = src.as_ptr() as *const u8;
let dest_u8 = dest.as_ptr() as *mut u8;
//count is 1 as working with single i32 value
let count = 1;
unsafe {
kani::assume(kani::mem::can_dereference(src_u8));
kani::assume(kani::mem::can_dereference(
src_u8.add(core::mem::size_of::<i32>() - 1),
));
kani::assume(kani::mem::can_dereference(dest_u8));
kani::assume(kani::mem::can_dereference(
dest_u8.add(core::mem::size_of::<i32>() - 1),
));
src.copy_to(dest, count);
}
}
#[kani::proof_for_contract(NonNull::<T>::copy_from)]
pub fn non_null_check_copy_from() {
// Create source and destination values
let mut src_value: i32 = kani::any();
let mut dest_value: i32 = 0;

// Create NonNull pointers
let src = NonNull::new(&mut src_value as *mut i32).unwrap();
let dest = NonNull::new(&mut dest_value as *mut i32).unwrap();
//casting the pointer
let src_u8 = src.as_ptr() as *const u8;
let dest_u8 = dest.as_ptr() as *mut u8;
//count is 1 as working with single i32 value
let count = 1;
unsafe {
kani::assume(kani::mem::can_dereference(src_u8));
kani::assume(kani::mem::can_dereference(
src_u8.add(core::mem::size_of::<i32>() - 1),
));
kani::assume(kani::mem::can_dereference(dest_u8));
kani::assume(kani::mem::can_dereference(
dest_u8.add(core::mem::size_of::<i32>() - 1),
));
src.copy_from(dest, count);
}
}
#[kani::proof_for_contract(NonNull::<T>::copy_to_nonoverlapping)]
pub fn non_null_check_copy_to_nonoverlapping() {
let mut src_value: i32 = kani::any();
let mut dest_value: i32 = 0;

let src = NonNull::new(&mut src_value as *mut i32).unwrap();
let dest = NonNull::new(&mut dest_value as *mut i32).unwrap();
//casting the pointer
let src_u8 = src.as_ptr() as *const u8;
let dest_u8 = dest.as_ptr() as *mut u8;
//count represents no of elements to copy
let count = 1;
unsafe {
kani::assume(kani::mem::can_dereference(src_u8));
kani::assume(kani::mem::can_dereference(
src_u8.add(core::mem::size_of::<i32>() - 1),
));
kani::assume(kani::mem::can_dereference(dest_u8));
kani::assume(kani::mem::can_dereference(
dest_u8.add(core::mem::size_of::<i32>() - 1),
));
src.copy_to_nonoverlapping(dest, count);
}
}
#[kani::proof_for_contract(NonNull::<T>::copy_from_nonoverlapping)]
pub fn non_null_check_copy_from_nonoverlapping() {
let mut src_value: i32 = kani::any();
let mut dest_value: i32 = 0;

let src = NonNull::new(&mut src_value as *mut i32).unwrap();
let dest = NonNull::new(&mut dest_value as *mut i32).unwrap();
//casting the pointer
let src_u8 = src.as_ptr() as *const u8;
let dest_u8 = dest.as_ptr() as *mut u8;
//count represents no of elements to copy
let count = 1;

unsafe {
kani::assume(kani::mem::can_dereference(src_u8));
kani::assume(kani::mem::can_dereference(
src_u8.add(core::mem::size_of::<i32>() - 1),
));
kani::assume(kani::mem::can_dereference(dest_u8));
kani::assume(kani::mem::can_dereference(
dest_u8.add(core::mem::size_of::<i32>() - 1),
));
dest.copy_from_nonoverlapping(src, count);
}
}
}
Loading