Skip to content

Commit ee84ff9

Browse files
RalfJungRalfJung
committed
miri genmc: fix exit() handling
1 parent 3c5c558 commit ee84ff9

File tree

4 files changed

+141
-3
lines changed

4 files changed

+141
-3
lines changed

‎compiler/rustc_const_eval/src/interpret/step.rs‎

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -561,8 +561,11 @@ impl<'tcx, M: Machine<'tcx>> InterpCx<'tcx, M> {
561561
if fn_abi.can_unwind { unwind } else { mir::UnwindAction::Unreachable },
562562
)?;
563563
// Sanity-check that `eval_fn_call` either pushed a new frame or
564-
// did a jump to another block.
565-
if self.frame_idx() == old_stack && self.frame().loc == old_loc {
564+
// did a jump to another block. We disable the sanity check for functions that
565+
// can't return, since Miri sometimes does have to keep the location the same
566+
// for those (which is fine since execution will continue on a different thread).
567+
if target.is_some() && self.frame_idx() == old_stack && self.frame().loc == old_loc
568+
{
566569
span_bug!(terminator.source_info.span, "evaluating this call made no progress");
567570
}
568571
}

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -538,7 +538,7 @@ trait EvalContextExtPriv<'tcx>: crate::MiriInterpCxExt<'tcx> {
538538
code,
539539
crate::concurrency::ExitType::ExitCalled,
540540
)?;
541-
todo!(); // FIXME(genmc): Add a way to return here that is allowed to not do progress (can't use existing EmulateItemResult variants).
541+
return interp_ok(EmulateItemResult::AlreadyJumped);
542542
}
543543
throw_machine_stop!(TerminationInfo::Exit { code, leak_check: false });
544544
}

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

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
//@ compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
2+
3+
fn main() {
4+
std::thread::spawn(|| {
5+
unsafe { std::hint::unreachable_unchecked() }; //~ERROR: entering unreachable code
6+
});
7+
// If we exit immediately, we might entirely miss the UB in the other thread.
8+
std::process::exit(0);
9+
}

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

