tests/genmc/fail/data_race/atomic_ptr_write_dealloc_race.rs

//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows

// Test that use-after-free bugs involving atomic pointers are detected in GenMC mode.
// Compared to `atomic_ptr_dealloc_write_race.rs`, this variant checks that the data race is still detected, even if the write happens before the free.
//
// FIXME(genmc): We currently cannot show the two spans related to this error (only the second one),
// since there is no mapping between GenMC events (shown with `-Zmiri-genmc-print-genmc-output`) and Miri spans.

#![no_main]

#[path = "../../../utils/genmc.rs"]
mod genmc;
#[path = "../../../utils/mod.rs"]
mod utils;

use std::sync::atomic::AtomicPtr;
use std::sync::atomic::Ordering::*;

use crate::genmc::*;
use crate::utils::*;

static X: AtomicPtr<u64> = AtomicPtr::new(std::ptr::null_mut());
static Y: AtomicPtr<u64> = AtomicPtr::new(std::ptr::null_mut());

#[unsafe(no_mangle)]
fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
    unsafe {
        let ids = [
            spawn_pthread_closure(|| {
                let ptr = X.load(SeqCst);
                miri_genmc_assume(!ptr.is_null());
                *ptr = 42;
            }),
            spawn_pthread_closure(|| {
                let mut z: u64 = 1234;
                X.store(&raw mut z, SeqCst); // The other thread can read this value and then access `z` after it is deallocated.
                for _ in 0..10 {
                    // We do some extra loads here so GenMC schedules the pointer write on the other thread first.
                    Y.load(Relaxed);
                }
                // `z` gets dropped on the next line, at which point GenMC will detect the data race with the write in the other thread.
            }), //~ ERROR: Undefined Behavior
        ];
        join_pthreads(ids);
        0
    }
}