Skip to content

Commit 8b5c104

Browse files
Patrick-6Patrick-6
committed
Add tests for invalid Mutex unlocking.
1 parent 3bd9d4f commit 8b5c104

File tree

4 files changed

+157
-0
lines changed

4 files changed

+157
-0
lines changed

‎tests/genmc/fail/intercept/mutex_diff_thread_unlock.rs‎

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
2+
//@error-in-other-file: Undefined Behavior
3+
4+
// Test that GenMC throws an error if a `std::sync::Mutex` is unlocked from a different thread than the one that locked it.
5+
//
6+
// GenMC assumes a `pthread`-like API, which does not allow unlocking a mutex from a different thread.
7+
// This test will cause an error on all platforms, even if that platform allows for unlocking on a different thread.
8+
9+
#![no_main]
10+
11+
use std::sync::Mutex;
12+
13+
static MUTEX: Mutex<u64> = Mutex::new(0);
14+
15+
#[derive(Copy, Clone)]
16+
struct EvilSend<T>(pub T);
17+
unsafe impl<T> Send for EvilSend<T> {}
18+
19+
#[unsafe(no_mangle)]
20+
fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
21+
let guard = EvilSend(MUTEX.lock().unwrap());
22+
let handle = std::thread::spawn(move || {
23+
let guard = guard; // avoid field capturing
24+
drop(guard);
25+
});
26+
handle.join().unwrap();
27+
0
28+
}

‎tests/genmc/fail/intercept/mutex_diff_thread_unlock.stderr‎

Lines changed: 86 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,86 @@
1+
Running GenMC Verification...
2+
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.
3+
--> RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
4+
|
5+
LL | || self
6+
| ________________^
7+
LL | | .state
8+
LL | | .compare_exchange_weak(state, state + READ_LOCKED, Acquire, Relaxed)
9+
| |____________________________________________________________________________________^ GenMC might miss possible behaviors of this code
10+
|
11+
= note: BACKTRACE:
12+
= note: inside `std::sys::sync::PLATFORM::futex::RwLock::read` at RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
13+
= note: inside `std::sync::RwLock::<()>::read` at RUSTLIB/std/src/sync/poison/rwlock.rs:LL:CC
14+
= note: inside `std::sys::env::PLATFORM::env_read_lock` at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
15+
= note: inside closure at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
16+
= 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
17+
= 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
18+
= note: inside `std::sys::env::PLATFORM::getenv` at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
19+
= note: inside `std::env::_var_os` at RUSTLIB/std/src/env.rs:LL:CC
20+
= note: inside `std::env::var_os::<&str>` at RUSTLIB/std/src/env.rs:LL:CC
21+
= note: inside closure at RUSTLIB/std/src/thread/mod.rs:LL:CC
22+
note: inside `miri_start`
23+
--> tests/genmc/fail/intercept/mutex_diff_thread_unlock.rs:LL:CC
24+
|
25+
LL | let handle = std::thread::spawn(move || {
26+
| __________________^
27+
LL | | let guard = guard; // avoid field capturing
28+
LL | | drop(guard);
29+
LL | | });
30+
| |______^
31+
32+
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
33+
--> RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
34+
|
35+
LL | || self
36+
| ________________^
37+
LL | | .state
38+
LL | | .compare_exchange_weak(state, state + READ_LOCKED, Acquire, Relaxed)
39+
| |____________________________________________________________________________________^ GenMC might miss possible behaviors of this code
40+
|
41+
= note: BACKTRACE:
42+
= note: inside `std::sys::sync::PLATFORM::futex::RwLock::read` at RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
43+
= note: inside `std::sync::RwLock::<()>::read` at RUSTLIB/std/src/sync/poison/rwlock.rs:LL:CC
44+
= note: inside `std::sys::env::PLATFORM::env_read_lock` at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
45+
= note: inside closure at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
46+
= 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
47+
= 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
48+
= note: inside `std::sys::env::PLATFORM::getenv` at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
49+
= note: inside `std::env::_var_os` at RUSTLIB/std/src/env.rs:LL:CC
50+
= note: inside `std::env::var_os::<&str>` at RUSTLIB/std/src/env.rs:LL:CC
51+
= note: inside closure at RUSTLIB/std/src/thread/mod.rs:LL:CC
52+
note: inside `miri_start`
53+
--> tests/genmc/fail/intercept/mutex_diff_thread_unlock.rs:LL:CC
54+
|
55+
LL | let handle = std::thread::spawn(move || {
56+
| __________________^
57+
LL | | let guard = guard; // avoid field capturing
58+
LL | | drop(guard);
59+
LL | | });
60+
| |______^
61+
62+
error: Undefined Behavior: Invalid unlock() operation
63+
--> RUSTLIB/std/src/sync/poison/mutex.rs:LL:CC
64+
|
65+
LL | self.lock.inner.unlock();
66+
| ^^^^^^^^^^^^^^^^^^^^^^^^ Undefined Behavior occurred here
67+
|
68+
= help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
69+
= help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
70+
= note: BACKTRACE on thread `unnamed-ID`:
71+
= note: inside `<std::sync::MutexGuard<'_, u64> as std::ops::Drop>::drop` at RUSTLIB/std/src/sync/poison/mutex.rs:LL:CC
72+
= note: inside `std::ptr::drop_in_place::<std::sync::MutexGuard<'_, u64>> - shim(Some(std::sync::MutexGuard<'_, u64>))` at RUSTLIB/core/src/ptr/mod.rs:LL:CC
73+
= note: inside `std::ptr::drop_in_place::<EvilSend<std::sync::MutexGuard<'_, u64>>> - shim(Some(EvilSend<std::sync::MutexGuard<'_, u64>>))` at RUSTLIB/core/src/ptr/mod.rs:LL:CC
74+
= note: inside `std::mem::drop::<EvilSend<std::sync::MutexGuard<'_, u64>>>` at RUSTLIB/core/src/mem/mod.rs:LL:CC
75+
note: inside closure
76+
--> tests/genmc/fail/intercept/mutex_diff_thread_unlock.rs:LL:CC
77+
|
78+
LL | drop(guard);
79+
| ^^^^^^^^^^^
80+
81+
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
82+
83+
note: add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report
84+
85+
error: aborting due to 1 previous error; 2 warnings emitted
86+

