diff --git a/src/concurrency/genmc/helper.rs b/src/concurrency/genmc/helper.rs index 1870a8e4e2..34314c84db 100644 --- a/src/concurrency/genmc/helper.rs +++ b/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) -> 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), } diff --git a/src/concurrency/genmc/mod.rs b/src/concurrency/genmc/mod.rs index dfd7d4b526..a4eab95fbe 100644 --- a/src/concurrency/genmc/mod.rs +++ b/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, }; diff --git a/src/concurrency/genmc/scheduling.rs b/src/concurrency/genmc/scheduling.rs index 253446e3eb..e704346ad2 100644 --- a/src/concurrency/genmc/scheduling.rs +++ b/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( diff --git a/src/diagnostics.rs b/src/diagnostics.rs index 7e8c49bf9f..787a213df9 100644 --- a/src/diagnostics.rs +++ b/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)); }