Rollup merge of #148991 - RalfJung:genmc-exit, r=oli-obk

miri genmc: fix exit() handling

In genmc mode, Miri does not want to stop execution when `exit` is called. Instead we want to continue running other threads to ensure we covered all possible concurrent behaviors (including the ones where the exiting thread was delayed so the other threads took their turns first). However, the core interpreter has a sanity check that prevents us from just doing nothing in `exit`. This leaves us in a pickle: there's nowhere we can jump to (exit has return type `!` so there's no next block), but if we don't jump anywhere we ICE.

The first commit fixes that by disabling the sanity check when there is no block to jump to. That still catches the mistake of forgetting to jump for the vast majority of shims.

We currently don't build Miri's genmc integration in rustc CI so I had to hack the feature into the bootstrap miri integration. That turned out to use the wrong Miri binary, which is fixed by the second commit: we can just rely on CARGO_BIN_EXE_miri, there's no need for a MIRI environment variable.

r? ``@oli-obk``

Author: matthiaskrgr

compiler/rustc_const_eval/src/interpret/step.rs

@@ -561,8 +561,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

@@ -722,7 +722,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.