Clean up TODOs and comments, improve error handling.

Author: Patrick-6

genmc-sys/build.rs

@@ -26,9 +26,9 @@ mod downloading {
     use super::GENMC_DOWNLOAD_PATH;
 
     /// The GenMC repository the we get our commit from.
-    pub(crate) const GENMC_GITHUB_URL: &str = "https://github.com/MPI-SWS/genmc.git";
+    pub(crate) const GENMC_GITHUB_URL: &str = "https://github.com/Patrick-6/genmc.git";
     /// The GenMC commit we depend on. It must be available on the specified GenMC repository.
-    pub(crate) const GENMC_COMMIT: &str = "3438dd2c1202cd4a47ed7881d099abf23e4167ab";
+    pub(crate) const GENMC_COMMIT: &str = "56997d85fc9c07f75431570d49ce4892b22b8e6e";
 
     pub(crate) fn download_genmc() -> PathBuf {
         let Ok(genmc_download_path) = PathBuf::from_str(GENMC_DOWNLOAD_PATH);

genmc-sys/src/lib.rs

@@ -66,18 +66,20 @@ mod ffi {
 
     /**** \/ Result & Error types \/ ****/
 
+    // FIXME(genmc): Rework error handling (likely requires changes on the GenMC side).
+
     #[must_use]
     #[derive(Debug)]
     struct LoadResult {
         is_read_opt: bool,
-        read_value: GenmcScalar,     // TODO GENMC: handle bigger values
-        error: UniquePtr<CxxString>, // TODO GENMC: pass more error info here
+        read_value: GenmcScalar,
+        error: UniquePtr<CxxString>,
     }
 
     #[must_use]
     #[derive(Debug)]
     struct StoreResult {
-        error: UniquePtr<CxxString>, // TODO GENMC: pass more error info here
+        error: UniquePtr<CxxString>,
         isCoMaxWrite: bool,
     }
 

src/alloc_addresses/mod.rs

@@ -33,7 +33,7 @@ pub struct GlobalStateInner {
     /// sorted by address. We cannot use a `HashMap` since we can be given an address that is offset
     /// from the base address, and we need to find the `AllocId` it belongs to. This is not the
     /// *full* inverse of `base_addr`; dead allocations have been removed.
-    /// TODO GENMC: keep dead allocations in GenMC mode?
+    /// FIXME(genmc,dead allocs): keep dead allocations in GenMC mode?
     int_to_ptr_map: Vec<(u64, AllocId)>,
     /// The base address for each allocation.  We cannot put that into
     /// `AllocExtra` because function pointers also have a base address, and
@@ -516,7 +516,7 @@ impl<'tcx> MiriMachine<'tcx> {
         let pos =
             global_state.int_to_ptr_map.binary_search_by_key(&addr, |(addr, _)| *addr).unwrap();
 
-        // TODO GENMC(DOCUMENTATION):
+        // FIXME(genmc,dead allocs): keep dead allocations in GenMC mode?
         if self.data_race.as_genmc_ref().is_none() {
             let removed = global_state.int_to_ptr_map.remove(pos);
             assert_eq!(removed, (addr, dead_id)); // double-check that we removed the right thing

src/concurrency/genmc/config.rs

@@ -27,17 +27,11 @@ impl GenmcConfig {
         if trimmed_arg.is_empty() {
             return Ok(()); // this corresponds to "-Zmiri-genmc"
         }
-        let genmc_config = genmc_config.as_mut().unwrap();
+        let _genmc_config = genmc_config.as_mut().unwrap();
         let Some(trimmed_arg) = trimmed_arg.strip_prefix("-") else {
             return Err(format!("Invalid GenMC argument \"-Zmiri-genmc{trimmed_arg}\""));
         };
-        if trimmed_arg == "symmetry-reduction" {
-            // TODO GENMC (PERFORMANCE): maybe make this the default, have an option to turn it off instead
-            genmc_config.params.do_symmetry_reduction = true;
-        } else {
-            // TODO GENMC: how to properly handle this?
-            return Err(format!("Invalid GenMC argument: \"-Zmiri-genmc-{trimmed_arg}\""));
-        }
-        return Ok(());
+        // FIXME(genmc): Add parsing for remaining parameters.
+        return Err(format!("Invalid GenMC argument: \"-Zmiri-genmc-{trimmed_arg}\""));
     }
 }

src/concurrency/genmc/helper.rs

@@ -63,8 +63,8 @@ pub fn scalar_to_genmc_scalar<'tcx>(
 ) -> InterpResult<'tcx, GenmcScalar> {
     interp_ok(match scalar {
         rustc_const_eval::interpret::Scalar::Int(scalar_int) => {
-            // TODO GENMC: u128 support
-            let value: u64 = scalar_int.to_uint(scalar_int.size()).try_into().unwrap(); // TODO GENMC: doesn't work for size != 8
+            // FIXME(genmc): 128bit atomics support
+            let value: u64 = scalar_int.to_uint(scalar_int.size()).try_into().unwrap();
             GenmcScalar { value, is_init: true }
         }
         rustc_const_eval::interpret::Scalar::Ptr(_pointer, _size) =>

src/concurrency/genmc/miri_genmc.rs

@@ -12,7 +12,8 @@ pub fn run_genmc_mode(
         tracing::info!("Miri-GenMC loop {}", rep + 1);
         let result = eval_entry(genmc_ctx.clone());
 
-        // TODO GENMC (ERROR REPORTING): we currently do this here, so we can still print the GenMC graph above
+        // FIXME(genmc): tell GenMC to print the execution graph here (if requested by the user).
+
         let return_code = result?;
 
         let is_exploration_done = genmc_ctx.is_exploration_done();
@@ -33,7 +34,7 @@ pub fn run_genmc_mode(
                 eprintln!("Number of blocked executions seen: {blocked_execution_count}");
             }
 
-            // TODO GENMC: what is an appropriate return code? (since there are possibly many)
+            // Return the return code of the last execution.
             return Some(return_code);
         }
     }

src/concurrency/genmc/mod.rs

@@ -43,7 +43,7 @@ struct ExitStatus {
 pub struct GenmcCtx {
     handle: RefCell<UniquePtr<MiriGenMCShim>>,
 
-    // TODO GENMC (PERFORMANCE): could use one RefCell for all internals instead of multiple
+    // FIXME(genmc,performance): we could use one RefCell for all internals instead of multiple
     thread_infos: RefCell<ThreadInfoManager>,
 
     /// Some actions Miri does are allowed to cause data races.
@@ -54,6 +54,8 @@ pub struct GenmcCtx {
     /// The `AllocId` for globals is stable across executions, so we can use it as an identifier.
     global_allocations: Arc<GlobalAllocationHandler>,
 
+    /// The exit status of the program.
+    /// `None` if no thread has called `exit` and the main thread isn't finished yet.
     exit_status: Cell<Option<ExitStatus>>,
 }
 
@@ -126,9 +128,10 @@ impl GenmcCtx {
         let mut mc = self.handle.borrow_mut();
         let result = mc.as_mut().unwrap().handleExecutionEnd();
         if let Some(msg) = result.as_ref() {
+            // FIXME(genmc): error handling (may need changes on GenMC side first).
             let msg = msg.to_string_lossy().to_string();
             info!("GenMC: execution ended with error \"{msg}\"");
-            Err(msg) // TODO GENMC: add more error info here, and possibly handle this without requiring to clone the CxxString
+            Err(msg)
         } else {
             Ok(())
         }
@@ -162,7 +165,7 @@ impl GenmcCtx {
         old_val: Option<Scalar>,
     ) -> InterpResult<'tcx, Scalar> {
         info!("GenMC: atomic_load: old_val: {old_val:?}");
-        assert!(!self.allow_data_races.get()); // TODO GENMC: handle this properly
+        assert!(!self.allow_data_races.get()); // FIXME(genmc): ensure correct behavior whereever `allow_data_races` is used.
         let ordering = ordering.convert();
         let genmc_old_value = option_scalar_to_genmc_scalar(ecx, old_val)?;
         let read_value =
@@ -181,7 +184,7 @@ impl GenmcCtx {
         old_value: Option<Scalar>,
         ordering: AtomicWriteOrd,
     ) -> InterpResult<'tcx, bool> {
-        assert!(!self.allow_data_races.get()); // TODO GENMC: handle this properly
+        assert!(!self.allow_data_races.get());
         let ordering = ordering.convert();
         let genmc_value = scalar_to_genmc_scalar(ecx, value)?;
         let genmc_old_value = option_scalar_to_genmc_scalar(ecx, old_value)?;
@@ -319,7 +322,6 @@ impl GenmcCtx {
         machine: &MiriMachine<'tcx>,
         address: Size,
         size: Size,
-        // old_value: Option<Scalar>, // TODO GENMC(mixed atomic-non-atomic): is this needed?
     ) -> InterpResult<'tcx> {
         info!(
             "GenMC: received memory_store (non-atomic): address: {:#x}, size: {}",
@@ -336,7 +338,6 @@ impl GenmcCtx {
         }
 
         if size.bytes() <= 8 {
-            // TODO GENMC(mixed atomic-non-atomics): anything to do here?
             let _is_co_max_write = self.atomic_store_impl(
                 machine,
                 address,
@@ -436,7 +437,6 @@ impl GenmcCtx {
         let pinned_mc = mc.as_mut().unwrap();
         pinned_mc.handleFree(genmc_tid.0, genmc_address, genmc_size);
 
-        // TODO GENMC (ERROR HANDLING): can this ever fail?
         interp_ok(())
     }
 
@@ -445,11 +445,11 @@ impl GenmcCtx {
     pub(crate) fn handle_thread_create<'tcx>(
         &self,
         threads: &ThreadManager<'tcx>,
-        _start_routine: crate::Pointer, // TODO GENMC: pass info to GenMC
+        _start_routine: crate::Pointer, // FIXME(genmc): symmetry reduction will need this info
         _func_arg: &crate::ImmTy<'tcx>,
         new_thread_id: ThreadId,
     ) -> InterpResult<'tcx> {
-        assert!(!self.allow_data_races.get()); // TODO GENMC: handle this properly
+        assert!(!self.allow_data_races.get());
         let mut thread_infos = self.thread_infos.borrow_mut();
 
         let curr_thread_id = threads.active_thread();
@@ -467,7 +467,7 @@ impl GenmcCtx {
         active_thread_id: ThreadId,
         child_thread_id: ThreadId,
     ) -> InterpResult<'tcx> {
-        assert!(!self.allow_data_races.get()); // TODO GENMC: handle this properly
+        assert!(!self.allow_data_races.get());
         let thread_infos = self.thread_infos.borrow();
 
         let genmc_curr_tid = thread_infos.get_info(active_thread_id).genmc_tid;
@@ -480,7 +480,7 @@ impl GenmcCtx {
     }
 
     pub(crate) fn handle_thread_finish<'tcx>(&self, threads: &ThreadManager<'tcx>) {
-        assert!(!self.allow_data_races.get()); // TODO GENMC: handle this properly
+        assert!(!self.allow_data_races.get());
         let curr_thread_id = threads.active_thread();
 
         let thread_infos = self.thread_infos.borrow();
@@ -544,7 +544,7 @@ impl GenmcCtx {
         if size.bytes() > 8 {
             throw_unsup_format!("{UNSUPPORTED_ATOMICS_SIZE_MSG}");
         }
-        assert!(!self.allow_data_races.get()); // TODO GENMC: handle this properly
+        assert!(!self.allow_data_races.get());
         let thread_infos = self.thread_infos.borrow();
         let curr_thread_id = machine.threads.active_thread();
         let genmc_tid = thread_infos.get_info(curr_thread_id).genmc_tid;
@@ -571,9 +571,10 @@ impl GenmcCtx {
         }
 
         if let Some(error) = load_result.error.as_ref() {
+            // FIXME(genmc): error handling
             let msg = error.to_string_lossy().to_string();
             info!("GenMC: load operation returned an error: \"{msg}\"");
-            throw_ub_format!("{}", msg); // TODO GENMC: proper error handling: find correct error here
+            throw_ub_format!("{}", msg);
         }
 
         info!("GenMC: load returned value: {:?}", load_result.read_value);
@@ -621,9 +622,10 @@ impl GenmcCtx {
         );
 
         if let Some(error) = store_result.error.as_ref() {
+            // FIXME(genmc): error handling
             let msg = error.to_string_lossy().to_string();
             info!("GenMC: store operation returned an error: \"{msg}\"");
-            throw_ub_format!("{}", msg); // TODO GENMC: proper error handling: find correct error here
+            throw_ub_format!("{}", msg);
         }
 
         interp_ok(store_result.isCoMaxWrite)
@@ -635,7 +637,7 @@ impl GenmcCtx {
         &self,
         ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
     ) -> InterpResult<'tcx, ThreadId> {
-        assert!(!self.allow_data_races.get()); // TODO GENMC: handle this properly
+        assert!(!self.allow_data_races.get());
         let thread_manager = &ecx.machine.threads;
         let active_thread_id = thread_manager.active_thread();
 
@@ -674,7 +676,6 @@ impl GenmcCtx {
         let result =
             pinned_mc.scheduleNext(curr_thread_info.genmc_tid.0, curr_thread_next_instr_kind);
         if result >= 0 {
-            // TODO GENMC: can we ensure this thread_id is valid?
             let genmc_next_thread_id = result.try_into().unwrap();
             let genmc_next_thread_id = GenmcThreadId(genmc_next_thread_id);
             let thread_infos = self.thread_infos.borrow();

src/concurrency/genmc/thread_info_manager.rs

@@ -57,7 +57,7 @@ impl ThreadInfoManager {
         let index = self.thread_infos.len();
         let genmc_tid = GenmcThreadId(index.try_into().unwrap());
         let thread_info = ThreadInfo::new(thread_id, genmc_tid);
-        // TODO GENMC: Document this in place where ThreadIds are created
+        // FIXME(genmc): Document this in place where ThreadIds are created
         assert!(
             self.tid_map.insert(thread_id, genmc_tid).is_none(),
             "Cannot reuse thread ids: thread id {thread_id:?} already inserted"
@@ -76,6 +76,14 @@ impl ThreadInfoManager {
     #[must_use]
     pub fn get_info_genmc(&self, genmc_tid: GenmcThreadId) -> &ThreadInfo {
         let index: usize = genmc_tid.0.try_into().unwrap();
-        &self.thread_infos[index]
+        let Some(infos) = self.thread_infos.get(index) else {
+            panic!(
+                "GenMC returned invalid thread id: {}, existing thread ids: {}..{}",
+                genmc_tid.0,
+                GENMC_MAIN_THREAD_ID.0,
+                self.thread_infos.len()
+            );
+        };
+        infos
     }
 }