Skip to content

Commit 1d00266

Browse files
RalfJungRalfJung
committed
make genmc tests less dependent on std internals
1 parent 4dff7b8 commit 1d00266

File tree

9 files changed

+4
-240
lines changed

9 files changed

+4
-240
lines changed

‎src/tools/miri/tests/genmc/pass/std/arc.check_count.stderr‎

Lines changed: 0 additions & 52 deletions
Original file line numberDiff line numberDiff line change
@@ -6,20 +6,8 @@ LL | intrinsics::atomic_cxchgweak::<T, { AO::Relaxed }, { AO::Re
66
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
77
|
88
= note: BACKTRACE:
9-
= note: inside `std::sync::atomic::atomic_compare_exchange_weak::<u64>` at RUSTLIB/core/src/sync/atomic.rs:LL:CC
10-
= note: inside `std::sync::atomic::AtomicU64::compare_exchange_weak` at RUSTLIB/core/src/sync/atomic.rs:LL:CC
11-
= note: inside `std::thread::ThreadId::new` at RUSTLIB/std/src/thread/mod.rs:LL:CC
129
= note: inside closure at RUSTLIB/std/src/thread/current.rs:LL:CC
13-
= note: inside `std::option::Option::<std::thread::ThreadId>::unwrap_or_else::<{closure@std::thread::current::id::get_or_init::{closure#0}}>` at RUSTLIB/core/src/option.rs:LL:CC
14-
= note: inside `std::thread::current::id::get_or_init` at RUSTLIB/std/src/thread/current.rs:LL:CC
15-
= note: inside `std::thread::current_id` at RUSTLIB/std/src/thread/current.rs:LL:CC
16-
= note: inside `std::rt::init` at RUSTLIB/std/src/rt.rs:LL:CC
1710
= note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
18-
= 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
19-
= note: inside `std::panicking::catch_unwind::<isize, {closure@std::rt::lang_start_internal::{closure#0}}>` at RUSTLIB/std/src/panicking.rs:LL:CC
20-
= note: inside `std::panic::catch_unwind::<{closure@std::rt::lang_start_internal::{closure#0}}, isize>` at RUSTLIB/std/src/panic.rs:LL:CC
21-
= note: inside `std::rt::lang_start_internal` at RUSTLIB/std/src/rt.rs:LL:CC
22-
= note: inside `std::rt::lang_start::<()>` at RUSTLIB/std/src/rt.rs:LL:CC
2311

2412
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.
2513
--> RUSTLIB/alloc/src/sync.rs:LL:CC
@@ -28,7 +16,6 @@ LL | match this.inner().weak.compare_exchange_weak(cur, cur + 1, Acq
2816
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
2917
|
3018
= note: BACKTRACE:
31-
= note: inside `std::sync::Arc::<i32>::downgrade` at RUSTLIB/alloc/src/sync.rs:LL:CC
3219
note: inside `main`
3320
--> tests/genmc/pass/std/arc.rs:LL:CC
3421
|
@@ -42,7 +29,6 @@ LL | match this.inner().weak.compare_exchange_weak(cur, cur + 1, Acq
4229
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
4330
|
4431
= note: BACKTRACE:
45-
= note: inside `std::sync::Arc::<i32>::downgrade` at RUSTLIB/alloc/src/sync.rs:LL:CC
4632
note: inside `main`
4733
--> tests/genmc/pass/std/arc.rs:LL:CC
4834
|
@@ -59,15 +45,7 @@ LL | | .compare_exchange_weak(state, state + READ_LOCKED, Acquir
5945
| |____________________________________________________________________________________^ GenMC might miss possible behaviors of this code
6046
|
6147
= note: BACKTRACE:
62-
= note: inside `std::sys::sync::PLATFORM::futex::RwLock::read` at RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
63-
= note: inside `std::sync::RwLock::<()>::read` at RUSTLIB/std/src/sync/poison/rwlock.rs:LL:CC
64-
= note: inside `std::sys::env::PLATFORM::env_read_lock` at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
6548
= note: inside closure at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
66-
= 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
67-
= 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
68-
= note: inside `std::sys::env::PLATFORM::getenv` at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
69-
= note: inside `std::env::_var_os` at RUSTLIB/std/src/env.rs:LL:CC
70-
= note: inside `std::env::var_os::<&str>` at RUSTLIB/std/src/env.rs:LL:CC
7149
= note: inside closure at RUSTLIB/std/src/thread/mod.rs:LL:CC
7250
note: inside `main`
7351
--> tests/genmc/pass/std/arc.rs:LL:CC
@@ -88,15 +66,7 @@ LL | | .compare_exchange_weak(state, state + READ_LOCKED, Acquir
8866
| |____________________________________________________________________________________^ GenMC might miss possible behaviors of this code
8967
|
9068
= note: BACKTRACE:
91-
= note: inside `std::sys::sync::PLATFORM::futex::RwLock::read` at RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
92-
= note: inside `std::sync::RwLock::<()>::read` at RUSTLIB/std/src/sync/poison/rwlock.rs:LL:CC
93-
= note: inside `std::sys::env::PLATFORM::env_read_lock` at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
9469
= note: inside closure at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
95-
= 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
96-
= 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
97-
= note: inside `std::sys::env::PLATFORM::getenv` at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
98-
= note: inside `std::env::_var_os` at RUSTLIB/std/src/env.rs:LL:CC
99-
= note: inside `std::env::var_os::<&str>` at RUSTLIB/std/src/env.rs:LL:CC
10070
= note: inside closure at RUSTLIB/std/src/thread/mod.rs:LL:CC
10171
note: inside `main`
10272
--> tests/genmc/pass/std/arc.rs:LL:CC
@@ -114,10 +84,6 @@ LL | if this.inner().weak.compare_exchange(1, usize::MAX, Acquire, Relax
11484
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
11585
|
11686
= note: BACKTRACE:
117-
= note: inside `std::sync::Arc::<std::thread::Packet<'_, ()>>::is_unique` at RUSTLIB/alloc/src/sync.rs:LL:CC
118-
= note: inside `std::sync::Arc::<std::thread::Packet<'_, ()>>::get_mut` at RUSTLIB/alloc/src/sync.rs:LL:CC
119-
= note: inside `std::thread::JoinInner::<'_, ()>::join` at RUSTLIB/std/src/thread/mod.rs:LL:CC
120-
= note: inside `std::thread::JoinHandle::<()>::join` at RUSTLIB/std/src/thread/mod.rs:LL:CC
12187
note: inside `main`
12288
--> tests/genmc/pass/std/arc.rs:LL:CC
12389
|
@@ -131,17 +97,7 @@ LL | intrinsics::atomic_cxchgweak::<T, { AO::Acquire }, { AO::Ac
13197
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
13298
|
13399
= note: BACKTRACE:
134-
= note: inside `std::sync::atomic::atomic_compare_exchange_weak::<u32>` at RUSTLIB/core/src/sync/atomic.rs:LL:CC
135-
= note: inside `std::sync::atomic::AtomicU32::compare_exchange_weak` at RUSTLIB/core/src/sync/atomic.rs:LL:CC
136-
= note: inside `std::sys::sync::PLATFORM::futex::Once::call` at RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
137-
= note: inside `std::sync::Once::call_once::<{closure@std::rt::cleanup::{closure#0}}>` at RUSTLIB/std/src/sync/poison/once.rs:LL:CC
138-
= note: inside `std::rt::cleanup` at RUSTLIB/std/src/rt.rs:LL:CC
139100
= note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
140-
= 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
141-
= note: inside `std::panicking::catch_unwind::<isize, {closure@std::rt::lang_start_internal::{closure#0}}>` at RUSTLIB/std/src/panicking.rs:LL:CC
142-
= note: inside `std::panic::catch_unwind::<{closure@std::rt::lang_start_internal::{closure#0}}, isize>` at RUSTLIB/std/src/panic.rs:LL:CC
143-
= note: inside `std::rt::lang_start_internal` at RUSTLIB/std/src/rt.rs:LL:CC
144-
= note: inside `std::rt::lang_start::<()>` at RUSTLIB/std/src/rt.rs:LL:CC
145101

146102
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.
147103
--> RUSTLIB/core/src/sync/atomic.rs:LL:CC
@@ -150,14 +106,6 @@ LL | intrinsics::atomic_cxchg::<T, { AO::Acquire }, { AO::Relaxe
150106
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
151107
|
152108
= note: BACKTRACE:
153-
= note: inside `std::sync::atomic::atomic_compare_exchange::<*mut i32>` at RUSTLIB/core/src/sync/atomic.rs:LL:CC
154-
= note: inside `std::sync::atomic::AtomicPtr::<i32>::compare_exchange` at RUSTLIB/core/src/sync/atomic.rs:LL:CC
155-
= note: inside `std::sys::exit_guard::unique_thread_exit` at RUSTLIB/std/src/sys/exit_guard.rs:LL:CC
156109
= note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
157-
= 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
158-
= note: inside `std::panicking::catch_unwind::<isize, {closure@std::rt::lang_start_internal::{closure#0}}>` at RUSTLIB/std/src/panicking.rs:LL:CC
159-
= note: inside `std::panic::catch_unwind::<{closure@std::rt::lang_start_internal::{closure#0}}, isize>` at RUSTLIB/std/src/panic.rs:LL:CC
160-
= note: inside `std::rt::lang_start_internal` at RUSTLIB/std/src/rt.rs:LL:CC
161-
= note: inside `std::rt::lang_start::<()>` at RUSTLIB/std/src/rt.rs:LL:CC
162110

163111
Verification complete with 4 executions. No errors found.

‎src/tools/miri/tests/genmc/pass/std/arc.rs‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
22
//@revisions: check_count try_upgrade
3+
//@normalize-stderr-test: "\n *= note: inside `std::.*" -> ""
34

45
// Check that various operations on `std::sync::Arc` are handled properly in GenMC mode.
56
//

0 commit comments

Comments
 (0)