ReferencePropagation introduces UB into code that is accepted by Stacked Borrows

[RalfJung]

This program is accepted by Stacked Borrows:

fn main() {
    struct Foo(u64);
    impl Foo {
        fn add(&mut self, n: u64) -> u64 {
            self.0 + n
        }
    }

    let mut f = Foo(0);
    let alias = &mut f.0 as *mut u64;
    let res = f.add(unsafe {
        *alias = 42;
        0
    });
    assert_eq!(res, 42);
}

That is a Stacked Borrows limitation; it is caused by the fact that 2-phase borrows cannot be modeled properly with just a Stack.
However, it also shows that defining an aliasing model that rejects this code is non-trivial, and we should be very careful with optimizations on such code until we have a clear plan for how to model this.

And yet, it turns out that running this code with mir-opt-level=2 introduces UB:

error: Undefined Behavior: trying to retag from <1484> for Unique permission at alloc702[0x0], but that tag does not exist in the borrow stack for this location
  --> 2phase.rs:4:16
   |
4  |         fn add(&mut self, n: u64) -> u64 {
   |                ^^^^^^^^^
   |                |
   |                trying to retag from <1484> for Unique permission at alloc702[0x0], but that tag does not exist in the borrow stack for this location
   |                this error occurs as part of function-entry retag at alloc702[0x0..0x8]
   |
   = help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
   = help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
help: <1484> was created by a SharedReadWrite retag at offsets [0x0..0x8]
  --> 2phase.rs:11:15
   |
11 |     let res = f.add(unsafe {
   |               ^
help: <1484> was later invalidated at offsets [0x0..0x8] by a write access
  --> 2phase.rs:14:9
   |
14 |         *alias = 42;
   |         ^^^^^^^^^^^
   = note: BACKTRACE (of the first span):
   = note: inside `main::Foo::add` at 2phase.rs:4:16: 4:25
note: inside `main`
  --> 2phase.rs:11:15
   |
11 |       let res = f.add(unsafe {
   |  _______________^
12 | |         // This is the access at fault, but it's not immediately apparent because
13 | |         // the reference that got invalidated is not under a Protector.
14 | |         *alias = 42;
15 | |         0
16 | |     });
   | |______^

This is quite surprising, I thought we were very conservative in terms of doing optimizations that rely on the aliasing model. I have not yet figured out where exactly this comes from.
Cc @rust-lang/opsem @rust-lang/wg-mir-opt @cjgillot

[saethlin]

ReferencePropagation is the pass that's causing this.

RUSTFLAGS=-Zmir-enable-passes=+ReferencePropagation cargo +nightly miri run

will cause this to report UB.

[RalfJung]

The only diff from that pass is

@@ -48,16 +48,12 @@
     bb0: {
         StorageLive(_1);
         _1 = main::Foo(const 0_u64);
-        StorageLive(_2);
-        StorageLive(_3);
         _3 = &mut (_1.0: u64);
-        _2 = &raw mut (*_3);
-        StorageDead(_3);
         StorageLive(_4);
         StorageLive(_5);
         _5 = &mut _1;
         StorageLive(_6);
-        (*_2) = const 42_u64;
+        (_1.0: u64) = const 42_u64;
         _6 = const 0_u64;
         _4 = main::Foo::add(move _5, move _6) -> [return: bb1, unwind continue];
     }

This replaces an access through *_2 with an access through _1.0, i.e. *alias = 42 becomes a direct assignment to variable f. This is UB since a two-phase borrow has been derived from f to be passed as an argument to add, and writing to f invalidates that 2-phase borrow.

[RalfJung]

The MIR pass contains this comment:

/// This pass aims to transform the following pattern:
///   _1 = &raw? mut? PLACE;
///   _3 = *_1;
///   _4 = &raw? mut? *_1;
///
/// Into
///   _1 = &raw? mut? PLACE;
///   _3 = PLACE;
///   _4 = &raw? mut? PLACE;
[...]
/// For `&mut` borrows, we also need to preserve the uniqueness property:
/// we must avoid creating a state where we interleave uses of `*_1` and `_2`.
/// To do it, we only perform full instantiation of mutable borrows:
/// we replace either all or none of the occurrences of `*_1`.

There's no _2 in the code so the comment is hard to interpret. I guess it refers to PLACE.

I am not entirely sure how that is sufficient. _1 is a (direct) child of PLACE. In Stacked Borrows terms, _1 might have permission SharedReadWrite; accesses to such places are more aliasing-permissive than accesses to Unique places. Replacing _1 by PLACE can replace an SRW access by a Unique access, which can introduce UB.

In Tree Borrows I think this reasoning is fine, since the permission of the reference being written to doesn't matter for the aliasing model, only the relative position -- and all other children of PLACE see a foreign access no matter whether it is done through PLACE or _2.

That means it should be possible to also produce a miscompile here with raw pointers instead of two-phase borrows...