Skip to content

Commit

Permalink
adjust for init_allocation_extra
Browse files Browse the repository at this point in the history
  • Loading branch information
RalfJung committed Nov 29, 2019
1 parent 0978e4f commit 234f59d
Show file tree
Hide file tree
Showing 2 changed files with 20 additions and 15 deletions.
21 changes: 9 additions & 12 deletions src/machine.rs
Original file line number Diff line number Diff line change
Expand Up @@ -291,27 +291,24 @@ impl<'mir, 'tcx> Machine<'mir, 'tcx> for Evaluator<'tcx> {
Ok(())
}

fn tag_allocation<'b>(
fn init_allocation_extra<'b>(
memory_extra: &MemoryExtra,
id: AllocId,
alloc: Cow<'b, Allocation>,
kind: Option<MemoryKind<Self::MemoryKinds>>,
) -> (
Cow<'b, Allocation<Self::PointerTag, Self::AllocExtra>>,
Self::PointerTag,
) {
) -> Cow<'b, Allocation<Self::PointerTag, Self::AllocExtra>> {
let kind = kind.expect("we set our STATIC_KIND so this cannot be None");
let alloc = alloc.into_owned();
let (stacks, base_tag) = if !memory_extra.validate {
(None, Tag::Untagged)
} else {
let (stacks, base_tag) = Stacks::new_allocation(
let stacks = if memory_extra.validate {
Some(Stacks::new_allocation(
id,
alloc.size,
Rc::clone(&memory_extra.stacked_borrows),
kind,
);
(Some(stacks), base_tag)
))
} else {
// No stacks.
None
};
let mut stacked_borrows = memory_extra.stacked_borrows.borrow_mut();
let alloc: Allocation<Tag, Self::AllocExtra> = alloc.with_tags_and_extra(
Expand All @@ -328,7 +325,7 @@ impl<'mir, 'tcx> Machine<'mir, 'tcx> for Evaluator<'tcx> {
stacked_borrows: stacks,
},
);
(Cow::Owned(alloc), base_tag)
Cow::Owned(alloc)
}

#[inline(always)]
Expand Down
14 changes: 11 additions & 3 deletions src/stacked_borrows.rs
Original file line number Diff line number Diff line change
Expand Up @@ -462,7 +462,7 @@ impl Stacks {
size: Size,
extra: MemoryExtra,
kind: MemoryKind<MiriMemoryKind>,
) -> (Self, Tag) {
) -> Self {
let (tag, perm) = match kind {
MemoryKind::Stack =>
// New unique borrow. This tag is not accessible by the program,
Expand All @@ -472,12 +472,15 @@ impl Stacks {
// and in particular, *all* raw pointers.
(Tag::Tagged(extra.borrow_mut().new_ptr()), Permission::Unique),
MemoryKind::Machine(MiriMemoryKind::Static) =>
// Statics are inherently shared, so we do not derive any uniqueness assumptions
// from direct accesses to a static. Thus, the base permission is `SharedReadWrite`.
(extra.borrow_mut().static_base_ptr(id), Permission::SharedReadWrite),
_ =>
// Everything else we handle entirely untagged for now.
// FIXME: experiment with more precise tracking.
(Tag::Untagged, Permission::SharedReadWrite),
};
let stack = Stacks::new(size, perm, tag, extra);
(stack, tag)
Stacks::new(size, perm, tag, extra)
}

#[inline(always)]
Expand Down Expand Up @@ -591,7 +594,12 @@ trait EvalContextPrivExt<'mir, 'tcx: 'mir>: crate::MiriEvalContextExt<'mir, 'tcx

// Compute new borrow.
let new_tag = match kind {
// Give up tracking for raw pointers.
// FIXME: Experiment with more precise tracking. Blocked on `&raw`
// because `Rc::into_raw` currently creates intermediate references,
// breaking `Rc::from_raw`.
RefKind::Raw { .. } => Tag::Untagged,
// All other pointesr are properly tracked.
_ => Tag::Tagged(this.memory.extra.stacked_borrows.borrow_mut().new_ptr()),
};

Expand Down

0 comments on commit 234f59d

Please sign in to comment.