@@ -14,18 +14,15 @@ use tracing::{debug, info};
1414
1515use self :: global_allocations:: { EvalContextExt as _, GlobalAllocationHandler } ;
1616use self :: helper:: {
17- MAX_ACCESS_SIZE , Warnings , emit_warning , genmc_scalar_to_scalar ,
18- maybe_upgrade_compare_exchange_success_orderings , scalar_to_genmc_scalar, to_genmc_rmw_op,
17+ MAX_ACCESS_SIZE , genmc_scalar_to_scalar , maybe_upgrade_compare_exchange_success_orderings ,
18+ scalar_to_genmc_scalar, to_genmc_rmw_op,
1919} ;
2020use self :: run:: GenmcMode ;
2121use self :: thread_id_map:: ThreadIdMap ;
2222use crate :: concurrency:: genmc:: helper:: split_access;
23+ use crate :: diagnostics:: SpanDedupDiagnostic ;
2324use crate :: intrinsics:: AtomicRmwOp ;
24- use crate :: {
25- AtomicFenceOrd , AtomicReadOrd , AtomicRwOrd , AtomicWriteOrd , MemoryKind , MiriConfig ,
26- MiriMachine , MiriMemoryKind , NonHaltingDiagnostic , Scalar , TerminationInfo , ThreadId ,
27- ThreadManager , VisitProvenance , VisitWith ,
28- } ;
25+ use crate :: * ;
2926
3027mod config;
3128mod global_allocations;
@@ -104,18 +101,11 @@ struct GlobalState {
104101 /// Keep track of global allocations, to ensure they keep the same address across different executions, even if the order of allocations changes.
105102 /// The `AllocId` for globals is stable across executions, so we can use it as an identifier.
106103 global_allocations : GlobalAllocationHandler ,
107-
108- /// Cache for which warnings have already been shown to the user.
109- /// `None` if warnings are disabled.
110- warning_cache : Option < Warnings > ,
111104}
112105
113106impl GlobalState {
114- fn new ( target_usize_max : u64 , print_warnings : bool ) -> Self {
115- Self {
116- global_allocations : GlobalAllocationHandler :: new ( target_usize_max) ,
117- warning_cache : print_warnings. then ( Default :: default) ,
118- }
107+ fn new ( target_usize_max : u64 ) -> Self {
108+ Self { global_allocations : GlobalAllocationHandler :: new ( target_usize_max) }
119109 }
120110}
121111
@@ -412,27 +402,24 @@ impl GenmcCtx {
412402 let upgraded_success_ordering =
413403 maybe_upgrade_compare_exchange_success_orderings ( success, fail) ;
414404
415- if let Some ( warning_cache) = & self . global_state . warning_cache {
416- // FIXME(genmc): remove once GenMC supports failure memory ordering in `compare_exchange`.
417- let ( effective_failure_ordering, _) =
418- upgraded_success_ordering. split_memory_orderings ( ) ;
419- // Return a warning if the actual orderings don't match the upgraded ones.
420- if success != upgraded_success_ordering || effective_failure_ordering != fail {
421- emit_warning ( ecx, & warning_cache. compare_exchange_failure_ordering , || {
422- NonHaltingDiagnostic :: GenmcCompareExchangeOrderingMismatch {
423- success_ordering : success,
424- upgraded_success_ordering,
425- failure_ordering : fail,
426- effective_failure_ordering,
427- }
428- } ) ;
429- }
430- // FIXME(genmc): remove once GenMC implements spurious failures for `compare_exchange_weak`.
431- if can_fail_spuriously {
432- emit_warning ( ecx, & warning_cache. compare_exchange_weak , || {
433- NonHaltingDiagnostic :: GenmcCompareExchangeWeak
434- } ) ;
435- }
405+ // FIXME(genmc): remove once GenMC supports failure memory ordering in `compare_exchange`.
406+ let ( effective_failure_ordering, _) = upgraded_success_ordering. split_memory_orderings ( ) ;
407+ // Return a warning if the actual orderings don't match the upgraded ones.
408+ if success != upgraded_success_ordering || effective_failure_ordering != fail {
409+ static DEDUP : SpanDedupDiagnostic = SpanDedupDiagnostic :: new ( ) ;
410+ ecx. dedup_diagnostic ( & DEDUP , |_first| {
411+ NonHaltingDiagnostic :: GenmcCompareExchangeOrderingMismatch {
412+ success_ordering : success,
413+ upgraded_success_ordering,
414+ failure_ordering : fail,
415+ effective_failure_ordering,
416+ }
417+ } ) ;
418+ }
419+ // FIXME(genmc): remove once GenMC implements spurious failures for `compare_exchange_weak`.
420+ if can_fail_spuriously {
421+ static DEDUP : SpanDedupDiagnostic = SpanDedupDiagnostic :: new ( ) ;
422+ ecx. dedup_diagnostic ( & DEDUP , |_first| NonHaltingDiagnostic :: GenmcCompareExchangeWeak ) ;
436423 }
437424
438425 debug ! (
0 commit comments