Merge pull request #4606 from RalfJung/alloc_addrs

alloc_addresses: track more explicitly whether we are in charge of generating addresses

Author: RalfJung

src/alloc_addresses/mod.rs

@@ -42,20 +42,19 @@ pub struct GlobalStateInner {
     /// they do not have an `AllocExtra`.
     /// This is the inverse of `int_to_ptr_map`.
     base_addr: FxHashMap<AllocId, u64>,
-    /// Temporarily store prepared memory space for global allocations the first time their memory
-    /// address is required. This is used to ensure that the memory is allocated before Miri assigns
-    /// it an internal address, which is important for matching the internal address to the machine
-    /// address so FFI can read from pointers.
-    prepared_alloc_bytes: FxHashMap<AllocId, MiriAllocBytes>,
-    /// A pool of addresses we can reuse for future allocations.
-    reuse: ReusePool,
-    /// Whether an allocation has been exposed or not. This cannot be put
+    /// The set of exposed allocations. This cannot be put
     /// into `AllocExtra` for the same reason as `base_addr`.
     exposed: FxHashSet<AllocId>,
-    /// The generator for new addresses in a given range.
-    address_generator: AddressGenerator,
     /// The provenance to use for int2ptr casts
     provenance_mode: ProvenanceMode,
+    /// The generator for new addresses in a given range, and a pool for address reuse. This is
+    /// `None` if addresses are generated elsewhere (in native-lib mode or with GenMC).
+    address_generation: Option<(AddressGenerator, ReusePool)>,
+    /// Native-lib mode only: Temporarily store prepared memory space for global allocations the
+    /// first time their memory address is required. This is used to ensure that the memory is
+    /// allocated before Miri assigns it an internal address, which is important for matching the
+    /// internal address to the machine address so FFI can read from pointers.
+    prepared_alloc_bytes: Option<FxHashMap<AllocId, MiriAllocBytes>>,
 }
 
 impl VisitProvenance for GlobalStateInner {
@@ -64,9 +63,8 @@ impl VisitProvenance for GlobalStateInner {
             int_to_ptr_map: _,
             base_addr: _,
             prepared_alloc_bytes: _,
-            reuse: _,
             exposed: _,
-            address_generator: _,
+            address_generation: _,
             provenance_mode: _,
         } = self;
         // Though base_addr, int_to_ptr_map, and exposed contain AllocIds, we do not want to visit them.
@@ -83,11 +81,16 @@ impl GlobalStateInner {
         GlobalStateInner {
             int_to_ptr_map: Vec::default(),
             base_addr: FxHashMap::default(),
-            prepared_alloc_bytes: FxHashMap::default(),
-            reuse: ReusePool::new(config),
             exposed: FxHashSet::default(),
-            address_generator: AddressGenerator::new(stack_addr..tcx.target_usize_max()),
             provenance_mode: config.provenance_mode,
+            address_generation: (config.native_lib.is_empty() && config.genmc_config.is_none())
+                .then(|| {
+                    (
+                        AddressGenerator::new(stack_addr..tcx.target_usize_max()),
+                        ReusePool::new(config),
+                    )
+                }),
+            prepared_alloc_bytes: (!config.native_lib.is_empty()).then(FxHashMap::default),
         }
     }
 
@@ -147,6 +150,8 @@ trait EvalContextExtPriv<'tcx>: crate::MiriInterpCxExt<'tcx> {
                         // Store prepared allocation to be picked up for use later.
                         global_state
                             .prepared_alloc_bytes
+                            .as_mut()
+                            .unwrap()
                             .try_insert(alloc_id, prepared_bytes)
                             .unwrap();
                         ptr
@@ -173,29 +178,25 @@ trait EvalContextExtPriv<'tcx>: crate::MiriInterpCxExt<'tcx> {
             // We don't have to expose this pointer yet, we do that in `prepare_for_native_call`.
             return interp_ok(base_ptr.addr().to_u64());
         }
-        // We are not in native lib mode, so we control the addresses ourselves.
+        // We are not in native lib or genmc mode, so we control the addresses ourselves.
+        let (addr_gen, reuse) = global_state.address_generation.as_mut().unwrap();
         let mut rng = this.machine.rng.borrow_mut();
-        if let Some((reuse_addr, clock)) = global_state.reuse.take_addr(
-            &mut *rng,
-            info.size,
-            info.align,
-            memory_kind,
-            this.active_thread(),
-        ) {
+        if let Some((reuse_addr, clock)) =
+            reuse.take_addr(&mut *rng, info.size, info.align, memory_kind, this.active_thread())
+        {
             if let Some(clock) = clock {
                 this.acquire_clock(&clock)?;
             }
             interp_ok(reuse_addr)
         } else {
             // We have to pick a fresh address.
-            let new_addr =
-                global_state.address_generator.generate(info.size, info.align, &mut rng)?;
+            let new_addr = addr_gen.generate(info.size, info.align, &mut rng)?;
 
             // If we filled up more than half the address space, start aggressively reusing
             // addresses to avoid running out.
-            let remaining_range = global_state.address_generator.get_remaining();
+            let remaining_range = addr_gen.get_remaining();
             if remaining_range.start > remaining_range.end / 2 {
-                global_state.reuse.address_space_shortage();
+                reuse.address_space_shortage();
             }
 
             interp_ok(new_addr)
@@ -414,6 +415,8 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
             let mut global_state = this.machine.alloc_addresses.borrow_mut();
             let mut prepared_alloc_bytes = global_state
                 .prepared_alloc_bytes
+                .as_mut()
+                .unwrap()
                 .remove(&id)
                 .unwrap_or_else(|| panic!("alloc bytes for {id:?} have not been prepared"));
             // Sanity-check that the prepared allocation has the right size and alignment.
@@ -496,15 +499,17 @@ impl<'tcx> MiriMachine<'tcx> {
         // `alloc_id_from_addr` any more.
         global_state.exposed.remove(&dead_id);
         // Also remember this address for future reuse.
-        let thread = self.threads.active_thread();
-        global_state.reuse.add_addr(rng, addr, size, align, kind, thread, || {
-            // We already excluded GenMC above. We cannot use `self.release_clock` as
-            // `self.alloc_addresses` is borrowed.
-            if let Some(data_race) = self.data_race.as_vclocks_ref() {
-                data_race.release_clock(&self.threads, |clock| clock.clone())
-            } else {
-                VClock::default()
-            }
-        })
+        if let Some((_addr_gen, reuse)) = global_state.address_generation.as_mut() {
+            let thread = self.threads.active_thread();
+            reuse.add_addr(rng, addr, size, align, kind, thread, || {
+                // We cannot be in GenMC mode as then `address_generation` is `None`. We cannot use
+                // `self.release_clock` as `self.alloc_addresses` is borrowed.
+                if let Some(data_race) = self.data_race.as_vclocks_ref() {
+                    data_race.release_clock(&self.threads, |clock| clock.clone())
+                } else {
+                    VClock::default()
+                }
+            })
+        }
     }
 }

src/machine.rs

@@ -777,9 +777,8 @@ impl<'tcx> MiriMachine<'tcx> {
             local_crates,
             extern_statics: FxHashMap::default(),
             rng: RefCell::new(rng),
-            allocator: if !config.native_lib.is_empty() {
-                Some(Rc::new(RefCell::new(crate::alloc::isolated_alloc::IsolatedAlloc::new())))
-            } else { None },
+            allocator: (!config.native_lib.is_empty())
+                .then(|| Rc::new(RefCell::new(crate::alloc::isolated_alloc::IsolatedAlloc::new()))),
             tracked_alloc_ids: config.tracked_alloc_ids.clone(),
             track_alloc_accesses: config.track_alloc_accesses,
             check_alignment: config.check_alignment,