Add weak memory config option

diff --git a/src/bin/miri.rs b/src/bin/miri.rs
index e3f38956dae25b04721e30d36b061f936d5b37a4..907e620404b9bba5817bfc32a25abfef66719540 100644 (file)
--- a/src/bin/miri.rs
+++ b/src/bin/miri.rs
@@ -318,6 +318,7 @@ fn main() {
             miri_config.stacked_borrows = false;
         } else if arg == "-Zmiri-disable-data-race-detector" {
             miri_config.data_race_detector = false;
+            miri_config.weak_memory_emulation = false;
         } else if arg == "-Zmiri-disable-alignment-check" {
             miri_config.check_alignment = miri::AlignmentCheck::None;
         } else if arg == "-Zmiri-symbolic-alignment-check" {
@@ -340,6 +341,8 @@ fn main() {
                 isolation_enabled = Some(false);
             }
             miri_config.isolated_op = miri::IsolatedOp::Allow;
+        } else if arg == "-Zmiri-disable-weak-memory-emulation" {
+            miri_config.weak_memory_emulation = false;
         } else if let Some(param) = arg.strip_prefix("-Zmiri-isolation-error=") {
             if matches!(isolation_enabled, Some(false)) {
                 panic!("-Zmiri-isolation-error cannot be used along with -Zmiri-disable-isolation");

diff --git a/src/eval.rs b/src/eval.rs
index a782dfa3fce17d9d7859f7e8172f1812316d2be7..bdf527a0d13e0565a479859ca39d8b6ce2750555 100644 (file)
--- a/src/eval.rs
+++ b/src/eval.rs
@@ -105,6 +105,8 @@ pub struct MiriConfig {
     pub tag_raw: bool,
     /// Determine if data race detection should be enabled
     pub data_race_detector: bool,
+    /// Determine if weak memory emulation should be enabled. Requires data race detection to be enabled
+    pub weak_memory_emulation: bool,
     /// Rate of spurious failures for compare_exchange_weak atomic operations,
     /// between 0.0 and 1.0, defaulting to 0.8 (80% chance of failure).
     pub cmpxchg_weak_failure_rate: f64,
@@ -142,6 +144,7 @@ fn default() -> MiriConfig {
             tracked_alloc_ids: HashSet::default(),
             tag_raw: false,
             data_race_detector: true,
+            weak_memory_emulation: true,
             cmpxchg_weak_failure_rate: 0.8,
             measureme_out: None,
             panic_on_unsupported: false,

diff --git a/src/machine.rs b/src/machine.rs
index 369bb92c6f3982606c06d5ebd1c211778d8ba44b..2060bba0b8530bf56601ad102f95f95c54848144 100644 (file)
--- a/src/machine.rs
+++ b/src/machine.rs
@@ -323,6 +323,9 @@ pub struct Evaluator<'mir, 'tcx> {
 
     /// Corresponds to -Zmiri-mute-stdout-stderr and doesn't write the output but acts as if it succeeded.
     pub(crate) mute_stdout_stderr: bool,
+
+    /// Whether weak memory emulation is enabled
+    pub(crate) weak_memory: bool,
 }
 
 impl<'mir, 'tcx> Evaluator<'mir, 'tcx> {
@@ -378,6 +381,7 @@ pub(crate) fn new(config: &MiriConfig, layout_cx: LayoutCx<'tcx, TyCtxt<'tcx>>)
             check_alignment: config.check_alignment,
             cmpxchg_weak_failure_rate: config.cmpxchg_weak_failure_rate,
             mute_stdout_stderr: config.mute_stdout_stderr,
+            weak_memory: config.weak_memory_emulation,
         }
     }