miri genmc: fix exit() handling

compiler/rustc_const_eval/src/interpret/step.rs

@@ -562,8 +562,11 @@ impl<'tcx, M: Machine<'tcx>> InterpCx<'tcx, M> {
                     if fn_abi.can_unwind { unwind } else { mir::UnwindAction::Unreachable },
                 )?;
                 // Sanity-check that `eval_fn_call` either pushed a new frame or
-                // did a jump to another block.
-                if self.frame_idx() == old_stack && self.frame().loc == old_loc {
+                // did a jump to another block. We disable the sanity check for functions that
+                // can't return, since Miri sometimes does have to keep the location the same
+                // for those (which is fine since execution will continue on a different thread).
+                if target.is_some() && self.frame_idx() == old_stack && self.frame().loc == old_loc
+                {
                     span_bug!(terminator.source_info.span, "evaluating this call made no progress");
                 }
             }

src/bootstrap/src/core/build_steps/test.rs

@@ -665,7 +665,6 @@ impl Step for Miri {
         // miri tests need to know about the stage sysroot
         cargo.env("MIRI_SYSROOT", &miri_sysroot);
         cargo.env("MIRI_HOST_SYSROOT", &host_sysroot);
-        cargo.env("MIRI", &miri.tool_path);
 
         // Set the target.
         cargo.env("MIRI_TEST_TARGET", target.rustc_target_arg());

src/tools/miri/src/shims/foreign_items.rs

@@ -538,7 +538,7 @@ trait EvalContextExtPriv<'tcx>: crate::MiriInterpCxExt<'tcx> {
                         code,
                         crate::concurrency::ExitType::ExitCalled,
                     )?;
-                    todo!(); // FIXME(genmc): Add a way to return here that is allowed to not do progress (can't use existing EmulateItemResult variants).
+                    return interp_ok(EmulateItemResult::AlreadyJumped);
                 }
                 throw_machine_stop!(TerminationInfo::Exit { code, leak_check: false });
             }

src/tools/miri/tests/genmc/fail/shims/exit.rs

@@ -0,0 +1,9 @@
+//@ compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
+
+fn main() {
+    std::thread::spawn(|| {
+        unsafe { std::hint::unreachable_unchecked() }; //~ERROR: entering unreachable code
+    });
+    // If we exit immediately, we might entirely miss the UB in the other thread.
+    std::process::exit(0);
+}

src/tools/miri/tests/genmc/fail/shims/exit.stderr

