Skip to content

Commit

Permalink
Handle wildcard pointers in SB
Browse files Browse the repository at this point in the history
  • Loading branch information
carbotaniuman committed Jun 15, 2022
1 parent e7507d6 commit 81df2af
Show file tree
Hide file tree
Showing 7 changed files with 282 additions and 88 deletions.
26 changes: 21 additions & 5 deletions src/machine.rs
Original file line number Diff line number Diff line change
Expand Up @@ -489,7 +489,7 @@ impl<'mir, 'tcx> Machine<'mir, 'tcx> for Evaluator<'mir, 'tcx> {
type AllocExtra = AllocExtra;

type PointerTag = Tag;
type TagExtra = SbTag;
type TagExtra = Option<SbTag>;

type MemoryMap =
MonoHashMap<AllocId, (MemoryKind<MiriMemoryKind>, Allocation<Tag, Self::AllocExtra>)>;
Expand Down Expand Up @@ -695,8 +695,24 @@ impl<'mir, 'tcx> Machine<'mir, 'tcx> for Evaluator<'mir, 'tcx> {
ptr: Pointer<Self::PointerTag>,
) -> InterpResult<'tcx> {
match ptr.provenance {
Tag::Concrete(concrete) =>
intptrcast::GlobalStateInner::expose_addr(ecx, concrete.alloc_id),
Tag::Concrete(ConcreteTag { alloc_id, sb }) => {
intptrcast::GlobalStateInner::expose_addr(ecx, alloc_id);

let (size, _) =
ecx.get_alloc_size_and_align(alloc_id, AllocCheck::MaybeDead).unwrap();

// Function pointers and dead objects don't have an alloc_extra so we ignore them.
if let Ok(alloc_extra) = ecx.get_alloc_extra(alloc_id) {
if let Some(stacked_borrows) = &alloc_extra.stacked_borrows {
stacked_borrows.ptr_exposed(
alloc_id,
sb,
alloc_range(Size::from_bytes(0), size),
ecx.machine.stacked_borrows.as_ref().unwrap(),
)?;
}
}
}
Tag::Wildcard => {
// No need to do anything for wildcard pointers as
// their provenances have already been previously exposed.
Expand All @@ -715,8 +731,8 @@ impl<'mir, 'tcx> Machine<'mir, 'tcx> for Evaluator<'mir, 'tcx> {

rel.map(|(alloc_id, size)| {
let sb = match ptr.provenance {
Tag::Concrete(ConcreteTag { sb, .. }) => sb,
Tag::Wildcard => SbTag::Untagged,
Tag::Concrete(ConcreteTag { sb, .. }) => Some(sb),
Tag::Wildcard => None,
};
(alloc_id, size, sb)
})
Expand Down
Loading

0 comments on commit 81df2af

Please sign in to comment.