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

Propose new Kani API to compare two objects byte-by-byte #3693

Open
QinyuanWu opened this issue Nov 7, 2024 · 2 comments
Open

Propose new Kani API to compare two objects byte-by-byte #3693

QinyuanWu opened this issue Nov 7, 2024 · 2 comments
Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature.

Comments

@QinyuanWu
Copy link

QinyuanWu commented Nov 7, 2024

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>);

@zhassan-aws

@zhassan-aws
Copy link
Contributor

As @celinval explained to me, adding a generic API is tricky because of padding bytes. So, the comparison will likely have to implemented for specific types in which we can guarantee a UB-free comparison.

@celinval: please correct me if I misunderstood.

@celinval
Copy link
Contributor

celinval commented Nov 8, 2024

My main point is that we need to decide how this API will behave when the type contains padding bytes / uninitialized memory.

Interesting enough, it seems that CBMC memcmp completely ignores them. 🤔 diffblue/cbmc#8499

zhassan-aws pushed a commit to model-checking/verify-rust-std that referenced this issue Nov 25, 2024
…_raw_parts`, `to_raw_parts` in NonNull (#127)

Towards #53 

Contracts and harnesses for `dangling`, `from_raw_parts`,
`slice_from_raw_parts`, `to_raw_parts` in NonNull
### Discussion

1. `NonNull::slice_from_raw_parts`:
[requested](model-checking/kani#3693) new Kani
API to compare byte by byte
2. `NonNull::to_raw_parts`: [unstable vtable comparison
'Eq'](#139)

### Verification Result
```
SUMMARY:
 ** 0 of 141 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 0.17378491s

Complete - 6 successfully verified harnesses, 0 failures, 6 total.
```

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature.
Projects
None yet
Development

No branches or pull requests

3 participants