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

Contract implementation is unsafe and may trigger UB #3293

Open
celinval opened this issue Jun 25, 2024 · 1 comment
Open

Contract implementation is unsafe and may trigger UB #3293

celinval opened this issue Jun 25, 2024 · 1 comment
Labels
[C] Bug This is a bug. Something isn't working. Z-Contracts Issue related to code contracts

Comments

@celinval
Copy link
Contributor

Looking at the kani::internal::Pointer implementation for *mut T:

impl<'a, T> Pointer<'a> for *mut T {
type Inner = T;
unsafe fn decouple_lifetime(&self) -> &'a Self::Inner {
&**self as &'a T
}

This can trigger UB if the location pointed by *mut T does not contain a valid value of type T since it is converting it to a &T.
Converting *const T into &mut T and *mut T to &mut T is also unsafe, and may break aliasing rules.

@celinval celinval added the [C] Bug This is a bug. Something isn't working. label Jun 25, 2024
@feliperodri feliperodri added this to the Function Contracts milestone Jun 26, 2024
@celinval
Copy link
Contributor Author

Note that #3363 removes the decouple_lifetime function, but untracked_deref function is still unsafe and my cause UB for arguments that are dropped inside the function.

I was wondering if we can use something similar to Prusti's snapshots: https://viperproject.github.io/prusti-dev/dev-guide/encoding/types-snap.html to replace untracked_deref.

@tautschnig tautschnig added the Z-Contracts Issue related to code contracts label Aug 1, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
[C] Bug This is a bug. Something isn't working. Z-Contracts Issue related to code contracts
Projects
None yet
Development

No branches or pull requests

3 participants