Is there a same object check in Kani?

[QinyuanWu]

Is there a way for Kani to check whether two pointers are pointing to the same object, similar to __CPROVER_same_object? For example, in non_null::offset_from one of the desired requires clause is that the two pointers passed in should be pointing to the same object. Thanks!
@zhassan-aws @Jimmycreative

[zhassan-aws]

A same_allocation API was merged in model-checking/kani#3583. It should be available for usage in this repo soon.

[xsxszab]

@xsxszab Have you tried casting a pointer with valid memory allocation to unit using as *mut ()? For example, trait_object as *const dyn SampleTrait as *mut ()

I've tried it using the following code and it produced the same failed check:

#[kani::proof]
fn test_unit_type() {
  let unit_obj = ();
  let ptr1: *const () = &unit_obj;
  let ptr2: *const () = &unit_obj;
  assert!(kani::mem::same_allocation(ptr1, ptr2));
}

[zhassan-aws]

@xsxszab Please file an issue in the Kani repository.

[xsxszab]

@xsxszab Please file an issue in the Kani repository.

Sure, the tracking issue is here.

[celinval]

@xsxszab Have you tried casting a pointer with valid memory allocation to unit using as *mut ()? For example, trait_object as *const dyn SampleTrait as *mut ()

I've tried it using the following code and it produced the same failed check:

#[kani::proof]
fn test_unit_type() {
  let unit_obj = ();
  let ptr1: *const () = &unit_obj;
  let ptr2: *const () = &unit_obj;
  assert!(kani::mem::same_allocation(ptr1, ptr2));
}

The main problem with this example is that an zero sized type (ZST) object is not allocated. That's why you are getting this error. Your contract has to account to that, i.e.:, check if the type is not a ZST first.