Challenge 3: Verifying Raw Pointer Arithmetic Operations

[feliperodri]

Tracking issue for Challenge 3: Verifying Raw Pointer Arithmetic Operations.

[unseenmars]

Here’s Kai from CMU III. We’re taking on this challenge and will keep you updated on our progress along the way.

[szlee118]

Problem 1: Defining Valid Input Space for Pointer Parameters (solved)

Challenge:

Our main challenge in writing function contracts is precisely defining the valid input space for pointer parameters. Specifically, we are struggling to express accurate kani::requires attributes for pointer parameters in the functions we need to verify.

For non-pointer inputs like u64, defining the valid input space is straightforward. For example, in the gcd(x, y) function, the valid input space can be represented by a precondition like #[kani::requires(x != 0 && y != 0)]. However, for pointer parameters, defining the valid input space is non-trivial. We need a way to exclude invalid pointers (such as dangling, misaligned, or out-of-bounds pointers) while covering all valid ones to ensure the function contract remains sound. The challenge lies in expressing these conditions using kani::requires attributes.

So far, we haven’t found a feasible solution or a Kani API that directly addresses this problem. Could you provide guidance on how we can define preconditions for pointer parameters in our function contracts?

Answer:

There’s an API called can_dereference that can be used for this purpose: can_dereference API
You can see an example of its usage in this test: valid_ptr.rs

Problem 2: Handling Undefined Behavior in Function Verification (solved)

Challenge:

We are also encountering an issue related to undefined behavior (UB) in the verification of pointer arithmetic functions, such as *const T::offset. If the function contains potential safety issues, such as valid inputs that trigger UB, Kani (as documented here: Kani undefined behavior documentation) cannot perform checks once UB occurs. This creates a dilemma: we need to verify whether the function may cause UB, but Kani’s checks become ineffective in the presence of UB. Could you advise on how we can approach this situation?

Answer:

Kani automatically checks for certain types of UB (e.g. a dereference operation is valid), and verification will fail if one of those types of UB were found in a function. For other properties, such as this one mentioned in the documentation of offset:

the entire memory range between self and the result must be in bounds of that allocated object.

One needs to express this property as a requires clause that the function is annotated with.

[xsxszab]

Problem 3: Determining the valid value range for *const T::offset(self, count: i32)'s count parameter

To write a function contract for this function, we need to add a precondition that defines the valid input range for the count parameter. However, we cannot infer this information solely based on the input pointer. For example, consider the following pointers:

let nums = vec![0i32, 1, 2, 3];
let n = 42;
let ptr1: *const i32 = nums.as_ptr();
let ptr2: *const i32 = ptr1.wrapping_offset(1);
let ptr3: *const i32 = &n;

All of these pointers are of type *const i32—the only information we know when inside the offset function. However, when we call the .offset(count) method on them, the valid range of count differs for each pointer. Thus, it becomes unclear how to properly write the kani::requires attribute for the count parameter.

Is there a way to resolve this issue?

Problem 4: determing whether two raw pointers point to the same object during runtime

To implement function contracts for *const T::offset_from(self, origin: *const T), we need to guarantee that both self and origin point to the same allocated object. Is there any way to access and compare the provenance information of these raw pointers to guarantee that they belong to the same object?

[stogaru]

@feliperodri , the other two people working on this issue are @stogaru and @MayureshJoshi25.

[MayureshJoshi25]

Mayuresh here! Would be working on this challenge and would report any problems/doubts on the way.

[xsxszab]

Problem 5: Calling Pointer Arithmetic Methods on dyn Trait Pointers

Calling pointer arithmetic methods, such as add or sub, requires the pointee type to be sized. However, dyn Trait objects are inherently unsized, resulting in a compile-time error when attempting to call these methods on a pointer to a dyn Trait. For example:

struct ConcreteType {
    size: i32,   
}

trait AbstractTrait {}

impl AbstractTrait for ConcreteType {} 

fn get_box(size: i32) -> Box<dyn AbstractTrait> {
    Box::new(ConcreteType { size })
}

fn test() {
    let rand_box = get_box(42);
    let ptr = Box::into_raw(rand_box);
    unsafe { let ptr1 = ptr.offset(0); } // error
}

In our challenge, we need to verify function contracts for at least one dyn Trait type, but we are blocked by this issue. Is there a workaround for handling this scenario?

[xsxszab]

Problem 6: Precondition #[requires(kani::mem::can_dereference(self))] Fails on function <*mut T>::byte_add

Issue:
When adding the precondition #[requires(kani::mem::can_dereference(self))] to the function byte_add (pub const unsafe fn byte_add(self, count: usize) -> Self), running Kani produces the following error:

error[E0277]: the trait bound `<T as ptr::metadata::Pointee>::Metadata: kani::mem::PtrProperties<T>` is not satisfied
   --> /Users/xsxsz/vscode-projects/verify-rust-std/library/core/src/ptr/mut_ptr.rs:440:43
    |
440 |     #[requires(kani::mem::can_dereference(self))]
    |                -------------------------- ^^^^ the trait `kani::mem::PtrProperties<T>` is not implemented for `<T as ptr::metadata::Pointee>::Metadata`
    |                |
    |                required by a bound introduced by this call
    |
note: required by a bound in `kani::mem::can_dereference`
   --> /Users/xsxsz/vscode-projects/verify-rust-std/library/core/src/lib.rs:426:1
    |
426 | kani_core::kani_lib!(core);
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^
    | |
    | required by a bound in this function
    | required by this bound in `can_dereference`
    = note: this error originates in the macro `kani_core::kani_mem` which comes from the expansion of the macro `kani_core::kani_lib` (in Nightly builds, run with -Z macro-backtrace for more info)
help: consider further restricting the associated type
    |
444 |     pub const unsafe fn byte_offset(self, count: isize) -> Self where <T as ptr::metadata::Pointee>::Metadata: kani::mem::PtrProperties<T> {
    |                                                                 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

error: aborting due to 1 previous error

Context:
This precondition works for other non-byte pointer methods including add, sub, offset, and offset_from. However, it consistently fails with the same error on all byte-prefixed functions, including byte_add, byte_sub, byte_offset, and byte_offset_from. Additionally, this behavior is consistent on both const and mutpointer methods.

We are currently using a custom-built version of Kani from the features/verify-rust-std branch, not the stable release. This branch is necessary for us as it enables verification on primitive types.

Question:
Is this issue a bug of the branch we are using, or is it a feature that has yet to be implemented in Kani? We're uncertain if this behavior is a bug or an expected result.

[xsxszab]

Hi @feliperodri, after contacting with Team 4, we have a few updates on the issues we've been discussing in today's (Oct. 11) meeting:

• For Problem 3 and 4, We’ve confirmed that Zyad, Team 4’s POC, is already working on new Kani APIs to address these issues.
• Regarding the new problem mentioned in today’s meeting: We initially discovered this problem during our joint meeting with Team 4 on Oct. 9, and they have received clarification during their sponsor meeting, so we don't need to post a new Problem here. Specifically, a pointer that points one byte past the end of its allocated object is still valid, but cannot be dereferenced. For example, vec.as_ptr().add(vec.len()) is a valid pointer, but dereferencing it would result in undefined behavior.