Inconsistency between stacked borrows and my mental model

[alice]

So I was reading the Stacked Borrows Implemented blog post, and realized that the following is not considered UB by stacked borrows:

fn main() {
    let x = &mut 1u8;

    // Create raw pointer
    let y = x as *mut u8;

    // Assert uniqueness of x
    *x = 7;

    // Create another raw pointer
    x as *mut u8;

    // Read x through y, which was created before we asserted uniqueness.
    let _val = unsafe { *y };
}

playground

I found it really surprising that reading through y is not considered UB here, because in my mental model, y would have been invalidated by asserting uniqueness with the write.

Note that if you remove the immediately-ignored raw pointer, miri will complain. I don't have any questions, I just found this surprising and wanted to share it.

[mbrubeck]

I asked about a vaguely similar case in this Zulip thread, where @RustyYato and @RalfJung replied:

Yato: Yes, all raw pointers have the same tag (which is untagged) right now, so making a new raw pointer to the same location revives old raw pointers incorrectly.

RalfJ: note however that to match what LLVM does with noalias , we need to eventually also track raw pointers better and then that kind of code would stop working

So I believe this is a known limitation of the current Stacked Borrows model which might be changed in future revisions.

[RalfJung]

@mbrubeck

So I believe this is a known limitation of the current Stacked Borrows model which might be changed in future revisions.

Exactly.