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

Stacked Borrows: redo retag-to-raw #106

Closed
RalfJung opened this issue Mar 26, 2019 · 3 comments
Closed

Stacked Borrows: redo retag-to-raw #106

RalfJung opened this issue Mar 26, 2019 · 3 comments
Labels
A-aliasing-model Topic: Related to the aliasing model (e.g. Stacked/Tree Borrows)

Comments

@RalfJung
Copy link
Member

RalfJung commented Mar 26, 2019

@matthewjasper realized that the current rules for retag-to-raw are not working well when the redundant reborrows around raw ptr casts are gone:

let mut x = 12;
let x = &mut x;

&*x; // Stack is frozen

let raw = &raw mut *x; // No longer creates a temporary `&mut i32`
unsafe { *raw = 42; } // Error because no Raw item got pushed

However, this will likely mean that &raw const x and &raw mut x are not the same operation, because the following code must not be UB:

let mut x = 12;
let x = &mut x;

let shr = &*x; // Stack is frozen

let raw = &raw const *x; // If this unfreezes...
let _val = *shr; // ... then this is UB

Also see this discussion on Zulip.

@RalfJung RalfJung added the A-aliasing-model Topic: Related to the aliasing model (e.g. Stacked/Tree Borrows) label Mar 26, 2019
@RalfJung
Copy link
Member Author

Also see this long post of mine on an old topic about coercing mutable references to *const T, which I only now realized is closely related.

@RalfJung
Copy link
Member Author

I also just realized that currently, x as *mut T where x: &mut T effectively counts as a write access, because of the implicit reborrow. Things would likely break if that were to change. And it actually makes some sense, we want to push a new tag after all and we should only do that after popping old stuff away.

@RalfJung
Copy link
Member Author

I think this is basically solved on the Stacked Borrows side, but we need to figure out what we really want (x: &mut T) as *const T to mean. That is tracked at rust-lang/rust#56604.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
A-aliasing-model Topic: Related to the aliasing model (e.g. Stacked/Tree Borrows)
Projects
None yet
Development

No branches or pull requests

1 participant