Skip to content

Commit 8568c89

Browse files
committed
genmc,tests: Throw when GenMC runs out of memory
GenMC can currently allocate up to 4GB per thread. If it cannot allocated any more memory, it will return nullptr. This commit adds a test in Miri that ensures we gracefully throw if this ever happens.
1 parent 11f09d8 commit 8568c89

File tree

4 files changed

+78
-2
lines changed

4 files changed

+78
-2
lines changed

src/concurrency/genmc/mod.rs

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -592,9 +592,11 @@ impl GenmcCtx {
592592
genmc_size,
593593
alignment.bytes(),
594594
);
595+
if chosen_address == 0 {
596+
throw_exhaust!(AddressSpaceFull);
597+
}
595598

596-
// Non-global addresses should not be in the global address space or null.
597-
assert_ne!(0, chosen_address, "GenMC malloc returned nullptr.");
599+
// Non-global addresses should not be in the global address space.
598600
assert_eq!(0, chosen_address & GENMC_GLOBAL_ADDRESSES_MASK);
599601
// Sanity check the address alignment:
600602
assert!(
Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
Running GenMC Verification...
2+
error: resource exhaustion: there are no more free addresses in the address space
3+
--> RUSTLIB/alloc/src/raw_vec/mod.rs:LL:CC
4+
|
5+
LL | AllocInit::Uninitialized => alloc.allocate(layout),
6+
| ^^^^^^^^^^^^^^^^^^^^^^ resource exhaustion occurred here
7+
|
8+
= note: BACKTRACE:
9+
= note: inside `alloc::raw_vec::RawVecInner::try_allocate_in` at RUSTLIB/alloc/src/raw_vec/mod.rs:LL:CC
10+
= note: inside `alloc::raw_vec::RawVecInner::with_capacity_in` at RUSTLIB/alloc/src/raw_vec/mod.rs:LL:CC
11+
= note: inside `alloc::raw_vec::RawVec::<u8>::with_capacity_in` at RUSTLIB/alloc/src/raw_vec/mod.rs:LL:CC
12+
= note: inside `std::vec::Vec::<u8>::with_capacity_in` at RUSTLIB/alloc/src/vec/mod.rs:LL:CC
13+
= note: inside `std::vec::Vec::<u8>::with_capacity` at RUSTLIB/alloc/src/vec/mod.rs:LL:CC
14+
note: inside `miri_start`
15+
--> tests/genmc/fail/simple/alloc_large.rs:LL:CC
16+
|
17+
LL | let _v = Vec::<u8>::with_capacity(1024 * 1024 * 1024);
18+
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
19+
20+
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
21+
22+
note: add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report
23+
24+
error: aborting due to 1 previous error
25+
Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
//@revisions: single multiple
2+
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
3+
//@error-in-other-file: resource exhaustion
4+
5+
// Ensure that we emit a proper error if GenMC fails to fulfill an allocation.
6+
// Two variants: one for a single large allocation, one for multiple ones
7+
// that are individually below the limit, but together are too big.
8+
9+
#![no_main]
10+
11+
#[path = "../../../utils/genmc.rs"]
12+
mod genmc;
13+
14+
#[unsafe(no_mangle)]
15+
fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
16+
if cfg!(multiple) {
17+
for _i in 1..8 {
18+
let _v = Vec::<u8>::with_capacity(1024 * 1024 * 1024);
19+
}
20+
} else {
21+
let _v = Vec::<u8>::with_capacity(8 * 1024 * 1024 * 1024);
22+
}
23+
0
24+
}
Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
Running GenMC Verification...
2+
error: resource exhaustion: there are no more free addresses in the address space
3+
--> RUSTLIB/alloc/src/raw_vec/mod.rs:LL:CC
4+
|
5+
LL | AllocInit::Uninitialized => alloc.allocate(layout),
6+
| ^^^^^^^^^^^^^^^^^^^^^^ resource exhaustion occurred here
7+
|
8+
= note: BACKTRACE:
9+
= note: inside `alloc::raw_vec::RawVecInner::try_allocate_in` at RUSTLIB/alloc/src/raw_vec/mod.rs:LL:CC
10+
= note: inside `alloc::raw_vec::RawVecInner::with_capacity_in` at RUSTLIB/alloc/src/raw_vec/mod.rs:LL:CC
11+
= note: inside `alloc::raw_vec::RawVec::<u8>::with_capacity_in` at RUSTLIB/alloc/src/raw_vec/mod.rs:LL:CC
12+
= note: inside `std::vec::Vec::<u8>::with_capacity_in` at RUSTLIB/alloc/src/vec/mod.rs:LL:CC
13+
= note: inside `std::vec::Vec::<u8>::with_capacity` at RUSTLIB/alloc/src/vec/mod.rs:LL:CC
14+
note: inside `miri_start`
15+
--> tests/genmc/fail/simple/alloc_large.rs:LL:CC
16+
|
17+
LL | let _v = Vec::<u8>::with_capacity(8 * 1024 * 1024 * 1024);
18+
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
19+
20+
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
21+
22+
note: add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report
23+
24+
error: aborting due to 1 previous error
25+

0 commit comments

Comments
 (0)