Challenge 6: Safety of NonNull

[tautschnig]

Challenge 6: Safety of NonNull

[zhassan-aws]

Continuing the discussion from #84.

I found that without supplying the --harness option, both proofs in unique.rs and non_null.rs are not run.

This sounds like a bug. Can you:

1. Post the full log from Kani including the command you used to run it
2. Point to a branch on which I can reproduce this issue

?

I ended up changing the harness function name to a unique one(--harness non_null_check_new_unchecked) and that was successful(the fully-qualified name still has an error).

Can you post the harness name printed in the Kani output? The name is included in a line of the form:

Checking harness <harness-name>

[zhassan-aws]

A second question is if the contract has specified a pre-condition(e.g. !ptr.is_null()), does that mean in the harness we don't need to make the assumption that xptr is not null? In other words, the ensures clause acts like an assume statement?

Correct. When verifying a contract (using proof_for_contract), a requires clause acts as an assumption, and the ensures clause acts like an assertion. When stubbing a function using its contract (using stub_verified), a requires clause acts as an assertion, and the ensures clause acts like an assumption.

[QinyuanWu]

@zhassan-aws I realized I didn't find these proofs being run was because kani has not finished running proofs in the other modules yet, I will let it run for longer to get the complete result for all proofs in the library.

I found that without supplying the --harness option, both proofs in unique.rs and non_null.rs are not run.

This sounds like a bug. Can you:

1. Post the full log from Kani including the command you used to run it
2. Point to a branch on which I can reproduce this issue

I found the correct full name to be ptr::non_null::verify instead of core::ptr::non_null::verify for all proofs in non_null.rs. Thank you so much!

?

I ended up changing the harness function name to a unique one(--harness non_null_check_new_unchecked) and that was successful(the fully-qualified name still has an error).

Can you post the harness name printed in the Kani output? The name is included in a line of the form:

Checking harness <harness-name>

[QinyuanWu]

@zhassan-aws Following up on our meeting just now, would you please give us a rundown on Kani's capability to verify the four undefined behaviors for challenge 6? You mentioned that Kani can verify property 1,2, and 4(partially) and we also want to know which flags are verifying these properties. For property 3 is there a timeline on when the check would be released?

1. Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
2. Reading from uninitialized memory.
3. Mutating immutable bytes.
4. Producing an invalid value.

[gracemqz]

@feliperodri Hi Felipe, this is Grace from CMU III, I'm the project manager of Team 4. Could you please assign me to the issue as well?

[zhassan-aws]

You mentioned that Kani can verify property 1,2, and 4(partially) and we also want to know which flags are verifying these properties.

Correct. No flags are needed for 1 and 2 (the checks are ON by default). For 4, the -Z valid-value-checks flag needs to be passed to Kani. The currently supported cases are outlined in model-checking/kani#3085.

For property 3 is there a timeline on when the check would be released?

