Clean up TODOs and comments, improve error handling and remove accidental changes.

Patrick-6 · Patrick-6 · commit a42452b78686 · 2025-07-30T16:25:07.000+02:00
diff --git a/Cargo.toml b/Cargo.toml
@@ -17,9 +17,6 @@ name = "miri"
 test = false    # we have no unit tests
 doctest = false # and no doc tests
 
-[profile.bench]
-debug = true
-
 [dependencies]
 getrandom = { version = "0.3", features = ["std"] }
 rand = "0.9"
diff --git a/genmc-sys/.gitignore b/genmc-sys/.gitignore
@@ -1,2 +1 @@
 genmc-src*/
-genmc*/
diff --git a/genmc-sys/build.rs b/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);
diff --git a/genmc-sys/src/lib.rs b/genmc-sys/src/lib.rs
@@ -3,7 +3,7 @@ pub use cxx::UniquePtr;
 pub use self::ffi::*;
 
 /// Defined in "genmc/src/Support/SAddr.hpp"
-/// FIXME: currently we use `getGlobalAllocStaticMask()` to ensure the constant is consistent between Miri and GenMC,
+/// FIXME(genmc): `getGlobalAllocStaticMask()` is used to ensure the constant is consistent between Miri and GenMC,
 ///   but if https://github.com/dtolnay/cxx/issues/1051 is fixed we could share the constant directly.
 pub const GENMC_GLOBAL_ADDRESSES_MASK: u64 = 1 << 63;
 
@@ -36,9 +36,9 @@ mod ffi {
     /// (The fields of this struct are visible to both Rust and C++)
     #[derive(Clone, Debug)]
     struct GenmcParams {
-        // pub genmc_seed: u64; // OR: Option<u64>
         pub print_random_schedule_seed: bool,
         pub do_symmetry_reduction: bool,
+        // FIXME(GenMC): Add remaining parameters.
     }
 
     #[derive(Debug)]
@@ -68,18 +68,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,
     }
 
diff --git a/genmc-sys/src_cpp/MiriInterface.cpp b/genmc-sys/src_cpp/MiriInterface.cpp
@@ -77,12 +77,13 @@ auto MiriGenMCShim::createHandle(const GenmcParams &config)
 
 	// FIXME(genmc): implement symmetry reduction.
 	ERROR_ON(config.do_symmetry_reduction,
-		 "Symmetry reduction is currently unsupported in GenMC mode.");
+			 "Symmetry reduction is currently unsupported in GenMC mode.");
 	conf->symmetryReduction = config.do_symmetry_reduction;
 
 	// FIXME(genmc): expose this setting to Miri (useful for testing Miri-GenMC).
 	conf->schedulePolicy = SchedulePolicy::WF;
 
+	// FIXME(genmc): implement estimation mode.
 	conf->estimate = false;
 	const auto mode = GenMCDriver::Mode(GenMCDriver::VerificationMode{});
 
diff --git a/genmc-sys/src_cpp/MiriInterface.hpp b/genmc-sys/src_cpp/MiriInterface.hpp
@@ -24,14 +24,6 @@ struct GenmcParams;
 
 using ThreadId = int;
 
