@@ -14,18 +14,15 @@ use tracing::{debug, info};
14
14
15
15
use self :: global_allocations:: { EvalContextExt as _, GlobalAllocationHandler } ;
16
16
use 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,
19
19
} ;
20
20
use self :: run:: GenmcMode ;
21
21
use self :: thread_id_map:: ThreadIdMap ;
22
22
use crate :: concurrency:: genmc:: helper:: split_access;
23
+ use crate :: diagnostics:: SpanDedupDiagnostic ;
23
24
use 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 :: * ;
29
26
30
27
mod config;
31
28
mod global_allocations;
@@ -104,18 +101,11 @@ struct GlobalState {
104
101
/// Keep track of global allocations, to ensure they keep the same address across different executions, even if the order of allocations changes.
105
102
/// The `AllocId` for globals is stable across executions, so we can use it as an identifier.
106
103
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 > ,
111
104
}
112
105
113
106
impl 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) }
119
109
}
120
110
}
121
111
@@ -412,27 +402,24 @@ impl GenmcCtx {
412
402
let upgraded_success_ordering =
413
403
maybe_upgrade_compare_exchange_success_orderings ( success, fail) ;
414
404
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 ) ;
436
423
}
437
424
438
425
debug ! (
0 commit comments