diff options
32 files changed, 164 insertions, 45 deletions
diff --git a/src/tools/miri/src/stacked_borrows/mod.rs b/src/tools/miri/src/stacked_borrows/mod.rs index e412f645066..5093cddfd3b 100644 --- a/src/tools/miri/src/stacked_borrows/mod.rs +++ b/src/tools/miri/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/src/tools/miri/tests/fail/data_race/alloc_read_race.rs b/src/tools/miri/tests/fail/data_race/alloc_read_race.rs index 0bd3068af1f..6040452a166 100644 --- a/src/tools/miri/tests/fail/data_race/alloc_read_race.rs +++ b/src/tools/miri/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/src/tools/miri/tests/fail/data_race/alloc_write_race.rs b/src/tools/miri/tests/fail/data_race/alloc_write_race.rs index 7991280721e..51d431b36f3 100644 --- a/src/tools/miri/tests/fail/data_race/alloc_write_race.rs +++ b/src/tools/miri/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/src/tools/miri/tests/fail/data_race/atomic_read_na_write_race1.rs b/src/tools/miri/tests/fail/data_race/atomic_read_na_write_race1.rs index 2b0446d724a..79c6760b7c4 100644 --- a/src/tools/miri/tests/fail/data_race/atomic_read_na_write_race1.rs +++ b/src/tools/miri/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/src/tools/miri/tests/fail/data_race/atomic_read_na_write_race2.rs b/src/tools/miri/tests/fail/data_race/atomic_read_na_write_race2.rs index ef5157515c6..e069ac4ad6a 100644 --- a/src/tools/miri/tests/fail/data_race/atomic_read_na_write_race2.rs +++ b/src/tools/miri/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/src/tools/miri/tests/fail/data_race/atomic_write_na_read_race1.rs b/src/tools/miri/tests/fail/data_race/atomic_write_na_read_race1.rs index 8c17e767484..9c025a0153d 100644 --- a/src/tools/miri/tests/fail/data_race/atomic_write_na_read_race1.rs +++ b/src/tools/miri/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/src/tools/miri/tests/fail/data_race/atomic_write_na_read_race2.rs b/src/tools/miri/tests/fail/data_race/atomic_write_na_read_race2.rs index f14d7c704db..30b3c486374 100644 --- a/src/tools/miri/tests/fail/data_race/atomic_write_na_read_race2.rs +++ b/src/tools/miri/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/src/tools/miri/tests/fail/data_race/atomic_write_na_write_race1.rs b/src/tools/miri/tests/fail/data_race/atomic_write_na_write_race1.rs index 0804b334075..02b17cc57b6 100644 --- a/src/tools/miri/tests/fail/data_race/atomic_write_na_write_race1.rs +++ b/src/tools/miri/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/src/tools/miri/tests/fail/data_race/atomic_write_na_write_race2.rs b/src/tools/miri/tests/fail/data_race/atomic_write_na_write_race2.rs index 658cddcc9c5..b5f4966d884 100644 --- a/src/tools/miri/tests/fail/data_race/atomic_write_na_write_race2.rs +++ b/src/tools/miri/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/src/tools/miri/tests/fail/data_race/dangling_thread_async_race.rs b/src/tools/miri/tests/fail/data_race/dangling_thread_async_race.rs index af2588e9232..9922468e5f8 100644 --- a/src/tools/miri/tests/fail/data_race/dangling_thread_async_race.rs +++ b/src/tools/miri/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/src/tools/miri/tests/fail/data_race/dangling_thread_race.rs b/src/tools/miri/tests/fail/data_race/dangling_thread_race.rs index 1ee619c3f99..8c8a6ac87f3 100644 --- a/src/tools/miri/tests/fail/data_race/dangling_thread_race.rs +++ b/src/tools/miri/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/src/tools/miri/tests/fail/data_race/dealloc_read_race1.rs b/src/tools/miri/tests/fail/data_race/dealloc_read_race1.rs index cbc02549a25..8e1216f5bf0 100644 --- a/src/tools/miri/tests/fail/data_race/dealloc_read_race1.rs +++ b/src/tools/miri/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/src/tools/miri/tests/fail/data_race/dealloc_read_race2.rs b/src/tools/miri/tests/fail/data_race/dealloc_read_race2.rs index 24cce5d6fac..38f76af9de1 100644 --- a/src/tools/miri/tests/fail/data_race/dealloc_read_race2.rs +++ b/src/tools/miri/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/src/tools/miri/tests/fail/data_race/dealloc_read_race_stack.rs b/src/tools/miri/tests/fail/data_race/dealloc_read_race_stack.rs index 5484370f35c..665e5ce4a17 100644 --- a/src/tools/miri/tests/fail/data_race/dealloc_read_race_stack.rs +++ b/src/tools/miri/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/src/tools/miri/tests/fail/data_race/dealloc_write_race1.rs b/src/tools/miri/tests/fail/data_race/dealloc_write_race1.rs index 23bf73fe8c5..b36c6b5ac0e 100644 --- a/src/tools/miri/tests/fail/data_race/dealloc_write_race1.rs +++ b/src/tools/miri/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/src/tools/miri/tests/fail/data_race/dealloc_write_race2.rs b/src/tools/miri/tests/fail/data_race/dealloc_write_race2.rs index 7c8033e2335..4af8b904626 100644 --- a/src/tools/miri/tests/fail/data_race/dealloc_write_race2.rs +++ b/src/tools/miri/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/src/tools/miri/tests/fail/data_race/dealloc_write_race_stack.rs b/src/tools/miri/tests/fail/data_race/dealloc_write_race_stack.rs index 1872abfe021..f851ce95785 100644 --- a/src/tools/miri/tests/fail/data_race/dealloc_write_race_stack.rs +++ b/src/tools/miri/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/src/tools/miri/tests/fail/data_race/enable_after_join_to_main.rs b/src/tools/miri/tests/fail/data_race/enable_after_join_to_main.rs index c11239da7fe..27aa16a122f 100644 --- a/src/tools/miri/tests/fail/data_race/enable_after_join_to_main.rs +++ b/src/tools/miri/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/src/tools/miri/tests/fail/data_race/fence_after_load.rs b/src/tools/miri/tests/fail/data_race/fence_after_load.rs index ae443908598..4d436d51f98 100644 --- a/src/tools/miri/tests/fail/data_race/fence_after_load.rs +++ b/src/tools/miri/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/src/tools/miri/tests/fail/data_race/read_write_race.rs b/src/tools/miri/tests/fail/data_race/read_write_race.rs index 482dd2df7df..b26ec6c4142 100644 --- a/src/tools/miri/tests/fail/data_race/read_write_race.rs +++ b/src/tools/miri/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/src/tools/miri/tests/fail/data_race/read_write_race_stack.rs b/src/tools/miri/tests/fail/data_race/read_write_race_stack.rs index 1b4932439b0..2fbac173993 100644 --- a/src/tools/miri/tests/fail/data_race/read_write_race_stack.rs +++ b/src/tools/miri/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/src/tools/miri/tests/fail/data_race/relax_acquire_race.rs b/src/tools/miri/tests/fail/data_race/relax_acquire_race.rs index 240b4c90eb2..24040a94961 100644 --- a/src/tools/miri/tests/fail/data_race/relax_acquire_race.rs +++ b/src/tools/miri/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/src/tools/miri/tests/fail/data_race/release_seq_race.rs b/src/tools/miri/tests/fail/data_race/release_seq_race.rs index 5ae80127835..2d7246858e1 100644 --- a/src/tools/miri/tests/fail/data_race/release_seq_race.rs +++ b/src/tools/miri/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/src/tools/miri/tests/fail/data_race/release_seq_race_same_thread.rs b/src/tools/miri/tests/fail/data_race/release_seq_race_same_thread.rs index 63e6dc2dd71..0f974e1c56d 100644 --- a/src/tools/miri/tests/fail/data_race/release_seq_race_same_thread.rs +++ b/src/tools/miri/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/src/tools/miri/tests/fail/data_race/rmw_race.rs b/src/tools/miri/tests/fail/data_race/rmw_race.rs index 122780d11aa..2d13da30b46 100644 --- a/src/tools/miri/tests/fail/data_race/rmw_race.rs +++ b/src/tools/miri/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/src/tools/miri/tests/fail/data_race/stack_pop_race.rs b/src/tools/miri/tests/fail/data_race/stack_pop_race.rs index 163f46eacc1..cf5c2ed81cb 100644 --- a/src/tools/miri/tests/fail/data_race/stack_pop_race.rs +++ b/src/tools/miri/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/src/tools/miri/tests/fail/data_race/write_write_race.rs b/src/tools/miri/tests/fail/data_race/write_write_race.rs index 13c31c87cbb..60e9ac2ac6c 100644 --- a/src/tools/miri/tests/fail/data_race/write_write_race.rs +++ b/src/tools/miri/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/src/tools/miri/tests/fail/data_race/write_write_race_stack.rs b/src/tools/miri/tests/fail/data_race/write_write_race_stack.rs index 731ac8b26aa..0a29dc13cba 100644 --- a/src/tools/miri/tests/fail/data_race/write_write_race_stack.rs +++ b/src/tools/miri/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/src/tools/miri/tests/fail/stacked_borrows/retag_data_race_read.rs b/src/tools/miri/tests/fail/stacked_borrows/retag_data_race_read.rs new file mode 100644 index 00000000000..309d7a22be6 --- /dev/null +++ b/src/tools/miri/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/src/tools/miri/tests/fail/stacked_borrows/retag_data_race_read.stderr b/src/tools/miri/tests/fail/stacked_borrows/retag_data_race_read.stderr new file mode 100644 index 00000000000..f25d689524d --- /dev/null +++ b/src/tools/miri/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/src/tools/miri/tests/fail/stacked_borrows/retag_data_race_write.rs b/src/tools/miri/tests/fail/stacked_borrows/retag_data_race_write.rs new file mode 100644 index 00000000000..9368a0a919e --- /dev/null +++ b/src/tools/miri/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/src/tools/miri/tests/fail/stacked_borrows/retag_data_race_write.stderr b/src/tools/miri/tests/fail/stacked_borrows/retag_data_race_write.stderr new file mode 100644 index 00000000000..f97e6bb11e9 --- /dev/null +++ b/src/tools/miri/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 + |