Contract and harness for as_ptr, cast, as_mut_ptr, and as_non_null_ptr

[Dhvani-Kapadia]

Description

This PR includes contracts and proof harnesses for the four APIs as_ptr, cast, as_mut_ptr, and as_non_null_ptr which are part of the NonNull library in Rust.

Changes Overview:

Covered APIs:
NonNull::as_ptr: Acquires the underlying *mut pointer
NonNull::cast: Casts to a pointer of another type
NonNull:: as_mut_ptr: Returns raw pointer to array's buffer
NonNull::as_non_null_ptr: Returns a non-null pointer to slice's buffer

Proof harness:
non_null_check_as_ptr
non_null_check_cast
non_null_check_as_mut_ptr
non_null_check_as_non_null_ptr

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:

SUMMARY:
 ** 0 of 128 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 0.8232234s

Complete - 4 successfully verified harnesses, 0 failures, 4 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.

[Dhvani-Kapadia]

@zhassan-aws , I have made the required changes based on your feedback. Kindly review it again.

[Dhvani-Kapadia]

I made the changes and the contracts were successful. `
SUMMARY:
** 0 of 127 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 0.7873746s

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

[celinval]

Thanks

[zhassan-aws]

Please resolve the conflicts, and I'll go ahead and merge.

[Dhvani-Kapadia]

@zhassan-aws , I have resolved the conflicts. Thanks for helping revert the submodule!

[zhassan-aws]

trigger approval workflow

[tautschnig]

@Dhvani-Kapadia Can you please review the CI failures?

[QinyuanWu]

@Dhvani-Kapadia @zhassan-aws @celinval The two compiler errors are

error: const function that might be (indirectly) exposed to stable cannot use `#[feature(slice_ptr_get)]`
    --> /Users/owo/Desktop/verify-rust-std/library/core/src/ptr/non_null.rs:1483:9
     |
1483 |         self.as_non_null_ptr().as_ptr()
     |         ^^^^^^^^^^^^^^^^^^^^^^
     |
     = help: mark the callee as `#[rustc_const_stable_indirect]` if it does not itself require any unsafe features
help: if the caller is not (yet) meant to be exposed to stable, add `#[rustc_const_unstable]` (this is what you probably want to do)
     |
1481 +     #[rustc_const_unstable(feature = "...", issue = "...")]
1482 |     #[ensures(|result: &*mut T| *result == self.pointer as *mut T)]
     |
help: otherwise, as a last resort `#[rustc_allow_const_fn_unstable]` can be used to bypass stability checks (this requires team approval)
     |
1481 +     #[rustc_allow_const_fn_unstable(slice_ptr_get)]
1482 |     #[ensures(|result: &*mut T| *result == self.pointer as *mut T)]
     |

error: const function that might be (indirectly) exposed to stable cannot use `#[feature(slice_ptr_get)]`
   --> /Users/owo/Desktop/verify-rust-std/library/core/src/ffi/c_str.rs:536:9
    |
536 | / ...   unsafe { NonNull::new_unchecked(&self.inner as *const [c_char] as *...
537 | | ...       .as_non_null_ptr()
    | |____________________________^
    |
    = help: mark the callee as `#[rustc_const_stable_indirect]` if it does not itself require any unsafe features
help: if the caller is not (yet) meant to be exposed to stable, add `#[rustc_const_unstable]` (this is what you probably want to do)
    |
533 +     #[rustc_const_unstable(feature = "...", issue = "...")]
534 |     const fn as_non_null_ptr(&self) -> NonNull<c_char> {
    |
help: otherwise, as a last resort `#[rustc_allow_const_fn_unstable]` can be used to bypass stability checks (this requires team approval)
    |
533 +     #[rustc_allow_const_fn_unstable(slice_ptr_get)]
534 |     const fn as_non_null_ptr(&self) -> NonNull<c_char> {
    |

After looking into the code it seems like the error is in the implementation of the function:

    //nonnull.rs
    #[ensures(|result: &*mut T| *result == self.pointer as *mut T)]
    pub const fn as_mut_ptr(self) -> *mut T {
        self.as_non_null_ptr().as_ptr() // line 1483
    }
    //c_str.rs
    #[inline]
    #[must_use]
    const fn as_non_null_ptr(&self) -> NonNull<c_char> {
        // FIXME(const_trait_impl) replace with `NonNull::from`
        // SAFETY: a reference is never null
        unsafe { NonNull::new_unchecked(&self.inner as *const [c_char] as *mut [c_char]) } //line 536
            .as_non_null_ptr()
    }

This is using kani commit db9516b292cf4f4b1a414d55e746f82d34fbc9f4. Is this an issue with the recent update with kani?

[Dhvani-Kapadia]

Hey @zhassan-aws , could you please merge it