Merge pull request #4790 from RalfJung/native-lib-many-seeds
show a warning when combing native-lib mode and many-seeds
diff --git a/src/bin/miri.rs b/src/bin/miri.rs
index efe7071..19fbf90 100644
--- a/src/bin/miri.rs
+++ b/src/bin/miri.rs
@@ -710,20 +710,18 @@
if !miri_config.native_lib.is_empty() && miri_config.provenance_mode == ProvenanceMode::Strict {
fatal_error!("strict provenance is not compatible with calling native functions");
}
+ // Native calls and many-seeds are an "intersting" combination.
+ if !miri_config.native_lib.is_empty() && many_seeds.is_some() {
+ eprintln!(
+ "warning: `-Zmiri-many-seeds` runs multiple instances of the program in the same address space, \
+ so if the native library has global state, it will leak across execution bundaries"
+ );
+ }
// You can set either one seed or many.
if many_seeds.is_some() && miri_config.seed.is_some() {
fatal_error!("Only one of `-Zmiri-seed` and `-Zmiri-many-seeds can be set");
}
-
- // Ensure we have parallelism for many-seeds mode.
- if many_seeds.is_some() && !rustc_args.iter().any(|arg| arg.starts_with("-Zthreads=")) {
- // Clamp to 20 threads; things get a less efficient beyond that due to lock contention.
- let threads = std::thread::available_parallelism().map_or(1, |n| n.get()).min(20);
- rustc_args.push(format!("-Zthreads={threads}"));
- }
- let many_seeds =
- many_seeds.map(|seeds| ManySeedsConfig { seeds, keep_going: many_seeds_keep_going });
-
+ // We cannot emulate weak memory without the data race detector.
if miri_config.weak_memory_emulation && !miri_config.data_race_detector {
fatal_error!(
"Weak memory emulation cannot be enabled when the data race detector is disabled"
@@ -737,6 +735,15 @@
fatal_error!("Invalid settings: {err}");
}
+ // Ensure we have parallelism for many-seeds mode.
+ if many_seeds.is_some() && !rustc_args.iter().any(|arg| arg.starts_with("-Zthreads=")) {
+ // Clamp to 20 threads; things get a less efficient beyond that due to lock contention.
+ let threads = std::thread::available_parallelism().map_or(1, |n| n.get()).min(20);
+ rustc_args.push(format!("-Zthreads={threads}"));
+ }
+ let many_seeds =
+ many_seeds.map(|seeds| ManySeedsConfig { seeds, keep_going: many_seeds_keep_going });
+
debug!("rustc arguments: {:?}", rustc_args);
debug!("crate arguments: {:?}", miri_config.args);
if !miri_config.native_lib.is_empty() && miri_config.native_lib_enable_tracing {
diff --git a/src/diagnostics.rs b/src/diagnostics.rs
index 189f493..10467fa 100644
--- a/src/diagnostics.rs
+++ b/src/diagnostics.rs
@@ -548,7 +548,7 @@
/// We want to present a multi-line span message for some errors. Diagnostics do not support this
/// directly, so we pass the lines as a `Vec<String>` and display each line after the first with an
/// additional `span_label` or `note` call.
-pub fn report_msg<'tcx>(
+fn report_msg<'tcx>(
diag_level: DiagLevel,
title: String,
span_msg: Vec<String>,
