Skip to content

Commit 0afab59

Browse files
committed
TB: Reborrow policy and connection to the main machine
1 parent 7d4e8b9 commit 0afab59

File tree

2 files changed

+608
-1
lines changed

2 files changed

+608
-1
lines changed

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

Lines changed: 69 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ use rustc_target::abi::Size;
1111

1212
use crate::*;
1313
pub mod stacked_borrows;
14+
pub mod tree_borrows;
1415

1516
pub type CallId = NonZeroU64;
1617

@@ -230,8 +231,10 @@ impl GlobalStateInner {
230231
/// Which borrow tracking method to use
231232
#[derive(Debug, Copy, Clone, PartialEq, Eq)]
232233
pub enum BorrowTrackerMethod {
233-
/// Stacked Borrows, as implemented in borrow_tracker/stacked
234+
/// Stacked Borrows, as implemented in borrow_tracker/stacked_borrows
234235
StackedBorrows,
236+
/// Tree borrows, as implemented in borrow_tracker/tree_borrows
237+
TreeBorrows,
235238
}
236239

237240
impl BorrowTrackerMethod {
@@ -258,6 +261,10 @@ impl GlobalStateInner {
258261
AllocState::StackedBorrows(Box::new(RefCell::new(Stacks::new_allocation(
259262
id, alloc_size, self, kind, machine,
260263
)))),
264+
BorrowTrackerMethod::TreeBorrows =>
265+
AllocState::TreeBorrows(Box::new(RefCell::new(Tree::new_allocation(
266+
id, alloc_size, self, kind, machine,
267+
)))),
261268
}
262269
}
263270
}
@@ -273,6 +280,7 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriInterpCxExt<'mir, 'tcx> {
273280
let method = this.machine.borrow_tracker.as_ref().unwrap().borrow().borrow_tracker_method;
274281
match method {
275282
BorrowTrackerMethod::StackedBorrows => this.sb_retag_ptr_value(kind, val),
283+
BorrowTrackerMethod::TreeBorrows => this.tb_retag_ptr_value(kind, val),
276284
}
277285
}
278286

@@ -285,6 +293,7 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriInterpCxExt<'mir, 'tcx> {
285293
let method = this.machine.borrow_tracker.as_ref().unwrap().borrow().borrow_tracker_method;
286294
match method {
287295
BorrowTrackerMethod::StackedBorrows => this.sb_retag_place_contents(kind, place),
296+
BorrowTrackerMethod::TreeBorrows => this.tb_retag_place_contents(kind, place),
288297
}
289298
}
290299

@@ -293,6 +302,7 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriInterpCxExt<'mir, 'tcx> {
293302
let method = this.machine.borrow_tracker.as_ref().unwrap().borrow().borrow_tracker_method;
294303
match method {
295304
BorrowTrackerMethod::StackedBorrows => this.sb_retag_return_place(),
305+
BorrowTrackerMethod::TreeBorrows => this.tb_retag_return_place(),
296306
}
297307
}
298308

