Skip to content

Commit 9b29953

Browse files
committed
Use an implicit write and disable it for functions with raw pointers in signature
1 parent 52b02f9 commit 9b29953

File tree

9 files changed

+61
-18
lines changed

9 files changed

+61
-18
lines changed

src/borrow_tracker/tree_borrows/mod.rs

Lines changed: 44 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,11 @@
11
use rustc_abi::{BackendRepr, Size};
22
use rustc_middle::mir::{Mutability, RetagKind};
33
use rustc_middle::ty::layout::HasTypingEnv;
4-
use rustc_middle::ty::{self, Ty};
4+
use rustc_middle::ty::{self, InstanceKind, Ty};
55

66
use self::foreign_access_skipping::IdempotentForeignAccess;
77
use self::tree::LocationState;
8+
use crate::borrow_tracker::tree_borrows::diagnostics::AccessCause;
89
use crate::borrow_tracker::{GlobalState, GlobalStateInner, ProtectorKind};
910
use crate::concurrency::data_race::NaReadType;
1011
use crate::*;
@@ -130,6 +131,8 @@ pub struct NewPermission {
130131
/// Whether this pointer is part of the arguments of a function call.
131132
/// `protector` is `Some(_)` for all pointers marked `noalias`.
132133
protector: Option<ProtectorKind>,
134+
/// Whether an implicit write should be performed on retag.
135+
do_a_write: bool,
133136
}
134137

135138
impl<'tcx> NewPermission {
@@ -156,6 +159,23 @@ impl<'tcx> NewPermission {
156159
.get_tree_borrows_params()
157160
.start_mut_ref_on_fn_entry_as_active;
158161

162+
let current_function_involves_raw_pointers = 'b: {
163+
let instance = cx
164+
.machine
165+
.threads
166+
.active_thread_stack()
167+
.last()
168+
.expect("Current frame has no stack")
169+
.instance();
170+
let ty = instance.ty(*cx.tcx, cx.typing_env());
171+
if !ty.is_fn() {
172+
break 'b false;
173+
}
174+
let sig = ty.fn_sig(*cx.tcx);
175+
matches!(instance.def, InstanceKind::Item(_))
176+
&& sig.inputs_and_output().skip_binder().iter().any(|x| x.is_raw_ptr())
177+
};
178+
159179
if matches!(ref_mutability, Some(Mutability::Mut) | None if !ty_is_unpin) {
160180
// Mutable reference / Box to pinning type: retagging is a NOP.
161181
// FIXME: with `UnsafePinned`, this should do proper per-byte tracking.
@@ -165,9 +185,6 @@ impl<'tcx> NewPermission {
165185
let freeze_perm = match ref_mutability {
166186
// Shared references are frozen.
167187
Some(Mutability::Not) => Permission::new_frozen(),
168-
// Mutable references on fn entry are activated based on config
169-
Some(Mutability::Mut) if start_mut_ref_on_fn_entry_as_active && is_protected =>
170-
Permission::new_active(),
171188
// Mutable references and Boxes are reserved.
172189
_ => Permission::new_reserved_frz(),
173190
};
@@ -196,6 +213,10 @@ impl<'tcx> NewPermission {
196213
// Weak protector for boxes
197214
ProtectorKind::WeakProtector
198215
}),
216+
do_a_write: start_mut_ref_on_fn_entry_as_active
217+
&& is_protected
218+
&& !current_function_involves_raw_pointers
219+
&& matches!(ref_mutability, Some(Mutability::Mut)),
199220
})
200221
}
201222
}
@@ -396,11 +417,28 @@ trait EvalContextPrivExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
396417
base_offset,
397418
orig_tag,
398419
new_tag,
399-
inside_perms,
420+
inside_perms.clone(),
400421
new_perm.outside_perm,
401422
protected,
402423
this.machine.current_span(),
403424
)?;
425+
if new_perm.do_a_write {
426+
for (perm_range, _) in inside_perms.iter_all() {
427+
// Some reborrows incur a write access to the new pointer, to make it active.
428+
// Adjust range to be relative to allocation start (rather than to `place`).
429+
let range_in_alloc = AllocRange {
430+
start: Size::from_bytes(perm_range.start) + base_offset,
431+
size: Size::from_bytes(perm_range.end - perm_range.start),
432+
};
433+
tree_borrows.perform_access(
434+
new_tag,
435+
Some((range_in_alloc, AccessKind::Write, AccessCause::Reborrow)),
436+
this.machine.borrow_tracker.as_ref().unwrap(),
437+
alloc_id,
438+
this.machine.current_span(),
439+
)?;
440+
}
441+
}
404442
drop(tree_borrows);
405443

406444
interp_ok(Some(Provenance::Concrete { alloc_id, tag: new_tag }))
@@ -600,6 +638,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
600638
nonfreeze_access: true,
601639
outside_perm: Permission::new_reserved_frz(),
602640
protector: Some(ProtectorKind::StrongProtector),
641+
do_a_write: false,
603642
};
604643
this.tb_retag_place(place, new_perm)
605644
}