For 3, the timeline is not clear at the moment. There is experimental support added in a branch of the Kani repository (i.e. it's not included in the Kani releases): https://github.com/model-checking/kani/tree/features/aliasing-checks. We can perhaps experiment with the current support and see if it's sufficient.

[QinyuanWu]

@zhassan-aws How should we interpret unreachable code results? For one of the checks for new_unchecked, it showed the following:

Check 14: ptr::non_null::NonNull::<i32>::new_unchecked::{closure#1}.unreachable.1
	 - Status: SUCCESS
	 - Description: "unreachable code"
	 - Location: library/core/src/ptr/non_null.rs:200:5 in function ptr::non_null::NonNull::<i32>::new_unchecked::{closure#1}

What does this mean? Is this normal or does that indicate we need to modify the harness? Thanks!

[zhassan-aws]

Hi @QinyuanWu. This indicates that some code that should be unreachable (as indicated by the check name) was indeed proven to be unreachable (as indicated by the SUCCESS status). So, nothing to be alarmed about.

[QinyuanWu]

Thank you @zhassan-aws. Is it possible to view the source coverage as well? I added -Z source-coverage, but I didn't see any coverage report in the output. The entire command I used was: kani verify-std -Z unstable-options "path/to/library" -Z function-contracts -Z mem-predicates -Z source-coverage --harness ptr::non_null::verify::non_null_check_new which verifies both non_null_check_new and non_null_check_new_unchecked.

[zhassan-aws]

For instance, this program:

#[kani::proof]
fn foo() {
    let x: i8 = kani::any();
    let y: i8 = kani::any();
    let z = (x as i16).checked_add(y as i16);
    // unwrap the result using a match
    let z = match z {
        Some(z) => z,
        None => unreachable!(),
    };
}

calls unreachable in the None arm because the addition is not expected to overflow. When we run Kani, it produces:

RESULTS:
Check 1: foo.unreachable.1
         - Status: SUCCESS
         - Description: "unreachable code"
         - Location: test.rs:7:19 in function foo

Check 2: foo.assertion.1
         - Status: SUCCESS
         - Description: "internal error: entered unreachable code: "
         - Location: test.rs:9:17 in function foo


SUMMARY:
 ** 0 of 2 failed

VERIFICATION:- SUCCESSFUL

and thus it proved the None case is indeed unreachable.

[QinyuanWu]

@zhassan-aws Opened PR for non_null::new and non_null:new_unchecked. It seems like I don't have permission to assign the PR to this issue.

[QinyuanWu]

Thank you @zhassan-aws. Is it possible to view the source coverage as well? I added -Z source-coverage, but I didn't see any coverage report in the output. The entire command I used was: kani verify-std -Z unstable-options "path/to/library" -Z function-contracts -Z mem-predicates -Z source-coverage --harness ptr::non_null::verify::non_null_check_new which verifies both non_null_check_new and non_null_check_new_unchecked.

@zhassan-aws would appreciate any guidance on the coverage. Thank you!

[zhassan-aws]

It seems like I don't have permission to assign the PR to this issue.

If you type in the PR description "Towards #53" the PR will be linked to this issue.

[zhassan-aws]

@zhassan-aws would appreciate any guidance on the coverage. Thank you!

You also need to pass --coverage in addition to -Zsource-coverage.

[Jimmycreative]

Hi this is Jimmy from team 4. Currently I am working on the harness for sub function in the non null challenge. When I tried to run the harness for sub, I encountered something below: It looks like there is something wrong with kani. My kani version is 0.55.0. Rustc version: 1.83.0-nightly Cargo : 1.83.0-nightly. Any suggestion for this problem? Thanks in advance

The command I used

kani verify-std -Z unstable-options "/Desktop/verify-rust-std/library" -Z function-contracts -Z mem-predicates --harness ptr::non_null::verify::check_sub

warning: build failed, waiting for other jobs to finish...
error: Failed to compile `core` due to an internal compiler error.: error: internal compiler error: Kani unexpectedly panicked at panicked at kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs:46:14:
                                called `Option::unwrap()` on a `None` value.

[zhassan-aws]

Hi @Jimmycreative. I believe this is the same crash in model-checking/kani#3467. Can you post the harness/contract to confirm?

@carolynzech did you find a workaround for this crash?

[carolynzech]

@carolynzech did you find a workaround for this crash?

Depends on what's causing the crash -- @Jimmycreative I would make sure that your harness is actually invoking sub. If it is, can you post a link to your fork so we can take a look?

[QinyuanWu]

@carolynzech After investigating we found that not invoking the target function was the issue. Thank you!

[Dhvani-Kapadia]

Hi @carolynzech and @feliperodri. I am Dhvani Kapadia from AWS Team 4, working on this challenge. Could you please assign me to the issue as well?

[Jimmycreative]

Clarifying Questions Regarding the sub Function and Pointer Arithmetic

@carolynzech @zhassan-aws
I'm currently working on the sub function in the proof and got stuck. I have a few clarifying questions that I believe will help me move forward and contribute more effectively to the project. Thanks in advance:

Context:
From my understanding, for sub to work correctly, self needs to point to an address within a contiguous memory space—such as an array, vector, or other block of memory—since performing the sub operation on a pointer that points to a single int (or any other non-contiguous object) could lead to undefined behavior. This is because subtracting from a pointer in such a case might make the pointer point to an unknown memory address, potentially outside the bounds of valid memory.

//contract
#[kani::requires(!self.as_ptr().is_null())]
#[kani::requires(count <= isize::MAX as usize)] // Ensure count fits within isize range
#[kani::requires(count.checked_mul(core::mem::size_of::<T>()).is_some())] // Prevent offset overflow
#[kani::ensures(|result: &NonNull<T>| result.as_ptr() == self.as_ptr().offset(-(count as isize)))]
pub const unsafe fn sub(self, count: usize) -> Self
where
    T: Sized,
{
    if T::IS_ZST {
        // Pointer arithmetic does nothing when the pointee is a ZST.
        self
    } else {
        // SAFETY: the caller must uphold the safety contract for `offset`.
        // Because the pointee is *not* a ZST, that means that `count` is
        // at most `isize::MAX`, and thus the negation cannot overflow.
        unsafe { self.offset((count as isize).unchecked_neg()) }
    }
}

//proof
#[kani::proof_for_contract(NonNull::sub)]
fn check_sub() {
 
    let size: usize = kani::any();  // Non-deterministic size for the vector

    // Create a vector of non-deterministic values
    let mut v = Vec::new();
    for _ in 0..size {
        v.push(kani::any()); // Pushing non-deterministic values into the vector
    }

    // Get a raw pointer to the vector
    let raw_ptr: *mut i32 = v.as_ptr() as *mut i32;

    // Wrap the raw pointer in a NonNull pointer
    let ptr = unsafe { NonNull::new(raw_ptr).unwrap() };

    // Create a non-deterministic count value for the number of elements to subtract
    let count: usize = kani::any();

    unsafe {
        let result = ptr.sub(count);
    }
}

Questions:

1. Can we assume that in the proof, we don't need to create objects that do not have contiguous memory spaces (such as a single int, char, etc.)? In other words, should the proof only be concerned with scenarios where self points to contiguous memory blocks (like arrays or vectors)?
2. Regarding the input creation in the proof, do we need to generate arrays (or other contiguous memory blocks) for all possible types (such as i32, i64, etc.) that could exist in contiguous memory (The code above only consider Vec i32)? Additionally, does the proof need to explore all possible addresses that self could point to within those arrays or vectors, or can we focus on specific cases such as the address of the first element in the vec shown in above code?
3. After I ran the proof shown above, it failed on 1 case below: Not really sure how to fix this:
   1 of 1804 failed (1 unreachable)
   Failed Checks: offset: attempt to compute number in bytes which would overflow
   File: "core/src/ptr/non_null.rs", line 487, in ptr::non_null::NonNull::::offset

Would really appreciate any guidance and suggestion. Thanks again!

[zhassan-aws]

Hi @Jimmycreative.

self needs to point to an address within a contiguous memory space—such as an array, vector, or other block of memory

That's correct.

Can we assume that in the proof, we don't need to create objects that do not have contiguous memory spaces (such as a single int, char, etc.)?

If the harness creates a block of memory with an arbitrary size, then it would subsume the case of a single int, char, etc. since these have a block of memory of size 1. So, the short answer is yes.

Regarding the input creation in the proof, do we need to generate arrays (or other contiguous memory blocks) for all possible types (such as i32, i64, etc.) that could exist in contiguous memory (The code above only consider Vec i32)?

Since we can't prove things for all possible types with Kani, it would be good to have a sample number of types. A good list of types is mentioned in Challenge 3: https://model-checking.github.io/verify-rust-std/challenges/0003-pointer-arithmentic.html#assumptions.

Additionally, does the proof need to explore all possible addresses that self could point to within those arrays or vectors, or can we focus on specific cases such as the address of the first element in the vec shown in above code?

It should. Note that a subtraction would not be possible for the first element in the vector since the subtraction operation would take the pointer out of the block of allocated memory.

After I ran the proof shown above, it failed on 1 case below

I would guess that this is due to violating this requirement for offset:

    /// * The computed offset, `count * size_of::<T>()` bytes, must not overflow `isize`.

i.e. even though the multiplication did not overflow for a usize (which is specified as a requires clause), it exceeds isize::MAX.

[Jimmycreative]

@zhassan-aws Thanks for your reply! It's really helpful!

The proof works now only handle the array with a fixed size and uses the last element for subtraction. The element is i32 type. Is this ok for the current stage? Or maybe we need to consider more scenarios you mentioned above? Any suggestion? Thanks in advance.

#[kani::requires(!self.as_ptr().is_null())]
#[kani::requires(count <= isize::MAX as usize)] // Ensure count fits within isize range
#[kani::requires(count.checked_mul(core::mem::size_of::<T>()).is_some())] // Prevent offset overflow
#[kani::requires(count * core::mem::size_of::<T>() <= isize::MAX as usize)]
#[kani::ensures(|result: &NonNull<T>| result.as_ptr() == self.as_ptr().offset(-(count as isize)))]
pub const unsafe fn sub(self, count: usize) -> Self
where
    T: Sized,
{
    if T::IS_ZST {
        // Pointer arithmetic does nothing when the pointee is a ZST.
        self
    } else {
        // SAFETY: the caller must uphold the safety contract for `offset`.
        // Because the pointee is *not* a ZST, that means that `count` is
        // at most `isize::MAX`, and thus the negation cannot overflow.
        unsafe { self.offset((count as isize).unchecked_neg()) }
    }
}

#[kani::proof_for_contract(NonNull::sub)]
pub fn non_null_check_sub() {
    const SIZE: usize = 10;
    kani::assume(SIZE > 0);
    
    let arr: [i32; SIZE] = kani::any();  // Create a non-deterministic array of size SIZE
    let raw_ptr: *mut i32 = arr.as_ptr() as *mut i32;  // Get a raw pointer to the array
    
    // Point to the last element of the array
    let last_ptr = unsafe { NonNull::new(raw_ptr.add(SIZE - 1)).unwrap() };  // Pointer to the last element
    
    let count: usize = kani::any();  // Create a non-deterministic count value

    // Ensure that the subtraction does not go out of the bounds of the array
    kani::assume(count < SIZE);  // Ensure count is less than SIZE to stay within bounds

    unsafe {
        // Perform the pointer subtraction from the last element
        let result = last_ptr.sub(count);
    }
}

[danielhumanmod]

Hi AWS Team,

I have a question regarding how to write function contracts using size_of. I’ve encountered difficulties when using size_of within the requires, which leads to compilation errors if the object in question does not meet the Sized constraint in Rust. As an alternative, I am currently specifying these preconditions in the proof harness using Kani::assume, but I’m wondering if there’s a better approach for handling this.

Current Code:

// Function Contracts
#[must_use]
    #[inline(always)]
    #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
    #[rustc_allow_const_fn_unstable(set_ptr_value)]
    #[stable(feature = "non_null_convenience", since = "1.80.0")]
    #[rustc_const_stable(feature = "non_null_convenience", since = "1.80.0")]
    #[ensures(
        |result: &NonNull<T>|
        (result.as_ptr() as *const () as usize) == ((self.as_ptr() as *const () as usize) + count)
    )]
    pub const unsafe fn byte_add(self, count: usize) -> Self {
        // SAFETY: the caller must uphold the safety contract for `add` and `byte_add` has the same
        // safety contract.
        // Additionally safety contract of `add` guarantees that the resulting pointer is pointing
        // to an allocation, there can't be an allocation at null, thus it's safe to construct
        // `NonNull`.
        unsafe { NonNull { pointer: self.pointer.byte_add(count) } }
    }

// proof harness
#[kani::proof_for_contract(NonNull::byte_add)]
    pub fn non_null_byte_add_proof() {
        let arr: [i32; 8] = kani::any();
        let raw_ptr: *mut i32 = arr.as_ptr() as *mut i32;
        let ptr = unsafe { NonNull::new(raw_ptr).unwrap() };
        let count: usize = kani::any();
        kani::assume(!ptr.as_ptr().is_null());
        kani::assume(count >= 0 && count <= (isize::MAX as usize) / mem::size_of::<i32>());
        unsafe {
            kani::assume(count <= mem::size_of_val(&*ptr.as_ptr()) / mem::size_of::<i32>());
        }
        unsafe {
            let result = ptr.byte_add(count);
        }
    }

What I want to achieve is make this line works in requires:

// Current in proof harness
 kani::assume(count <= mem::size_of_val(&*ptr.as_ptr()) / mem::size_of::<i32>());

// Ideally in function contracts
#[requires(count <= mem::size_of_val(&*ptr.as_ptr()) / mem::size_of::<T>());

[danielhumanmod]

BTW can you assign this challenge issue to @danielhumanmod @Jimmycreative as well, thanks!

[QinyuanWu]

@zhassan-aws Is let arr: [i32; 8] = kani::any(); the valid way to create a length 8 array with random i32 values as array elements? In our meeting last time kani::any_array was mentioned. Would you please give us an example of how to initialize it and is it any different than the first approach? Thank you!

[QinyuanWu]

@carolynzech Would you please point us to the align_offset example that uses kani::any_where to slice the array? We could not find it in the repo. We are trying:

let arr: [i32; 8] = kani::any();
let end = kani::any_where(|x| *x <= 8);
let slice = arr[..end];

But encountered the following error:

Kani Rust Verifier 0.55.0 (standalone)
error[E0277]: the size for values of type `[i32]` cannot be known at compilation time
    --> /Users/danieltu/Developer/verify-rust-std/library/core/src/ptr/non_null.rs:1804:13
     |
1804 |         let slice = arr[..end];
     |             ^^^^^ doesn't have a size known at compile-time
     |
     = help: the trait `marker::Sized` is not implemented for `[i32]`
help: this trait has no implementations, consider adding one
    --> /Users/danieltu/Developer/verify-rust-std/library/core/src/marker.rs:146:1
     |
146  | pub trait Sized {
     | ^^^^^^^^^^^^^^^
     = note: all local variables must have a statically known size
     = help: unsized locals are gated as an unstable feature
help: consider borrowing here
     |
1804 |         let slice = &arr[..end];
     |                     +

error: aborting due to 1 previous error

For more information about this error, try `rustc --explain E0277`.
error: Failed to execute cargo (exit status: 101). Found 2 compilation errors.

[zhassan-aws]

Add an ampersand before arr:

let slice = &arr[..end];

[zhassan-aws]

@zhassan-aws Is let arr: [i32; 8] = kani::any(); the valid way to create a length 8 array with random i32 values as array elements? In our meeting last time kani::any_array was mentioned. Would you please give us an example of how to initialize it and is it any different than the first approach? Thank you!

They're both the same: for let arr: [i32; 8] = kani::any();, kani::any() calls kani::any_array() under the hood.

[Dhvani-Kapadia]

@zhassan-aws and @carolynzech, could you please provide examples of using a mapping function in a harness? I'm writing a harness for the map_addr function, which takes a function f as an argument. I'm having trouble implementing this correctly in the harness

[zhassan-aws]

Here's one example:

let x: i32 = kani::any();
let ptr1 = &x as *const i32;
let ptr2 = ptr1.map_addr(|addr| addr + 4);

Is that what you're looking for?

[Dhvani-Kapadia]

Thanks, the issue got resolved