genmc: slightly simplify exit handling; get rid of GenmcBlockedExecution

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 });
-        }
-
-        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);
+        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);
+            }
         }
-        // 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(())
     }
 }

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 => {

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]