@@ -0,0 +1,126 @@
+Running GenMC Verification...
+warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
+  --> RUSTLIB/std/src/thread/mod.rs:LL:CC
+   |
+LL |                     match COUNTER.compare_exchange_weak(last, id, Ordering::Relaxed, Ordering::Relaxed) {
+   |                           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
+   |
+   = note: BACKTRACE:
+   = note: inside `std::thread::ThreadId::new` at RUSTLIB/std/src/thread/mod.rs:LL:CC
+   = note: inside closure at RUSTLIB/std/src/thread/current.rs:LL:CC
+   = note: inside `std::thread::current::id::get_or_init` at RUSTLIB/std/src/thread/current.rs:LL:CC
+   = note: inside `std::thread::current_id` at RUSTLIB/std/src/thread/current.rs:LL:CC
+   = note: inside `std::rt::init` at RUSTLIB/std/src/rt.rs:LL:CC
+   = note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
+   = note: inside `std::panicking::catch_unwind::do_call::<{closure@std::rt::lang_start_internal::{closure#0}}, isize>` at RUSTLIB/std/src/panicking.rs:LL:CC
+   = note: inside `std::panicking::catch_unwind::<isize, {closure@std::rt::lang_start_internal::{closure#0}}>` at RUSTLIB/std/src/panicking.rs:LL:CC
+   = note: inside `std::panic::catch_unwind::<{closure@std::rt::lang_start_internal::{closure#0}}, isize>` at RUSTLIB/std/src/panic.rs:LL:CC
+   = note: inside `std::rt::lang_start_internal` at RUSTLIB/std/src/rt.rs:LL:CC
+   = note: inside `std::rt::lang_start::<()>` at RUSTLIB/std/src/rt.rs:LL:CC
+
+warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access.
+  --> RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
+   |
+LL |               || self
+   |  ________________^
+LL | |                 .state
+LL | |                 .compare_exchange_weak(state, state + READ_LOCKED, Acquire, Relaxed)
+   | |____________________________________________________________________________________^ GenMC might miss possible behaviors of this code
+   |
+   = note: BACKTRACE:
+   = note: inside `std::sys::sync::PLATFORM::futex::RwLock::read` at RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
+   = note: inside `std::sync::RwLock::<()>::read` at RUSTLIB/std/src/sync/poison/rwlock.rs:LL:CC
+   = note: inside `std::sys::env::PLATFORM::env_read_lock` at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
+   = note: inside closure at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
+   = note: inside `std::sys::pal::PLATFORM::small_c_string::run_with_cstr_stack::<std::option::Option<std::ffi::OsString>>` at RUSTLIB/std/src/sys/pal/PLATFORM/small_c_string.rs:LL:CC
+   = note: inside `std::sys::pal::PLATFORM::small_c_string::run_with_cstr::<std::option::Option<std::ffi::OsString>>` at RUSTLIB/std/src/sys/pal/PLATFORM/small_c_string.rs:LL:CC
+   = note: inside `std::sys::env::PLATFORM::getenv` at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
+   = note: inside `std::env::_var_os` at RUSTLIB/std/src/env.rs:LL:CC
+   = note: inside `std::env::var_os::<&str>` at RUSTLIB/std/src/env.rs:LL:CC
+   = note: inside closure at RUSTLIB/std/src/thread/mod.rs:LL:CC
+note: inside `main`
+  --> tests/genmc/fail/shims/exit.rs:LL:CC
+   |
+LL | /     std::thread::spawn(|| {
+LL | |         unsafe { std::hint::unreachable_unchecked() };
+LL | |     });
+   | |______^
+
+warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
+  --> RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
+   |
+LL |               || self
+   |  ________________^
+LL | |                 .state
+LL | |                 .compare_exchange_weak(state, state + READ_LOCKED, Acquire, Relaxed)
+   | |____________________________________________________________________________________^ GenMC might miss possible behaviors of this code
+   |
+   = note: BACKTRACE:
+   = note: inside `std::sys::sync::PLATFORM::futex::RwLock::read` at RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
+   = note: inside `std::sync::RwLock::<()>::read` at RUSTLIB/std/src/sync/poison/rwlock.rs:LL:CC
+   = note: inside `std::sys::env::PLATFORM::env_read_lock` at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
+   = note: inside closure at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
+   = note: inside `std::sys::pal::PLATFORM::small_c_string::run_with_cstr_stack::<std::option::Option<std::ffi::OsString>>` at RUSTLIB/std/src/sys/pal/PLATFORM/small_c_string.rs:LL:CC
+   = note: inside `std::sys::pal::PLATFORM::small_c_string::run_with_cstr::<std::option::Option<std::ffi::OsString>>` at RUSTLIB/std/src/sys/pal/PLATFORM/small_c_string.rs:LL:CC
+   = note: inside `std::sys::env::PLATFORM::getenv` at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
+   = note: inside `std::env::_var_os` at RUSTLIB/std/src/env.rs:LL:CC
+   = note: inside `std::env::var_os::<&str>` at RUSTLIB/std/src/env.rs:LL:CC
+   = note: inside closure at RUSTLIB/std/src/thread/mod.rs:LL:CC
+note: inside `main`
+  --> tests/genmc/fail/shims/exit.rs:LL:CC
+   |
+LL | /     std::thread::spawn(|| {
+LL | |         unsafe { std::hint::unreachable_unchecked() };
+LL | |     });
+   | |______^
+
+warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
+  --> RUSTLIB/std/src/rt.rs:LL:CC
+   |
+LL | /     CLEANUP.call_once(|| unsafe {
+LL | |         // Flush stdout and disable buffering.
+LL | |         crate::io::cleanup();
+...  |
+LL | |     });
+   | |______^ GenMC might miss possible behaviors of this code
+   |
+   = note: BACKTRACE:
+   = note: inside `std::rt::cleanup` at RUSTLIB/std/src/rt.rs:LL:CC
+   = note: inside `std::process::exit` at RUSTLIB/std/src/process.rs:LL:CC
+note: inside `main`
+  --> tests/genmc/fail/shims/exit.rs:LL:CC
+   |
+LL |     std::process::exit(0);
+   |     ^^^^^^^^^^^^^^^^^^^^^
+
+warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access.
+  --> RUSTLIB/std/src/sys/exit_guard.rs:LL:CC
+   |
+LL |             match EXITING_THREAD_ID.compare_exchange(ptr::null_mut(), this_thread_id, Acquire, Relaxed) {
+   |                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
+   |
+   = note: BACKTRACE:
+   = note: inside `std::sys::exit_guard::unique_thread_exit` at RUSTLIB/std/src/sys/exit_guard.rs:LL:CC
+   = note: inside `std::sys::pal::PLATFORM::os::exit` at RUSTLIB/std/src/sys/pal/PLATFORM/os.rs:LL:CC
+   = note: inside `std::process::exit` at RUSTLIB/std/src/process.rs:LL:CC
+note: inside `main`
+  --> tests/genmc/fail/shims/exit.rs:LL:CC
+   |
+LL |     std::process::exit(0);
+   |     ^^^^^^^^^^^^^^^^^^^^^
+
+error: Undefined Behavior: entering unreachable code
+  --> tests/genmc/fail/shims/exit.rs:LL:CC
+   |
+LL |         unsafe { std::hint::unreachable_unchecked() };
+   |                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Undefined Behavior occurred here
+   |
+   = help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
+   = help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
+
+note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
+
+note: add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report
+
+error: aborting due to 1 previous error; 5 warnings emitted
+

src/tools/miri/tests/ui.rs

@@ -27,7 +27,7 @@ enum Mode {
 }
 
 fn miri_path() -> PathBuf {
-    PathBuf::from(env::var("MIRI").unwrap_or_else(|_| env!("CARGO_BIN_EXE_miri").into()))
+    env!("CARGO_BIN_EXE_miri").into()
 }
 
 // Build the shared object file for testing native function calls.