Compilation Error When Stubbing Functions That Return Pointers Using Function Contracts

[xsxszab]

Problem Description
When attempting to stub a function with a verified function contract using kani::stub_verified, a compilation error occurs if the function's return value is a pointer.

Example
The following code is executed using kani 0.56.0 and command kani -Zfunction-contracts <filename>

// This function contract performs no meaningful checks.
// Its sole purpose is to enable stubbing of the `get_same_ptr` function.
#[kani::requires(true)]
#[kani::ensures(|result| true)]
fn get_same_ptr(ptr: *const u8) -> *const u8 {
    ptr
}

fn test_func() {
    let s: &str = "123";
    let ptr: *const u8 = s.as_ptr();    
    get_same_ptr(ptr);
}

#[kani::proof]
#[kani::stub_verified(get_same_ptr)]
fn check_test_func() {
    test_func();    
}

Running this code generates the following error:

error: `*const u8` doesn't implement `kani::Arbitrary`.
  --> /Users/xsxsz/github_repos/kani/library/kani/src/lib.rs:52:1
   |
52 | kani_core::kani_lib!(kani);
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^
   |
   = help: All objects in the modifies clause must implement the Arbitrary. The return type must also implement the Arbitrary trait if you are checking recursion or using verified stub.
   = note: this error originates in the macro `kani_core::kani_intrinsics` which comes from the expansion of the macro `kani_core::kani_lib` (in Nightly builds, run with -Z macro-backtrace for more info)

error: aborting due to 1 previous error

Possible Cause of the Issue
According to Kani's blog post, the issue can be explained as follows: When stubbing a function with its contracts, Kani performs these steps:

1. Convert preconditions into an assert!() clause.
2. Define a kani::any() variable to represent the output.
3. Constrain the output range using kani::assume() based on the postconditions.

In this case, the Arbitrary trait (required by kani::any) is not implemented for pointers, this makes sense as generating a random pointer without memory allocation context is pointless. As a result, Step 2 causes compilation errors. Is there any workaround for stubbing function with pointer return values?

[xsxszab]

@feliperodri Hi Felipe, this is the issue we discussed in today's meeting. It's currently blocking our efforts to verify functions using function contracts for pointer arithmetic operations.