diff --git a/src/tools/miri/src/concurrency/genmc/mod.rs b/src/tools/miri/src/concurrency/genmc/mod.rs index bc475c680b5b..6628e096a25d 100644 --- a/src/tools/miri/src/concurrency/genmc/mod.rs +++ b/src/tools/miri/src/concurrency/genmc/mod.rs @@ -8,9 +8,9 @@ use genmc_sys::{ use rustc_abi::{Align, Size}; use rustc_const_eval::interpret::{AllocId, InterpCx, InterpResult, interp_ok}; use rustc_data_structures::fx::FxHashMap; -use rustc_middle::{throw_machine_stop, throw_ub_format, throw_unsup_format}; +use rustc_middle::{throw_ub_format, throw_unsup_format}; // FIXME(genmc,tracing): Implement some work-around for enabling debug/trace level logging (currently disabled statically in rustc). -use tracing::{debug, info}; +use tracing::debug; use self::global_allocations::{EvalContextExt as _, GlobalAllocationHandler}; use self::helper::{ @@ -63,12 +63,6 @@ struct ExitStatus { exit_type: ExitType, } -impl ExitStatus { - fn do_leak_check(self) -> bool { - matches!(self.exit_type, ExitType::MainThreadFinish) - } -} - /// State that is reset at the start of every execution. #[derive(Debug, Default)] struct PerExecutionState { @@ -223,8 +217,6 @@ impl GenmcCtx { /// Inform GenMC that the program's execution has ended. /// - /// This function must be called even when the execution is blocked - /// (i.e., it returned a `InterpErrorKind::MachineStop` with error kind `TerminationInfo::GenmcBlockedExecution`). /// Don't call this function if an error was found. /// /// GenMC detects certain errors only when the execution ends. @@ -694,39 +686,37 @@ impl GenmcCtx { } /// Handle a call to `libc::exit` or the exit of the main thread. - /// Unless an error is returned, the program should continue executing (in a different thread, chosen by the next scheduling call). + /// Unless an error is returned, the program should continue executing (in a different thread, + /// chosen by the next scheduling call). pub(crate) fn handle_exit<'tcx>( &self, thread: ThreadId, exit_code: i32, exit_type: ExitType, ) -> InterpResult<'tcx> { - // Calling `libc::exit` doesn't do cleanup, so we skip the leak check in that case. - let exit_status = ExitStatus { exit_code, exit_type }; - if let Some(old_exit_status) = self.exec_state.exit_status.get() { throw_ub_format!( - "`exit` called twice, first with status {old_exit_status:?}, now with status {exit_status:?}", + "`exit` called twice, first with exit code {old_exit_code}, now with status {exit_code}", + old_exit_code = old_exit_status.exit_code, ); } - // FIXME(genmc): Add a flag to continue exploration even when the program exits with a non-zero exit code. - if exit_code != 0 { - info!("GenMC: 'exit' called with non-zero argument, aborting execution."); - let leak_check = exit_status.do_leak_check(); - throw_machine_stop!(TerminationInfo::Exit { code: exit_code, leak_check }); + match exit_type { + ExitType::ExitCalled => { + // `exit` kills the current thread; we have to tell GenMC about this. + let thread_infos = self.exec_state.thread_id_manager.borrow(); + let genmc_tid = thread_infos.get_genmc_tid(thread); + self.handle.borrow_mut().pin_mut().handle_thread_kill(genmc_tid); + } + ExitType::MainThreadFinish => { + // The main thread has already exited so we don't call `handle_thread_kill` again. + assert_eq!(thread, ThreadId::MAIN_THREAD); + } } - - if matches!(exit_type, ExitType::ExitCalled) { - let thread_infos = self.exec_state.thread_id_manager.borrow(); - let genmc_tid = thread_infos.get_genmc_tid(thread); - - self.handle.borrow_mut().pin_mut().handle_thread_kill(genmc_tid); - } else { - assert_eq!(thread, ThreadId::MAIN_THREAD); - } - // We continue executing now, so we store the exit status. - self.exec_state.exit_status.set(Some(exit_status)); + // To cover all possible behaviors, we have to continue execution the other threads: + // whatever they do next could also have happened before the `exit` call. So we just + // remember the exit status and use it when the other threads are done. + self.exec_state.exit_status.set(Some(ExitStatus { exit_code, exit_type })); interp_ok(()) } } diff --git a/src/tools/miri/src/concurrency/genmc/scheduling.rs b/src/tools/miri/src/concurrency/genmc/scheduling.rs index 0703e0595b33..c760126d787d 100644 --- a/src/tools/miri/src/concurrency/genmc/scheduling.rs +++ b/src/tools/miri/src/concurrency/genmc/scheduling.rs @@ -118,14 +118,21 @@ impl GenmcCtx { // Depending on the exec_state, we either schedule the given thread, or we are finished with this execution. match result.exec_state { ExecutionState::Ok => interp_ok(Some(thread_infos.get_miri_tid(result.next_thread))), - ExecutionState::Blocked => throw_machine_stop!(TerminationInfo::GenmcBlockedExecution), + ExecutionState::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, + }); + } ExecutionState::Finished => { let exit_status = self.exec_state.exit_status.get().expect( "If the execution is finished, we should have a return value from the program.", ); throw_machine_stop!(TerminationInfo::Exit { code: exit_status.exit_code, - leak_check: exit_status.do_leak_check() + leak_check: matches!(exit_status.exit_type, super::ExitType::MainThreadFinish), }); } ExecutionState::Error => { diff --git a/src/tools/miri/src/diagnostics.rs b/src/tools/miri/src/diagnostics.rs index 70543c653b6d..bb8ba196983c 100644 --- a/src/tools/miri/src/diagnostics.rs +++ b/src/tools/miri/src/diagnostics.rs @@ -33,9 +33,6 @@ pub enum TerminationInfo { }, Int2PtrWithStrictProvenance, Deadlock, - /// In GenMC mode, executions can get blocked, which stops the current execution without running any cleanup. - /// No leak checks should be performed if this happens, since they would give false positives. - GenmcBlockedExecution, MultipleSymbolDefinitions { link_name: Symbol, first: SpanData, @@ -80,8 +77,6 @@ impl fmt::Display for TerminationInfo { StackedBorrowsUb { msg, .. } => write!(f, "{msg}"), TreeBorrowsUb { title, .. } => write!(f, "{title}"), Deadlock => write!(f, "the evaluated program deadlocked"), - GenmcBlockedExecution => - write!(f, "GenMC determined that the execution got blocked (this is not an error)"), MultipleSymbolDefinitions { link_name, .. } => write!(f, "multiple definitions of symbol `{link_name}`"), SymbolShimClashing { link_name, .. } => @@ -254,13 +249,6 @@ pub fn report_result<'tcx>( labels.push(format!("this thread got stuck here")); None } - GenmcBlockedExecution => { - // This case should only happen in GenMC mode. - assert!(ecx.machine.data_race.as_genmc_ref().is_some()); - // The program got blocked by GenMC without finishing the execution. - // No cleanup code was executed, so we don't do any leak checks. - return Some((0, false)); - } MultipleSymbolDefinitions { .. } | SymbolShimClashing { .. } => None, }; #[rustfmt::skip]