Contract & Harnesses for byte_sub, offset, map_addr and with_addr

[Dhvani-Kapadia]

Description

This PR includes contracts and proof harnesses for the four APIs, offset , byte_sub, map_addr, and with_addr which are part of the NonNull library in Rust.

Changes Overview:

Covered APIs:
NonNull::offset: Adds an offset to a pointer
NonNull::byte_sub: Calculates an offset from a pointer in bytes.
NonNull:: map_addr: Creates a new pointer by mapping self's address to a new one
NonNull::with_addr: Creates a new pointer with the given address

Proof harness:
non_null_check_offset
non_null_check_byte_sub
non_null_check_map_addr
non_null_check_with_addr

Revalidation

To revalidate the verification results, run kani verify-std -Z unstable-options "path/to/library" -Z function-contracts -Z mem-predicates --harness ptr::non_null::verify. This will run all four harnesses in the module. All default checks should pass:

VERIFICATION:- SUCCESSFUL
Verification Time: 0.57787573s

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

Towards issue #53

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

[carolynzech]

Also, re your PR description: it seems like the issue you mention for #91 was resolved by building Kani from source. Can you update your PR description if that is the case? Please also add "Towards #ISSUE-NUMBER" with the appropriate issue link for your challenge.

[QinyuanWu]

Please make sure to remove all other edits that are not in non_null.rs.

[Dhvani-Kapadia]

I wanted to use can_dereference for map_addr but got multiple compilation errors.
#[ensures(|result: &Self| kani::mem::can_dereference(result.as_ptr()))] . So ended up not including it in the contract. Could you please let me know if my usage of it is correct or provide examples?

[carolynzech]

I wanted to use can_dereference for map_addr but got multiple compilation errors. #[ensures(|result: &Self| kani::mem::can_dereference(result.as_ptr()))] . So ended up not including it in the contract. Could you please let me know if my usage of it is correct or provide examples?

@Dhvani-Kapadia I suspect this is another import error--you should be importing crate::ub_checks::can_dereference. Please include the text of your errors in the future--they are very helpful for debugging! As for examples, I would recommend searching for usages of this function elsewhere in this repository (intrinsics.rs has some).

[carolynzech]

Almost there! Please run rustfmt on the file, fix the conflicts with this file and the main branch, and address these comments, then re-request my review.

[feliperodri]

The documentation says

If the computed offset is non-zero, then self must be derived from a pointer to some allocated object, and the entire memory range between self and the result must be in bounds of that allocated object.

So should we be explicit and state same_allocation only if the computed offset is non-zero?

[feliperodri]

Why 100? Could you make this a const and add a explanation for the number to be used across all harnesses?

[Dhvani-Kapadia]

For testing locally I used the value 100. I wanted to provide big enough size to cover all cases. Should I use 1000, which is used insuband sub_ptr which have been recently merged?