-enum class StoreEventType : uint8_t
-{
-	Normal,
-	CompareExchange,
-};
-
-// TODO GENMC: fix naming conventions
-
 struct MiriGenMCShim : private GenMCDriver
 {
 
@@ -52,7 +44,6 @@ struct MiriGenMCShim : private GenMCDriver
 
 	/**** Memory access handling ****/
 
-	///////////////////
 	[[nodiscard]] LoadResult handleLoad(ThreadId thread_id, uint64_t address, uint64_t size,
 										MemOrdering ord, GenmcScalar old_val);
 	[[nodiscard]] StoreResult handleStore(ThreadId thread_id, uint64_t address, uint64_t size,
@@ -111,8 +102,7 @@ struct MiriGenMCShim : private GenMCDriver
 
 /**** Functions available to Miri ****/
 
-// NOTE: CXX doesn't seem to support exposing static methods to Rust, so we expose this
-// function instead
+// NOTE: CXX doesn't support exposing static methods to Rust currently, so we expose this function instead.
 std::unique_ptr<MiriGenMCShim> createGenmcHandle(const GenmcParams &config);
 
 constexpr auto getGlobalAllocStaticMask() -> uint64_t { return SAddr::staticMask; }
diff --git a/miri-script/src/commands.rs b/miri-script/src/commands.rs
@@ -112,8 +112,8 @@ impl Command {
             Command::Check { features, flags } => Self::check(features, flags),
             Command::Test { bless, target, coverage, features, flags } =>
                 Self::test(bless, target, coverage, features, flags),
-            Command::Run { dep, verbose, target, edition, features, flags, flamegraph } =>
-                Self::run(dep, verbose, target, edition, features, flags, flamegraph),
+            Command::Run { dep, verbose, target, edition, features, flags } =>
+                Self::run(dep, verbose, target, edition, features, flags),
             Command::Doc { features, flags } => Self::doc(features, flags),
             Command::Fmt { flags } => Self::fmt(flags),
             Command::Clippy { features, flags } => Self::clippy(features, flags),
@@ -463,7 +463,6 @@ impl Command {
         edition: Option<String>,
         features: Vec<String>,
         flags: Vec<String>,
-        flamegraph: bool,
     ) -> Result<()> {
         let mut e = MiriEnv::new()?;
 
@@ -499,18 +498,11 @@ impl Command {
         // The basic command that executes the Miri driver.
         let mut cmd = if dep {
             // We invoke the test suite as that has all the logic for running with dependencies.
-            let cmd = e
-                .cargo_cmd(".", "test", &features)
+            e.cargo_cmd(".", "test", &features)
                 .args(&["--test", "ui"])
                 .args(quiet_flag)
-                .arg("--");
-            if flamegraph {
-                cmd.args(&["--miri-run-dep-mode-flamegraph"])
-            } else {
-                cmd.args(&["--miri-run-dep-mode"])
-            }
-        } else if flamegraph {
-            cmd!(e.sh, "flamegraph -- {miri_bin}")
+                .arg("--")
+                .args(&["--miri-run-dep-mode"])
         } else {
             cmd!(e.sh, "{miri_bin}")
         };
diff --git a/miri-script/src/main.rs b/miri-script/src/main.rs
@@ -96,9 +96,6 @@ pub enum Command {
         /// The flags set in `MIRIFLAGS` are added in front of these flags.
         #[arg(trailing_var_arg = true, allow_hyphen_values = true)]
         flags: Vec<String>,
-        /// Run with flamegraph (requires cargo-flamegraph to be installed)
-        #[arg(long)]
-        flamegraph: bool,
     },
     /// Build documentation.
     Doc {
diff --git a/src/alloc_addresses/mod.rs b/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
@@ -510,7 +510,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
diff --git a/src/concurrency/genmc/config.rs b/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}\""));
-        }
-        Ok(())
+        // FIXME(genmc): Add parsing for remaining parameters.
+        Err(format!("Invalid GenMC argument: \"-Zmiri-genmc-{trimmed_arg}\""))
     }
 }
diff --git a/src/concurrency/genmc/helper.rs b/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) =>
diff --git a/src/concurrency/genmc/miri_genmc.rs b/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();
@@ -32,7 +33,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);
         }
     }
diff --git a/src/concurrency/genmc/mod.rs b/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();
@@ -554,7 +554,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;
@@ -581,9 +581,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);
@@ -631,9 +632,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)
@@ -645,7 +647,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();
 
@@ -684,7 +686,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();
diff --git a/src/concurrency/genmc/thread_info_manager.rs b/src/concurrency/genmc/thread_info_manager.rs
diff --git a/tests/ui.rs b/tests/ui.rs
