genmc: rename 'invalid' to 'moot'

src/concurrency/genmc/helper.rs

@@ -16,7 +16,8 @@ pub(super) const MAX_ACCESS_SIZE: u64 = 8;
 // FIXME(genmc): improve error handling.
 pub(super) fn get_outcome<'tcx, T>(result: GenmcHandlerResult<T>) -> InterpResult<'tcx, T> {
     match result {
-        GenmcHandlerResult::Invalid => throw_machine_stop!(TerminationInfo::GenmcInvalid),
+        // A handler producing an invalid result means that the execution is moot.
+        GenmcHandlerResult::Invalid => throw_machine_stop!(TerminationInfo::GenmcMoot),
         GenmcHandlerResult::Error(e) => throw_ub_format!("{e}"),
         GenmcHandlerResult::Ok(outcome) => interp_ok(outcome),
     }

src/concurrency/genmc/mod.rs

@@ -527,7 +527,7 @@ impl GenmcCtx {
             alignment.bytes(),
         );
         let chosen_address = match malloc_result.into_genmc_result() {
-            GenmcHandlerResult::Invalid => throw_machine_stop!(TerminationInfo::GenmcInvalid),
+            GenmcHandlerResult::Invalid => throw_machine_stop!(TerminationInfo::GenmcMoot),
             GenmcHandlerResult::Error(_e) => throw_exhaust!(AddressSpaceFull),
             GenmcHandlerResult::Ok(a) => a,
         };

src/concurrency/genmc/scheduling.rs

@@ -120,12 +120,8 @@ impl GenmcCtx {
         match result.exec_status {
             ExecutionStatus::Ok => interp_ok(Some(thread_infos.get_miri_tid(result.next_thread))),
             ExecutionStatus::Blocked => {
-                // This execution doesn't need further exploration. We treat this as "success, no
-                // leak check needed", which makes it a NOP in the big outer loop.
-                throw_machine_stop!(TerminationInfo::Exit {
-                    code: 0, // success
-                    leak_check: false,
-                });
+                // This execution is "moot", it doesn't need further exploration.
+                throw_machine_stop!(TerminationInfo::GenmcMoot);
             }
             ExecutionStatus::Finished => {
                 let exit_status = self.exec_state.exit_status.get().expect(

src/diagnostics.rs

@@ -32,9 +32,9 @@ pub enum TerminationInfo {
         history: tree_diagnostics::HistoryData,
     },
     Int2PtrWithStrictProvenance,
-    /// GenMC deemed this execution invalid, so Miri drops it, i.e., it skips to the next execution
-    /// (mirrors GenMC's `Invalid` result).
-    GenmcInvalid,
+    /// GenMC deemed this execution "moot" or invalid, so Miri drops it, i.e., it skips to the next
+    /// execution. Mirrors GenMC's `Invalid` result or a "moot" result from the scheduler.
+    GenmcMoot,
     /// All threads are blocked.
     GlobalDeadlock,
     /// Some thread discovered a deadlock condition (e.g. in a mutex with reentrancy checking).
@@ -84,7 +84,7 @@ impl fmt::Display for TerminationInfo {
             TreeBorrowsUb { title, .. } => write!(f, "{title}"),
             GlobalDeadlock => write!(f, "the evaluated program deadlocked"),
             LocalDeadlock => write!(f, "a thread deadlocked"),
-            GenmcInvalid => write!(f, "GenMC wants to skip this execution"),
+            GenmcMoot => write!(f, "GenMC wants to skip this execution"),
             MultipleSymbolDefinitions { link_name, .. } =>
                 write!(f, "multiple definitions of symbol `{link_name}`"),
             SymbolShimClashing { link_name, .. } =>
@@ -258,7 +258,7 @@ pub fn report_result<'tcx>(
                 Some("unsupported operation"),
             StackedBorrowsUb { .. } | TreeBorrowsUb { .. } | DataRace { .. } =>
                 Some("Undefined Behavior"),
-            GenmcInvalid => {
+            GenmcMoot => {
                 assert!(ecx.machine.data_race.as_genmc_ref().is_some());
                 return Some((0, false));
             }