Handle wildcard pointers in SB

[carbotaniuman]

This uses an permissive Unknown implementation, where a wildcard pointer (and any SRW derived from a wildcard pointer) can access any previously-exposed SB tag. This is missing any meaningful test-cases, and all of the edge-cases have not yet been worked through.

I think there's also some bugs here with differing Unknowns in different ranges and having things behave really weirdly too, alongside some issues with retagging to SRO or Unique.

[RalfJung]

Thanks a lot for working on this. :)
However, I think the logic for this is not quite right yet; I left some comments.

[RalfJung]

This is missing any meaningful test-cases, and all of the edge-cases have not yet been worked through.

I think enabling stacked borrows for the existing permissive provenance tests (as you did), and the existing stacked-borrows/int-to-ptr.rs is a good baseline. The test you added that is based on rust-lang/unsafe-code-guidelines#273 is great; I think it is extremely meaningful -- but we don't need UnsafeCell any more and your version also added an extra write that I think makes it the wrong test; here's what we should do instead I think:

#![feature(strict_provenance)]
use std::ptr;

/// Ensure that we do not just pick the topmost possible item on int2ptr casts.
fn example(variant: bool) { unsafe {
    fn not_so_innocent(x: &mut u32) -> usize {
        let x_raw4 = x as *mut u32;
        x_raw4.expose_addr()
    }

    let mut c = 42u32;

    let x_unique1 = &mut c;
    // [..., Unique(1)]
    
    let x_raw2 = x_unique1 as *mut u32;
    let x_raw2_addr = x_raw2.expose_addr();
    // [..., Unique(1), SharedRW(2)]
    
    let x_unique3 = &mut *x_raw2;
    // [.., Unique(1), SharedRW(2), Unique(3)]
    
    assert_eq!(not_so_innocent(x_unique3), x_raw2_addr);
    // [.., Unique(1), SharedRW(2), Unique(3), ..., SharedRW(4)]
    
    // Do an int2ptr cast. This can pick tag 2 or 4 (the two previously exposed tags).
    // 4 is the "obvious" choice (topmost tag, what we used to do with untagged pointers).
    // And indeed if `variant == true` it is the only possible choice.
    // But if `variant == false` then 2 is the only possible choice!
    let x_wildcard = ptr::from_exposed_addr_mut::<i32>(x_raw2_addr);
    
    if variant {
        // If we picked 2, this will invalidate 3.
        *x_wildcard = 10;
        // Now we use 3. Only possible if above we picked 4.
        *x_unique3 = 12;
    } else {
        // This invalidates tag 4.
        *x_unique3 = 10;
        // Now try to write with the "guessed" tag; it must be 2.
        *x_wildcard = 12;
    }
} }

fn main() {
    example(false);
    example(true);
}

In terms of failing tests, the important ones are the ones in fail/stacked_borrows -- they should all keep failing. You could try running MIRIFLAGS="-Zmiri-permissive-provenance" ./miri test fail/stacked to see how they are doing.

In terms of further passing tests, here's another very simple one:

fn main() { unsafe {
    let root = &mut 42;
    let root_raw = root as *mut i32;
    let addr1 = root_raw as usize;
    let child = &mut *root_raw;
    let child_raw = child as *mut i32;
    let addr2 = child_raw as usize;
    assert_eq!(addr1, addr2);
    // First use child.
    *(addr2 as *mut i32) -= 2; // picks child_raw
    *child -= 2;
    // Then use root.
    *(addr1 as *mut i32) += 2; // picks root_raw
    *root += 2;
    // Value should be unchanged.
    assert_eq!(*root, 42);
} }

[bors]

☔ The latest upstream changes (presumably #2183) made this pull request unmergeable. Please resolve the merge conflicts.

[RalfJung]

All right I think this is now a pretty reasonable first implementation for permissive provenance in Stacked Borrows. :) It can even detect some incorrect uses of mutable and shared references derived from wildcard pointers. It probably still misses some UB that the "Untagged" approach would have caught, but on the flip side it is actually correct and doesn't suffer from rust-lang/unsafe-code-guidelines#273. Also it misses no UB when you never use a wildcard pointer (i.e., a pointer obtained via from_exposed_addr or an int2ptr cast).

@saethlin could you check if the changes to your diagnostics code make sense? It is mostly doing nothing now when encountering a wildcard pointer, which can probably be improved -- in a follow-up PR, if anyone wants to work on that. :)

[saethlin]

This collapsing behavior seems very important and is worth having a note (or is it a help? I think it might be a help) for, like we do for tag invalidation. That's certainly something I can do after this PR.

[RalfJung]

Note that collapsing is not part of the spec -- it is part of the approximation Miri does because the exact spec (as documented here) cannot be reasonably implemented. So, in the future, if we find a better way to approximate this, we might change this.

I guess what I am saying is -- this might be even harder to communicate than the regular Stacked Borrows rules, since these are derived rules that are computed from the actual rules.

[saethlin]

The changes to the diagnostic code mostly make sense, but for me the question is whether these diagnostics help a user make sense of errors they've never seen before. I'll run this over a bunch of crates over the next few days and probably want to upgrade the diagnostics as I indicated.

But in case this is what you were asking, I don't see anything that's bad enough to warrant immediate concern, on account of how this is all behind a non-default flag.

[RalfJung]

Thanks! Yes that is basically what I was asking.

Though I do plan to make this flag on-by-default very soon. However, all the new cases can only arise in code that actually uses from_exposed_addr, and meanwhile this entirely removes all the confusion caused by Untagged, so I think it is still a net win.

[RalfJung]

Thanks a lot @carbotaniuman for laying the foundation here! With this patch, -Zmiri-permissive-provenance should be production-ready (but with room for improvement in its diagnostics). I am very excited about getting rid of Untagged soon. :)

@bors r+

[bors]

📌 Commit 58c79c5 has been approved by RalfJung

[bors]

⌛ Testing commit 58c79c5 with merge 3b4402c...

[bors]

☀️ Test successful - checks-actions
Approved by: RalfJung
Pushing 3b4402c to master...