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

Function Contracts: Interior Mutability Tests #3351

Merged
merged 38 commits into from
Jul 30, 2024

Conversation

pi314mm
Copy link
Contributor

@pi314mm pi314mm commented Jul 17, 2024

Test cases for interior mutability using Cell, OnceCell, UnsafeCell, and RefCell.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

Matias Scharager added 2 commits July 17, 2024 17:35
@pi314mm pi314mm added this to the Function Contracts milestone Jul 17, 2024
@pi314mm pi314mm self-assigned this Jul 17, 2024
Copy link
Contributor

@feliperodri feliperodri left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We also need to update our RFC to describe any limitations around interior mutability.

@feliperodri
Copy link
Contributor

The transmute is safe here because Cell and UnsafeCell are guaranteed to have the same memory layout as their underlying type. https://doc.rust-lang.org/stable/std/cell/struct.UnsafeCell.html#memory-layout

This comment should be included in the test cases.

@pi314mm pi314mm marked this pull request as ready for review July 19, 2024 16:39
@pi314mm pi314mm requested a review from a team as a code owner July 19, 2024 16:39
Copy link
Contributor

@celinval celinval left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't think you need the transmute in any of these cases. You should be able to use the public methods to get the data address or a copy of the data.

We have two problems, and I think it might be helpful to think about them separately, although you might want to add a test that has both. The first problem is interior mutability, and the second one is encapsulation.

Using transmute is necessary if you want to break encapsulation. The interior mutability could be a problem for identifying expressions that are side-effect free.

rfc/src/rfcs/0009-function-contracts.md Outdated Show resolved Hide resolved
@feliperodri feliperodri enabled auto-merge (squash) July 30, 2024 03:29
@feliperodri feliperodri merged commit 1e0b71d into model-checking:main Jul 30, 2024
27 checks passed
@pi314mm pi314mm deleted the int-mut-tests branch July 30, 2024 04:59
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants