From 3b15db84194ac0bd6155e108178a47ba17121fb7 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Sat, 26 Nov 2022 13:22:19 +0100
Subject: [PATCH 1/4] !Unpin retags must still be reads, to check
 dereferenceable

also fix ICE on deallocation error and avoid redundant find_granting on retag
---
 src/stacked_borrows/diagnostics.rs            | 19 ++--
 src/stacked_borrows/mod.rs                    | 96 +++++++++----------
 src/stacked_borrows/stack.rs                  |  4 +-
 .../fail/stacked_borrows/illegal_dealloc1.rs  | 14 +++
 .../stacked_borrows/illegal_dealloc1.stderr   | 30 ++++++
 .../notunpin_dereferenceable_fakeread.rs      | 17 ++++
 .../notunpin_dereferenceable_fakeread.stderr  | 28 ++++++
 7 files changed, 151 insertions(+), 57 deletions(-)
 create mode 100644 tests/fail/stacked_borrows/illegal_dealloc1.rs
 create mode 100644 tests/fail/stacked_borrows/illegal_dealloc1.stderr
 create mode 100644 tests/fail/stacked_borrows/notunpin_dereferenceable_fakeread.rs
 create mode 100644 tests/fail/stacked_borrows/notunpin_dereferenceable_fakeread.stderr

