Skip to content

Commit 9ab5846

Browse files
committed
Add assertion about Mutex size.
1 parent 3c99efa commit 9ab5846

File tree

1 file changed

+13
-2
lines changed

1 file changed

+13
-2
lines changed

src/concurrency/genmc/intercept.rs

Lines changed: 13 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
use rustc_middle::{throw_unsup_format, ty};
22
use tracing::debug;
33

4+
use crate::concurrency::genmc::MAX_ACCESS_SIZE;
45
use crate::concurrency::thread::EvalContextExt as _;
56
use crate::*;
67

@@ -27,10 +28,15 @@ trait EvalContextExtPriv<'tcx>: crate::MiriInterpCxExt<'tcx> {
2728
let this = self.eval_context_mut();
2829
let genmc_ctx = this.machine.data_race.as_genmc_ref().unwrap();
2930

31+
let size = mutex.layout.size.bytes();
32+
assert!(
33+
size < MAX_ACCESS_SIZE,
34+
"Mutex is larger than maximal size of a memory access supported by GenMC ({size} >= {MAX_ACCESS_SIZE})"
35+
);
3036
let result = genmc_ctx.handle.borrow_mut().pin_mut().handle_mutex_lock(
3137
genmc_ctx.active_thread_genmc_tid(&this.machine),
3238
mutex.ptr().addr().bytes(),
33-
mutex.layout.size.bytes(),
39+
size,
3440
);
3541
if let Some(error) = result.error.as_ref() {
3642
// FIXME(genmc): improve error handling.
@@ -87,10 +93,15 @@ trait EvalContextExtPriv<'tcx>: crate::MiriInterpCxExt<'tcx> {
8793
debug!("GenMC: handling Mutex::try_lock()");
8894
let this = self.eval_context_mut();
8995
let genmc_ctx = this.machine.data_race.as_genmc_ref().unwrap();
96+
let size = mutex.layout.size.bytes();
97+
assert!(
98+
size < MAX_ACCESS_SIZE,
99+
"Mutex is larger than maximal size of a memory access supported by GenMC ({size} >= {MAX_ACCESS_SIZE})"
100+
);
90101
let result = genmc_ctx.handle.borrow_mut().pin_mut().handle_mutex_try_lock(
91102
genmc_ctx.active_thread_genmc_tid(&this.machine),
92103
mutex.ptr().addr().bytes(),
93-
mutex.layout.size.bytes(),
104+
size,
94105
);
95106
if let Some(error) = result.error.as_ref() {
96107
// FIXME(genmc): improve error handling.

0 commit comments

Comments
 (0)