Skip to content

Commit e637e42

Browse files
authored
Merge pull request #4947 from quiode/tb-strong-mode
tree borrows: implicit writes
2 parents a87cc71 + 8a513be commit e637e42

104 files changed

Lines changed: 1013 additions & 128 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

src/tools/miri/README.md

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -511,6 +511,8 @@ to Miri failing to detect cases of undefined behavior in a program.
511511
of Rust will be stricter than Tree Borrows. In other words, if you use Tree Borrows,
512512
even if your code is accepted today, it might be declared UB in the future.
513513
This is much less likely with Stacked Borrows.
514+
* `-Zmiri-tree-borrows-implicit-writes` enables implicit writes for all `&mut` function arguments.
515+
This makes Tree Borrows less permissive.
514516
* `-Zmiri-tree-borrows-no-precise-interior-mut` makes Tree Borrows
515517
track interior mutable data on the level of references instead of on the
516518
byte-level as is done by default. Therefore, with this flag, Tree

src/tools/miri/src/bin/miri.rs

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -515,6 +515,7 @@ fn main() -> ExitCode {
515515
miri_config.borrow_tracker =
516516
Some(BorrowTrackerMethod::TreeBorrows(TreeBorrowsParams {
517517
precise_interior_mut: true,
518+
implicit_writes: false,
518519
}));
519520
} else if arg == "-Zmiri-tree-borrows-no-precise-interior-mut" {
520521
match &mut miri_config.borrow_tracker {
@@ -526,6 +527,16 @@ fn main() -> ExitCode {
526527
"`-Zmiri-tree-borrows` is required before `-Zmiri-tree-borrows-no-precise-interior-mut`"
527528
),
528529
};
530+
} else if arg == "-Zmiri-tree-borrows-implicit-writes" {
531+
match &mut miri_config.borrow_tracker {
532+
Some(BorrowTrackerMethod::TreeBorrows(params)) => {
533+
params.implicit_writes = true;
534+
}
535+
_ =>
536+
fatal_error!(
537+
"`-Zmiri-tree-borrows` is required before `-Zmiri-tree-borrows-implicit-writes`"
538+
),
539+
};
529540
} else if arg == "-Zmiri-disable-data-race-detector" {
530541
miri_config.data_race_detector = false;
531542
miri_config.weak_memory_emulation = false;

src/tools/miri/src/borrow_tracker/mod.rs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -224,6 +224,8 @@ pub enum BorrowTrackerMethod {
224224
#[derive(Debug, Copy, Clone, PartialEq, Eq)]
225225
pub struct TreeBorrowsParams {
226226
pub precise_interior_mut: bool,
227+
/// Controls whether `&mut` function arguments are immediately activated with an implicit write.
228+
pub implicit_writes: bool,
227229
}
228230

229231
impl BorrowTrackerMethod {

src/tools/miri/src/borrow_tracker/tree_borrows/diagnostics.rs

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ use crate::*;
1515
#[derive(Clone, Copy, Debug)]
1616
pub enum AccessCause {
1717
Explicit(AccessKind),
18-
Reborrow,
18+
Reborrow(AccessKind),
1919
Dealloc,
2020
FnExit(AccessKind),
2121
}
@@ -24,7 +24,7 @@ impl fmt::Display for AccessCause {
2424
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
2525
match self {
2626
Self::Explicit(kind) => write!(f, "{kind}"),
27-
Self::Reborrow => write!(f, "reborrow"),
27+
Self::Reborrow(_) => write!(f, "reborrow"),
2828
Self::Dealloc => write!(f, "deallocation"),
2929
// This is dead code, since the protector release access itself can never
3030
// cause UB (while the protector is active, if some other access invalidates
@@ -40,7 +40,7 @@ impl AccessCause {
4040
let rel = if is_foreign { "foreign" } else { "child" };
4141
match self {
4242
Self::Explicit(kind) => format!("{rel} {kind}"),
43-
Self::Reborrow => format!("reborrow (acting as a {rel} read access)"),
43+
Self::Reborrow(kind) => format!("reborrow (acting as a {rel} {kind})"),
4444
Self::Dealloc => format!("deallocation (acting as a {rel} write access)"),
4545
Self::FnExit(kind) => format!("protector release (acting as a {rel} {kind})"),
4646
}

src/tools/miri/src/borrow_tracker/tree_borrows/mod.rs

Lines changed: 102 additions & 51 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ use rustc_middle::ty::{self, Ty};
66
use self::foreign_access_skipping::IdempotentForeignAccess;
77
use self::tree::LocationState;
88
use crate::borrow_tracker::{AccessKind, GlobalState, GlobalStateInner, ProtectorKind};
9-
use crate::concurrency::data_race::NaReadType;
9+
use crate::concurrency::data_race::{NaReadType, NaWriteType};
1010
use crate::*;
1111

1212
pub mod diagnostics;
@@ -109,13 +109,8 @@ impl<'tcx> Tree {
109109
pub struct NewPermission {
110110
/// Permission for the frozen part of the range.
111111
freeze_perm: Permission,
112-
/// Whether a read access should be performed on the frozen part on a retag.
113-
freeze_access: bool,
114112
/// Permission for the non-frozen part of the range.
115113
nonfreeze_perm: Permission,
116-
/// Whether a read access should be performed on the non-frozen
117-
/// part on a retag.
118-
nonfreeze_access: bool,
119114
/// Permission for memory outside the range.
120115
outside_perm: Permission,
121116
/// Whether this pointer is part of the arguments of a function call.
@@ -138,36 +133,78 @@ impl<'tcx> NewPermission {
138133
let ty_is_freeze = pointee.is_freeze(*cx.tcx, cx.typing_env());
139134
let is_protected = retag_kind == RetagKind::FnEntry;
140135

136+
// Check if the implicit writes check has been enabled for this function using the `-Zmiri-tree-borrows-implicit-writes` flag
137+
let implicit_writes = cx
138+
.machine
139+
.borrow_tracker
140+
.as_ref()
141+
.unwrap()
142+
.borrow()
143+
.borrow_tracker_method
144+
.get_tree_borrows_params()
145+
.implicit_writes;
146+
141147
if matches!(ref_mutability, Some(Mutability::Mut) | None if !ty_is_unpin) {
142148
// Mutable reference / Box to pinning type: retagging is a NOP.
143149
// FIXME: with `UnsafePinned`, this should do proper per-byte tracking.
144150
return None;
145151
}
146152

147-
let freeze_perm = match ref_mutability {
148-
// Shared references are frozen.
149-
Some(Mutability::Not) => Permission::new_frozen(),
150-
// Mutable references and Boxes are reserved.
151-
_ => Permission::new_reserved_frz(),
152-
};
153-
let nonfreeze_perm = match ref_mutability {
154-
// Shared references are "transparent".
155-
Some(Mutability::Not) => Permission::new_cell(),
156-
// *Protected* mutable references and boxes are reserved without regarding for interior mutability.
157-
_ if is_protected => Permission::new_reserved_frz(),
158-
// Unprotected mutable references and boxes start in `ReservedIm`.
159-
_ => Permission::new_reserved_im(),
153+
enum Part {
154+
InsideFrozen,
155+
InsideUnsafeCell,
156+
Outside,
157+
}
158+
use Part::*;
159+
160+
let perm = |part: Part| {
161+
// Whether we should consider this byte to be frozen.
162+
// Outside bytes are frozen only if the entire type is frozen.
163+
let frozen = match part {
164+
InsideFrozen => true,
165+
InsideUnsafeCell => false,
166+
Outside => ty_is_freeze,
167+
};
168+
match ref_mutability {
169+
// Shared references
170+
Some(Mutability::Not) =>
171+
if frozen {
172+
Permission::new_frozen()
173+
} else {
174+
Permission::new_cell()
175+
},
176+
// Mutable references
177+
Some(Mutability::Mut) => {
178+
if is_protected && implicit_writes && !matches!(part, Outside) {
179+
// We cannot use `Unique` for the outside part.
180+
Permission::new_unique()
181+
} else if is_protected || frozen {
182+
// We also use this for protected `&mut UnsafeCell` as otherwise adding
183+
// `noalias` would not be sound.
184+
Permission::new_reserved_frz()
185+
} else {
186+
Permission::new_reserved_im()
187+
}
188+
}
189+
// Boxes
190+
None =>
191+
if is_protected && implicit_writes && !matches!(part, Outside) {
192+
// Boxes are treated the same as mutable references.
193+
Permission::new_unique()
194+
} else if is_protected || frozen {
195+
// We also use this for protected `Box<UnsafeCell>` as otherwise adding
196+
// `noalias` would not be sound.
197+
Permission::new_reserved_frz()
198+
} else {
199+
Permission::new_reserved_im()
200+
},
201+
}
160202
};
161203

162-
// Everything except for `Cell` gets an initial access.
163-
let initial_access = |perm: &Permission| !perm.is_cell();
164-
165204
Some(NewPermission {
166-
freeze_perm,
167-
freeze_access: initial_access(&freeze_perm),
168-
nonfreeze_perm,
169-
nonfreeze_access: initial_access(&nonfreeze_perm),
170-
outside_perm: if ty_is_freeze { freeze_perm } else { nonfreeze_perm },
205+
freeze_perm: perm(InsideFrozen),
206+
nonfreeze_perm: perm(InsideUnsafeCell),
207+
outside_perm: perm(Outside),
171208
protector: is_protected.then_some(if ref_mutability.is_some() {
172209
// Strong protector for references
173210
ProtectorKind::StrongProtector
@@ -288,13 +325,10 @@ trait EvalContextPrivExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
288325

289326
// Compute initial "inside" permissions.
290327
let loc_state = |frozen: bool| -> LocationState {
291-
let (perm, access) = if frozen {
292-
(new_perm.freeze_perm, new_perm.freeze_access)
293-
} else {
294-
(new_perm.nonfreeze_perm, new_perm.nonfreeze_access)
295-
};
328+
let perm = if frozen { new_perm.freeze_perm } else { new_perm.nonfreeze_perm };
296329
let sifa = perm.strongest_idempotent_foreign_access(protected);
297-
if access {
330+
331+
if perm.associated_access().is_some() {
298332
LocationState::new_accessed(perm, sifa)
299333
} else {
300334
LocationState::new_non_accessed(perm, sifa)
@@ -303,11 +337,10 @@ trait EvalContextPrivExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
303337
let inside_perms = if !precise_interior_mut {
304338
// For `!Freeze` types, just pretend the entire thing is an `UnsafeCell`.
305339
let ty_is_freeze = place.layout.ty.is_freeze(*this.tcx, this.typing_env());
306-
let state = loc_state(ty_is_freeze);
307-
DedupRangeMap::new(ptr_size, state)
340+
DedupRangeMap::new(ptr_size, loc_state(ty_is_freeze))
308341
} else {
309342
// The initial state will be overwritten by the visitor below.
310-
let mut perms_map: DedupRangeMap<LocationState> = DedupRangeMap::new(
343+
let mut perms_map = DedupRangeMap::new(
311344
ptr_size,
312345
LocationState::new_accessed(
313346
Permission::new_disabled(),
@@ -327,9 +360,18 @@ trait EvalContextPrivExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
327360
let alloc_extra = this.get_alloc_extra(alloc_id)?;
328361
let mut tree_borrows = alloc_extra.borrow_tracker_tb().borrow_mut();
329362

330-
for (perm_range, perm) in inside_perms.iter_all() {
331-
if perm.accessed() {
332-
// Some reborrows incur a read access to the parent.
363+
for (perm_range, loc_state) in inside_perms.iter_all() {
364+
if let Some(access) = loc_state.permission().associated_access() {
365+
// Some reborrows incur a read/write access to the parent.
366+
// As a write also implies a read, a single write is performed instead of a read and a write.
367+
368+
// writing to an immutable allocation (static variables) is UB, check this here
369+
if access == AccessKind::Write
370+
&& this.get_alloc_mutability(alloc_id).unwrap().is_not()
371+
{
372+
throw_ub!(WriteToReadOnly(alloc_id))
373+
}
374+
333375
// Adjust range to be relative to allocation start (rather than to `place`).
334376
let range_in_alloc = AllocRange {
335377
start: Size::from_bytes(perm_range.start) + base_offset,
@@ -339,8 +381,8 @@ trait EvalContextPrivExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
339381
tree_borrows.perform_access(
340382
parent_prov,
341383
range_in_alloc,
342-
AccessKind::Read,
343-
diagnostics::AccessCause::Reborrow,
384+
access,
385+
diagnostics::AccessCause::Reborrow(access),
344386
this.machine.borrow_tracker.as_ref().unwrap(),
345387
alloc_id,
346388
this.machine.current_user_relevant_span(),
@@ -349,17 +391,29 @@ trait EvalContextPrivExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
349391
// Also inform the data race model (but only if any bytes are actually affected).
350392
if range_in_alloc.size.bytes() > 0 {
351393
if let Some(data_race) = alloc_extra.data_race.as_vclocks_ref() {
352-
data_race.read_non_atomic(
353-
alloc_id,
354-
range_in_alloc,
355-
NaReadType::Retag,
356-
Some(place.layout.ty),
357-
&this.machine,
358-
)?
394+
match access {
395+
AccessKind::Read =>
396+
data_race.read_non_atomic(
397+
alloc_id,
398+
range_in_alloc,
399+
NaReadType::Retag,
400+
Some(place.layout.ty),
401+
&this.machine,
402+
)?,
403+
AccessKind::Write =>
404+
data_race.write_non_atomic(
405+
alloc_id,
406+
range_in_alloc,
407+
NaWriteType::Retag,
408+
Some(place.layout.ty),
409+
&this.machine,
410+
)?,
411+
};
359412
}
360413
}
361414
}
362415
}
416+
363417
// Record the parent-child pair in the tree.
364418
tree_borrows.new_child(
365419
base_offset,
@@ -370,7 +424,6 @@ trait EvalContextPrivExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
370424
protected,
371425
this.machine.current_user_relevant_span(),
372426
)?;
373-
drop(tree_borrows);
374427

375428
interp_ok(Some(new_prov))
376429
}
@@ -550,9 +603,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
550603
// argument doesn't matter
551604
// (`ty_is_freeze || true` in `new_reserved` will always be `true`).
552605
freeze_perm: Permission::new_reserved_frz(),
553-
freeze_access: true,
554606
nonfreeze_perm: Permission::new_reserved_frz(),
555-
nonfreeze_access: true,
556607
outside_perm: Permission::new_reserved_frz(),
557608
protector: Some(ProtectorKind::StrongProtector),
558609
};

src/tools/miri/src/borrow_tracker/tree_borrows/perms.rs

Lines changed: 10 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -91,7 +91,7 @@ impl PartialOrd for PermissionPriv {
9191
impl PermissionPriv {
9292
/// Check if `self` can be the initial state of a pointer.
9393
fn is_initial(&self) -> bool {
94-
matches!(self, ReservedFrz { conflicted: false } | Frozen | ReservedIM | Cell)
94+
matches!(self, ReservedFrz { conflicted: false } | Frozen | ReservedIM | Cell | Unique)
9595
}
9696

9797
/// Reject `ReservedIM` that cannot exist in the presence of a protector.
@@ -265,14 +265,17 @@ impl Permission {
265265
self.inner == Cell
266266
}
267267

268-
/// Default initial permission of the root of a new tree at inbounds positions.
269-
/// Must *only* be used for the root, this is not in general an "initial" permission!
268+
/// Check if `self` is a Permission of type `Unique`
269+
pub fn is_unique(&self) -> bool {
270+
self.inner == Unique
271+
}
272+
273+
/// Create a new Permission of type `Unique`
270274
pub fn new_unique() -> Self {
271275
Self { inner: Unique }
272276
}
273277

274-
/// Default initial permission of a reborrowed mutable reference that is either
275-
/// protected or not interior mutable.
278+
/// Create a new Permission of type `ReservedFrz` with conflictedReserved set to false
276279
pub fn new_reserved_frz() -> Self {
277280
Self { inner: ReservedFrz { conflicted: false } }
278281
}
@@ -304,8 +307,8 @@ impl Permission {
304307
self.inner.compatible_with_protector()
305308
}
306309

307-
/// What kind of access to perform before releasing the protector.
308-
pub fn protector_end_access(&self) -> Option<AccessKind> {
310+
/// What kind of access to perform before releasing the protector or on a reborrow.
311+
pub fn associated_access(&self) -> Option<AccessKind> {
309312
match self.inner {
310313
// Do not do perform access if it is a `Cell`, as this
311314
// can cause data races when using thread-safe data types.

src/tools/miri/src/borrow_tracker/tree_borrows/tree.rs

Lines changed: 10 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -63,6 +63,7 @@ impl LocationState {
6363
/// `sifa` is the (strongest) idempotent foreign access, see `foreign_access_skipping.rs`
6464
pub fn new_non_accessed(permission: Permission, sifa: IdempotentForeignAccess) -> Self {
6565
assert!(permission.is_initial() || permission.is_disabled());
66+
assert!(!permission.is_unique());
6667
Self { permission, accessed: false, idempotent_foreign_access: sifa }
6768
}
6869

@@ -73,6 +74,12 @@ impl LocationState {
7374
Self { permission, accessed: true, idempotent_foreign_access: sifa }
7475
}
7576

77+
/// Checks whether the current location state is ever reachable in a real execution.
78+
pub fn possible(&self) -> bool {
79+
// `Unique` can only be reached on actually accessed locations.
80+
self.accessed || !self.permission.is_unique()
81+
}
82+
7683
/// Check if the location has been accessed, i.e. if it has
7784
/// ever been accessed through a child pointer.
7885
pub fn accessed(&self) -> bool {
@@ -150,6 +157,7 @@ impl LocationState {
150157
if protected && self.accessed && transition.produces_disabled() {
151158
return Err(TransitionError::ProtectedDisabled(old_perm));
152159
}
160+
debug_assert!(self.possible());
153161
Ok(transition)
154162
}
155163

@@ -397,6 +405,7 @@ impl<'tcx> Tree {
397405
ProvenanceExtra::Wildcard => None,
398406
};
399407
assert!(outside_perm.is_initial());
408+
assert!(!outside_perm.is_unique());
400409

401410
let default_strongest_idempotent =
402411
outside_perm.strongest_idempotent_foreign_access(protected);
@@ -690,7 +699,7 @@ impl<'tcx> Tree {
690699
for (loc_range, loc) in self.locations.iter_mut_all() {
691700
// Only visit accessed permissions
692701
if let Some(p) = loc.perms.get(source_idx)
693-
&& let Some(access_kind) = p.permission.protector_end_access()
702+
&& let Some(access_kind) = p.permission.associated_access()
694703
&& p.accessed
695704
{
696705
let diagnostics = DiagnosticInfo {

0 commit comments

Comments
 (0)