Contracts & Harnesses for byte_add, byte_offset, and byte_offset_from

[danielhumanmod]

Description:

This PR introduces function contracts and proof harness for the NonNull pointer in the Rust core library. Specifically, it verifies three new APIs—byte_offset, byte_add, and byte_offset_from with Kani. These changes enhance the functionality of pointer arithmetic and verification for NonNull pointers.

Changes Overview:

Covered APIs:

1. NonNull::byte_add: Adds a specified byte offset to a pointer.
2. NonNull::byte_offset: Allows calculating an offset from a pointer in bytes.
3. NonNull::byte_offset_from: Calculates the distance between two pointers in bytes.

Proof harness:

1. non_null_byte_add_proof
2. non_null_byte_offset_proof
3. non_null_byte_offset_from_proof

Resolves #53

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[danielhumanmod]

Thanks for your suggestion @zhassan-aws! I've updated the code in the latest commit based on your comments. I’d appreciate it if you could take a look when you have a chance.

[danielhumanmod]

Hi @zhassan-aws , thanks for the review and suggestions. I have updated the code based on the comments, fix the unnecessary assume proof harness, using addr, and add unchecked_add to avoid overflow, appreciate if any further suggestion!

[zhassan-aws]

Nice. Thanks!

[celinval]

Please replace kani::requires and kani::ensures by safety::requires and safety::ensures. Thanks!

[celinval]

Looks good. Can you please add harnesses for the dangling pointers cases?

[celinval]

I believe it's safe to call this function with count == 0 even if self.pointer is dangling.

[danielhumanmod]

I believe it's safe to call this function with count == 0 even if self.pointer is dangling.

Appreciate the suggestion @celinval! But there is some failure with the my dangling proof:

Proof harness:

#[kani::proof_for_contract(NonNull::byte_add)]
    pub fn non_null_byte_add_dangling_proof() {
        let ptr = NonNull::<i32>::dangling();
        let count: usize = 0;
        unsafe {
            let _ = ptr.byte_add(count);
        }
    }

Error:

VERIFICATION RESULT:
 ** 1 of 178 failed
Failed Checks: Kani does not support reasoning about pointer to unallocated memory
 File: "/Users/danieltu/Developer/verify-rust-std/library/core/src/lib.rs", line 423, in kani::mem::cbmc::same_allocation::<i32>

VERIFICATION:- FAILED
Verification Time: 0.26384938s

I am not sure whether it is because I didn't create a proper dangling scenario, could you provide some suggestion on this? Thanks!

[celinval]

Did you extend the requires clause?

[danielhumanmod]

Did you extend the requires clause?

Hi @celinval, do you mind being more specific about it? Based on my understanding, we need to add a proof harness where ptr is dangling and count = 0. Any additional contract need to be added into the API?

[celinval]

This should also be safe if the pointers hold the same address, even if they are dangling

[danielhumanmod]

This should also be safe if the pointers hold the same address, even if they are dangling

Same as above, there is a failure:

Proof harness

#[kani::proof_for_contract(NonNull::byte_offset_from)]
    pub fn non_null_byte_offset_from_dangling_proof() {
        let origin = NonNull::<i32>::dangling();
        let ptr = origin;
        unsafe {
            let _ = ptr.byte_offset_from(origin);
        }
    }

Error:

VERIFICATION RESULT:
 ** 1 of 184 failed (1 unreachable)
Failed Checks: Kani does not support reasoning about pointer to unallocated memory
 File: "/Users/danieltu/Developer/verify-rust-std/library/core/src/lib.rs", line 423, in kani::mem::cbmc::same_allocation::<()>

VERIFICATION:- FAILED
Verification Time: 0.24433088s

[celinval]

Please see my question above.

[feliperodri]

@danielhumanmod could you resolve the conflicts?

[danielhumanmod]

@danielhumanmod could you resolve the conflicts?

Hi @feliperodri , I have solved the conflicts in latest commit, thanks for reminding that