adjust for init_allocation_extra

Author: RalfJung

src/machine.rs

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

src/stacked_borrows.rs

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