Proposal for new Kani API similar to CPROVER_r_ok and CPROVER_w_ok

[QinyuanWu]

Requested feature: Kani API to verify whether a segment in memory is valid for read or write, similar to CPROVER_r_ok and CPROVER_w_ok
Use case: Writing function contracts that meet the safety requirement where the pointer must be valid for reads or writes of a certain number of bytes. std::ptr::copy is an example.

Link to relevant documentation (Rust reference, Nomicon, RFC):
CPROVER memory primitives
The current workaround is to cast the pointer to the size of the number of bytes that need to be checked and use ub_checks::can_dereference on the pointer. However, a specific API like CPROVER_r_ok and CPROVER_w_ok would be more accurate. Thank you!
@Dhvani-Kapadia @zhassan-aws @celinval

[celinval]

Hi @QinyuanWu, just so I make sure I understand the request. Would you like an option that you can provide the size to be read or a function that only checks allocation status (or both)?

The can_dereference and can_write provide extra checks that CPROVER_r_ok doesn't provide, such as value validity, pointer alignment and memory initialization (if the feature is enabled). We're likely going to extend those APIs later to provide things such as aliasing checks.

[QinyuanWu]

@celinval We'd like an option to pass a specific size as the parameter to indicate the number of bytes we'd like to check just like the CBMC version:

• _Bool __CPROVER_r_ok(const void *p, size_t size)
• _Bool __CPROVER_w_ok(const void *p, size_t size)

For allocation status checks I would prefer separate APIs so that it's clear from the language of the contract regarding what properties are checked.

[celinval]

Hi @QinyuanWu, we can definitely add a new API that accepts different number of elements and potentially number of bytes.

I'm not so sure about the fine grained APIs, since these APIs are all fairly unstable, and some checks are still missing, I would prefer not exposing them. I also worry about making contracts very verbose and more error prone. For example, we have a lot of contracts that use can_dereference. If we were to use more fine-grained APIs, all these contracts would basically become the body of can_dereference:

kani/library/kani_core/src/mem.rs

Lines 122 to 134 in 9b2bbd3

	pub fn can_dereference<T>(ptr: *const T) -> bool
	where
	T: ?Sized,
	<T as Pointee>::Metadata: PtrProperties<T>,
	{
	let (thin_ptr, metadata) = ptr.to_raw_parts();
	// Need to assert `is_initialized` because non-determinism is used under the hood, so it
	// does not make sense to use it inside assumption context.
	metadata.is_ptr_aligned(thin_ptr, Internal)
	&& is_inbounds(&metadata, thin_ptr)
	&& assert_is_initialized(ptr)
	&& unsafe { has_valid_value(ptr) }
	}

And this is still incomplete since we are not handling alias yet.

BTW, you can take a look at #1496 for more background on why we don't directly expose CBMC's APIs.

[QinyuanWu]

@celinval Thank you and I agree with your point. Look forward to the new read_ok and write_ok API!