Stacked Borrows: using the topmost "untagged" item is not "monotonic"

[RalfJung]

In Stacked Borrows, pointers can be "untagged", and when such a pointer is used, the access is controlled by a corresponding untagged item in the borrow stack. This is the only case where there is ambiguity for which item to use: when a pointer is tagged, there is a guarantee that we will find at most one item with that tag in the borrow stack; but there can be multiple untagged items.

Currently, being "untagged" is what happens to raw pointers, and when a raw pointer is created from a reference, a corresponding untagged item is pushed onto the borrow stack. So multiple untagged items can exist when a pointer is switched back and forth between a reference and a raw pointer multiple times:

let x1 = &mut 0;
let x2 = x1 as *mut _; // pushes an untagged item
let x3 = &mut *x2; // pushes a tagged item on top of the untagged item
let x4 = x3 as *mut _; // pushes another untagged item onto the top

When an untagged pointer is used, Stacked Borrows says to simply look for the topmost untagged item that matches the access, and use that. (So when doing a write access, untagged read-only items are ignored.) I made up this rule assuming that this would be most permissive, i.e., I assumed making any other choice (like sometimes using an item further down the stack) would only disallow more programs. However, as @ocecaco noticed (I hope this is the right GitHub handle^^), my assumption was wrong. Here is their example where adding a SharedRW(⊥) (where ⊥ represents "untagged") on top of the stack introduces UB:

fn not_so_innocent(x: &mut UnsafeCell<u32>) {
    let x_raw: *mut UnsafeCell<u32> = x as *mut UnsafeCell<u32>;
}

unsafe fn example<'a>(c: &'a mut UnsafeCell<u32>) {
    let x_unique1: &'a mut UnsafeCell<u32> = &mut *c;
    // [..., Unique(1)]
    
    let x_raw1: *mut UnsafeCell<u32> = x_unique1 as *mut UnsafeCell<u32>;
    // [..., Unique(1), SharedRW(⊥)]
    
    let x_unique2: &'a mut UnsafeCell<u32> = &mut *x_raw1;
    // [.., Unique(1), SharedRW(⊥), Unique(2)]
    
    not_so_innocent(x_unique2);
    // [.., Unique(1), SharedRW(⊥), Unique(2), ..., SharedRW(⊥)]

    // There will be an additional SharedRW(_) on top of Unique(2) at this
    // point, if `not_so_innocent` is called.

    // Create a tagged SharedRW from untagged SharedRW, which will either end
    // up below or above Unique(2), depending on whether `not_so_innocent` was
    // called.
    // (This is where we need `UnsafeCell` to even get a tagged SharedRW;
    // alternatively we could use a version of Stacked Borrows that has tagged
    // raw pointers.)
    let x_sharedrw: &'a UnsafeCell<u32> = &*x_raw1;
    
    // Now write to the topmost Unique. If SharedRW(⊥) was added, this will
    // invalidate `x_sharedrw`!
    {
        *x_unique2 = UnsafeCell::new(10);
    }
    
    // Now try to write to the tagged SharedRW
    {
        *x_sharedrw.get() = 12;
    }
}

fn main() {
    unsafe { 
        example(&mut UnsafeCell::new(42u32));
    }
}

The issue is that using the topmost untagged item means that if we use this item as the basis for a reborrow, there are a lot of items below the new item, and using any one of those will invalidate our new item. Placing the new item further down would mean it could remain on the stack longer.

There are other examples of this, but the one above seems like the hardest to fix.

[RalfJung]

On Zulip the argument has been made that maybe fixing this issue (by enormously complicating the model or ruling out ptr2int2ptr roundtrips) is worse than just having somewhat unintuitive UB in certain corner cases.

[RalfJung]

Untagged pointers are gone, so this issue can be closed.