diff --git a/src/stacked_borrows/diagnostics.rs b/src/stacked_borrows/diagnostics.rs
index 662d8ada73..9970b79f8c 100644
--- a/src/stacked_borrows/diagnostics.rs
+++ b/src/stacked_borrows/diagnostics.rs
@@ -353,10 +353,12 @@ impl<'history, 'ecx, 'mir, 'tcx> DiagnosticCx<'history, 'ecx, 'mir, 'tcx> {
 
     /// Report a descriptive error when `new` could not be granted from `derived_from`.
     #[inline(never)] // This is only called on fatal code paths
-    pub(super) fn grant_error(&self, perm: Permission, stack: &Stack) -> InterpError<'tcx> {
+    pub(super) fn grant_error(&self, stack: &Stack) -> InterpError<'tcx> {
         let Operation::Retag(op) = &self.operation else {
             unreachable!("grant_error should only be called during a retag")
         };
+        let perm =
+            op.permission.expect("`start_grant` must be called before calling `grant_error`");
         let action = format!(
             "trying to retag from {:?} for {:?} permission at {:?}[{:#x}]",
             op.orig_tag,
@@ -374,8 +376,11 @@ impl<'history, 'ecx, 'mir, 'tcx> DiagnosticCx<'history, 'ecx, 'mir, 'tcx> {
     /// Report a descriptive error when `access` is not permitted based on `tag`.
     #[inline(never)] // This is only called on fatal code paths
     pub(super) fn access_error(&self, stack: &Stack) -> InterpError<'tcx> {
-        let Operation::Access(op) = &self.operation  else {
-            unreachable!("access_error should only be called during an access")
+        // Deallocation and retagging also do an access as part of their thing, so handle that here, too.
+        let op = match &self.operation {
+            Operation::Access(op) => op,
+            Operation::Retag(_) => return self.grant_error(stack),
+            Operation::Dealloc(_) => return self.dealloc_error(stack),
         };
         let action = format!(
             "attempting a {access} using {tag:?} at {alloc_id:?}[{offset:#x}]",
@@ -428,14 +433,16 @@ impl<'history, 'ecx, 'mir, 'tcx> DiagnosticCx<'history, 'ecx, 'mir, 'tcx> {
     }
 
     #[inline(never)] // This is only called on fatal code paths
-    pub fn dealloc_error(&self) -> InterpError<'tcx> {
+    pub fn dealloc_error(&self, stack: &Stack) -> InterpError<'tcx> {
         let Operation::Dealloc(op) = &self.operation else {
             unreachable!("dealloc_error should only be called during a deallocation")
         };
         err_sb_ub(
             format!(
-                "no item granting write access for deallocation to tag {:?} at {:?} found in borrow stack",
-                op.tag, self.history.id,
+                "attempting deallocation using {tag:?} at {alloc_id:?}{cause}",
+                tag = op.tag,
+                alloc_id = self.history.id,
+                cause = error_cause(stack, op.tag),
             ),
             None,
             op.tag.and_then(|tag| self.get_logs_relevant_to(tag, None)),
diff --git a/src/stacked_borrows/mod.rs b/src/stacked_borrows/mod.rs
index db4e19f911..1759eee358 100644
--- a/src/stacked_borrows/mod.rs
+++ b/src/stacked_borrows/mod.rs
@@ -392,7 +392,7 @@ impl<'tcx> Stack {
 
         // Step 1: Find granting item.
         let granting_idx =
-            self.find_granting(access, tag, exposed_tags).map_err(|_| dcx.access_error(self))?;
+            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.
@@ -476,8 +476,7 @@ impl<'tcx> Stack {
     ) -> InterpResult<'tcx> {
         // Step 1: Make a write access.
         // As part of this we do regular protector checking, i.e. even weakly protected items cause UB when popped.
-        self.access(AccessKind::Write, tag, global, dcx, exposed_tags)
-            .map_err(|_| dcx.dealloc_error())?;
+        self.access(AccessKind::Write, tag, global, dcx, exposed_tags)?;
 
         // Step 2: Pretend we remove the remaining items, checking if any are strongly protected.
         for idx in (0..self.len()).rev() {
@@ -489,39 +488,42 @@ impl<'tcx> Stack {
     }
 
     /// Derive a new pointer from one with the given tag.
-    /// `weak` controls whether this operation is weak or strong: weak granting does not act as
-    /// an access, and they add the new item directly on top of the one it is derived
-    /// from instead of all the way at the top of the stack.
-    /// `range` refers the entire operation, and `offset` refers to the specific location in
-    /// `range` that we are currently checking.
+    ///
+    /// `access` indicates which kind of memory access this retag itself should correspond to.
     fn grant(
         &mut self,
         derived_from: ProvenanceExtra,
         new: Item,
+        access: Option<AccessKind>,
         global: &GlobalStateInner,
         dcx: &mut DiagnosticCx<'_, '_, '_, 'tcx>,
         exposed_tags: &FxHashSet<SbTag>,
     ) -> InterpResult<'tcx> {
         dcx.start_grant(new.perm());
 
-        // Figure out which access `perm` corresponds to.
-        let access =
-            if new.perm().grants(AccessKind::Write) { AccessKind::Write } else { AccessKind::Read };
-
-        // Now we figure out which item grants our parent (`derived_from`) this kind of access.
-        // We use that to determine where to put the new item.
-        let granting_idx = self
-            .find_granting(access, derived_from, exposed_tags)
-            .map_err(|_| dcx.grant_error(new.perm(), self))?;
-
         // Compute where to put the new item.
         // Either way, we ensure that we insert the new item in a way such that between
         // `derived_from` and the new one, there are only items *compatible with* `derived_from`.
-        let new_idx = if new.perm() == Permission::SharedReadWrite {
-            assert!(
-                access == AccessKind::Write,
-                "this case only makes sense for stack-like accesses"
-            );
+        let new_idx = if let Some(access) = access {
+            // Simple case: We are just a regular memory access, and then push our thing on top,
+            // like a regular stack.
+            // This ensures F2b for `Unique`, by removing offending `SharedReadOnly`.
+            self.access(access, derived_from, global, dcx, exposed_tags)?;
+
+            // We insert "as far up as possible": We know only compatible items are remaining
+            // on top of `derived_from`, and we want the new item at the top so that we
+            // get the strongest possible guarantees.
+            // This ensures U1 and F1.
+            self.len()
+        } else {
+            // The tricky case: creating a new SRW permission without actually being an access.
+            assert!(new.perm() == Permission::SharedReadWrite);
+
+            // First we figure out which item grants our parent (`derived_from`) this kind of access.
+            // We use that to determine where to put the new item.
+            let granting_idx = self
+                .find_granting(AccessKind::Write, derived_from, exposed_tags)
+                .map_err(|()| dcx.grant_error(self))?;
 
             let (Some(granting_idx), ProvenanceExtra::Concrete(_)) = (granting_idx, derived_from) else {
                 // The parent is a wildcard pointer or matched the unknown bottom.
@@ -538,17 +540,6 @@ impl<'tcx> Stack {
             // 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)
-        } else {
-            // A "safe" reborrow for a pointer that actually expects some aliasing guarantees.
-            // Here, creating a reference actually counts as an access.
-            // This ensures F2b for `Unique`, by removing offending `SharedReadOnly`.
-            self.access(access, derived_from, global, dcx, exposed_tags)?;
-
-            // We insert "as far up as possible": We know only compatible items are remaining
-            // on top of `derived_from`, and we want the new item at the top so that we
-            // get the strongest possible guarantees.
-            // This ensures U1 and F1.
-            self.len()
         };
 
         // Put the new item there.
@@ -864,18 +855,22 @@ trait EvalContextPrivExt<'mir: 'ecx, 'tcx: 'mir, 'ecx>: crate::MiriInterpCxExt<'
         // Update the stacks.
         // Make sure that raw pointers and mutable shared references are reborrowed "weak":
         // There could be existing unique pointers reborrowed from them that should remain valid!
-        let perm = match kind {
-            RefKind::Unique { two_phase: false }
-                if place.layout.ty.is_unpin(*this.tcx, this.param_env()) =>
-            {
-                // Only if the type is unpin do we actually enforce uniqueness
-                Permission::Unique
+        let (perm, access) = match kind {
+            RefKind::Unique { two_phase } => {
+                // Permission is Unique only if the type is `Unpin` and this is not twophase
+                let perm = if !two_phase && place.layout.ty.is_unpin(*this.tcx, this.param_env()) {
+                    Permission::Unique
+                } else {
+                    Permission::SharedReadWrite
+                };
+                // We do an access for all full borrows, even if `!Unpin`.
+                let access = if !two_phase { Some(AccessKind::Write) } else { None };
+                (perm, access)
             }
-            RefKind::Unique { .. } => {
-                // Two-phase references and !Unpin references are treated as SharedReadWrite
-                Permission::SharedReadWrite
+            RefKind::Raw { mutable: true } => {
+                // Creating a raw ptr does not count as an access
+                (Permission::SharedReadWrite, None)
             }
-            RefKind::Raw { mutable: true } => Permission::SharedReadWrite,
             RefKind::Shared | RefKind::Raw { mutable: false } => {
                 // Shared references and *const are a whole different kind of game, the
                 // permission is not uniform across the entire range!
@@ -892,10 +887,13 @@ trait EvalContextPrivExt<'mir: 'ecx, 'tcx: 'mir, 'ecx>: crate::MiriInterpCxExt<'
                     // Adjust range.
                     range.start += base_offset;
                     // We are only ever `SharedReadOnly` inside the frozen bits.
-                    let perm = if frozen {
-                        Permission::SharedReadOnly
+                    let (perm, access) = if frozen {
+                        (Permission::SharedReadOnly, Some(AccessKind::Read))
                     } else {
-                        Permission::SharedReadWrite
+                        // Inside UnsafeCell, this does *not* count as an access, as there
+                        // might actually be mutable references further up the stack that
+                        // we have to keep alive.
+                        (Permission::SharedReadWrite, None)
                     };
                     let protected = if frozen {
                         protect.is_some()
@@ -914,7 +912,7 @@ trait EvalContextPrivExt<'mir: 'ecx, 'tcx: 'mir, 'ecx>: crate::MiriInterpCxExt<'
                         alloc_range(base_offset, size),
                     );
                     stacked_borrows.for_each(range, dcx, |stack, dcx, exposed_tags| {
-                        stack.grant(orig_tag, item, &global, dcx, exposed_tags)
+                        stack.grant(orig_tag, item, access, &global, dcx, exposed_tags)
                     })
                 })?;
                 return Ok(Some(alloc_id));
@@ -941,7 +939,7 @@ trait EvalContextPrivExt<'mir: 'ecx, 'tcx: 'mir, 'ecx>: crate::MiriInterpCxExt<'
             alloc_range(base_offset, size),
         );
         stacked_borrows.for_each(range, dcx, |stack, dcx, exposed_tags| {
-            stack.grant(orig_tag, item, &global, dcx, exposed_tags)
+            stack.grant(orig_tag, item, access, &global, dcx, exposed_tags)
         })?;
 
         Ok(Some(alloc_id))
diff --git a/src/stacked_borrows/stack.rs b/src/stacked_borrows/stack.rs
index aa549e34c5..51a6fba6df 100644
--- a/src/stacked_borrows/stack.rs
+++ b/src/stacked_borrows/stack.rs
@@ -367,10 +367,10 @@ impl<'tcx> Stack {
 
     /// Find all `Unique` elements in this borrow stack above `granting_idx`, pass a copy of them
     /// to the `visitor`, then set their `Permission` to `Disabled`.
-    pub fn disable_uniques_starting_at<V: FnMut(Item) -> crate::InterpResult<'tcx>>(
+    pub fn disable_uniques_starting_at(
         &mut self,
         disable_start: usize,
-        mut visitor: V,
+        mut visitor: impl FnMut(Item) -> crate::InterpResult<'tcx>,
     ) -> crate::InterpResult<'tcx> {
         #[cfg(feature = "stack-cache")]
         let unique_range = self.unique_range.clone();
diff --git a/tests/fail/stacked_borrows/illegal_dealloc1.rs b/tests/fail/stacked_borrows/illegal_dealloc1.rs
new file mode 100644
index 0000000000..670dd4baad
--- /dev/null
+++ b/tests/fail/stacked_borrows/illegal_dealloc1.rs
@@ -0,0 +1,14 @@
+//@error-pattern: /deallocation .* tag does not exist in the borrow stack/
+use std::alloc::{alloc, dealloc, Layout};
+
+fn main() {
+    unsafe {
+        let x = alloc(Layout::from_size_align_unchecked(1, 1));
+        let ptr1 = (&mut *x) as *mut u8;
+        let ptr2 = (&mut *ptr1) as *mut u8;
+        // Invalidate ptr2 by writing to ptr1.
+        ptr1.write(0);
+        // Deallocate through ptr2.
+        dealloc(ptr2, Layout::from_size_align_unchecked(1, 1));
+    }
+}
diff --git a/tests/fail/stacked_borrows/illegal_dealloc1.stderr b/tests/fail/stacked_borrows/illegal_dealloc1.stderr
new file mode 100644
index 0000000000..3b7802901a
--- /dev/null
+++ b/tests/fail/stacked_borrows/illegal_dealloc1.stderr
@@ -0,0 +1,30 @@
+error: Undefined Behavior: attempting deallocation using <TAG> at ALLOC, but that tag does not exist in the borrow stack for this location
+  --> RUSTLIB/alloc/src/alloc.rs:LL:CC
+   |
+LL |     unsafe { __rust_dealloc(ptr, layout.size(), layout.align()) }
+   |              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ attempting deallocation using <TAG> at ALLOC, but that tag does not exist in the borrow stack for this location
+   |
+   = 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: <TAG> was created by a SharedReadWrite retag at offsets [0x0..0x1]
+  --> $DIR/illegal_deALLOC.rs:LL:CC
+   |
+LL |         let ptr2 = (&mut *ptr1) as *mut u8;
+   |                    ^^^^^^^^^^^^
+help: <TAG> was later invalidated at offsets [0x0..0x1] by a write access
+  --> $DIR/illegal_deALLOC.rs:LL:CC
+   |
+LL |         ptr1.write(0);
+   |         ^^^^^^^^^^^^^
+   = note: BACKTRACE:
+   = note: inside `std::alloc::dealloc` at RUSTLIB/alloc/src/alloc.rs:LL:CC
+note: inside `main` at $DIR/illegal_deALLOC.rs:LL:CC
+  --> $DIR/illegal_deALLOC.rs:LL:CC
+   |
+LL |         dealloc(ptr2, Layout::from_size_align_unchecked(1, 1));
+   |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
+
+error: aborting due to previous error
+
diff --git a/tests/fail/stacked_borrows/notunpin_dereferenceable_fakeread.rs b/tests/fail/stacked_borrows/notunpin_dereferenceable_fakeread.rs
new file mode 100644
index 0000000000..d660921bfe
--- /dev/null
+++ b/tests/fail/stacked_borrows/notunpin_dereferenceable_fakeread.rs
@@ -0,0 +1,17 @@
+//! Reborrowing a `&mut !Unpin` must still act like a (fake) read.
+use std::marker::PhantomPinned;
+
+struct NotUnpin(i32, PhantomPinned);
+
+fn main() {
+    unsafe {
+        let mut x = NotUnpin(0, PhantomPinned);
+        // Mutable borrow of `Unpin` field (with lifetime laundering)
+        let fieldref = &mut *(&mut x.0 as *mut i32);
+        // Mutable reborrow of the entire `x`, which is `!Unpin` but should
+        // still count as a read since we would add `dereferenceable`.
+        let _xref = &mut x;
+        // That read should have invalidated `fieldref`.
+        *fieldref = 0; //~ ERROR: /write access .* tag does not exist in the borrow stack/
+    }
+}
diff --git a/tests/fail/stacked_borrows/notunpin_dereferenceable_fakeread.stderr b/tests/fail/stacked_borrows/notunpin_dereferenceable_fakeread.stderr
new file mode 100644
index 0000000000..3ef8a8e0e9
--- /dev/null
+++ b/tests/fail/stacked_borrows/notunpin_dereferenceable_fakeread.stderr
@@ -0,0 +1,28 @@
+error: Undefined Behavior: attempting a write access using <TAG> at ALLOC[0x0], but that tag does not exist in the borrow stack for this location
+  --> $DIR/notunpin_dereferenceable_fakeread.rs:LL:CC
+   |
+LL |         *fieldref = 0;
+   |         ^^^^^^^^^^^^^
+   |         |
+   |         attempting a write access using <TAG> at ALLOC[0x0], but that tag does not exist in the borrow stack for this location
+   |         this error occurs as part of an access 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
+help: <TAG> was created by a Unique retag at offsets [0x0..0x4]
+  --> $DIR/notunpin_dereferenceable_fakeread.rs:LL:CC
+   |
+LL |         let fieldref = &mut *(&mut x.0 as *mut i32);
+   |                        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+help: <TAG> was later invalidated at offsets [0x0..0x4] by a SharedReadWrite retag
+  --> $DIR/notunpin_dereferenceable_fakeread.rs:LL:CC
+   |
+LL |         let _xref = &mut x;
+   |                     ^^^^^^
+   = note: BACKTRACE:
+   = note: inside `main` at $DIR/notunpin_dereferenceable_fakeread.rs:LL:CC
+
+note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
+
+error: aborting due to previous error
+

From 528935d8ff084468172eba036d268892eab7d5ca Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Sat, 26 Nov 2022 14:42:27 +0100
Subject: [PATCH 2/4] slightly adjust and synchronize Machine passing for SB
 and DataRace

---
 src/concurrency/data_race.rs | 26 +++++++++++------------
 src/machine.rs               | 40 +++++++-----------------------------
 src/stacked_borrows/mod.rs   | 13 +++++-------
 3 files changed, 24 insertions(+), 55 deletions(-)

diff --git a/src/concurrency/data_race.rs b/src/concurrency/data_race.rs
index b0f7664621..d669cc1362 100644
--- a/src/concurrency/data_race.rs
+++ b/src/concurrency/data_race.rs
@@ -838,18 +838,18 @@ impl VClockAlloc {
         &self,
         alloc_id: AllocId,
         range: AllocRange,
-        global: &GlobalState,
-        thread_mgr: &ThreadManager<'_, '_>,
+        machine: &MiriMachine<'_, '_>,
     ) -> InterpResult<'tcx> {
+        let global = machine.data_race.as_ref().unwrap();
         if global.race_detecting() {
-            let (index, clocks) = global.current_thread_state(thread_mgr);
+            let (index, clocks) = global.current_thread_state(&machine.threads);
             let mut alloc_ranges = self.alloc_ranges.borrow_mut();
             for (offset, range) in alloc_ranges.iter_mut(range.start, range.size) {
                 if let Err(DataRace) = range.read_race_detect(&clocks, index) {
                     // Report data-race.
                     return Self::report_data_race(
                         global,
-                        thread_mgr,
+                        &machine.threads,
                         range,
                         "Read",
                         false,
@@ -869,17 +869,17 @@ impl VClockAlloc {
         alloc_id: AllocId,
         range: AllocRange,
         write_type: WriteType,
-        global: &mut GlobalState,
-        thread_mgr: &ThreadManager<'_, '_>,
+        machine: &mut MiriMachine<'_, '_>,
     ) -> InterpResult<'tcx> {
+        let global = machine.data_race.as_mut().unwrap();
         if global.race_detecting() {
-            let (index, clocks) = global.current_thread_state(thread_mgr);
+            let (index, clocks) = global.current_thread_state(&machine.threads);
             for (offset, range) in self.alloc_ranges.get_mut().iter_mut(range.start, range.size) {
                 if let Err(DataRace) = range.write_race_detect(&clocks, index, write_type) {
                     // Report data-race
                     return Self::report_data_race(
                         global,
-                        thread_mgr,
+                        &machine.threads,
                         range,
                         write_type.get_descriptor(),
                         false,
@@ -901,10 +901,9 @@ impl VClockAlloc {
         &mut self,
         alloc_id: AllocId,
         range: AllocRange,
-        global: &mut GlobalState,
-        thread_mgr: &ThreadManager<'_, '_>,
+        machine: &mut MiriMachine<'_, '_>,
     ) -> InterpResult<'tcx> {
-        self.unique_access(alloc_id, range, WriteType::Write, global, thread_mgr)
+        self.unique_access(alloc_id, range, WriteType::Write, machine)
     }
 
     /// Detect data-races for an unsynchronized deallocate operation, will not perform
@@ -915,10 +914,9 @@ impl VClockAlloc {
         &mut self,
         alloc_id: AllocId,
         range: AllocRange,
-        global: &mut GlobalState,
-        thread_mgr: &ThreadManager<'_, '_>,
+        machine: &mut MiriMachine<'_, '_>,
     ) -> InterpResult<'tcx> {
-        self.unique_access(alloc_id, range, WriteType::Deallocate, global, thread_mgr)
+        self.unique_access(alloc_id, range, WriteType::Deallocate, machine)
     }
 }
 
diff --git a/src/machine.rs b/src/machine.rs
index b7f434b555..edfef211dc 100644
--- a/src/machine.rs
+++ b/src/machine.rs
@@ -1003,21 +1003,12 @@ impl<'mir, 'tcx> Machine<'mir, 'tcx> for MiriMachine<'mir, 'tcx> {
         range: AllocRange,
     ) -> InterpResult<'tcx> {
         if let Some(data_race) = &alloc_extra.data_race {
-            data_race.read(
-                alloc_id,
-                range,
-                machine.data_race.as_ref().unwrap(),
-                &machine.threads,
-            )?;
+            data_race.read(alloc_id, range, machine)?;
         }
         if let Some(stacked_borrows) = &alloc_extra.stacked_borrows {
-            stacked_borrows.borrow_mut().before_memory_read(
-                alloc_id,
-                prov_extra,
-                range,
-                machine.stacked_borrows.as_ref().unwrap(),
-                machine,
-            )?;
+            stacked_borrows
+                .borrow_mut()
+                .before_memory_read(alloc_id, prov_extra, range, machine)?;
         }
         if let Some(weak_memory) = &alloc_extra.weak_memory {
             weak_memory.memory_accessed(range, machine.data_race.as_ref().unwrap());
@@ -1034,21 +1025,10 @@ impl<'mir, 'tcx> Machine<'mir, 'tcx> for MiriMachine<'mir, 'tcx> {
         range: AllocRange,
     ) -> InterpResult<'tcx> {
         if let Some(data_race) = &mut alloc_extra.data_race {
-            data_race.write(
-                alloc_id,
-                range,
-                machine.data_race.as_mut().unwrap(),
-                &machine.threads,
-            )?;
+            data_race.write(alloc_id, range, machine)?;
         }
         if let Some(stacked_borrows) = &mut alloc_extra.stacked_borrows {
-            stacked_borrows.get_mut().before_memory_write(
-                alloc_id,
-                prov_extra,
-                range,
-                machine.stacked_borrows.as_ref().unwrap(),
-                machine,
-            )?;
+            stacked_borrows.get_mut().before_memory_write(alloc_id, prov_extra, range, machine)?;
         }
         if let Some(weak_memory) = &alloc_extra.weak_memory {
             weak_memory.memory_accessed(range, machine.data_race.as_ref().unwrap());
@@ -1068,19 +1048,13 @@ impl<'mir, 'tcx> Machine<'mir, 'tcx> for MiriMachine<'mir, 'tcx> {
             machine.emit_diagnostic(NonHaltingDiagnostic::FreedAlloc(alloc_id));
         }
         if let Some(data_race) = &mut alloc_extra.data_race {
-            data_race.deallocate(
-                alloc_id,
-                range,
-                machine.data_race.as_mut().unwrap(),
-                &machine.threads,
-            )?;
+            data_race.deallocate(alloc_id, range, machine)?;
         }
         if let Some(stacked_borrows) = &mut alloc_extra.stacked_borrows {
             stacked_borrows.get_mut().before_memory_deallocation(
                 alloc_id,
                 prove_extra,
                 range,
-                machine.stacked_borrows.as_ref().unwrap(),
                 machine,
             )
         } else {
diff --git a/src/stacked_borrows/mod.rs b/src/stacked_borrows/mod.rs
index 1759eee358..e412f64506 100644
--- a/src/stacked_borrows/mod.rs
+++ b/src/stacked_borrows/mod.rs
@@ -644,7 +644,6 @@ impl Stacks {
         alloc_id: AllocId,
         tag: ProvenanceExtra,
         range: AllocRange,
-        state: &GlobalState,
         machine: &'ecx MiriMachine<'mir, 'tcx>,
     ) -> InterpResult<'tcx>
     where
@@ -657,7 +656,7 @@ impl Stacks {
             range.size.bytes()
         );
         let dcx = DiagnosticCxBuilder::read(machine, tag, range);
-        let state = state.borrow();
+        let state = machine.stacked_borrows.as_ref().unwrap().borrow();
         self.for_each(range, dcx, |stack, dcx, exposed_tags| {
             stack.access(AccessKind::Read, tag, &state, dcx, exposed_tags)
         })
@@ -669,8 +668,7 @@ impl Stacks {
         alloc_id: AllocId,
         tag: ProvenanceExtra,
         range: AllocRange,
-        state: &GlobalState,
-        machine: &'ecx MiriMachine<'mir, 'tcx>,
+        machine: &'ecx mut MiriMachine<'mir, 'tcx>,
     ) -> InterpResult<'tcx> {
         trace!(
             "write access with tag {:?}: {:?}, size {}",
@@ -679,7 +677,7 @@ impl Stacks {
             range.size.bytes()
         );
         let dcx = DiagnosticCxBuilder::write(machine, tag, range);
-        let state = state.borrow();
+        let state = machine.stacked_borrows.as_ref().unwrap().borrow();
         self.for_each(range, dcx, |stack, dcx, exposed_tags| {
             stack.access(AccessKind::Write, tag, &state, dcx, exposed_tags)
         })
@@ -691,12 +689,11 @@ impl Stacks {
         alloc_id: AllocId,
         tag: ProvenanceExtra,
         range: AllocRange,
-        state: &GlobalState,
-        machine: &'ecx MiriMachine<'mir, 'tcx>,
+        machine: &'ecx mut MiriMachine<'mir, 'tcx>,
     ) -> InterpResult<'tcx> {
         trace!("deallocation with tag {:?}: {:?}, size {}", tag, alloc_id, range.size.bytes());
         let dcx = DiagnosticCxBuilder::dealloc(machine, tag);
-        let state = state.borrow();
+        let state = machine.stacked_borrows.as_ref().unwrap().borrow();
         self.for_each(range, dcx, |stack, dcx, exposed_tags| {
             stack.dealloc(tag, &state, dcx, exposed_tags)
         })?;

From c75f23d4711ebee208e9c5f02af377d1e50c1405 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Sat, 26 Nov 2022 14:46:06 +0100
Subject: [PATCH 3/4] make Stacked Borrows retags act like data races

---
 src/stacked_borrows/mod.rs                    | 23 ++++++++++++--
 tests/fail/data_race/alloc_read_race.rs       |  2 +-
 tests/fail/data_race/alloc_write_race.rs      |  2 +-
 .../data_race/atomic_read_na_write_race1.rs   |  4 +--
 .../data_race/atomic_read_na_write_race2.rs   |  4 +--
 .../data_race/atomic_write_na_read_race1.rs   |  4 +--
 .../data_race/atomic_write_na_read_race2.rs   |  4 +--
 .../data_race/atomic_write_na_write_race1.rs  |  4 +--
 .../data_race/atomic_write_na_write_race2.rs  |  4 +--
 .../data_race/dangling_thread_async_race.rs   |  4 +--
 tests/fail/data_race/dangling_thread_race.rs  |  4 +--
 tests/fail/data_race/dealloc_read_race1.rs    |  4 +--
 tests/fail/data_race/dealloc_read_race2.rs    |  4 +--
 .../fail/data_race/dealloc_read_race_stack.rs |  2 +-
 tests/fail/data_race/dealloc_write_race1.rs   |  4 +--
 tests/fail/data_race/dealloc_write_race2.rs   |  4 +--
 .../data_race/dealloc_write_race_stack.rs     |  2 +-
 .../data_race/enable_after_join_to_main.rs    |  4 +--
 tests/fail/data_race/fence_after_load.rs      |  4 +--
 tests/fail/data_race/read_write_race.rs       |  4 +--
 tests/fail/data_race/read_write_race_stack.rs |  2 +-
 tests/fail/data_race/relax_acquire_race.rs    |  2 +-
 tests/fail/data_race/release_seq_race.rs      |  2 +-
 .../data_race/release_seq_race_same_thread.rs |  2 +-
 tests/fail/data_race/rmw_race.rs              |  2 +-
 tests/fail/data_race/stack_pop_race.rs        |  2 +-
 tests/fail/data_race/write_write_race.rs      |  2 +-
 .../fail/data_race/write_write_race_stack.rs  |  2 +-
 .../stacked_borrows/retag_data_race_read.rs   | 31 +++++++++++++++++++
 .../retag_data_race_read.stderr               | 20 ++++++++++++
 .../stacked_borrows/retag_data_race_write.rs  | 31 +++++++++++++++++++
 .../retag_data_race_write.stderr              | 20 ++++++++++++
 32 files changed, 164 insertions(+), 45 deletions(-)
 create mode 100644 tests/fail/stacked_borrows/retag_data_race_read.rs
 create mode 100644 tests/fail/stacked_borrows/retag_data_race_read.stderr
 create mode 100644 tests/fail/stacked_borrows/retag_data_race_write.rs
 create mode 100644 tests/fail/stacked_borrows/retag_data_race_write.stderr

diff --git a/src/stacked_borrows/mod.rs b/src/stacked_borrows/mod.rs
index e412f64506..5093cddfd3 100644
--- a/src/stacked_borrows/mod.rs
+++ b/src/stacked_borrows/mod.rs
@@ -874,8 +874,8 @@ trait EvalContextPrivExt<'mir: 'ecx, 'tcx: 'mir, 'ecx>: crate::MiriInterpCxExt<'
                 // We need a frozen-sensitive reborrow.
                 // We have to use shared references to alloc/memory_extra here since
                 // `visit_freeze_sensitive` needs to access the global state.
-                let extra = this.get_alloc_extra(alloc_id)?;
-                let mut stacked_borrows = extra
+                let alloc_extra = this.get_alloc_extra(alloc_id)?;
+                let mut stacked_borrows = alloc_extra
                     .stacked_borrows
                     .as_ref()
                     .expect("we should have Stacked Borrows data")
@@ -910,7 +910,16 @@ trait EvalContextPrivExt<'mir: 'ecx, 'tcx: 'mir, 'ecx>: crate::MiriInterpCxExt<'
                     );
                     stacked_borrows.for_each(range, dcx, |stack, dcx, exposed_tags| {
                         stack.grant(orig_tag, item, access, &global, dcx, exposed_tags)
-                    })
+                    })?;
+                    drop(global);
+                    if let Some(access) = access {
+                        assert!(access == AccessKind::Read);
+                        // Make sure the data race model also knows about this.
+                        if let Some(data_race) = alloc_extra.data_race.as_ref() {
+                            data_race.read(alloc_id, range, &this.machine)?;
+                        }
+                    }
+                    Ok(())
                 })?;
                 return Ok(Some(alloc_id));
             }
@@ -938,6 +947,14 @@ trait EvalContextPrivExt<'mir: 'ecx, 'tcx: 'mir, 'ecx>: crate::MiriInterpCxExt<'
         stacked_borrows.for_each(range, dcx, |stack, dcx, exposed_tags| {
             stack.grant(orig_tag, item, access, &global, dcx, exposed_tags)
         })?;
+        drop(global);
+        if let Some(access) = access {
+            assert!(access == AccessKind::Write);
+            // Make sure the data race model also knows about this.
+            if let Some(data_race) = alloc_extra.data_race.as_mut() {
+                data_race.write(alloc_id, range, machine)?;
+            }
+        }
 
         Ok(Some(alloc_id))
     }
diff --git a/tests/fail/data_race/alloc_read_race.rs b/tests/fail/data_race/alloc_read_race.rs
index 0bd3068af1..6040452a16 100644
--- a/tests/fail/data_race/alloc_read_race.rs
+++ b/tests/fail/data_race/alloc_read_race.rs
@@ -1,4 +1,4 @@
-//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0
+//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
 #![feature(new_uninit)]
 
 use std::mem::MaybeUninit;
diff --git a/tests/fail/data_race/alloc_write_race.rs b/tests/fail/data_race/alloc_write_race.rs
index 7991280721..51d431b36f 100644
--- a/tests/fail/data_race/alloc_write_race.rs
+++ b/tests/fail/data_race/alloc_write_race.rs
@@ -1,4 +1,4 @@
-//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0
+//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
 #![feature(new_uninit)]
 
 use std::ptr::null_mut;
diff --git a/tests/fail/data_race/atomic_read_na_write_race1.rs b/tests/fail/data_race/atomic_read_na_write_race1.rs
index 2b0446d724..79c6760b7c 100644
--- a/tests/fail/data_race/atomic_read_na_write_race1.rs
+++ b/tests/fail/data_race/atomic_read_na_write_race1.rs
@@ -1,5 +1,5 @@
-// We want to control preemption here.
-//@compile-flags: -Zmiri-preemption-rate=0
+// We want to control preemption here. Stacked borrows interferes by having its own accesses.
+//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
 
 use std::sync::atomic::{AtomicUsize, Ordering};
 use std::thread::spawn;
diff --git a/tests/fail/data_race/atomic_read_na_write_race2.rs b/tests/fail/data_race/atomic_read_na_write_race2.rs
index ef5157515c..e069ac4ad6 100644
--- a/tests/fail/data_race/atomic_read_na_write_race2.rs
+++ b/tests/fail/data_race/atomic_read_na_write_race2.rs
@@ -1,5 +1,5 @@
-// We want to control preemption here.
-//@compile-flags: -Zmiri-preemption-rate=0
+// We want to control preemption here. Stacked borrows interferes by having its own accesses.
+//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
 
 use std::sync::atomic::AtomicUsize;
 use std::sync::atomic::Ordering;
diff --git a/tests/fail/data_race/atomic_write_na_read_race1.rs b/tests/fail/data_race/atomic_write_na_read_race1.rs
index 8c17e76748..9c025a0153 100644
--- a/tests/fail/data_race/atomic_write_na_read_race1.rs
+++ b/tests/fail/data_race/atomic_write_na_read_race1.rs
@@ -1,5 +1,5 @@
-// We want to control preemption here.
-//@compile-flags: -Zmiri-preemption-rate=0
+// We want to control preemption here. Stacked borrows interferes by having its own accesses.
+//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
 
 use std::sync::atomic::AtomicUsize;
 use std::sync::atomic::Ordering;
diff --git a/tests/fail/data_race/atomic_write_na_read_race2.rs b/tests/fail/data_race/atomic_write_na_read_race2.rs
index f14d7c704d..30b3c48637 100644
--- a/tests/fail/data_race/atomic_write_na_read_race2.rs
+++ b/tests/fail/data_race/atomic_write_na_read_race2.rs
@@ -1,5 +1,5 @@
-// We want to control preemption here.
-//@compile-flags: -Zmiri-preemption-rate=0
+// We want to control preemption here. Stacked borrows interferes by having its own accesses.
+//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
 
 use std::sync::atomic::{AtomicUsize, Ordering};
 use std::thread::spawn;
diff --git a/tests/fail/data_race/atomic_write_na_write_race1.rs b/tests/fail/data_race/atomic_write_na_write_race1.rs
index 0804b33407..02b17cc57b 100644
--- a/tests/fail/data_race/atomic_write_na_write_race1.rs
+++ b/tests/fail/data_race/atomic_write_na_write_race1.rs
@@ -1,5 +1,5 @@
-// We want to control preemption here.
-//@compile-flags: -Zmiri-preemption-rate=0
+// We want to control preemption here. Stacked borrows interferes by having its own accesses.
+//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
 
 use std::sync::atomic::{AtomicUsize, Ordering};
 use std::thread::spawn;
diff --git a/tests/fail/data_race/atomic_write_na_write_race2.rs b/tests/fail/data_race/atomic_write_na_write_race2.rs
index 658cddcc9c..b5f4966d88 100644
--- a/tests/fail/data_race/atomic_write_na_write_race2.rs
+++ b/tests/fail/data_race/atomic_write_na_write_race2.rs
@@ -1,5 +1,5 @@
-// We want to control preemption here.
-//@compile-flags: -Zmiri-preemption-rate=0
+// We want to control preemption here. Stacked borrows interferes by having its own accesses.
+//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
 
 use std::sync::atomic::AtomicUsize;
 use std::sync::atomic::Ordering;
diff --git a/tests/fail/data_race/dangling_thread_async_race.rs b/tests/fail/data_race/dangling_thread_async_race.rs
index af2588e923..9922468e5f 100644
--- a/tests/fail/data_race/dangling_thread_async_race.rs
+++ b/tests/fail/data_race/dangling_thread_async_race.rs
@@ -1,5 +1,5 @@
-// We want to control preemption here.
-//@compile-flags: -Zmiri-disable-isolation -Zmiri-preemption-rate=0
+// We want to control preemption here. Stacked borrows interferes by having its own accesses.
+//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
 
 use std::mem;
 use std::thread::{sleep, spawn};
diff --git a/tests/fail/data_race/dangling_thread_race.rs b/tests/fail/data_race/dangling_thread_race.rs
index 1ee619c3f9..8c8a6ac87f 100644
--- a/tests/fail/data_race/dangling_thread_race.rs
+++ b/tests/fail/data_race/dangling_thread_race.rs
@@ -1,5 +1,5 @@
-// We want to control preemption here.
-//@compile-flags: -Zmiri-disable-isolation -Zmiri-preemption-rate=0
+// We want to control preemption here. Stacked borrows interferes by having its own accesses.
+//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
 
 use std::mem;
 use std::thread::{sleep, spawn};
diff --git a/tests/fail/data_race/dealloc_read_race1.rs b/tests/fail/data_race/dealloc_read_race1.rs
index cbc02549a2..8e1216f5bf 100644
--- a/tests/fail/data_race/dealloc_read_race1.rs
+++ b/tests/fail/data_race/dealloc_read_race1.rs
@@ -1,5 +1,5 @@
-// We want to control preemption here.
-//@compile-flags: -Zmiri-preemption-rate=0
+// We want to control preemption here. Stacked borrows interferes by having its own accesses.
+//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
 
 use std::thread::spawn;
 
diff --git a/tests/fail/data_race/dealloc_read_race2.rs b/tests/fail/data_race/dealloc_read_race2.rs
index 24cce5d6fa..38f76af9de 100644
--- a/tests/fail/data_race/dealloc_read_race2.rs
+++ b/tests/fail/data_race/dealloc_read_race2.rs
@@ -1,5 +1,5 @@
-// We want to control preemption here.
-//@compile-flags: -Zmiri-preemption-rate=0
+// We want to control preemption here. Stacked borrows interferes by having its own accesses.
+//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
 
 use std::thread::spawn;
 
diff --git a/tests/fail/data_race/dealloc_read_race_stack.rs b/tests/fail/data_race/dealloc_read_race_stack.rs
index 5484370f35..665e5ce4a1 100644
--- a/tests/fail/data_race/dealloc_read_race_stack.rs
+++ b/tests/fail/data_race/dealloc_read_race_stack.rs
@@ -1,4 +1,4 @@
-//@compile-flags: -Zmiri-disable-isolation -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0
+//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
 
 use std::ptr::null_mut;
 use std::sync::atomic::{AtomicPtr, Ordering};
diff --git a/tests/fail/data_race/dealloc_write_race1.rs b/tests/fail/data_race/dealloc_write_race1.rs
index 23bf73fe8c..b36c6b5ac0 100644
--- a/tests/fail/data_race/dealloc_write_race1.rs
+++ b/tests/fail/data_race/dealloc_write_race1.rs
@@ -1,5 +1,5 @@
-// We want to control preemption here.
-//@compile-flags: -Zmiri-preemption-rate=0
+// We want to control preemption here. Stacked borrows interferes by having its own accesses.
+//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
 
 use std::thread::spawn;
 
diff --git a/tests/fail/data_race/dealloc_write_race2.rs b/tests/fail/data_race/dealloc_write_race2.rs
index 7c8033e233..4af8b90462 100644
--- a/tests/fail/data_race/dealloc_write_race2.rs
+++ b/tests/fail/data_race/dealloc_write_race2.rs
@@ -1,5 +1,5 @@
-// We want to control preemption here.
-//@compile-flags: -Zmiri-preemption-rate=0
+// We want to control preemption here. Stacked borrows interferes by having its own accesses.
+//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
 
 use std::thread::spawn;
 
diff --git a/tests/fail/data_race/dealloc_write_race_stack.rs b/tests/fail/data_race/dealloc_write_race_stack.rs
index 1872abfe02..f851ce9578 100644
--- a/tests/fail/data_race/dealloc_write_race_stack.rs
+++ b/tests/fail/data_race/dealloc_write_race_stack.rs
@@ -1,4 +1,4 @@
-//@compile-flags: -Zmiri-disable-isolation -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0
+//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
 
 use std::ptr::null_mut;
 use std::sync::atomic::{AtomicPtr, Ordering};
diff --git a/tests/fail/data_race/enable_after_join_to_main.rs b/tests/fail/data_race/enable_after_join_to_main.rs
index c11239da7f..27aa16a122 100644
--- a/tests/fail/data_race/enable_after_join_to_main.rs
+++ b/tests/fail/data_race/enable_after_join_to_main.rs
@@ -1,5 +1,5 @@
-// We want to control preemption here.
-//@compile-flags: -Zmiri-preemption-rate=0
+// We want to control preemption here. Stacked borrows interferes by having its own accesses.
+//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
 
 use std::thread::spawn;
 
diff --git a/tests/fail/data_race/fence_after_load.rs b/tests/fail/data_race/fence_after_load.rs
index ae44390859..4d436d51f9 100644
--- a/tests/fail/data_race/fence_after_load.rs
+++ b/tests/fail/data_race/fence_after_load.rs
@@ -1,5 +1,5 @@
-// We want to control preemption here.
-//@compile-flags: -Zmiri-disable-isolation -Zmiri-preemption-rate=0
+// We want to control preemption here. Stacked borrows interferes by having its own accesses.
+//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
 use std::sync::atomic::{fence, AtomicUsize, Ordering};
 use std::sync::Arc;
 use std::thread;
diff --git a/tests/fail/data_race/read_write_race.rs b/tests/fail/data_race/read_write_race.rs
index 482dd2df7d..b26ec6c414 100644
--- a/tests/fail/data_race/read_write_race.rs
+++ b/tests/fail/data_race/read_write_race.rs
@@ -1,5 +1,5 @@
-// We want to control preemption here.
-//@compile-flags: -Zmiri-preemption-rate=0
+// We want to control preemption here. Stacked borrows interferes by having its own accesses.
+//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
 
 use std::thread::spawn;
 
diff --git a/tests/fail/data_race/read_write_race_stack.rs b/tests/fail/data_race/read_write_race_stack.rs
index 1b4932439b..2fbac17399 100644
--- a/tests/fail/data_race/read_write_race_stack.rs
+++ b/tests/fail/data_race/read_write_race_stack.rs
@@ -1,4 +1,4 @@
-//@compile-flags: -Zmiri-disable-isolation -Zmir-opt-level=0 -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0
+//@compile-flags: -Zmir-opt-level=0 -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
 
 // Note: mir-opt-level set to 0 to prevent the read of stack_var in thread 1
 // from being optimized away and preventing the detection of the data-race.
diff --git a/tests/fail/data_race/relax_acquire_race.rs b/tests/fail/data_race/relax_acquire_race.rs
index 240b4c90eb..24040a9496 100644
--- a/tests/fail/data_race/relax_acquire_race.rs
+++ b/tests/fail/data_race/relax_acquire_race.rs
@@ -1,4 +1,4 @@
-//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0
+//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
 
 use std::sync::atomic::{AtomicUsize, Ordering};
 use std::thread::spawn;
diff --git a/tests/fail/data_race/release_seq_race.rs b/tests/fail/data_race/release_seq_race.rs
index 5ae8012783..2d7246858e 100644
--- a/tests/fail/data_race/release_seq_race.rs
+++ b/tests/fail/data_race/release_seq_race.rs
@@ -1,4 +1,4 @@
-//@compile-flags: -Zmiri-disable-isolation -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0
+//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
 
 use std::sync::atomic::{AtomicUsize, Ordering};
 use std::thread::{sleep, spawn};
diff --git a/tests/fail/data_race/release_seq_race_same_thread.rs b/tests/fail/data_race/release_seq_race_same_thread.rs
index 63e6dc2dd7..0f974e1c56 100644
--- a/tests/fail/data_race/release_seq_race_same_thread.rs
+++ b/tests/fail/data_race/release_seq_race_same_thread.rs
@@ -1,4 +1,4 @@
-//@compile-flags: -Zmiri-disable-isolation -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0
+//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
 
 use std::sync::atomic::{AtomicUsize, Ordering};
 use std::thread::spawn;
diff --git a/tests/fail/data_race/rmw_race.rs b/tests/fail/data_race/rmw_race.rs
index 122780d11a..2d13da30b4 100644
--- a/tests/fail/data_race/rmw_race.rs
+++ b/tests/fail/data_race/rmw_race.rs
@@ -1,4 +1,4 @@
-//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0
+//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
 
 use std::sync::atomic::{AtomicUsize, Ordering};
 use std::thread::spawn;
diff --git a/tests/fail/data_race/stack_pop_race.rs b/tests/fail/data_race/stack_pop_race.rs
index 163f46eacc..cf5c2ed81c 100644
--- a/tests/fail/data_race/stack_pop_race.rs
+++ b/tests/fail/data_race/stack_pop_race.rs
@@ -1,4 +1,4 @@
-//@compile-flags: -Zmiri-preemption-rate=0
+//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
 use std::thread;
 
 #[derive(Copy, Clone)]
diff --git a/tests/fail/data_race/write_write_race.rs b/tests/fail/data_race/write_write_race.rs
index 13c31c87cb..60e9ac2ac6 100644
--- a/tests/fail/data_race/write_write_race.rs
+++ b/tests/fail/data_race/write_write_race.rs
@@ -1,5 +1,5 @@
 // We want to control preemption here.
-//@compile-flags: -Zmiri-preemption-rate=0
+//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
 
 use std::thread::spawn;
 
diff --git a/tests/fail/data_race/write_write_race_stack.rs b/tests/fail/data_race/write_write_race_stack.rs
index 731ac8b26a..0a29dc13cb 100644
--- a/tests/fail/data_race/write_write_race_stack.rs
+++ b/tests/fail/data_race/write_write_race_stack.rs
@@ -1,4 +1,4 @@
-//@compile-flags: -Zmiri-disable-isolation -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0
+//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
 
 use std::ptr::null_mut;
 use std::sync::atomic::{AtomicPtr, Ordering};
diff --git a/tests/fail/stacked_borrows/retag_data_race_read.rs b/tests/fail/stacked_borrows/retag_data_race_read.rs
new file mode 100644
index 0000000000..309d7a22be
--- /dev/null
+++ b/tests/fail/stacked_borrows/retag_data_race_read.rs
@@ -0,0 +1,31 @@
+//! Make sure that a retag acts like a write for the data race model.
+//@compile-flags: -Zmiri-preemption-rate=0
+#[derive(Copy, Clone)]
+struct SendPtr(*mut u8);
+
+unsafe impl Send for SendPtr {}
+
+fn thread_1(p: SendPtr) {
+    let p = p.0;
+    unsafe {
+        let _r = &*p;
+    }
+}
+
+fn thread_2(p: SendPtr) {
+    let p = p.0;
+    unsafe {
+        *p = 5; //~ ERROR: Data race detected between Write on thread `<unnamed>` and Read on thread `<unnamed>`
+    }
+}
+
+fn main() {
+    let mut x = 0;
+    let p = std::ptr::addr_of_mut!(x);
+    let p = SendPtr(p);
+
+    let t1 = std::thread::spawn(move || thread_1(p));
+    let t2 = std::thread::spawn(move || thread_2(p));
+    let _ = t1.join();
+    let _ = t2.join();
+}
diff --git a/tests/fail/stacked_borrows/retag_data_race_read.stderr b/tests/fail/stacked_borrows/retag_data_race_read.stderr
new file mode 100644
index 0000000000..f25d689524
--- /dev/null
+++ b/tests/fail/stacked_borrows/retag_data_race_read.stderr
@@ -0,0 +1,20 @@
+error: Undefined Behavior: Data race detected between Write on thread `<unnamed>` and Read on thread `<unnamed>` at ALLOC
+  --> $DIR/retag_data_race_read.rs:LL:CC
+   |
+LL |         *p = 5;
+   |         ^^^^^^ Data race detected between Write on thread `<unnamed>` and Read on thread `<unnamed>` at ALLOC
+   |
+   = help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
+   = help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
+   = note: BACKTRACE:
+   = note: inside `thread_2` at $DIR/retag_data_race_read.rs:LL:CC
+note: inside closure at $DIR/retag_data_race_read.rs:LL:CC
+  --> $DIR/retag_data_race_read.rs:LL:CC
+   |
+LL |     let t2 = std::thread::spawn(move || thread_2(p));
+   |                                         ^^^^^^^^^^^
+
+note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
+
+error: aborting due to previous error
+
diff --git a/tests/fail/stacked_borrows/retag_data_race_write.rs b/tests/fail/stacked_borrows/retag_data_race_write.rs
new file mode 100644
index 0000000000..9368a0a919
--- /dev/null
+++ b/tests/fail/stacked_borrows/retag_data_race_write.rs
@@ -0,0 +1,31 @@
+//! Make sure that a retag acts like a write for the data race model.
+//@compile-flags: -Zmiri-preemption-rate=0
+#[derive(Copy, Clone)]
+struct SendPtr(*mut u8);
+
+unsafe impl Send for SendPtr {}
+
+fn thread_1(p: SendPtr) {
+    let p = p.0;
+    unsafe {
+        let _r = &mut *p;
+    }
+}
+
+fn thread_2(p: SendPtr) {
+    let p = p.0;
+    unsafe {
+        *p = 5; //~ ERROR: Data race detected between Write on thread `<unnamed>` and Write on thread `<unnamed>`
+    }
+}
+
+fn main() {
+    let mut x = 0;
+    let p = std::ptr::addr_of_mut!(x);
+    let p = SendPtr(p);
+
+    let t1 = std::thread::spawn(move || thread_1(p));
+    let t2 = std::thread::spawn(move || thread_2(p));
+    let _ = t1.join();
+    let _ = t2.join();
+}
diff --git a/tests/fail/stacked_borrows/retag_data_race_write.stderr b/tests/fail/stacked_borrows/retag_data_race_write.stderr
new file mode 100644
index 0000000000..f97e6bb11e
--- /dev/null
+++ b/tests/fail/stacked_borrows/retag_data_race_write.stderr
@@ -0,0 +1,20 @@
+error: Undefined Behavior: Data race detected between Write on thread `<unnamed>` and Write on thread `<unnamed>` at ALLOC
+  --> $DIR/retag_data_race_write.rs:LL:CC
+   |
+LL |         *p = 5;
+   |         ^^^^^^ Data race detected between Write on thread `<unnamed>` and Write on thread `<unnamed>` at ALLOC
+   |
+   = help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
+   = help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
+   = note: BACKTRACE:
+   = note: inside `thread_2` at $DIR/retag_data_race_write.rs:LL:CC
+note: inside closure at $DIR/retag_data_race_write.rs:LL:CC
+  --> $DIR/retag_data_race_write.rs:LL:CC
+   |
+LL |     let t2 = std::thread::spawn(move || thread_2(p));
+   |                                         ^^^^^^^^^^^
+
+note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
+
+error: aborting due to previous error
+

From 776460fc8dd343c1bcc772529b84f37a684cbb52 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Sun, 27 Nov 2022 00:06:00 +0100
Subject: [PATCH 4/4] nits

---
 src/stacked_borrows/mod.rs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/stacked_borrows/mod.rs b/src/stacked_borrows/mod.rs
index 5093cddfd3..f6f5c063b3 100644
--- a/src/stacked_borrows/mod.rs
+++ b/src/stacked_borrows/mod.rs
@@ -913,7 +913,7 @@ trait EvalContextPrivExt<'mir: 'ecx, 'tcx: 'mir, 'ecx>: crate::MiriInterpCxExt<'
                     })?;
                     drop(global);
                     if let Some(access) = access {
-                        assert!(access == AccessKind::Read);
+                        assert_eq!(access, AccessKind::Read);
                         // Make sure the data race model also knows about this.
                         if let Some(data_race) = alloc_extra.data_race.as_ref() {
                             data_race.read(alloc_id, range, &this.machine)?;
@@ -949,7 +949,7 @@ trait EvalContextPrivExt<'mir: 'ecx, 'tcx: 'mir, 'ecx>: crate::MiriInterpCxExt<'
         })?;
         drop(global);
         if let Some(access) = access {
-            assert!(access == AccessKind::Write);
+            assert_eq!(access, AccessKind::Write);
             // Make sure the data race model also knows about this.
             if let Some(data_race) = alloc_extra.data_race.as_mut() {
                 data_race.write(alloc_id, range, machine)?;