@@ -301,6 +311,34 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriInterpCxExt<'mir, 'tcx> {
301311
let method = this.machine.borrow_tracker.as_ref().unwrap().borrow().borrow_tracker_method;
302312
match method {
303313
BorrowTrackerMethod::StackedBorrows => this.sb_expose_tag(alloc_id, tag),
314+
BorrowTrackerMethod::TreeBorrows => this.tb_expose_tag(alloc_id, tag),
315+
}
316+
}
317+
318+
fn give_pointer_debug_name(
319+
&mut self,
320+
ptr: Pointer<Option<Provenance>>,
321+
nth_parent: u8,
322+
name: &str,
323+
) -> InterpResult<'tcx> {
324+
let this = self.eval_context_mut();
325+
let method = this.machine.borrow_tracker.as_ref().unwrap().borrow().borrow_tracker_method;
326+
match method {
327+
BorrowTrackerMethod::StackedBorrows => {
328+
this.tcx.tcx.sess.warn("Stacked Borrows does not support named pointers; `miri_pointer_name` is a no-op");
329+
Ok(())
330+
}
331+
BorrowTrackerMethod::TreeBorrows =>
332+
this.tb_give_pointer_debug_name(ptr, nth_parent, name),
333+
}
334+
}
335+
336+
fn print_borrow_state(&mut self, alloc_id: AllocId, show_unnamed: bool) -> InterpResult<'tcx> {
337+
let this = self.eval_context_mut();
338+
let method = this.machine.borrow_tracker.as_ref().unwrap().borrow().borrow_tracker_method;
339+
match method {
340+
BorrowTrackerMethod::StackedBorrows => this.print_stacks(alloc_id),
341+
BorrowTrackerMethod::TreeBorrows => this.print_tree(alloc_id, show_unnamed),
304342
}
305343
}
306344
}
@@ -310,6 +348,8 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriInterpCxExt<'mir, 'tcx> {
310348
pub enum AllocState {
311349
/// Data corresponding to Stacked Borrows
312350
StackedBorrows(Box<RefCell<stacked_borrows::AllocState>>),
351+
/// Data corresponding to Tree Borrows
352+
TreeBorrows(Box<RefCell<tree_borrows::AllocState>>),
313353
}
314354

315355
impl machine::AllocExtra {
@@ -328,6 +368,14 @@ impl machine::AllocExtra {
328368
_ => panic!("expected Stacked Borrows borrow tracking, got something else"),
329369
}
330370
}
371+
372+
#[track_caller]
373+
pub fn borrow_tracker_tb(&self) -> &RefCell<tree_borrows::AllocState> {
374+
match self.borrow_tracker {
375+
Some(AllocState::TreeBorrows(ref tb)) => tb,
376+
_ => panic!("expected Tree Borrows borrow tracking, got something else"),
377+
}
378+
}
331379
}
332380

333381
impl AllocState {
@@ -341,6 +389,14 @@ impl AllocState {
341389
match self {
342390
AllocState::StackedBorrows(sb) =>
343391
sb.borrow_mut().before_memory_read(alloc_id, prov_extra, range, machine),
392+
AllocState::TreeBorrows(tb) =>
393+
tb.borrow_mut().before_memory_access(
394+
AccessKind::Read,
395+
alloc_id,
396+
prov_extra,
397+
range,
398+
machine,
399+
),
344400
}
345401
}
346402

@@ -354,6 +410,14 @@ impl AllocState {
354410
match self {
355411
AllocState::StackedBorrows(sb) =>
356412
sb.get_mut().before_memory_write(alloc_id, prov_extra, range, machine),
413+
AllocState::TreeBorrows(tb) =>
414+
tb.get_mut().before_memory_access(
415+
AccessKind::Write,
416+
alloc_id,
417+
prov_extra,
418+
range,
419+
machine,
420+
),
357421
}
358422
}
359423

@@ -367,12 +431,15 @@ impl AllocState {
367431
match self {
368432
AllocState::StackedBorrows(sb) =>
369433
sb.get_mut().before_memory_deallocation(alloc_id, prov_extra, range, machine),
434+
AllocState::TreeBorrows(tb) =>
435+
tb.get_mut().before_memory_deallocation(alloc_id, prov_extra, range, machine),
370436
}
371437
}
372438

373439
pub fn remove_unreachable_tags(&self, tags: &FxHashSet<BorTag>) {
374440
match self {
375441
AllocState::StackedBorrows(sb) => sb.borrow_mut().remove_unreachable_tags(tags),
442+
AllocState::TreeBorrows(tb) => tb.borrow_mut().remove_unreachable_tags(tags),
376443
}
377444
}
378445
}
@@ -381,6 +448,7 @@ impl VisitTags for AllocState {
381448
fn visit_tags(&self, visit: &mut dyn FnMut(BorTag)) {
382449
match self {
383450
AllocState::StackedBorrows(sb) => sb.visit_tags(visit),
451+
AllocState::TreeBorrows(tb) => tb.visit_tags(visit),
384452
}
385453
}
386454
}

0 commit comments

Comments
 (0)