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

Why does Miri mark &mut->&mut reborrows as a read access? #1878

Closed
ssbr opened this issue Aug 24, 2021 · 4 comments
Closed

Why does Miri mark &mut->&mut reborrows as a read access? #1878

ssbr opened this issue Aug 24, 2021 · 4 comments

Comments

@ssbr
Copy link

ssbr commented Aug 24, 2021

Here's a demo program I put up on the playground: https://play.rust-lang.org/?version=stable&mode=debug&edition=2018&gist=5c600b9de975a4c261f7442b77d4421e

fn reborrow(r1: &mut i32) -> &mut i32 {
    let p = r1 as *mut _;
    /* CODE SNIPPETS GO HERE */
    let r2 = unsafe { &mut *p };
    r2
}

If we perform a write access to r1, it will invalidate p, but if we perform a read access, it will not. For example:

// OK: does not remove the SharedRW for p,
println!("{}", *r1);
// Not OK: any of these are mutable accesses to r1.
// They will pop both raw pointers and mut references until we get back to the tag for `r1`.
// This means that `p` is no longer allowed to be read or written.
*r1 = 42;
let _ = {&mut *r1};
let _ = {r1};  // or: std::mem::drop(r1);

I think I'm with this so far.

However, this also passes Miri:

fn mutate(x: &mut i32) {*x = 42;}
mutate(r1);

It seems to treat reborrowing as a write operation, except when it's part of function call, in which case it's a read operation.

In which case, there's a trick to make all of the not-OK code turn acceptable according to Miri: launder the reference through a reborrow / function call, so that we get a retagged mut reference which we can do write operations onto:

fn launder(x: &mut i32) -> &mut i32 {x}
let r3 = launder(r1);
// now all these are OK:
*r3 = 42;
let _ = {&mut *r3};
let _ = {r3};  // or: std::mem::drop(r3);

It doesn't make sense to me that these operations would be banned unless retagged through a function call. Since it allows the same runtime behavior anyway, then they should have the same status as either both-UB or both-defined-behavior, right?


As for docs: my understanding from reading the paper and the UCG page is that when you reborrow a mut reference, this counts as a write access.

The paper states that retagging in function call is e.g. equivalent to let x = &mut *y;, and &mut *y follows the rules for new-mutable-ref. Emphasis mine:

Rule (new-mutable-ref). Any time a new mutable reference gets created (via &mut expr) from some existing pointer value Pointer(ℓ,t) (the referent), first of all this is considered a use of that pointer value (so we follow use-1 below). [...]

Rule (use-1). Any time a pointer value Pointer(ℓ,t) gets used, an item with tag t must be in the stack for ℓ. If there are other tags above it, pop them, so that the item with tag t is on top of the stack afterwards. If Unique(t) is not in the stack at all, this program has undefined behavior.

(use-2 is about pointers, so doesn't come into play.)

Similarly, the UCG page, emphasis mine:

We consider this operation as corresponding to a write access if new.perm.grants(AccessKind::Write), and to a read access otherwise. [...] Check if we are adding a SharedReadWrite. [...] If no, perform the actions of the corresponding access.

So my uninformed, uneducated reading is pointing me towards launder not being a valid trick, and all of these things being UB.

@RalfJung
Copy link
Member

Hm, yes that is a very interesting case; thanks for sharing! I will have to dig deeper to figure out why Miri accepts this.

@RalfJung
Copy link
Member

RalfJung commented Sep 29, 2021

I think I know what is going on... when you call a function that takes an &mut T, Rust will not create a regular mutable reference, it will create a two-phase borrow. Stacked Borrows does not have good support for two-phase borrows, so they are treated essentially like raw pointers. So your launder call is actually very different from the "Not OK" case, and much more like

    fn launder<T>(x: *mut T) -> &mut T {&mut *x}
    let r3 = launder(r1 as *mut _);
    *r3 = 42;
    let _ = {&mut *r3};
    let _ = {r3};

So basically what your code does is cast r1 to a raw pointer twice, and using one of those raw pointers does not invalidate the other -- that is the entire point of raw pointers, they do not make aliasing assumptions.

I hope future Rust aliasing models can properly account for two-phase borrows, but in Stacked Borrows I decided to give up on them so that I can at least get something finished that supports "regular" mutable and shared references.

So, this is an instance of rust-lang/unsafe-code-guidelines#85.

@ssbr
Copy link
Author

ssbr commented Sep 29, 2021

Ah. I think two-phase borrows aren't discussed in the paper, but your explanation makes sense. If I understand correctly, since all mut argument reborrows are two-phase borrows, this means that all mut argument reborrows are implicitly thrown through a mutable pointer first for purposes of aliasing semantics.

That said, it's surprising. launder really does look to me like "regular" use of mutable references, as it was valid before two-phase borrows existed.

What do you want to do with this bug? Close in favor of rust-lang/unsafe-code-guidelines#85 ?

@RalfJung
Copy link
Member

That said, it's surprising. launder really does look to me like "regular" use of mutable references, as it was valid before two-phase borrows existed.

I agree! I don't want this code to be accepted. But rejecting it without also rejecting safe code that does "funny" things with two-phase borrows is hard.

Yeah let's close this issue; there is no Miri bug but an issue in the underlying operational model. Thanks for reporting it, it is a very good test case for potential fixes to the two-phase borrow situation!

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

No branches or pull requests

2 participants