Skip to content

Commit

Permalink
Clean up arbitrary pointer
Browse files Browse the repository at this point in the history
  • Loading branch information
@celinval
celinval committed Sep 20, 2024
1 parent 87dc890 commit 6827756
Showing 1 changed file with 97 additions and 103 deletions.
200 changes: 97 additions & 103 deletions library/core/src/intrinsics.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3616,152 +3616,146 @@ mod verify {
assert_eq!(x, old_y);
}

/// Note that in `core` we cannot check allocated pointers.
#[derive(Copy, Clone, Debug, PartialEq, Eq, kani::Arbitrary)]
enum PtrKind {
enum AllocationStatus {
/// Dangling pointers
Dangling,
/// Pointer to dead object
DeadObj,
/// Null pointers
Null,
/// Stack pointers
Stack,
/// Overlapping pointers
Overlap,
/// Unaligned pointers
Unaligned,
/// Pointer to uninitialized memory
Uninitialized,
/// In bounds pointer (it may be unaligned)
InBounds,
/// Out of bounds
OutBounds,
}

struct ArbitraryPointers<T> {
src: *const T,
dst: *mut T,
dst_kind: PtrKind,
src_kind: PtrKind,
struct PointerGenerator<T, const BUF_LEN: usize> {
// Internal allocation that may be used to generate valid pointers.
buf: MaybeUninit<[T; BUF_LEN]>,
}

impl<T: kani::Arbitrary> ArbitraryPointers<T> {
const MAX_SIZE_T: usize = 100;
const SIZE_T: usize = size_of::<T>();

const IS_VALID: () = assert!(Self::SIZE_T < Self::MAX_SIZE_T, "Exceeded supported type size");
struct ArbitraryPointer<T> {
pub ptr: *mut T,
pub status: AllocationStatus,
pub is_initialized: bool,
}

fn with_arbitrary<F>(harness: F) where F: FnOnce(ArbitraryPointers<T>) {
impl<T: kani::Arbitrary, const BUF_LEN: usize> PointerGenerator<T, BUF_LEN> {
const SZ : usize = BUF_LEN * size_of::<T>();

#[repr(C)]
struct WithUninit<const SIZE: usize> {
bytes: [MaybeUninit<u8>; SIZE],
pub fn new() -> Self {
PointerGenerator {
buf: MaybeUninit::uninit()
}
}

#[repr(C)]
#[repr(packed)]
#[derive(kani::Arbitrary)]
struct Unaligned<T> {
first: u8,
val: T, // If alignment of T > 1, this value will be unaligned but valid otherwise.
}

let mut single = kani::any::<T>();
let single_ptr = addr_of_mut!(single);

let mut array: [T; 100] = kani::any();
let array_ptr = addr_of_mut!(array) as *mut T;
/// Create another ArbitraryPointer that may have the same precedence as the `other` pointer.
///
/// I.e.: Non-deterministically derive a pointer from the given pointer or create a new
/// arbitrary pointer.
pub fn generate_ptr(&mut self) -> ArbitraryPointer<T> {
// Create an arbitrary pointer, but leave `ptr` as unset for now.
let mut arbitrary = ArbitraryPointer {
ptr: ptr::null_mut::<T>(),
is_initialized: false,
status: kani::any(),
};

let mut unaligned: Unaligned<T> = kani::any();
let unaligned_ptr = addr_of_mut!(unaligned.val) as *mut T;
let buf_ptr = addr_of_mut!(self.buf) as *mut T;

let mut uninit = WithUninit { bytes: [MaybeUninit::zeroed(); Self::MAX_SIZE_T] };
for i in 0..Self::SIZE_T {
if kani::any() {
uninit.bytes[i] = MaybeUninit::uninit();
// Offset is used to potentially generate unaligned pointer.
let offset = kani::any_where(|b: &usize| *b < size_of::<T>());
let ptr = match arbitrary.status {
AllocationStatus::Dangling => {
crate::ptr::dangling_mut::<T>().wrapping_add(offset)
}
}
let uninit_ptr = &mut uninit as *mut _ as *mut T;

let arbitrary = ArbitraryPointers::from(single_ptr, array_ptr, unaligned_ptr, uninit_ptr);
harness(arbitrary);
}

fn from(ptr1: *mut T, ptr2: *mut T, unaligned: *mut T, uninit: *mut T) -> Self {
let (src_kind, src) = ArbitraryPointers::any(ptr1, ptr2, unaligned, uninit);
let (dst_kind, dst) = ArbitraryPointers::any(ptr2, ptr1, unaligned, uninit);
ArbitraryPointers {
src_kind,
src,
dst_kind,
dst,
}
}

fn any(unique: *mut T, overlap: *mut T, unaligned: *mut T, uninit: *mut T) -> (PtrKind, *mut T) {
let kind = kani::any::<PtrKind>();
let ptr = match kind {
PtrKind::Dangling => {
crate::ptr::dangling_mut::<T>()
AllocationStatus::DeadObj => {
let mut obj: T = kani::any();
&mut obj as *mut _
}
PtrKind::Null => {
AllocationStatus::Null => {
crate::ptr::null_mut::<T>()
}
PtrKind::Stack => {
unique
AllocationStatus::InBounds => {
let pos = kani::any_where(|i: &usize| *i < (BUF_LEN - 1));
let ptr: *mut T = buf_ptr.wrapping_add(pos).wrapping_byte_add(offset);
if kani::any() {
arbitrary.is_initialized = true;
// This should be in bounds of arbitrary.alloc.
unsafe { ptr.write_unaligned(kani::any()) };
}
ptr
}
PtrKind::Overlap => {
if kani::any() { unique } else { overlap }
}
PtrKind::Unaligned => {
unaligned
}
PtrKind::Uninitialized => {
uninit
AllocationStatus::OutBounds => {
if kani::any() {
buf_ptr.wrapping_add(BUF_LEN).wrapping_byte_sub(offset)
} else {
buf_ptr.wrapping_add(BUF_LEN).wrapping_byte_add(offset)
}
}
};
(kind, ptr)

arbitrary
}
}


#[kani::proof_for_contract(copy)]
fn check_copy() {
ArbitraryPointers::<u32>::with_arbitrary(|arbitrary| {
// Skip dangling for now since it makes Kani contract panic.
// Verify this case in a separate harness.
kani::assume(arbitrary.dst_kind != PtrKind::Dangling);
kani::assume(arbitrary.src_kind != PtrKind::Dangling);
unsafe { copy(arbitrary.src, arbitrary.dst, kani::any()) }
});
let mut generator = PointerGenerator::<char, 10>::new();
let src = generator.generate_ptr();
let dst = if kani::any() {
generator.generate_ptr();
} else {
PointerGenerator::<char, 10>::new().generate_ptr()
};
// Skip dangling for now since it makes Kani contract panic.
// Verify this case in a separate harness.
kani::assume(src.status != AllocationStatus::Dangling);
kani::assume(dst.status != AllocationStatus::Dangling);
unsafe { copy(src.ptr, dst.ptr, kani::any()) }
}

/// This harness fails because Kani cannot assume a pointer is valid.
///
/// The specification should ensure the pointers passed are allocated, and this harness should
/// succeed since `copy` ensures would reject dangling pointers.
#[cfg(ignore)]
#[kani::should_panic]
#[kani::proof_for_contract(copy)]
fn check_copy_dangling() {
ArbitraryPointers::<u32>::with_arbitrary(|arbitrary| {
let mut generator = PointerGenerator::<char, 10>::new();
let src = generator.generate_ptr();
let dst = generator.generate_ptr();
// Verify the dangling case.
kani::assume(arbitrary.dst_kind == PtrKind::Dangling || arbitrary.src_kind == PtrKind::Dangling);
unsafe { copy(arbitrary.src, arbitrary.dst, kani::any()) }
});
kani::assume(src.status == AllocationStatus::Dangling || dst.status == AllocationStatus::Dangling);
unsafe { copy(src.ptr, dst.ptr, kani::any()) }
}

#[kani::proof_for_contract(copy_nonoverlapping)]
fn check_copy_nonoverlapping() {
ArbitraryPointers::<u32>::with_arbitrary(|arbitrary| {
// Skip dangling for now since it makes Kani contract panic.
// Verify this case in a separate harness.
kani::assume(arbitrary.dst_kind != PtrKind::Dangling);
kani::assume(arbitrary.src_kind != PtrKind::Dangling);
unsafe { copy_nonoverlapping(arbitrary.src, arbitrary.dst, kani::any()) }
});
let mut generator = PointerGenerator::<char, 10>::new();
let src = generator.generate_ptr();
// Destination may or may not have the same precedence as src.
let dst = if kani::any() {
generator.generate_ptr();
} else {
PointerGenerator::<char, 10>::new().generate_ptr()
};
// Skip dangling for now since it makes Kani contract panic.
// Verify this case in a separate harness.
kani::assume(src.status != AllocationStatus::Dangling);
kani::assume(dst.status != AllocationStatus::Dangling);
unsafe { copy_nonoverlapping(src.ptr, dst.ptr, kani::any()) }
}

#[kani::proof_for_contract(write_bytes)]
fn check_write_bytes() {
ArbitraryPointers::<u32>::with_arbitrary(|arbitrary| {
// Skip dangling for now since it makes Kani contract panic.
// Verify this case in a separate harness.
kani::assume(arbitrary.dst_kind != PtrKind::Dangling);
unsafe { write_bytes(arbitrary.dst, kani::any(), kani::any()) }
});
let mut generator = PointerGenerator::<char, 10>::new();
let src = generator.generate_ptr();
kani::assume(src.status != AllocationStatus::Dangling);
// Skip dangling for now since it makes Kani contract panic.
// Verify this case in a separate harness.
unsafe { write_bytes(src.ptr, kani::any(), kani::any()) }
}
}

0 comments on commit 6827756

Please sign in to comment.