src/borrow_tracker/tree_borrows/perms.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -90,7 +90,7 @@ impl PartialOrd for PermissionPriv {
9090
impl PermissionPriv {
9191
/// Check if `self` can be the initial state of a pointer.
9292
fn is_initial(&self) -> bool {
93-
matches!(self, ReservedFrz { conflicted: false } | Frozen | ReservedIM | Cell | Active)
93+
matches!(self, ReservedFrz { conflicted: false } | Frozen | ReservedIM | Cell)
9494
}
9595

9696
/// Reject `ReservedIM` that cannot exist in the presence of a protector.

tests/fail/both_borrows/spurious_write_may_be_added.tree.stderr

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -12,11 +12,11 @@ help: the accessed tag <TAG> was created here, in the initial state Frozen
1212
|
1313
LL | let target_alias = &*target;
1414
| ^^^^^^^^
15-
help: the accessed tag <TAG> later transitioned to Disabled due to a protector release (acting as a foreign write access) on every location previously accessed by this tag
15+
help: the accessed tag <TAG> later transitioned to Disabled due to a reborrow (acting as a foreign read access) at offsets [0x0..0x4]
1616
--> tests/fail/both_borrows/spurious_write_may_be_added.rs:LL:CC
1717
|
1818
LL | fn may_insert_spurious_write(_x: &mut u32) {}
19-
| ^
19+
| ^^
2020
= help: this transition corresponds to a loss of read permissions
2121
= note: BACKTRACE (of the first span):
2222
= note: inside `main` at tests/fail/both_borrows/spurious_write_may_be_added.rs:LL:CC

tests/fail/both_borrows/spurious_write_may_be_added_data_race.tree.stderr

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -8,19 +8,18 @@ LL | let _val = unsafe { *ptr.0 };
88
|
99
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
1010
= help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/tree-borrows.md for further information
11-
= help: the accessed tag <TAG> is foreign to the protected tag <TAG> (i.e., it is not a child)
12-
= help: this foreign read access would cause the protected tag <TAG> (currently Active) to become Disabled
13-
= help: protected tags must never be Disabled
14-
help: the accessed tag <TAG> was created here
11+
= help: the accessed tag <TAG> has state Disabled which forbids this child read access
12+
help: the accessed tag <TAG> was created here, in the initial state Frozen
1513
--> tests/fail/both_borrows/spurious_write_may_be_added_data_race.rs:LL:CC
1614
|
1715
LL | let target_alias = &*target;
1816
| ^^^^^^^^
19-
help: the protected tag <TAG> was created here, in the initial state Active
17+
help: the accessed tag <TAG> later transitioned to Disabled due to a reborrow (acting as a foreign read access) at offsets [0x0..0x4]
2018
--> tests/fail/both_borrows/spurious_write_may_be_added_data_race.rs:LL:CC
2119
|
2220
LL | fn may_insert_spurious_write(_x: &mut u32, b: IdxBarrier) {
2321
| ^^
22+
= help: this transition corresponds to a loss of read permissions
2423
= note: BACKTRACE (of the first span) on thread `unnamed-ID`:
2524
= note: inside closure at tests/fail/both_borrows/spurious_write_may_be_added_data_race.rs:LL:CC
2625

tests/pass/both_borrows/2phase.rs

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
1-
//@revisions: stack tree
1+
//@revisions: stack tree tree_strong
22
//@[tree]compile-flags: -Zmiri-tree-borrows
3+
//@[tree_strong]compile-flags: -Zmiri-tree-borrows-strong
34

45
trait S: Sized {
56
fn tpb(&mut self, _s: Self) {}

tests/pass/both_borrows/basic_aliasing_model.rs

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
1-
//@revisions: stack tree
1+
//@revisions: stack tree tree_strong
22
//@[tree]compile-flags: -Zmiri-tree-borrows
3+
//@[tree_strong]compile-flags: -Zmiri-tree-borrows-strong
34
#![feature(allocator_api)]
45
use std::alloc::{Layout, alloc, dealloc};
56
use std::cell::Cell;

tests/pass/both_borrows/interior_mutability.rs

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
1-
//@revisions: stack tree
1+
//@revisions: stack tree tree_strong
22
//@[tree]compile-flags: -Zmiri-tree-borrows
3+
//@[tree_strong]compile-flags: -Zmiri-tree-borrows-strong
34
#![allow(dangerous_implicit_autorefs)]
45

56
use std::cell::{Cell, Ref, RefCell, RefMut, UnsafeCell};

tests/pass/both_borrows/smallvec.rs

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,9 @@
22
//! What makes it interesting as a test is that it relies on Stacked Borrow's "quirk"
33
//! in a fundamental, hard-to-fix-without-full-trees way.
44
5-
//@revisions: stack tree
5+
//@revisions: stack tree tree_strong
66
//@[tree]compile-flags: -Zmiri-tree-borrows
7+
//@[tree_strong]compile-flags: -Zmiri-tree-borrows-strong
78

89
use std::marker::PhantomData;
910
use std::mem::{ManuallyDrop, MaybeUninit};

tests/pass/both_borrows/unsafe_pinned.rs

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
1-
//@revisions: stack tree
1+
//@revisions: stack tree tree_strong
22
//@[tree]compile-flags: -Zmiri-tree-borrows
3+
//@[tree_strong]compile-flags: -Zmiri-tree-borrows-strong
34
#![feature(unsafe_pinned)]
45

56
use std::pin::UnsafePinned;

0 commit comments

Comments
 (0)