Prove correctness for NonNull::read_unaligned

[QinyuanWu]

In the harness for NonNull::read_unaligned I want to check whether the returned value matches expectation, so I tried comparing byte by byte:

    pub fn non_null_check_read_unaligned() {
        const SIZE: usize = 100;
        // cast a random offset of an u8 array to usize
        let offset: usize = kani::any();
        kani::assume(offset >= 0 && offset < SIZE - 4);
        let arr: [u8; SIZE] = kani::any();  
        let unaligned_ptr = &arr[offset] as *const u8 as *const usize;
        // create a NonNull pointer from the unaligned pointer
        let nonnull_ptr = NonNull::new(unaligned_ptr as *mut usize).unwrap();
        unsafe { 
            let result = nonnull_ptr.read_unaligned();
            let raw_result_ptr = result as *const u8;
            let raw_original_ptr = &arr[offset] as *const u8;
            for i in 0..core::mem::size_of::<usize>() {
                  // Dereference and compare each byte
                  assert_eq!(*raw_original_ptr.add(i), *raw_result_ptr.add(i));
            }
        }

Coontract for read_unaligned:

    #[requires(ub_checks::can_dereference(self.pointer))]
    pub const unsafe fn read_unaligned(self) -> T
    where
        T: Sized,
    {
        // SAFETY: the caller must uphold the safety contract for `read_unaligned`.
        unsafe { ptr::read_unaligned(self.pointer) }
    }

However the following checks failed:

Check 43: panicking::assert_failed_inner.assertion.2
	 - Status: FAILURE
	 - Description: "This is a placeholder message; Kani doesn't support message formatted at runtime"
	 - Location: library/core/src/panicking.rs:412:17 in function panicking::assert_failed_inner

Check 79: ptr::const_ptr::<impl *const u8>::add.arithmetic_overflow.2
	 - Status: FAILURE
	 - Description: "attempt to compute offset which would overflow"
	 - Location: library/core/src/ptr/const_ptr.rs:857:18 in function ptr::const_ptr::<impl *const u8>::add

Check 172: ptr::non_null::verify::non_null_check_read_unaligned.pointer_dereference.7
	 - Status: FAILURE
	 - Description: "dereference failure: pointer NULL"
	 - Location: library/core/src/macros/mod.rs:46:35 in function ptr::non_null::verify::non_null_check_read_unaligned

Check 173: ptr::non_null::verify::non_null_check_read_unaligned.pointer_dereference.8
	 - Status: FAILURE
	 - Description: "dereference failure: pointer invalid"
	 - Location: library/core/src/macros/mod.rs:46:35 in function ptr::non_null::verify::non_null_check_read_unaligned

Check 174: ptr::non_null::verify::non_null_check_read_unaligned.pointer_dereference.9
	 - Status: FAILURE
	 - Description: "dereference failure: deallocated dynamic object"
	 - Location: library/core/src/macros/mod.rs:46:35 in function ptr::non_null::verify::non_null_check_read_unaligned

Check 175: ptr::non_null::verify::non_null_check_read_unaligned.pointer_dereference.10
	 - Status: FAILURE
	 - Description: "dereference failure: dead object"
	 - Location: library/core/src/macros/mod.rs:46:35 in function ptr::non_null::verify::non_null_check_read_unaligned

Check 176: ptr::non_null::verify::non_null_check_read_unaligned.pointer_dereference.11
	 - Status: FAILURE
	 - Description: "dereference failure: pointer outside object bounds"
	 - Location: library/core/src/macros/mod.rs:46:35 in function ptr::non_null::verify::non_null_check_read_unaligned

Check 177: ptr::non_null::verify::non_null_check_read_unaligned.pointer_dereference.12
	 - Status: FAILURE
	 - Description: "dereference failure: invalid integer address"
	 - Location: library/core/src/macros/mod.rs:46:35 in function ptr::non_null::verify::non_null_check_read_unaligned

Appreciate any guidance. @zhassan-aws I checked this example but in that proof we know the concrete value so here the value is non-deterministic so I have to use a loop to compare the bytes.

[zhassan-aws]

Hi @QinyuanWu. One problem in the harness is that usize is 8 bytes on 64-bit platforms. So the add operations in the loop could exceed the boundary of the array (since offset is only constrained to be SIZE - 4).

[zhassan-aws]

The other issue in the harness is this line:

            let raw_result_ptr = result as *const u8;

The read_unaligned method returns the value, and so we need to get the address of it, i.e.:

            let raw_result_ptr = &result as *const usize as *const u8;

[zhassan-aws]

Also, please file a feature request in https://github.com/model-checking/kani for an byte-by-byte comparison API.

[QinyuanWu]

Opened proposal