Remove code for warning about missing GenMC support

Author: Patrick-6

src/concurrency/genmc/mapping.rs

@@ -34,17 +34,6 @@ impl AtomicFenceOrd {
 }
 
 impl AtomicRwOrd {
-    /// Split up an atomic read-write memory ordering into a separate read and write ordering.
-    pub(super) fn split_memory_orderings(self) -> (AtomicReadOrd, AtomicWriteOrd) {
-        match self {
-            AtomicRwOrd::Relaxed => (AtomicReadOrd::Relaxed, AtomicWriteOrd::Relaxed),
-            AtomicRwOrd::Acquire => (AtomicReadOrd::Acquire, AtomicWriteOrd::Relaxed),
-            AtomicRwOrd::Release => (AtomicReadOrd::Relaxed, AtomicWriteOrd::Release),
-            AtomicRwOrd::AcqRel => (AtomicReadOrd::Acquire, AtomicWriteOrd::Release),
-            AtomicRwOrd::SeqCst => (AtomicReadOrd::SeqCst, AtomicWriteOrd::SeqCst),
-        }
-    }
-
     /// Split up the atomic success ordering of a read-modify-write operation into GenMC's representation.
     /// Note that both returned orderings are currently identical, because this is what GenMC expects.
     pub(super) fn to_genmc_memory_orderings(self) -> (MemOrdering, MemOrdering) {

src/concurrency/genmc/mod.rs

@@ -19,7 +19,6 @@ use self::helper::{
 use self::mapping::{min_max_to_genmc_rmw_op, to_genmc_rmw_op};
 use self::thread_info_manager::ThreadInfoManager;
 use crate::concurrency::genmc::helper::{is_terminator_atomic, split_access};
-use crate::concurrency::genmc::warnings::WarningsCache;
 use crate::concurrency::thread::{EvalContextExt as _, ThreadState};
 use crate::{
     AtomicFenceOrd, AtomicReadOrd, AtomicRwOrd, AtomicWriteOrd, BlockReason, MemoryKind,
@@ -33,7 +32,6 @@ mod helper;
 mod mapping;
 pub mod miri_genmc;
 mod thread_info_manager;
-mod warnings;
 
 pub use genmc_sys::GenmcParams;
 
@@ -61,11 +59,7 @@ pub struct GenmcCtx {
     /// Keep track of global allocations, to ensure they keep the same address across different executions, even if the order of allocations changes.
     /// The `AllocId` for globals is stable across executions, so we can use it as an identifier.
     global_allocations: Arc<GlobalAllocationHandler>,
-    // TODO GENMC: maybe make this a (base, size), maybe BTreeMap/sorted vector for reverse lookups
-    //          GenMC needs to have access to that
-    // TODO: look at code of "pub struct GlobalStateInner"
-    warnings_cache: RefCell<WarningsCache>,
-    // terminator_cache: RefCell<FxHashMap<rustc_middle::ty::Ty<'tcx>, bool>>,
+
     exit_status: Cell<Option<ExitStatus>>,
 }
 
@@ -85,7 +79,6 @@ impl GenmcCtx {
             thread_infos: Default::default(),
             allow_data_races: Cell::new(false),
             global_allocations: Default::default(),
-            warnings_cache: Default::default(),
             exit_status: Cell::new(None),
         }
     }
@@ -358,13 +351,6 @@ impl GenmcCtx {
     ) -> InterpResult<'tcx, (Scalar, bool, bool)> {
         assert!(!self.allow_data_races.get()); // TODO GENMC: handle this properly
 
-        // FIXME(genmc): remove once GenMC supports failure memory ordering in `compare_exchange`.
-        self.warnings_cache.borrow_mut().warn_once_rmw_failure_ordering(&ecx.tcx, success, fail);
-        // FIXME(genmc): remove once GenMC implements spurious failures for `compare_exchange_weak`.
-        if can_fail_spuriously {
-            self.warnings_cache.borrow_mut().warn_once_compare_exchange_weak(&ecx.tcx);
-        }
-
         let machine = &ecx.machine;
         let (success_load_ordering, success_store_ordering) = success.to_genmc_memory_orderings();
         let fail_load_ordering = fail.convert();

src/concurrency/genmc/warnings.rs

@@ -1,6 +1,2 @@
-warning: GenMC mode currently does not model spurious failures of `compare_exchange_weak`. This may lead to missed bugs (possible unsoundness)!
-
-warning: GenMC currently does not model the atomic failure ordering for `compare_exchange`. Failure ordering 'Relaxed' is treated like 'Acquire', which means that Miri might miss bugs related to this memory access (possible unsoundness)!
-
 (GenMC) Verification complete. No errors were detected.
 Number of complete executions explored: 1

tests/genmc/pass/thread/empty_main.stderr

@@ -1,8 +1,2 @@
-warning: GenMC currently does not model the atomic failure ordering for `compare_exchange`. Failure ordering 'Relaxed' is treated like 'Acquire', which means that Miri might miss bugs related to this memory access (possible unsoundness)!
-
-warning: GenMC mode currently does not model spurious failures of `compare_exchange_weak`. This may lead to missed bugs (possible unsoundness)!
-
-warning: GenMC currently does not model the atomic failure ordering for `compare_exchange`. Failure ordering 'Acquire' is treated like 'Relaxed', which means that Miri might incorrectly detect errors related to this memory access (possible false positives).
-
 (GenMC) Verification complete. No errors were detected.
 Number of complete executions explored: 1

tests/genmc/pass/thread/miri_main_spawn_threads.stderr

@@ -1,8 +1,2 @@
-warning: GenMC mode currently does not model spurious failures of `compare_exchange_weak`. This may lead to missed bugs (possible unsoundness)!
-
-warning: GenMC currently does not model the atomic failure ordering for `compare_exchange`. Failure ordering 'Relaxed' is treated like 'Acquire', which means that Miri might miss bugs related to this memory access (possible unsoundness)!
-
-warning: GenMC currently does not model the atomic failure ordering for `compare_exchange`. Failure ordering 'Acquire' is treated like 'Relaxed', which means that Miri might incorrectly detect errors related to this memory access (possible false positives).
-
 (GenMC) Verification complete. No errors were detected.
 Number of complete executions explored: 1