[WIP] Stacked Borrows: remove the 'quirk', properly pop items on read

Author: RalfJung

src/tools/miri/src/borrow_tracker/stacked_borrows/mod.rs

@@ -169,13 +169,31 @@ enum ItemInvalidationCause {
 
 /// Core per-location operations: access, dealloc, reborrow.
 impl<'tcx> Stack {
-    /// Find the first write-incompatible item above the given one --
-    /// i.e, find the height to which the stack will be truncated when writing to `granting`.
-    fn find_first_write_incompatible(&self, granting: usize) -> usize {
-        // The SharedReadWrite *just* above us are compatible, to skip those.
-        let mut idx = granting + 1;
+    /// Find the first incompatible item above the given one --
+    /// i.e, find the height to which the stack will be truncated when accessing `granting`.
+    /// `None` means the access used the unknown bottom.
+    fn find_first_incompatible(&self, access: AccessKind, granting: Option<usize>) -> usize {
+        let mut idx = match granting {
+            Some(granting) => {
+                // Start scanning above the granting item.
+                // The granting_idx *might* be approximate, but any lower idx would remove more
+                // things. Even if this is a Unique and the lower idx is an SRW (which removes
+                // less), there is an SRW group boundary here so strictly more would get removed.
+                granting + 1
+            }
+            None => {
+                // If the access uses the unknown bottom, scan the entire stack.
+                0
+            }
+        };
         while let Some(item) = self.get(idx) {
-            if item.perm() == Permission::SharedReadWrite {
+            // SRW is compatible with everything; SRO is compatible with reads.
+            let compatible = match (item.perm(), access) {
+                (Permission::SharedReadWrite, _) => true,
+                (Permission::SharedReadOnly, AccessKind::Read) => true,
+                _ => false,
+            };
+            if compatible {
                 // Go on.
                 idx += 1;
             } else {
@@ -245,48 +263,15 @@ impl<'tcx> Stack {
             self.find_granting(access, tag, exposed_tags).map_err(|()| dcx.access_error(self))?;
 
         // Step 2: Remove incompatible items above them.  Make sure we do not remove protected
-        // items.  Behavior differs for reads and writes.
+        // items. This ensures U2 for all accesses, and F2a on write accesses.
         // In case of wildcards/unknown matches, we remove everything that is *definitely* gone.
-        if access == AccessKind::Write {
-            // Remove everything above the write-compatible items, like a proper stack. This makes sure read-only and unique
-            // pointers become invalid on write accesses (ensures F2a, and ensures U2 for write accesses).
-            let first_incompatible_idx = if let Some(granting_idx) = granting_idx {
-                // The granting_idx *might* be approximate, but any lower idx would remove more
-                // things. Even if this is a Unique and the lower idx is an SRW (which removes
-                // less), there is an SRW group boundary here so strictly more would get removed.
-                self.find_first_write_incompatible(granting_idx)
-            } else {
-                // We are writing to something in the unknown part.
-                // There is a SRW group boundary between the unknown and the known, so everything is incompatible.
-                0
-            };
-            self.pop_items_after(first_incompatible_idx, |item| {
-                Stack::item_invalidated(&item, global, dcx, ItemInvalidationCause::Conflict)?;
-                dcx.log_invalidation(item.tag());
-                interp_ok(())
-            })?;
-        } else {
-            // On a read, *disable* all `Unique` above the granting item.  This ensures U2 for read accesses.
-            // The reason this is not following the stack discipline (by removing the first Unique and
-            // everything on top of it) is that in `let raw = &mut *x as *mut _; let _val = *x;`, the second statement
-            // would pop the `Unique` from the reborrow of the first statement, and subsequently also pop the
-            // `SharedReadWrite` for `raw`.
-            // This pattern occurs a lot in the standard library: create a raw pointer, then also create a shared
-            // reference and use that.
-            // We *disable* instead of removing `Unique` to avoid "connecting" two neighbouring blocks of SRWs.
-            let first_incompatible_idx = if let Some(granting_idx) = granting_idx {
-                // The granting_idx *might* be approximate, but any lower idx would disable more things.
-                granting_idx + 1
-            } else {
-                // We are reading from something in the unknown part. That means *all* `Unique` we know about are dead now.
-                0
-            };
-            self.disable_uniques_starting_at(first_incompatible_idx, |item| {
-                Stack::item_invalidated(&item, global, dcx, ItemInvalidationCause::Conflict)?;
-                dcx.log_invalidation(item.tag());
-                interp_ok(())
-            })?;
-        }
+
+        let first_incompatible_idx = self.find_first_incompatible(access, granting_idx);
+        self.pop_items_after(first_incompatible_idx, |item| {
+            Stack::item_invalidated(&item, global, dcx, ItemInvalidationCause::Conflict)?;
+            dcx.log_invalidation(item.tag());
+            interp_ok(())
+        })?;
 
         // If this was an approximate action, we now collapse everything into an unknown.
         if granting_idx.is_none() || matches!(tag, ProvenanceExtra::Wildcard) {
@@ -393,7 +378,7 @@ impl<'tcx> Stack {
             // access.  Instead of popping the stack, we insert the item at the place the stack would
             // be popped to (i.e., we insert it above all the write-compatible items).
             // This ensures F2b by adding the new item below any potentially existing `SharedReadOnly`.
-            self.find_first_write_incompatible(granting_idx)
+            self.find_first_incompatible(AccessKind::Write, Some(granting_idx))
         };
 
         // Put the new item there.

src/tools/miri/tests/fail/stacked_borrows/disable_mut_does_not_merge_srw.stderr

@@ -14,11 +14,11 @@ help: <TAG> was created by a Unique retag at offsets [0x0..0x4]
    |
 LL |             let mutref = &mut *base;
    |                          ^^^^^^^^^^
-help: <TAG> was later invalidated at offsets [0x0..0x4] by a write access
+help: <TAG> was later invalidated at offsets [0x0..0x4] by a read access
   --> tests/fail/stacked_borrows/disable_mut_does_not_merge_srw.rs:LL:CC
    |
-LL |         *base = 1;
-   |         ^^^^^^^^^
+LL |         let _val = *base;
+   |                    ^^^^^
    = note: BACKTRACE (of the first span):
    = note: inside `main` at tests/fail/stacked_borrows/disable_mut_does_not_merge_srw.rs:LL:CC
 

src/tools/miri/tests/fail/stacked_borrows/illegal_read_despite_exposed1.rs

@@ -8,7 +8,7 @@ fn main() {
         // From the exposed ptr, we get a new unique ptr.
         let root2 = &mut *exposed_ptr;
         let _fool = root2 as *mut _; // this would have fooled the old untagged pointer logic
-        // Stack: Unknown(<N), Unique(N), SRW(N+1)
+        // Stack: Unknown(<N), Unique(N)
         // And we test that it has uniqueness by doing a conflicting write.
         *exposed_ptr = 0;
         // Stack: Unknown(<N)

src/tools/miri/tests/fail/stacked_borrows/illegal_write_despite_exposed1.rs

@@ -7,7 +7,7 @@ fn main() {
         let exposed_ptr = addr as *mut i32;
         // From the exposed ptr, we get a new SRO ptr.
         let root2 = &*exposed_ptr;
-        // Stack: Unknown(<N), SRO(N), SRO(N+1)
+        // Stack: Unknown(<N), SRO(N)
         // And we test that it is read-only by doing a conflicting write.
         // (The write is still fine, using the `root as *mut i32` provenance which got exposed.)
         *exposed_ptr = 0;

src/tools/miri/tests/fail/stacked_borrows/interior_mut2.rs

@@ -15,16 +15,17 @@ fn main() {
         // stack: [c: SharedReadWrite, inner_uniq: Unique, inner_shr: SharedReadWrite]
 
         let _val = c.get().read(); // invalidates inner_uniq
-        // stack: [c: SharedReadWrite, inner_uniq: Disabled, inner_shr: SharedReadWrite]
+        // stack: [c: SharedReadWrite]
 
         // We have to be careful not to add any raw pointers above inner_uniq in
         // the stack, hence the use of unsafe_cell_get.
-        let _val = *unsafe_cell_get(inner_shr); // this still works
+        // This used to work, but since we removed the "quirk" it fails here.
+        let _val = *unsafe_cell_get(inner_shr); //~ ERROR: /retag .* tag does not exist in the borrow stack/
 
         *c.get() = UnsafeCell::new(0); // now inner_shr gets invalidated
         // stack: [c: SharedReadWrite]
 
-        // now this does not work any more
-        let _val = *inner_shr.get(); //~ ERROR: /retag .* tag does not exist in the borrow stack/
+        // this definitely should not work
+        let _val = *inner_shr.get();
     }
 }

src/tools/miri/tests/fail/stacked_borrows/interior_mut2.stderr

@@ -1,11 +1,11 @@
 error: Undefined Behavior: trying to retag from <TAG> for SharedReadWrite permission at ALLOC[0x0], but that tag does not exist in the borrow stack for this location
   --> tests/fail/stacked_borrows/interior_mut2.rs:LL:CC
    |
-LL |         let _val = *inner_shr.get();
-   |                     ^^^^^^^^^
-   |                     |
-   |                     trying to retag from <TAG> for SharedReadWrite permission at ALLOC[0x0], but that tag does not exist in the borrow stack for this location
-   |                     this error occurs as part of retag at ALLOC[0x0..0x4]
+LL |         let _val = *unsafe_cell_get(inner_shr);
+   |                                     ^^^^^^^^^
+   |                                     |
+   |                                     trying to retag from <TAG> for SharedReadWrite permission at ALLOC[0x0], but that tag does not exist in the borrow stack for this location
+   |                                     this error occurs as part of retag at ALLOC[0x0..0x4]
    |
    = 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
@@ -14,11 +14,11 @@ help: <TAG> was created by a SharedReadWrite retag at offsets [0x0..0x4]
    |
 LL |         let inner_shr = &*inner_uniq;
    |                         ^^^^^^^^^^^^
-help: <TAG> was later invalidated at offsets [0x0..0x4] by a write access
+help: <TAG> was later invalidated at offsets [0x0..0x4] by a read access
   --> tests/fail/stacked_borrows/interior_mut2.rs:LL:CC
    |
-LL |         *c.get() = UnsafeCell::new(0); // now inner_shr gets invalidated
-   |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+LL |         let _val = c.get().read(); // invalidates inner_uniq
+   |                    ^^^^^^^^^^^^^^
    = note: BACKTRACE (of the first span):
    = note: inside `main` at tests/fail/stacked_borrows/interior_mut2.rs:LL:CC
 

src/tools/miri/tests/pass/stacked_borrows/stack-printing.stdout

@@ -2,5 +2,5 @@
 0..1: [ SharedReadWrite<TAG> ]
 0..1: [ SharedReadWrite<TAG> ]
 0..1: [ SharedReadWrite<TAG> Unique<TAG> Unique<TAG> Unique<TAG> Unique<TAG> Unique<TAG> Unique<TAG> Unique<TAG> ]
-0..1: [ SharedReadWrite<TAG> Disabled<TAG> Disabled<TAG> Disabled<TAG> Disabled<TAG> Disabled<TAG> Disabled<TAG> Disabled<TAG> SharedReadOnly<TAG> ]
+0..1: [ SharedReadWrite<TAG> SharedReadOnly<TAG> ]
 0..1: [ unknown-bottom(..<TAG>) ]