Support `__CPROVER_r_ok`

[danielsn]

http://cprover.diffblue.com/memory-primitives.html

[giltho]

It would be interesting to analyse the actual use case for this.

If this is used for C FFI, it might be that the only time you actually want to check this property is when you cast your *const T into a &T, because that's when Rust requires the invariant to hold. What I mean is, given Rust, I'm not 100% sure this API should be exposed or implied by the chose types. Maybe Kani itself should be adding this check when the cast is operated?

[celinval]

It would be interesting to analyse the actual use case for this.

If this is used for C FFI, it might be that the only time you actually want to check this property is when you cast your *const T into a &T, because that's when Rust requires the invariant to hold. What I mean is, given Rust, I'm not 100% sure this API should be exposed or implied by the chose types. Maybe Kani itself should be adding this check when the cast is operated?

I do agree that Kani should automatically add those checks when there are casting / transmute involving raw pointers. I think adding this API is likely the first step.

Other obvious usages for me that I expect users to explicitly add them: C FFI, stubbing, and contracts.

Another not so obvious usage for me is debugging. Even though UB only happens when you try to access the memory, it may be very helpful to add extra checks to pinpoint when the invalid pointer was created.

[celinval]

Adding more details from duplicated issue (#2690):

Requested feature: Create a method to ensure a pointer is valid. Use case: Verifying unsafe operations Link to relevant documentation (Rust reference, Nomicon, RFC):

The method I was thinking would be something like:

pub fn is_ptr_valid<T: ?Sized>(ptr: *const T) -> bool {
    let sz = intrinsics::size_of_val(ptr);
    // Kani intrinsic that translates to __CPROVER_r_ok
    is_read_ok(ptr, sz)
}

[celinval]

I gave this API a thought, and I don't think we should directly map this to CBMC's __CPROVER_r_ok. This CBMC function is written in a way where it will always return true if the pointer is valid, but it will return a non_det value if the pointer is not valid.

According to CBMC's documentation, this function does not have a well-defined behavior when invoked with an non-null invalid pointer.

IMHO, this is not intuitive at all, and it can lead to a lot of confusion. Basically, this function is only reliable in two different contexts:

1. One to assert a pointer is always valid, i.e.:

assert(__CPROVER_r_ok(ptr));

2. And the second to assume that a pointer is never valid:

assume(!__CPROVER_r_ok(ptr));

Note that the second one is still considered UB per CBMC's manual.

[celinval]

See https://github.com/diffblue/cbmc/issues/8199 for more context on why I don't believe this is a good API for us to support. I will close this issue and reopen #2690 since it captures the desired behavior.