Auto merge of #3031 - RalfJung:foreign-read, r=RalfJung

tree borrows: more comments in foreign_read transition

1 files changed, 17 insertions, 3 deletions

diff --git a/src/tools/miri/src/borrow_tracker/tree_borrows/perms.rs b/src/tools/miri/src/borrow_tracker/tree_borrows/perms.rs
index 0ce29ac5437..dab216bc5b1 100644
--- a/src/tools/miri/src/borrow_tracker/tree_borrows/perms.rs
+++ b/src/tools/miri/src/borrow_tracker/tree_borrows/perms.rs
@@ -68,17 +68,31 @@ mod transition {
     fn foreign_read(state: PermissionPriv, protected: bool) -> Option<PermissionPriv> {
         use Option::*;
         Some(match state {
+            // Non-writeable states just ignore foreign reads.
+            non_writeable @ (Frozen | Disabled) => non_writeable,
+            // Writeable states are more tricky, and depend on whether things are protected.
             // The inner data `ty_is_freeze` of `Reserved` is always irrelevant for Read
             // accesses, since the data is not being mutated. Hence the `{ .. }`
-            res @ Reserved { .. } if !protected => res,
-            Reserved { .. } => Frozen, // protected reserved
+            res @ Reserved { .. } =>
+                if protected {
+                    // Someone else read, make sure we won't write.
+                    // We could make this `Disabled` but it doesn't look like we get anything out of that extra UB.
+                    Frozen
+                } else {
+                    // Before activation and without protectors, foreign reads are fine.
+                    // That's the entire point of 2-phase borrows.
+                    res
+                },
             Active =>
                 if protected {
+                    // We wrote, someone else reads -- that's bad.
+                    // (If this is initialized, this move-to-protected will mean insta-UB.)
                     Disabled
                 } else {
+                    // We don't want to disable here to allow read-read reordering: it is crucial
+                    // that the foreign read does not invalidate future reads through this tag.
                     Frozen
                 },
-            non_writeable @ (Frozen | Disabled) => non_writeable,
         })
     }