Lines changed: 126 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,126 @@
1+
Running GenMC Verification...
2+
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
3+
--> RUSTLIB/std/src/thread/mod.rs:LL:CC
4+
|
5+
LL | match COUNTER.compare_exchange_weak(last, id, Ordering::Relaxed, Ordering::Relaxed) {
6+
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
7+
|
8+
= note: BACKTRACE:
9+
= note: inside `std::thread::ThreadId::new` at RUSTLIB/std/src/thread/mod.rs:LL:CC
10+
= note: inside closure at RUSTLIB/std/src/thread/current.rs:LL:CC
11+
= note: inside `std::thread::current::id::get_or_init` at RUSTLIB/std/src/thread/current.rs:LL:CC
12+
= note: inside `std::thread::current_id` at RUSTLIB/std/src/thread/current.rs:LL:CC
13+
= note: inside `std::rt::init` at RUSTLIB/std/src/rt.rs:LL:CC
14+
= note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
15+
= 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
16+
= note: inside `std::panicking::catch_unwind::<isize, {closure@std::rt::lang_start_internal::{closure#0}}>` at RUSTLIB/std/src/panicking.rs:LL:CC
17+
= note: inside `std::panic::catch_unwind::<{closure@std::rt::lang_start_internal::{closure#0}}, isize>` at RUSTLIB/std/src/panic.rs:LL:CC
18+
= note: inside `std::rt::lang_start_internal` at RUSTLIB/std/src/rt.rs:LL:CC
19+
= note: inside `std::rt::lang_start::<()>` at RUSTLIB/std/src/rt.rs:LL:CC
20+
21+
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.
22+
--> RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
23+
|
24+
LL | || self
25+
| ________________^
26+
LL | | .state
27+
LL | | .compare_exchange_weak(state, state + READ_LOCKED, Acquire, Relaxed)
28+
| |____________________________________________________________________________________^ GenMC might miss possible behaviors of this code
29+
|
30+
= note: BACKTRACE:
31+
= note: inside `std::sys::sync::PLATFORM::futex::RwLock::read` at RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
32+
= note: inside `std::sync::RwLock::<()>::read` at RUSTLIB/std/src/sync/poison/rwlock.rs:LL:CC
33+
= note: inside `std::sys::env::PLATFORM::env_read_lock` at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
34+
= note: inside closure at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
35+
= 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
36+
= 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
37+
= note: inside `std::sys::env::PLATFORM::getenv` at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
38+
= note: inside `std::env::_var_os` at RUSTLIB/std/src/env.rs:LL:CC
39+
= note: inside `std::env::var_os::<&str>` at RUSTLIB/std/src/env.rs:LL:CC
40+
= note: inside closure at RUSTLIB/std/src/thread/mod.rs:LL:CC
41+
note: inside `main`
42+
--> tests/genmc/fail/shims/exit.rs:LL:CC
43+
|
44+
LL | / std::thread::spawn(|| {
45+
LL | | unsafe { std::hint::unreachable_unchecked() };
46+
LL | | });
47+
| |______^
48+
49+
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
50+
--> RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
51+
|
52+
LL | || self
53+
| ________________^
54+
LL | | .state
55+
LL | | .compare_exchange_weak(state, state + READ_LOCKED, Acquire, Relaxed)
56+
| |____________________________________________________________________________________^ GenMC might miss possible behaviors of this code
57+
|
58+
= note: BACKTRACE:
59+
= note: inside `std::sys::sync::PLATFORM::futex::RwLock::read` at RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
60+
= note: inside `std::sync::RwLock::<()>::read` at RUSTLIB/std/src/sync/poison/rwlock.rs:LL:CC
61+
= note: inside `std::sys::env::PLATFORM::env_read_lock` at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
62+
= note: inside closure at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
63+
= 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
64+
= 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
65+
= note: inside `std::sys::env::PLATFORM::getenv` at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
66+
= note: inside `std::env::_var_os` at RUSTLIB/std/src/env.rs:LL:CC
67+
= note: inside `std::env::var_os::<&str>` at RUSTLIB/std/src/env.rs:LL:CC
68+
= note: inside closure at RUSTLIB/std/src/thread/mod.rs:LL:CC
69+
note: inside `main`
70+
--> tests/genmc/fail/shims/exit.rs:LL:CC
71+
|
72+
LL | / std::thread::spawn(|| {
73+
LL | | unsafe { std::hint::unreachable_unchecked() };
74+
LL | | });
75+
| |______^
76+
77+
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
78+
--> RUSTLIB/std/src/rt.rs:LL:CC
79+
|
80+
LL | / CLEANUP.call_once(|| unsafe {
81+
LL | | // Flush stdout and disable buffering.
82+
LL | | crate::io::cleanup();
83+
... |
84+
LL | | });
85+
| |______^ GenMC might miss possible behaviors of this code
86+
|
87+
= note: BACKTRACE:
88+
= note: inside `std::rt::cleanup` at RUSTLIB/std/src/rt.rs:LL:CC
89+
= note: inside `std::process::exit` at RUSTLIB/std/src/process.rs:LL:CC
90+
note: inside `main`
91+
--> tests/genmc/fail/shims/exit.rs:LL:CC
92+
|
93+
LL | std::process::exit(0);
94+
| ^^^^^^^^^^^^^^^^^^^^^
95+
96+
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.
97+
--> RUSTLIB/std/src/sys/exit_guard.rs:LL:CC
98+
|
99+
LL | match EXITING_THREAD_ID.compare_exchange(ptr::null_mut(), this_thread_id, Acquire, Relaxed) {
100+
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
101+
|
102+
= note: BACKTRACE:
103+
= note: inside `std::sys::exit_guard::unique_thread_exit` at RUSTLIB/std/src/sys/exit_guard.rs:LL:CC
104+
= note: inside `std::sys::pal::PLATFORM::os::exit` at RUSTLIB/std/src/sys/pal/PLATFORM/os.rs:LL:CC
105+
= note: inside `std::process::exit` at RUSTLIB/std/src/process.rs:LL:CC
106+
note: inside `main`
107+
--> tests/genmc/fail/shims/exit.rs:LL:CC
108+
|
109+
LL | std::process::exit(0);
110+
| ^^^^^^^^^^^^^^^^^^^^^
111+
112+
error: Undefined Behavior: entering unreachable code
113+
--> tests/genmc/fail/shims/exit.rs:LL:CC
114+
|
115+
LL | unsafe { std::hint::unreachable_unchecked() };
116+
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Undefined Behavior occurred here
117+
|
118+
= help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
119+
= help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
120+
121+
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
122+
123+
note: add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report
124+
125+
error: aborting due to 1 previous error; 5 warnings emitted
126+

0 commit comments

Comments
 (0)