Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Feature Request: Support for Unsized Types in kani::mem::same_allocation API #3663

Open
xsxszab opened this issue Oct 30, 2024 · 0 comments
Open
Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature.

Comments

@xsxszab
Copy link

xsxszab commented Oct 30, 2024

Description
The same_allocation API currently does not accept pointers to unsized types, such as dyn Trait. This feature is essential for implementing function contracts for certain pointer arithmetic operations within Rust's standard library. For example:

// library/core/src/ptr/mut_ptr.rs
impl<T: ?Sized> *mut T {
    pub const unsafe fn byte_add(self, count: usize) -> Self {
        unsafe { self.cast::<u8>().add(count).with_metadata_of(self) }
    }
}

In this case, same_allocation could be used in an ensures clause to restrict that both the input and output pointers reference the same object, like so:

#[ensures(|result| kani::mem::same_allocation(self as *const T, *result as *const T))]

However, this code currently fails to compile because T may be unsized. Extending same_allocation to handle unsized types would greatly benefit cases where function contracts contain unsized pointers.

@xsxszab xsxszab added the [C] Feature / Enhancement A new feature request or enhancement to an existing feature. label Oct 30, 2024
@xsxszab xsxszab changed the title **Feature Request**: Support for Unsized Types in kani::mem::same_allocation API Feature Request: Support for Unsized Types in kani::mem::same_allocation API Oct 30, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature.
Projects
None yet
Development

No branches or pull requests

1 participant