mikros/rust
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

adjust for init_allocation_extra

Browse Source
This commit is contained in:
Ralf Jung 2019-11-29 19:50:37 +01:00
parent ae53b1222a
commit 1b3434c67d
2 changed files with 20 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

21
src/machine.rs
View File

@ -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(
@ -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)]

14
src/stacked_borrows.rs
View File

@ -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,
@ -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)]
@ -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()),
};