diagnostics: Explain why programs might run OOM in GenMC mode

GenMC's allocator can currently only allocate up to 4GB per thread.

Authored-by: Ralf Jung

Author: michaliskok

src/diagnostics.rs

@@ -362,6 +362,10 @@ pub fn report_result<'tcx>(
                 vec![
                     note!("this is likely not a bug in the program; it indicates that the program performed an operation that Miri does not support"),
                 ],
+            ResourceExhaustion(ResourceExhaustionInfo::AddressSpaceFull) if ecx.machine.data_race.as_genmc_ref().is_some() =>
+                vec![
+                    note!("in GenMC mode, the address space is limited to 4GB per thread, and addresses cannot be reused")
+                ],
             UndefinedBehavior(AlignmentCheckFailed { .. })
                 if ecx.machine.check_alignment == AlignmentCheck::Symbolic
             =>

tests/genmc/fail/simple/alloc_large.multiple.stderr

@@ -5,6 +5,7 @@ error: resource exhaustion: there are no more free addresses in the address spac
 LL |             AllocInit::Uninitialized => alloc.allocate(layout),
    |                                         ^^^^^^^^^^^^^^^^^^^^^^ resource exhaustion occurred here
    |
+   = help: in GenMC mode, the address space is limited to 4GB per thread, and addresses cannot be reused
    = note: BACKTRACE:
    = note: inside `alloc::raw_vec::RawVecInner::try_allocate_in` at RUSTLIB/alloc/src/raw_vec/mod.rs:LL:CC
    = note: inside `alloc::raw_vec::RawVecInner::with_capacity_in` at RUSTLIB/alloc/src/raw_vec/mod.rs:LL:CC

tests/genmc/fail/simple/alloc_large.single.stderr

@@ -5,6 +5,7 @@ error: resource exhaustion: there are no more free addresses in the address spac
 LL |             AllocInit::Uninitialized => alloc.allocate(layout),
    |                                         ^^^^^^^^^^^^^^^^^^^^^^ resource exhaustion occurred here
    |
+   = help: in GenMC mode, the address space is limited to 4GB per thread, and addresses cannot be reused
    = note: BACKTRACE:
    = note: inside `alloc::raw_vec::RawVecInner::try_allocate_in` at RUSTLIB/alloc/src/raw_vec/mod.rs:LL:CC
    = note: inside `alloc::raw_vec::RawVecInner::with_capacity_in` at RUSTLIB/alloc/src/raw_vec/mod.rs:LL:CC