Propose new Kani API to compare two objects byte-by-byte #3693
Description
Requested feature: byte-by-byte object comparison API
Use case: Compare and check whether two objects pointed by two pointers have the same value byte-by-byte up till a specific size. Something like:
kani::compare_byte_by_byte(pointer1: *const<T> , pointer2: *const<T> , size: usize)For example, we want to compare the result with the data that was passed in:
#[ensures(|result| !result.pointer.is_null() && compare_byte_by_byte(data.pointer, result.pointer, len * size_of<T>))]
pub const fn slice_from_raw_parts(data: NonNull<T>, len: usize) -> Self {
unsafe { Self::new_unchecked(super::slice_from_raw_parts_mut(data.as_ptr(), len)) }
}Another example is to compare an aligned and intentionally unaligned pointer to see if they point to the same sequence of n bytes:
// aligned_ptr is *const u8, unaligned_ptr is *const usize, both pointing to the same array of u8 elements
let result = kani::compare_byte_by_byte(aligned_ptr, unaligned_ptr as *const u8, mem::size_of<usize>);