Skip to content

Commit ed5a655

Browse files
RalfJungRalfJung
authored
Merge pull request #4376 from yoctocell/tb-interior-mut-flag
TB: Add flag to disable the more precise interior mutability tracking
2 parents 65ad80e + 4e8d583 commit ed5a655

File tree

8 files changed

+154
-35
lines changed

8 files changed

+154
-35
lines changed

‎src/tools/miri/README.md

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -460,6 +460,10 @@ to Miri failing to detect cases of undefined behavior in a program.
460460
This is much less likely with Stacked Borrows.
461461
Using Tree Borrows currently implies `-Zmiri-strict-provenance` because integer-to-pointer
462462
casts are not supported in this mode, but that may change in the future.
463+
* `-Zmiri-tree-borrows-no-precise-interior-mut` makes Tree Borrows
464+
track interior mutable data on the level of references instead of on the
465+
byte-level as is done by default. Therefore, with this flag, Tree
466+
Borrows will be more permissive.
463467
* `-Zmiri-force-page-size=<num>` overrides the default page size for an architecture, in multiples of 1k.
464468
`4` is default for most targets. This value should always be a power of 2 and nonzero.
465469

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

Lines changed: 17 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,7 @@ use std::sync::{Arc, Once};
3535

3636
use miri::{
3737
BacktraceStyle, BorrowTrackerMethod, GenmcConfig, GenmcCtx, MiriConfig, MiriEntryFnType,
38-
ProvenanceMode, RetagFields, ValidationMode,
38+
ProvenanceMode, RetagFields, TreeBorrowsParams, ValidationMode,
3939
};
4040
use rustc_abi::ExternAbi;
4141
use rustc_data_structures::sync;
@@ -554,8 +554,21 @@ fn main() {
554554
} else if arg == "-Zmiri-disable-stacked-borrows" {
555555
miri_config.borrow_tracker = None;
556556
} else if arg == "-Zmiri-tree-borrows" {
557-
miri_config.borrow_tracker = Some(BorrowTrackerMethod::TreeBorrows);
557+
miri_config.borrow_tracker =
558+
Some(BorrowTrackerMethod::TreeBorrows(TreeBorrowsParams {
559+
precise_interior_mut: true,
560+
}));
558561
miri_config.provenance_mode = ProvenanceMode::Strict;
562+
} else if arg == "-Zmiri-tree-borrows-no-precise-interior-mut" {
563+
match &mut miri_config.borrow_tracker {
564+
Some(BorrowTrackerMethod::TreeBorrows(params)) => {
565+
params.precise_interior_mut = false;
566+
}
567+
_ =>
568+
show_error!(
569+
"`-Zmiri-tree-borrows` is required before `-Zmiri-tree-borrows-no-precise-interior-mut`"
570+
),
571+
};
559572
} else if arg == "-Zmiri-disable-data-race-detector" {
560573
miri_config.data_race_detector = false;
561574
miri_config.weak_memory_emulation = false;
@@ -732,7 +745,7 @@ fn main() {
732745
}
733746
}
734747
// Tree Borrows implies strict provenance, and is not compatible with native calls.
735-
if matches!(miri_config.borrow_tracker, Some(BorrowTrackerMethod::TreeBorrows)) {
748+
if matches!(miri_config.borrow_tracker, Some(BorrowTrackerMethod::TreeBorrows { .. })) {
736749
if miri_config.provenance_mode != ProvenanceMode::Strict {
737750
show_error!(
738751
"Tree Borrows does not support integer-to-pointer casts, and hence requires strict provenance"
@@ -742,6 +755,7 @@ fn main() {
742755
show_error!("Tree Borrows is not compatible with calling native functions");
743756
}
744757
}
758+
745759
// Native calls and strict provenance are not compatible.
746760
if !miri_config.native_lib.is_empty() && miri_config.provenance_mode == ProvenanceMode::Strict {
747761
show_error!("strict provenance is not compatible with calling native functions");

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

Lines changed: 21 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -226,7 +226,13 @@ pub enum BorrowTrackerMethod {
226226
/// Stacked Borrows, as implemented in borrow_tracker/stacked_borrows
227227
StackedBorrows,
228228
/// Tree borrows, as implemented in borrow_tracker/tree_borrows
229-
TreeBorrows,
229+
TreeBorrows(TreeBorrowsParams),
230+
}
231+
232+
/// Parameters that Tree Borrows can take.
233+
#[derive(Debug, Copy, Clone, PartialEq, Eq)]
234+
pub struct TreeBorrowsParams {
235+
pub precise_interior_mut: bool,
230236
}
231237

232238
impl BorrowTrackerMethod {
@@ -237,6 +243,13 @@ impl BorrowTrackerMethod {
237243
config.retag_fields,
238244
))
239245
}
246+
247+
pub fn get_tree_borrows_params(self) -> TreeBorrowsParams {
248+
match self {
249+
BorrowTrackerMethod::TreeBorrows(params) => params,
250+
_ => panic!("can only be called when `BorrowTrackerMethod` is `TreeBorrows`"),
251+
}
252+
}
240253
}
241254

242255
impl GlobalStateInner {
@@ -252,7 +265,7 @@ impl GlobalStateInner {
252265
AllocState::StackedBorrows(Box::new(RefCell::new(Stacks::new_allocation(
253266
id, alloc_size, self, kind, machine,
254267
)))),
255-
BorrowTrackerMethod::TreeBorrows =>
268+
BorrowTrackerMethod::TreeBorrows { .. } =>
256269
AllocState::TreeBorrows(Box::new(RefCell::new(Tree::new_allocation(
257270
id, alloc_size, self, kind, machine,
258271
)))),
@@ -271,7 +284,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
271284
let method = this.machine.borrow_tracker.as_ref().unwrap().borrow().borrow_tracker_method;
272285
match method {
273286
BorrowTrackerMethod::StackedBorrows => this.sb_retag_ptr_value(kind, val),
274-
BorrowTrackerMethod::TreeBorrows => this.tb_retag_ptr_value(kind, val),
287+
BorrowTrackerMethod::TreeBorrows { .. } => this.tb_retag_ptr_value(kind, val),
275288
}
276289
}
277290

@@ -284,7 +297,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
284297
let method = this.machine.borrow_tracker.as_ref().unwrap().borrow().borrow_tracker_method;
285298
match method {
286299
BorrowTrackerMethod::StackedBorrows => this.sb_retag_place_contents(kind, place),
287-
BorrowTrackerMethod::TreeBorrows => this.tb_retag_place_contents(kind, place),
300+
BorrowTrackerMethod::TreeBorrows { .. } => this.tb_retag_place_contents(kind, place),
288301
}
289302
}
290303

@@ -293,7 +306,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
293306
let method = this.machine.borrow_tracker.as_ref().unwrap().borrow().borrow_tracker_method;
294307
match method {
295308
BorrowTrackerMethod::StackedBorrows => this.sb_protect_place(place),
296-
BorrowTrackerMethod::TreeBorrows => this.tb_protect_place(place),
309+
BorrowTrackerMethod::TreeBorrows { .. } => this.tb_protect_place(place),
297310
}
298311
}
299312

@@ -302,7 +315,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
302315
let method = this.machine.borrow_tracker.as_ref().unwrap().borrow().borrow_tracker_method;
303316
match method {
304317
BorrowTrackerMethod::StackedBorrows => this.sb_expose_tag(alloc_id, tag),
305-
BorrowTrackerMethod::TreeBorrows => this.tb_expose_tag(alloc_id, tag),
318+
BorrowTrackerMethod::TreeBorrows { .. } => this.tb_expose_tag(alloc_id, tag),
306319
}
307320
}
308321

