From 8c600ac615020a348253f32cce2b205ba309bcb0 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Sat, 26 Nov 2022 14:46:06 +0100 Subject: [PATCH] make Stacked Borrows retags act like data races --- src/stacked_borrows/mod.rs | 23 ++++++++++++-- .../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 ++++++++++++ 5 files changed, 122 insertions(+), 3 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/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 `` and Read on thread `` + } +} + +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 `` and Read on thread `` at ALLOC + --> $DIR/retag_data_race_read.rs:LL:CC + | +LL | *p = 5; + | ^^^^^^ Data race detected between Write on thread `` and Read on thread `` 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 `` and Write on thread `` + } +} + +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 `` and Write on thread `` at ALLOC + --> $DIR/retag_data_race_write.rs:LL:CC + | +LL | *p = 5; + | ^^^^^^ Data race detected between Write on thread `` and Write on thread `` 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 +