Auto merge of #3054 - Vanille-N:spurious-fail, r=RalfJung

Issue discovered in TB: spurious reads are not (yet) possible in a concurrent setting

We discovered a week ago that in general, the current model of TB does not allow spurious reads because although reads provably never invalidate other reads, they migh invalidate writes.

Consider the code
```rs
fn f1(x: &u8) {}
fn f2(y: &mut u8) -> &mut u8 { &mut *y }

let mut data = 0;
let _ = thread::spawn(|| {
    f1(&mut data)
};
let _ = thread::spawn(|| {
    let y = f2(&mut data);
    *y = 42;
});
```
of which one possible interleaving is
```rs
1: retag x (&, protect) // x: [P]Frozen
2: retag y (&mut, protect) // y: [P]Reserved, x: [P]Frozen
1: return f1 // x: [P]Frozen -> Frozen, y: [P]Reserved
2: return f2 // x: Frozen, y: [P]Reserved -> Reserved
2: write y // x: Disabled, y: Active
```
that does not have UB.

Assume enough barriers to force this specific interleaving, and consider that the compiler could choose to insert a spurious read throug `x` during the call to `f1` which would produce
```rs
1: retag x (&, protect) // x: [P]Frozen
2: retag y (&mut, protect) // y: [P]Reserved, x: [P]Frozen
1: spurious read x // x:  [P]Frozen, y: [P]Reserved -> [P]Frozen
1: return f1 // x: [P]Frozen -> Frozen, y: [P]Frozen
2: return f2 // x: Frozen, y: [P]Frozen -> Frozen
2: write y // UB
```
Thus the target of the optimization (with a spurious read) has UB when the source did not.

This is bad.

SB is not affected because the code would be UB as early as `retag y`, this happens because we're trying to be a bit more subtle than that, and because the effects of a foreign read on a protected `&mut` bleed outside of the boundaries of the protector. Fortunately we have a fix planned, but in the meantime here are some `#[should_panic]` exhaustive tests to illustrate the issue.

The error message printed by the `#[should_panic]` tests flags the present issue in slightly more general terms: it says that the sequence `retag x (&, protect); retag y (&mut, protect);` produces the configuration `C_source := x: [P]Frozen, x: [P]Reserved`, and that inserting a spurious read through `x` turns it into `C_target := x: [P]Frozen, y: [P]Reserved`.
It then says that `C_source` is distinguishable from `C_target`, which means that there exists a sequence of instructions applied to both that triggers UB in `C_target` but not in `C_source`.
It happens that one such sequence is `1: return f1; 2: return f2; 2: write y;` as shown above, but it is not the only one, as for example the interleaving `1: return f1; 2: write y;` is also problematic.

Author: bors

src/borrow_tracker/tree_borrows/exhaustive.rs

@@ -0,0 +1,111 @@
+//! Exhaustive testing utilities.
+//! (These are used in Tree Borrows `#[test]`s for thorough verification
+//! of the behavior of the state machine of permissions,
+//! but the contents of this file are extremely generic)
+#![cfg(test)]
+
+pub trait Exhaustive: Sized {
+    fn exhaustive() -> Box<dyn Iterator<Item = Self>>;
+}
+
+macro_rules! precondition {
+    ($cond:expr) => {
+        if !$cond {
+            continue;
+        }
+    };
+}
+pub(crate) use precondition;
+
+// Trivial impls of `Exhaustive` for the standard types with 0, 1 and 2 elements respectively.
+
+impl Exhaustive for ! {
+    fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
+        Box::new(std::iter::empty())
+    }
+}
+
+impl Exhaustive for () {
+    fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
+        Box::new(std::iter::once(()))
+    }
+}
+
+impl Exhaustive for bool {
+    fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
+        Box::new(vec![true, false].into_iter())
+    }
+}
+
+// Some container impls for `Exhaustive`.
+
+impl<T> Exhaustive for Option<T>
+where
+    T: Exhaustive + 'static,
+{
+    fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
+        Box::new(std::iter::once(None).chain(T::exhaustive().map(Some)))
+    }
+}
+
+impl<T1, T2> Exhaustive for (T1, T2)
+where
+    T1: Exhaustive + Clone + 'static,
+    T2: Exhaustive + 'static,
+{
+    fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
+        Box::new(T1::exhaustive().flat_map(|t1| T2::exhaustive().map(move |t2| (t1.clone(), t2))))
+    }
+}
+
+impl<T> Exhaustive for [T; 1]
+where
+    T: Exhaustive + 'static,
+{
+    fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
+        Box::new(T::exhaustive().map(|t| [t]))
+    }
+}
+
+impl<T> Exhaustive for [T; 2]
+where
+    T: Exhaustive + Clone + 'static,
+{
+    fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
+        Box::new(T::exhaustive().flat_map(|t1| T::exhaustive().map(move |t2| [t1.clone(), t2])))
+    }
+}
+
+impl<T> Exhaustive for [T; 3]
+where
+    T: Exhaustive + Clone + 'static,
+{
+    fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
+        Box::new(
+            <[T; 2]>::exhaustive()
+                .flat_map(|[t1, t2]| T::exhaustive().map(move |t3| [t1.clone(), t2.clone(), t3])),
+        )
+    }
+}
+
+impl<T> Exhaustive for [T; 4]
+where
+    T: Exhaustive + Clone + 'static,
+{
+    fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
+        Box::new(<[T; 2]>::exhaustive().flat_map(|[t1, t2]| {
+            <[T; 2]>::exhaustive().map(move |[t3, t4]| [t1.clone(), t2.clone(), t3, t4])
+        }))
+    }
+}
+
+impl<T> Exhaustive for [T; 5]
+where
+    T: Exhaustive + Clone + 'static,
+{
+    fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
+        Box::new(<[T; 2]>::exhaustive().flat_map(|[t1, t2]| {
+            <[T; 3]>::exhaustive().map(move |[t3, t4, t5]| [t1.clone(), t2.clone(), t3, t4, t5])
+        }))
+    }
+}

src/borrow_tracker/tree_borrows/mod.rs

@@ -15,6 +15,10 @@ pub mod diagnostics;
 mod perms;
 mod tree;
 mod unimap;
+
+#[cfg(test)]
+mod exhaustive;
+
 use perms::Permission;
 pub use tree::Tree;
 
@@ -271,6 +275,10 @@ trait EvalContextPrivExt<'mir: 'ecx, 'tcx: 'mir, 'ecx>: crate::MiriInterpCxExt<'
             diagnostics::AccessCause::Reborrow,
         )?;
         // Record the parent-child pair in the tree.
+        // FIXME: We should eventually ensure that the following `assert` holds, because
+        // some "exhaustive" tests consider only the initial configurations that satisfy it.
+        // The culprit is `Permission::new_active` in `tb_protect_place`.
+        //assert!(new_perm.initial_state.is_initial());
         tree_borrows.new_child(orig_tag, new_tag, new_perm.initial_state, range, span)?;
         drop(tree_borrows);
 
@@ -283,7 +291,7 @@ trait EvalContextPrivExt<'mir: 'ecx, 'tcx: 'mir, 'ecx>: crate::MiriInterpCxExt<'
                 // interleaving, but wether UB happens can depend on whether a write occurs in the
                 // future...
                 let is_write = new_perm.initial_state.is_active()
-                    || (new_perm.initial_state.is_reserved() && new_perm.protector.is_some());
+                    || (new_perm.initial_state.is_reserved(None) && new_perm.protector.is_some());
                 if is_write {
                     // Need to get mutable access to alloc_extra.
                     // (Cannot always do this as we can do read-only reborrowing on read-only allocations.)