orlp / slotmap

Slotmap data structure for Rust
zlib License
1.08k stars 70 forks source link

`get_disjoint_mut` makes Miri unhappy #92

Open steffahn opened 1 year ago

steffahn commented 1 year ago

Running the doc test code, i.e.

fn main() {
    use slotmap::*;
    let mut sm = SlotMap::new();
    let ka = sm.insert("butter");
    let kb = sm.insert("apples");
    let kc = sm.insert("charlie");
    sm.remove(kc); // Make key c invalid.
    assert_eq!(sm.get_disjoint_mut([ka, kb, kc]), None); // Has invalid key.
    assert_eq!(sm.get_disjoint_mut([ka, ka]), None); // Not disjoint.
    let [a, b] = sm.get_disjoint_mut([ka, kb]).unwrap();
    std::mem::swap(a, b);
    assert_eq!(sm[ka], "apples");
    assert_eq!(sm[kb], "butter");
}

with

cargo miri run
error: Undefined Behavior: trying to retag from <6104> for Unique permission at alloc1887[0x18], but that tag does not exist in the borrow stack for this location
  --> src/main.rs:10:10
   |
10 |     let [a, b] = sm.get_disjoint_mut([ka, kb]).unwrap();
   |          ^
   |          |
   |          trying to retag from <6104> for Unique permission at alloc1887[0x18], but that tag does not exist in the borrow stack for this location
   |          this error occurs as part of retag at alloc1887[0x18..0x28]
   |
   = 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: <6104> was created by a SharedReadWrite retag at offsets [0x18..0x28]
  --> src/main.rs:10:18
   |
10 |     let [a, b] = sm.get_disjoint_mut([ka, kb]).unwrap();
   |                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
help: <6104> was later invalidated at offsets [0x0..0x60] by a Unique retag
  --> src/main.rs:10:18
   |
10 |     let [a, b] = sm.get_disjoint_mut([ka, kb]).unwrap();
   |                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   = note: BACKTRACE:
   = note: inside `main` at src/main.rs:10:10: 10:11

note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace

error: aborting due to previous error

I would assume that the use of slice::get_unchecked_mut to obtain multiple mutable references is problematic, though I haven’t fully tested that hypothesis yet. For comparison: There now also exists a slice::get_many_mut method on nightly, and that method deliberately uses the (also still unstable) pointer variant of get_unchecked_mut for slices; but no worries about this method being unstable, it essentially just performs a pointer addition anyways ^^

orlp commented 1 year ago

So this is something that's planned to be 'fixed' for the 2.0 slotmap rewrite, but you can rest easy for now. Miri uses a model called 'stacked borrows' which is not something the Rust compiler follows (and I personally hope it never does in the current form). The stacked borrows model is an incredibly strict and punishing memory model that invalidates pointers which still point at perfectly valid data for (in my opinion) no good reason.

I would like to doubly emphasize that what Miri calls 'undefined behavior' here is not something that's undefined behavior in the current rustc compiler. Slotmap does in fact check that the mutable references it creates are disjoint. It is strictly undefined behavior in an experimental model that Miri's author defined themselves.

CosmicHorrorDev commented 1 year ago

As an update this appears to pass under the other experimental Miri Tree Borrows model

$ MIRIFLAGS='-Zmiri-tree-borrows' cargo +nightly miri test

^^ doesn't report any issues