Miri complains about undefined behavior when using index_mut instead of square brackets to access disjoined array elements

[jplatte]

This code:

use std::ops::IndexMut as _;

fn main() {
    let mut array = [0, 1];
    {
        let a = unsafe { &mut *((&mut array[0]) as *mut i32) };
        let b = unsafe { &mut *((&mut array[1]) as *mut i32) };
        std::mem::swap(a, b);
    }

    {
        let a = unsafe { &mut *(array.index_mut(0) as *mut i32) };
        let b = unsafe { &mut *(array.index_mut(1) as *mut i32) };
        std::mem::swap(a, b);
    }
}

has Miri report an invalid retag at the second std::mem::swap even though the first and second code block look like they should be equivalent at least semantically. Error message:

error: Undefined Behavior: trying to retag from <2686> for SharedReadWrite permission at alloc1403[0x0], but that tag does not exist in the borrow stack for this location
  --> src/main.rs:14:24
   |
14 |         std::mem::swap(a, b);
   |                        ^
   |                        |
   |                        trying to retag from <2686> for SharedReadWrite permission at alloc1403[0x0], but that tag does not exist in the borrow stack for this location
   |                        this error occurs as part of two-phase retag at alloc1403[0x0..0x4]
   |
   = 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: <2686> was created by a Unique retag at offsets [0x0..0x4]
  --> src/main.rs:12:26
   |
12 |         let a = unsafe { &mut *(array.index_mut(0) as *mut i32) };
   |                          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
help: <2686> was later invalidated at offsets [0x0..0x8] by a Unique function-entry retag inside this call
  --> src/main.rs:13:33
   |
13 |         let b = unsafe { &mut *(array.index_mut(1) as *mut i32) };
   |                                 ^^^^^^^^^^^^^^^^^^
   = note: BACKTRACE (of the first span):
   = note: inside `main` at src/main.rs:14:24: 14:25

Is this a Miri bug, or somehow intentional?

[RalfJung]

This is a known weakness of Stacked Borrows, but is intentional: index_mut receives &mut self, which claims exclusive access to the entire array. The issue is tracked at rust-lang/unsafe-code-guidelines#133. The intended way to write such code in Stacked Borrows is to convert to a raw pointer once and then obtain both a and b from that raw pointer.

Tree Borrows handles such situations better than Stacked Borrows. Can you check whether -Zmiri-tree-borrows makes the code work?

(For the time being it is preferable to make your code work with both Stacked Borrows and Tree Borrows; we are considering both of these models to evaluate their trade-off: Tree Borrows sacrifices some optimizations to make this code legal.)

[jplatte]

But nominally, square bracket array access desugars to index_mut, no? That's what confuses me the most about this.

-Zmiri-tree-borrows does make things work, and that's how I'll be checking my code for the time being.

[bjorn3]

At the MIR level for arrays and slices [] with usize indexes doesn't desugar to .index_mut(). Just like + on integers and floats doesn't desugar to .add().

[RalfJung]

Yeah, primitive indexing is special. Tree Borrows doesn't fundamentally fix that specialness, it just makes the index_mut call with its &mut self much less likely to cause trouble.

Closing as an instance of rust-lang/unsafe-code-guidelines#133.

[jplatte]

Right, I had heard about that and was wondering if it was related. So the first inner block in main in the issue description works by accident? Or is primitive indexing being special in this way a feature?

[RalfJung]

As far as I am concerned it is not a feature but just a fact we have to learn to live with. E.g. * on references and raw pointers is also very different from a deref/deref_mut call. I don't think fixing that is realistic.