More cleanup

Author: Patrick-6

src/concurrency/genmc/dummy.rs

@@ -187,7 +187,6 @@ impl GenmcCtx {
         _alloc_id: AllocId,
         _address: Size,
         _size: Size,
-        _align: Align,
         _kind: MemoryKind,
     ) -> InterpResult<'tcx> {
         unreachable!()

src/concurrency/genmc/mod.rs

@@ -484,16 +484,8 @@ impl GenmcCtx {
     ) -> InterpResult<'tcx, u64> {
         let machine = &ecx.machine;
         let chosen_address = if memory_kind == MiriMemoryKind::Global.into() {
-            info!("GenMC: global memory allocation: {alloc_id:?}");
             ecx.get_global_allocation_address(&self.global_allocations, alloc_id)?
         } else {
-            // TODO GENMC: Does GenMC need to know about the kind of Memory?
-
-            // eprintln!(
-            //     "handle_alloc ({memory_kind:?}): Custom backtrace: {}",
-            //     std::backtrace::Backtrace::force_capture()
-            // );
-            // TODO GENMC: should we put this before the special handling for globals?
             if self.allow_data_races.get() {
                 unreachable!(); // FIXME(genmc): can this happen and if yes, how should this be handled?
             }
@@ -502,31 +494,24 @@ impl GenmcCtx {
             let genmc_tid = thread_infos.get_info(curr_thread).genmc_tid;
             // GenMC doesn't support ZSTs, so we set the minimum size to 1 byte
             let genmc_size = size.bytes().max(1);
-            info!(
-                "GenMC: handle_alloc (thread: {curr_thread:?} ({genmc_tid:?}), size: {}, alignment: {alignment:?}, memory_kind: {memory_kind:?})",
-                size.bytes()
-            );
 
             let alignment = alignment.bytes();
 
             let mut mc = self.handle.borrow_mut();
             let pinned_mc = mc.as_mut();
             let chosen_address = pinned_mc.handleMalloc(genmc_tid.0, genmc_size, alignment);
-            info!("GenMC: handle_alloc: got address '{chosen_address}' ({chosen_address:#x})");
 
-            // TODO GENMC:
-            if chosen_address == 0 {
-                throw_unsup_format!("TODO GENMC: we got address '0' from malloc");
-            }
+            assert_ne!(chosen_address, 0, "GenMC malloc returned nullptr.");
+            // Non-global addresses should not be in the global address space.
             assert_eq!(0, chosen_address & GENMC_GLOBAL_ADDRESSES_MASK);
             chosen_address
         };
+
         // Sanity check the address alignment:
-        assert_eq!(
+        debug_assert_eq!(
             0,
             chosen_address % alignment.bytes(),
-            "GenMC returned address {chosen_address} == {chosen_address:#x} with lower alignment than requested ({:})!",
-            alignment.bytes()
+            "Allocated address {chosen_address:#x} does not have requested alignment ({alignment:?})!"
         );
 
         interp_ok(chosen_address)
@@ -538,7 +523,6 @@ impl GenmcCtx {
         alloc_id: AllocId,
         address: Size,
         size: Size,
-        align: Align,
         kind: MemoryKind,
     ) -> InterpResult<'tcx> {
         assert_ne!(
@@ -552,10 +536,6 @@ impl GenmcCtx {
         let thread_infos = self.thread_infos.borrow();
         let curr_thread = machine.threads.active_thread();
         let genmc_tid = thread_infos.get_info(curr_thread).genmc_tid;
-        info!(
-            "GenMC: memory deallocation, thread: {curr_thread:?} ({genmc_tid:?}), address: {addr} == {addr:#x}, size: {size:?}, align: {align:?}, memory_kind: {kind:?}",
-            addr = address.bytes()
-        );
 
         let genmc_address = address.bytes();
         // GenMC doesn't support ZSTs, so we set the minimum size to 1 byte
@@ -585,14 +565,9 @@ impl GenmcCtx {
         let genmc_parent_tid = thread_infos.get_info(curr_thread_id).genmc_tid;
         let genmc_new_tid = thread_infos.add_thread(new_thread_id);
 
-        info!(
-            "GenMC: handling thread creation (thread {curr_thread_id:?} ({genmc_parent_tid:?}) spawned thread {new_thread_id:?} ({genmc_new_tid:?}))"
-        );
-
         let mut mc = self.handle.borrow_mut();
         mc.as_mut().handleThreadCreate(genmc_new_tid.0, genmc_parent_tid.0);
 
-        // TODO GENMC (ERROR HANDLING): can this ever fail?
         interp_ok(())
     }
 
@@ -607,10 +582,6 @@ impl GenmcCtx {
         let genmc_curr_tid = thread_infos.get_info(active_thread_id).genmc_tid;
         let genmc_child_tid = thread_infos.get_info(child_thread_id).genmc_tid;
 
-        info!(
-            "GenMC: handling thread joining (thread {active_thread_id:?} ({genmc_curr_tid:?}) joining thread {child_thread_id:?} ({genmc_child_tid:?}))"
-        );
-
         let mut mc = self.handle.borrow_mut();
         mc.as_mut().handleThreadJoin(genmc_curr_tid.0, genmc_child_tid.0);
 

src/concurrency/thread.rs

@@ -113,8 +113,8 @@ pub enum BlockReason {
 }
 
 /// The state of a thread.
-// TODO GENMC: is this ok to be pub?
-pub enum ThreadState<'tcx> {
+// FIXME(genmc,question): is this ok to be public?
+pub(crate) enum ThreadState<'tcx> {
     /// The thread is enabled and can be executed.
     Enabled,
     /// The thread is blocked on something.
@@ -136,16 +136,16 @@ impl<'tcx> std::fmt::Debug for ThreadState<'tcx> {
 }
 
 impl<'tcx> ThreadState<'tcx> {
-    // TODO GENMC: is it ok if these are pub?
-    pub fn is_enabled(&self) -> bool {
+    // FIXME(genmc,question): is it ok for these to be public?
+    pub(crate) fn is_enabled(&self) -> bool {
         matches!(self, ThreadState::Enabled)
     }
 
-    pub fn is_terminated(&self) -> bool {
+    pub(crate) fn is_terminated(&self) -> bool {
         matches!(self, ThreadState::Terminated)
     }
 
-    pub fn is_blocked_on(&self, reason: BlockReason) -> bool {
+    pub(crate) fn is_blocked_on(&self, reason: BlockReason) -> bool {
         matches!(*self, ThreadState::Blocked { reason: actual_reason, .. } if actual_reason == reason)
     }
 }
@@ -211,8 +211,8 @@ impl<'tcx> Thread<'tcx> {
         self.thread_name.as_deref()
     }
 
-    pub fn get_state(&self) -> &ThreadState<'tcx> {
-        // TODO GENMC: should this implementation detail be exposed?
+    // FIXME(genmc,question): is this ok to be public? (it exposes implementation details)
+    pub(crate) fn get_state(&self) -> &ThreadState<'tcx> {
         &self.state
     }
 
@@ -349,10 +349,10 @@ impl VisitProvenance for Frame<'_, Provenance, FrameExtra<'_>> {
     }
 }
 
+// FIXME(genmc,question): is this ok to be public?
 /// The moment in time when a blocked thread should be woken up.
-// TODO GENMC: is this ok to be pub?
 #[derive(Debug)]
-pub enum Timeout {
+pub(crate) enum Timeout {
     Monotonic(Instant),
     RealTime(SystemTime),
 }
@@ -499,8 +499,11 @@ impl<'tcx> ThreadManager<'tcx> {
         &mut self.threads[self.active_thread].stack
     }
 
-    /// TODO GENMC: this function can probably be removed once the GenmcCtx code is finished:
-    pub fn get_thread_stack(&self, id: ThreadId) -> &[Frame<'tcx, Provenance, FrameExtra<'tcx>>] {
+    // FIXME(genmc,question): is this ok to exist?
+    pub(crate) fn get_thread_stack(
+        &self,
+        id: ThreadId,
+    ) -> &[Frame<'tcx, Provenance, FrameExtra<'tcx>>] {
         &self.threads[id].stack
     }
 
@@ -538,11 +541,6 @@ impl<'tcx> ThreadManager<'tcx> {
         self.threads.len()
     }
 
-    /// Get the total of threads that are currently enabled, i.e., could continue executing.
-    pub fn get_enabled_thread_count(&self) -> usize {
-        self.threads.iter().filter(|t| t.state.is_enabled()).count()
-    }
-
     /// Get the total of threads that are currently live, i.e., not yet terminated.
     /// (They might be blocked.)
     pub fn get_live_thread_count(&self) -> usize {
@@ -934,10 +932,6 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
         assert!(thread.stack.is_empty(), "only threads with an empty stack can be terminated");
         thread.state = ThreadState::Terminated;
 
-        // TODO GENMC (QUESTION): Can we move this down to where the GenmcCtx is?
-        if let Some(data_race) = this.machine.data_race.as_vclocks_mut() {
-            data_race.thread_terminated(&this.machine.threads);
-        }
         // Deallocate TLS.
         let gone_thread = this.active_thread();
         {
@@ -969,10 +963,16 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
             }
         }
 
-        // Inform GenMC that the thread finished.
-        // This needs to happen once all accesses to the thread are done, including freeing any TLS statics.
-        if let Some(genmc_ctx) = this.machine.data_race.as_genmc_ref() {
-            genmc_ctx.handle_thread_finish(&this.machine.threads);
+        // FIXME(genmc,question): Is it correct to move this code here?
+        match &mut this.machine.data_race {
+            GlobalDataRaceHandler::None => {}
+            GlobalDataRaceHandler::Vclocks(data_race) =>
+                data_race.thread_terminated(&this.machine.threads),
+            GlobalDataRaceHandler::Genmc(genmc_ctx) => {
+                // Inform GenMC that the thread finished.
+                // This needs to happen once all accesses to the thread are done, including freeing any TLS statics.
+                genmc_ctx.handle_thread_finish(&this.machine.threads)
+            }
         }
 
         // Unblock joining threads.

src/machine.rs

@@ -1462,7 +1462,7 @@ impl<'tcx> Machine<'tcx> for MiriMachine<'tcx> {
         match &machine.data_race {
             GlobalDataRaceHandler::None => {}
             GlobalDataRaceHandler::Genmc(genmc_ctx) =>
-                genmc_ctx.handle_dealloc(machine, alloc_id, ptr.addr(), size, align, kind)?,
+                genmc_ctx.handle_dealloc(machine, alloc_id, ptr.addr(), size, kind)?,
             GlobalDataRaceHandler::Vclocks(_global_state) => {
                 let data_race = alloc_extra.data_race.as_vclocks_mut().unwrap();
                 data_race.write(
@@ -1673,7 +1673,6 @@ impl<'tcx> Machine<'tcx> for MiriMachine<'tcx> {
         frame: &Frame<'tcx, Provenance, FrameExtra<'tcx>>,
         local: mir::Local,
     ) -> InterpResult<'tcx> {
-        // TODO GENMC: does GenMC care about local reads/writes?
         if let Some(data_race) = &frame.extra.data_race {
             data_race.local_read(local, &ecx.machine);
         }
@@ -1685,7 +1684,6 @@ impl<'tcx> Machine<'tcx> for MiriMachine<'tcx> {
         local: mir::Local,
         storage_live: bool,
     ) -> InterpResult<'tcx> {
-        // TODO GENMC: does GenMC care about local reads/writes?
         if let Some(data_race) = &ecx.frame().extra.data_race {
             data_race.local_write(local, storage_live, &ecx.machine);
         }
@@ -1715,7 +1713,6 @@ impl<'tcx> Machine<'tcx> for MiriMachine<'tcx> {
                 machine,
             );
         }
-        // TODO GENMC: how to handle this (if at all)?
         interp_ok(())
     }