@@ -319,7 +332,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
319332
this.tcx.tcx.dcx().warn("Stacked Borrows does not support named pointers; `miri_pointer_name` is a no-op");
320333
interp_ok(())
321334
}
322-
BorrowTrackerMethod::TreeBorrows =>
335+
BorrowTrackerMethod::TreeBorrows { .. } =>
323336
this.tb_give_pointer_debug_name(ptr, nth_parent, name),
324337
}
325338
}
@@ -333,7 +346,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
333346
let method = borrow_tracker.borrow().borrow_tracker_method;
334347
match method {
335348
BorrowTrackerMethod::StackedBorrows => this.print_stacks(alloc_id),
336-
BorrowTrackerMethod::TreeBorrows => this.print_tree(alloc_id, show_unnamed),
349+
BorrowTrackerMethod::TreeBorrows { .. } => this.print_tree(alloc_id, show_unnamed),
337350
}
338351
}
339352

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

Lines changed: 65 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -312,8 +312,6 @@ trait EvalContextPrivExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
312312
}
313313

314314
let span = this.machine.current_span();
315-
let alloc_extra = this.get_alloc_extra(alloc_id)?;
316-
let mut tree_borrows = alloc_extra.borrow_tracker_tb().borrow_mut();
317315

318316
// Store initial permissions and their corresponding range.
319317
let mut perms_map: RangeMap<LocationState> = RangeMap::new(
@@ -342,36 +340,83 @@ trait EvalContextPrivExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
342340
assert!(new_perm.freeze_access);
343341

344342
let protected = new_perm.protector.is_some();
345-
this.visit_freeze_sensitive(place, ptr_size, |range, frozen| {
346-
has_unsafe_cell = has_unsafe_cell || !frozen;
347-
348-
// We are only ever `Frozen` inside the frozen bits.
349-
let (perm, access) = if frozen {
343+
let precise_interior_mut = this
344+
.machine
345+
.borrow_tracker
346+
.as_mut()
347+
.unwrap()
348+
.get_mut()
349+
.borrow_tracker_method
350+
.get_tree_borrows_params()
351+
.precise_interior_mut;
352+
353+
let default_perm = if !precise_interior_mut {
354+
// NOTE: Using `ty_is_freeze` doesn't give the same result as going through the range
355+
// and computing `has_unsafe_cell`. This is because of zero-sized `UnsafeCell`, for which
356+
// `has_unsafe_cell` is false, but `!ty_is_freeze` is true.
357+
let ty_is_freeze = place.layout.ty.is_freeze(*this.tcx, this.typing_env());
358+
let (perm, access) = if ty_is_freeze {
350359
(new_perm.freeze_perm, new_perm.freeze_access)
351360
} else {
352361
(new_perm.nonfreeze_perm, new_perm.nonfreeze_access)
353362
};
363+
let sifa = perm.strongest_idempotent_foreign_access(protected);
364+
let new_loc = if access {
365+
LocationState::new_accessed(perm, sifa)
366+
} else {
367+
LocationState::new_non_accessed(perm, sifa)
368+
};
369+
370+
for (_loc_range, loc) in perms_map.iter_mut_all() {
371+
*loc = new_loc;
372+
}
373+
374+
perm
375+
} else {
376+
this.visit_freeze_sensitive(place, ptr_size, |range, frozen| {
377+
has_unsafe_cell = has_unsafe_cell || !frozen;
354378

355-
// Store initial permissions.
356-
for (_loc_range, loc) in perms_map.iter_mut(range.start, range.size) {
379+
// We are only ever `Frozen` inside the frozen bits.
380+
let (perm, access) = if frozen {
381+
(new_perm.freeze_perm, new_perm.freeze_access)
382+
} else {
383+
(new_perm.nonfreeze_perm, new_perm.nonfreeze_access)
384+
};
357385
let sifa = perm.strongest_idempotent_foreign_access(protected);
358386
// NOTE: Currently, `access` is false if and only if `perm` is Cell, so this `if`
359387
// doesn't not change whether any code is UB or not. We could just always use
360388
// `new_accessed` and everything would stay the same. But that seems conceptually
361389
// odd, so we keep the initial "accessed" bit of the `LocationState` in sync with whether
362390
// a read access is performed below.
363-
if access {
364-
*loc = LocationState::new_accessed(perm, sifa);
391+
let new_loc = if access {
392+
LocationState::new_accessed(perm, sifa)
365393
} else {
366-
*loc = LocationState::new_non_accessed(perm, sifa);
394+
LocationState::new_non_accessed(perm, sifa)
395+
};
396+
397+
// Store initial permissions.
398+
for (_loc_range, loc) in perms_map.iter_mut(range.start, range.size) {
399+
*loc = new_loc;
367400
}
368-
}
369401

370-
// Some reborrows incur a read access to the parent.
371-
if access {
402+
interp_ok(())
403+
})?;
404+
405+
// Allow lazily writing to surrounding data if we found an `UnsafeCell`.
406+
if has_unsafe_cell { new_perm.nonfreeze_perm } else { new_perm.freeze_perm }
407+
};
408+
409+
let alloc_extra = this.get_alloc_extra(alloc_id)?;
410+
let mut tree_borrows = alloc_extra.borrow_tracker_tb().borrow_mut();
411+
412+
for (perm_range, perm) in perms_map.iter_mut_all() {
413+
if perm.is_accessed() {
414+
// Some reborrows incur a read access to the parent.
372415
// Adjust range to be relative to allocation start (rather than to `place`).
373-
let mut range_in_alloc = range;
374-
range_in_alloc.start += base_offset;
416+
let range_in_alloc = AllocRange {
417+
start: Size::from_bytes(perm_range.start) + base_offset,
418+
size: Size::from_bytes(perm_range.end - perm_range.start),
419+
};
375420

376421
tree_borrows.perform_access(
377422
orig_tag,
@@ -382,7 +427,7 @@ trait EvalContextPrivExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
382427
)?;
383428

384429
// Also inform the data race model (but only if any bytes are actually affected).
385-
if range.size.bytes() > 0 {
430+
if range_in_alloc.size.bytes() > 0 {
386431
if let Some(data_race) = alloc_extra.data_race.as_vclocks_ref() {
387432
data_race.read(
388433
alloc_id,
@@ -394,17 +439,15 @@ trait EvalContextPrivExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
394439
}
395440
}
396441
}
397-
interp_ok(())
398-
})?;
442+
}
399443

400444
// Record the parent-child pair in the tree.
401445
tree_borrows.new_child(
402446
base_offset,
403447
orig_tag,
404448
new_tag,
405449
perms_map,
406-
// Allow lazily writing to surrounding data if we found an `UnsafeCell`.
407-
if has_unsafe_cell { new_perm.nonfreeze_perm } else { new_perm.freeze_perm },
450+
default_perm,
408451
protected,
409452
span,
410453
)?;

‎src/tools/miri/src/diagnostics.rs

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -682,7 +682,10 @@ impl<'tcx> MiriMachine<'tcx> {
682682
),
683683
];
684684
if self.borrow_tracker.as_ref().is_some_and(|b| {
685-
matches!(b.borrow().borrow_tracker_method(), BorrowTrackerMethod::TreeBorrows)
685+
matches!(
686+
b.borrow().borrow_tracker_method(),
687+
BorrowTrackerMethod::TreeBorrows { .. }
688+
)
686689
}) {
687690
v.push(
688691
note!("Tree Borrows does not support integer-to-pointer casts, so the program is likely to go wrong when this pointer gets used")

‎src/tools/miri/src/lib.rs

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -114,7 +114,9 @@ pub use crate::borrow_tracker::stacked_borrows::{
114114
EvalContextExt as _, Item, Permission, Stack, Stacks,
115115
};
116116
pub use crate::borrow_tracker::tree_borrows::{EvalContextExt as _, Tree};
117-
pub use crate::borrow_tracker::{BorTag, BorrowTrackerMethod, EvalContextExt as _, RetagFields};
117+
pub use crate::borrow_tracker::{
118+
BorTag, BorrowTrackerMethod, EvalContextExt as _, RetagFields, TreeBorrowsParams,
119+
};
118120
pub use crate::clock::{Instant, MonotonicClock};
119121
pub use crate::concurrency::cpu_affinity::MAX_CPUS;
120122
pub use crate::concurrency::data_race::{

‎src/tools/miri/tests/pass/tree_borrows/cell-inside-struct.rs

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
//! The same as `tests/fail/tree-borrows/cell-inside-struct` but with
2+
//! precise tracking of interior mutability disabled.
3+
//@compile-flags: -Zmiri-tree-borrows -Zmiri-tree-borrows-no-precise-interior-mut
4+
#[path = "../../utils/mod.rs"]
5+
#[macro_use]
6+
mod utils;
7+
8+
use std::cell::Cell;
9+
10+
struct Foo {
11+
field1: u32,
12+
field2: Cell<u32>,
13+
}
14+
15+
pub fn main() {
16+
let root = Foo { field1: 42, field2: Cell::new(88) };
17+
unsafe {
18+
let a = &root;
19+
20+
name!(a as *const Foo, "a");
21+
22+
let a: *const Foo = a as *const Foo;
23+
let a: *mut Foo = a as *mut Foo;
24+
25+
let alloc_id = alloc_id!(a);
26+
print_state!(alloc_id);
27+
28+
// Writing to `field2`, which is interior mutable, should be allowed.
29+
(*a).field2.set(10);
30+
31+
// Writing to `field1` should be allowed because it also has the `Cell` permission.
32+
(*a).field1 = 88;
33+
}
34+
}

‎src/tools/miri/tests/pass/tree_borrows/cell-inside-struct.stderr

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
──────────────────────────────────────────────────
2+
Warning: this tree is indicative only. Some tags may have been hidden.
3+
0.. 8
4+
| Act | └─┬──<TAG=root of the allocation>
5+
|?Cel | └────<TAG=a>
6+
──────────────────────────────────────────────────

0 commit comments

Comments
 (0)