Skip to content

Commit 215ec38

Browse files
committed
track call IDs
1 parent e9370d2 commit 215ec38

File tree

2 files changed

+65
-16
lines changed

2 files changed

+65
-16
lines changed

src/lib.rs

Lines changed: 18 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -289,7 +289,7 @@ impl<'tcx> Evaluator<'tcx> {
289289
env_vars: HashMap::default(),
290290
tls: TlsData::default(),
291291
validate,
292-
stacked_borrows: stacked_borrows::State::new(),
292+
stacked_borrows: stacked_borrows::State::default(),
293293
}
294294
}
295295
}
@@ -301,7 +301,8 @@ type MiriEvalContext<'a, 'mir, 'tcx> = EvalContext<'a, 'mir, 'tcx, Evaluator<'tc
301301
impl<'a, 'mir, 'tcx> Machine<'a, 'mir, 'tcx> for Evaluator<'tcx> {
302302
type MemoryKinds = MiriMemoryKind;
303303

304-
type MemoryExtra = ();
304+
type FrameExtra = stacked_borrows::CallId;
305+
type MemoryExtra = stacked_borrows::MemoryState;
305306
type AllocExtra = stacked_borrows::Stacks;
306307
type PointerTag = Borrow;
307308

@@ -538,4 +539,19 @@ impl<'a, 'mir, 'tcx> Machine<'a, 'mir, 'tcx> for Evaluator<'tcx> {
538539
ecx.retag(fn_entry, place)
539540
}
540541
}
542+
543+
#[inline(always)]
544+
fn stack_push(
545+
ecx: &mut EvalContext<'a, 'mir, 'tcx, Self>,
546+
) -> EvalResult<'tcx, stacked_borrows::CallId> {
547+
Ok(ecx.memory().extra.borrow_mut().new_call())
548+
}
549+
550+
#[inline(always)]
551+
fn stack_pop(
552+
ecx: &mut EvalContext<'a, 'mir, 'tcx, Self>,
553+
extra: stacked_borrows::CallId,
554+
) -> EvalResult<'tcx> {
555+
Ok(ecx.memory().extra.borrow_mut().end_call(extra))
556+
}
541557
}

src/stacked_borrows.rs

Lines changed: 47 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,6 @@
11
use std::cell::RefCell;
2+
use std::collections::HashSet;
3+
use std::rc::Rc;
24

35
use rustc::ty::{self, layout::Size};
46
use rustc::hir::{Mutability, MutMutable, MutImmutable};
@@ -10,6 +12,7 @@ use crate::{
1012
};
1113

1214
pub type Timestamp = u64;
15+
pub type CallId = u64;
1316

1417
/// Information about which kind of borrow was used to create the reference this is tagged
1518
/// with.
@@ -80,15 +83,6 @@ pub struct Stack {
8083
frozen_since: Option<Timestamp>, // virtual frozen "item" on top of the stack
8184
}
8285

83-
impl Default for Stack {
84-
fn default() -> Self {
85-
Stack {
86-
borrows: vec![BorStackItem::Shr],
87-
frozen_since: None,
88-
}
89-
}
90-
}
91-
9286
impl Stack {
9387
#[inline(always)]
9488
pub fn is_frozen(&self) -> bool {
@@ -107,17 +101,50 @@ pub enum RefKind {
107101
Raw,
108102
}
109103

104+
/// Extra global state in the memory, available to the memory access hooks
105+
#[derive(Debug)]
106+
pub struct BarrierTracking {
107+
next_id: CallId,
108+
active_calls: HashSet<CallId>,
109+
}
110+
pub type MemoryState = Rc<RefCell<BarrierTracking>>;
111+
112+
impl Default for BarrierTracking {
113+
fn default() -> Self {
114+
BarrierTracking {
115+
next_id: 0,
116+
active_calls: HashSet::default(),
117+
}
118+
}
119+
}
120+
121+
impl BarrierTracking {
122+
pub fn new_call(&mut self) -> CallId {
123+
let id = self.next_id;
124+
trace!("new_call: Assigning ID {}", id);
125+
self.active_calls.insert(id);
126+
self.next_id += 1;
127+
id
128+
}
129+
130+
pub fn end_call(&mut self, id: CallId) {
131+
assert!(self.active_calls.remove(&id));
132+
}
133+
}
134+
110135
/// Extra global machine state
111136
#[derive(Clone, Debug)]
112137
pub struct State {
113138
clock: Timestamp
114139
}
115140

116-
impl State {
117-
pub fn new() -> State {
141+
impl Default for State {
142+
fn default() -> Self {
118143
State { clock: 0 }
119144
}
145+
}
120146

147+
impl State {
121148
fn increment_clock(&mut self) -> Timestamp {
122149
let val = self.clock;
123150
self.clock = val + 1;
@@ -130,6 +157,7 @@ impl State {
130157
pub struct Stacks {
131158
// Even reading memory can have effects on the stack, so we need a `RefCell` here.
132159
stacks: RefCell<RangeMap<Stack>>,
160+
barrier_tracking: MemoryState,
133161
}
134162

135163
/// Core per-location operations: deref, access, create.
@@ -358,11 +386,16 @@ impl<'tcx> Stacks {
358386
}
359387

360388
/// Hooks and glue
361-
impl AllocationExtra<Borrow, ()> for Stacks {
389+
impl AllocationExtra<Borrow, MemoryState> for Stacks {
362390
#[inline(always)]
363-
fn memory_allocated<'tcx>(size: Size, _extra: &()) -> Self {
391+
fn memory_allocated<'tcx>(size: Size, extra: &MemoryState) -> Self {
392+
let stack = Stack {
393+
borrows: vec![BorStackItem::Shr],
394+
frozen_since: None,
395+
};
364396
Stacks {
365-
stacks: RefCell::new(RangeMap::new(size, Stack::default()))
397+
stacks: RefCell::new(RangeMap::new(size, stack)),
398+
barrier_tracking: Rc::clone(extra),
366399
}
367400
}
368401

0 commit comments

Comments
 (0)