Skip to content

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.

@feliperodri feliperodri enabled auto-merge (squash) July 30, 2024 03:29
@feliperodri feliperodri merged commit 1e0b71d into model-checking:main Jul 30, 2024
@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