const in a Function that Writes to Memory

[Jimmycreative]

I am attempting to write a contract for the NonNull::write function. The write function is designed to overwrite a memory location with a new value without reading or dropping the old value. Here's the function signature:

/// Overwrites a memory location with the given value without reading or
/// dropping the old value.
///
/// See [`ptr::write`] for safety concerns and examples.
///
/// [`ptr::write`]: crate::ptr::write()
#[inline(always)]
#[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
#[stable(feature = "non_null_convenience", since = "1.80.0")]
#[rustc_const_unstable(feature = "const_ptr_write", issue = "86302")]
#[requires(!self.as_ptr().is_null())]
#[requires(self.as_ptr() as usize % core::mem::align_of::<T>() == 0)] // Ensure the pointer is properly aligned
#[ensures(|_| unsafe { *self.as_ptr() == val })]
pub const unsafe fn write(self, val: T)
where
    T: Sized,
{
    // SAFETY: the caller must uphold the safety contract for `write`.
    unsafe { ptr::write(self.as_ptr(), val) }
}

#[kani::proof_for_contract(NonNull::write)]
    pub fn non_null_check_write() {
        let mut data: i32 = kani::any();
        let ptr = unsafe { NonNull::new(&mut data as *mut i32).unwrap() };
        let new_value: i32 = kani::any();

        unsafe {
            // Perform the write operation
            ptr.write(new_value);
            assert_eq!(ptr::read(ptr.as_ptr()), new_value);
        }
    }

Issue Encountered

The primary issue I am facing relates to the use of the const qualifier on the write function and the attempt to use Kani's ensures condition to verify that the value at the pointer has been updated correctly.

Specifically:

The function does not read or drop the old value before writing, and this is by design. This means that we should not rely on reading the value to verify correctness, as this would contradict the stated behavior of write.

When attempting to add an ensures postcondition, such as:

#[ensures(|_| unsafe { *self.as_ptr() == val })]

I encountered the error:
"pub const unsafe fn write(self, val: T)
| ^^^ the destructor for this type cannot be evaluated in constant functions" or "consider further restricting this bound" error.

• The error is related to the fact that const fn cannot evaluate destructors, and Rust cannot guarantee that T is a trivial type without destructors. This is why a postcondition involving *self.as_ptr() == val leads to a compilation error.

Why This is Problematic

• The write function is const, meaning that it must be able to be evaluated at compile time. However, if T has a destructor, this destructor cannot be evaluated in a const context. This is what leads to the error when trying to verify the value using *self.as_ptr() == val.
• The original documentation of write explicitly states that the function will not read the old value or drop it. This implies that any verification relying on reading the value might contradict the intended behavior and result in undefined or incorrect usage.

Questions for Discussion

1. Is it possible to verify the correctness of a write operation without reading the value in a way that respects the function's intended behavior?
2. How can one write a meaningful postcondition for a write operation in const contexts, especially for generic types where destructors may be involved?
3. Are there alternative approaches to verification that I might consider in this scenario?

[zhassan-aws]

Hi @Jimmycreative. I'm unable to reproduce the same error. I'm getting a different error:

$ kani verify-std -Z unstable-options ./library -Zfunction-contracts -Zmem-predicates --harness non_null
Kani Rust Verifier 0.56.0 (standalone)
warning: /home/ubuntu/git/verify-rust-std/target/kani_verify_std/Cargo.toml: no edition set: defaulting to the 2015 edition while the latest is 2021
   Compiling proc-macro2 v1.0.89
   Compiling version_check v0.9.5
   Compiling unicode-ident v1.0.13
   Compiling syn v1.0.109
   Compiling safety v0.1.0 (/home/ubuntu/git/verify-rust-std/library/contracts/safety)
   Compiling compiler_builtins v0.1.123
   Compiling libc v0.2.158
   Compiling memchr v2.5.0
   Compiling std v0.0.0 (/home/ubuntu/git/verify-rust-std/library/std)
   Compiling proc-macro-error-attr v1.0.4
   Compiling proc-macro-error v1.0.4
   Compiling quote v1.0.37
   Compiling syn v2.0.85
   Compiling core v0.0.0 (/home/ubuntu/git/verify-rust-std/library/core)
error[E0369]: binary operation `==` cannot be applied to type `T`
    --> /home/ubuntu/git/verify-rust-std/library/core/src/ptr/non_null.rs:1029:43
     |
1029 |     #[ensures(|_| unsafe { *self.as_ptr() == val })]
     |                            -------------- ^^ --- T
     |                            |
     |                            T
     |
help: consider further restricting this bound
     |
173  | impl<T: ?Sized + cmp::PartialEq> NonNull<T> {
     |                ++++++++++++++++

For more information about this error, try `rustc --explain E0369`.
error: could not compile `core` (lib) due to 1 previous error
error: Failed to execute cargo (exit status: 101). Found 1 compilation errors.

Can you post the full log of the run including the command?

It would also help to push the changes to your fork and provide a link to it.

[Jimmycreative]

Thanks for your response! I have added the proof for this function above. I mentioned there are two errors occurred : "pub const unsafe fn write(self, val: T)
| ^^^ the destructor for this type cannot be evaluated in constant functions" or "consider further restricting this bound" error.

commented out the ensure statement will give this error: the destructor for this type cannot be evaluated in constant functions

with ensure statement it will give this like you mentioned above: consider further restricting this bound

the link : https://github.com/danielhumanmod/verify-rust-std/blob/jimmy/write_bytes/library/core/src/ptr/non_null.rs

/Users/Downloads/kani/scripts/kani verify-std -Z unstable-options "/Users/Desktop/verify-rust-std/library" -Z function-contracts -Z mem-predicates --harness ptr::non_null::verify
Kani Rust Verifier 0.56.0 (standalone)
    Updating crates.io index
   Compiling proc-macro2 v1.0.89
   Compiling unicode-ident v1.0.13
   Compiling version_check v0.9.5
   Compiling syn v1.0.109
   Compiling safety v0.1.0 
   Compiling compiler_builtins v0.1.123
   Compiling libc v0.2.158
   Compiling memchr v2.5.0
   Compiling std v0.0.0 
   Compiling proc-macro-error-attr v1.0.4
   Compiling proc-macro-error v1.0.4
   Compiling quote v1.0.37
   Compiling syn v2.0.85
   Compiling core v0.0.0 
error[E0493]: destructor of `T` cannot be evaluated at compile-time
    --> /Users/Desktop/verify-rust-std/library/core/src/ptr/non_null.rs:1031:37
     |
1031 |     pub const unsafe fn write(self, val: T)
     |                                     ^^^ the destructor for this type cannot be evaluated in constant functions

For more information about this error, try `rustc --explain E0493`.
error: could not compile `core` (lib) due to 1 previous error
error: Failed to execute cargo (exit status: 101). Found 1 compilation errors.

[zhassan-aws]

Thanks. I was able to reproduce the error. This seems to be a bug/limitation in Kani. I reproduced it on a small example and filed model-checking/kani#3667.

[Jimmycreative]

Hi

I tried to work on the write_volatile api, but got the error below. I already use can_write to make sure it is writable. Not sure is there anything I missed out. Thanks in advance:

SUMMARY:
 ** 1 of 123 failed (1 unreachable)
Failed Checks: Check that *dst is assignable

#[inline(always)]
#[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
#[stable(feature = "non_null_convenience", since = "1.80.0")]
#[requires(ub_checks::can_write(self.as_ptr()))]
#[requires(self.as_ptr() as usize % core::mem::size_of::<T>() == 0)]
pub unsafe fn write_volatile(self, val: T)
where
    T: Sized,
{
    // SAFETY: the caller must uphold the safety contract for `write_volatile`.
    unsafe { ptr::write_volatile(self.as_ptr(), val) }
}

#[kani::proof_for_contract(NonNull::write_volatile)]
pub fn non_null_check_write_volatile() {
    let mut data: i32 = kani::any();
    let ptr = unsafe { NonNull::new(&mut data as *mut i32).unwrap() };
    let new_value: i32 = kani::any();

    unsafe {
        // Perform the volatile write operation
        ptr.write_volatile(new_value);

        assert_eq!(ptr::read(ptr.as_ptr()), new_value);
    }
}

[zhassan-aws]

Which line is the failure pointing to?

[Jimmycreative]

The error comes from ptr/mod.rs. This line causes the issue: intrinsics::volatile_store(dst, src);

#[inline]
#[stable(feature = "volatile", since = "1.9.0")]
#[rustc_diagnostic_item = "ptr_write_volatile"]
#[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
#[safety::requires(ub_checks::can_write(dst))]
pub unsafe fn write_volatile<T>(dst: *mut T, src: T) {
    // SAFETY: the caller must uphold the safety contract for `volatile_store`.
    unsafe {
        ub_checks::assert_unsafe_precondition!(
            check_language_ub,
            "ptr::write_volatile requires that the pointer argument is aligned and non-null",
            (
                addr: *mut () = dst as *mut (),
                align: usize = align_of::<T>(),
            ) => ub_checks::is_aligned_and_not_null(addr, align)
        );
        intrinsics::volatile_store(dst, src); // this line causes the issue
    }
}