Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

get_disjoint_mut makes Miri unhappy #92

Open
steffahn opened this issue Dec 28, 2022 · 2 comments
Open

get_disjoint_mut makes Miri unhappy #92

steffahn opened this issue Dec 28, 2022 · 2 comments

Comments

@steffahn
Copy link

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
Copy link
Owner

orlp commented Dec 28, 2022

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
Copy link

CosmicHorrorDev commented Mar 28, 2023

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants