make Stacked Borrows retags act like data races

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))
     }

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;

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;

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;

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;

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;

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;

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;

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;

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};

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};

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;
 

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;
 

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};

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;
 

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;
 

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};

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;
 

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;

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;
 

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.

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;

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};

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;

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;

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)]

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;
 

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};

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();
+}

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
+

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();
+}

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
+