‎tests/genmc/fail/intercept/mutex_double_unlock.rs‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
2+
//@error-in-other-file: Undefined Behavior
3+
4+
// Test that GenMC can detect a double unlock of a `std::sync::Mutex`.
5+
6+
#![no_main]
7+
8+
use std::sync::Mutex;
9+
10+
static MUTEX: Mutex<u64> = Mutex::new(0);
11+
12+
#[unsafe(no_mangle)]
13+
fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
14+
let mut guard = MUTEX.lock().unwrap();
15+
unsafe {
16+
std::ptr::drop_in_place(&raw mut guard);
17+
}
18+
drop(guard);
19+
0
20+
}

‎tests/genmc/fail/intercept/mutex_double_unlock.stderr‎

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
Running GenMC Verification...
2+
error: Undefined Behavior: Invalid unlock() operation
3+
--> RUSTLIB/std/src/sync/poison/mutex.rs:LL:CC
4+
|
5+
LL | self.lock.inner.unlock();
6+
| ^^^^^^^^^^^^^^^^^^^^^^^^ Undefined Behavior occurred here
7+
|
8+
= help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
9+
= help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
10+
= note: BACKTRACE:
11+
= note: inside `<std::sync::MutexGuard<'_, u64> as std::ops::Drop>::drop` at RUSTLIB/std/src/sync/poison/mutex.rs:LL:CC
12+
= note: inside `std::ptr::drop_in_place::<std::sync::MutexGuard<'_, u64>> - shim(Some(std::sync::MutexGuard<'_, u64>))` at RUSTLIB/core/src/ptr/mod.rs:LL:CC
13+
= note: inside `std::mem::drop::<std::sync::MutexGuard<'_, u64>>` at RUSTLIB/core/src/mem/mod.rs:LL:CC
14+
note: inside `miri_start`
15+
--> tests/genmc/fail/intercept/mutex_double_unlock.rs:LL:CC
16+
|
17+
LL | drop(guard);
18+
| ^^^^^^^^^^^
19+
20+
note: add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report
21+
22+
error: aborting due to 1 previous error
23+

0 commit comments

Comments
 (0)