From 2c1f1f0e9bb706d9adbb71e0bc33923c4478eb85 Mon Sep 17 00:00:00 2001 From: Patrick-6 Date: Mon, 8 Sep 2025 10:17:14 +0200 Subject: [PATCH 1/2] Add GenMC estimation mode. Improve error handling and output printing. --- src/tools/miri/doc/genmc.md | 3 + .../genmc-sys/cpp/include/MiriInterface.hpp | 8 +- .../cpp/src/MiriInterface/Exploration.cpp | 14 ++ .../genmc-sys/cpp/src/MiriInterface/Setup.cpp | 21 ++- src/tools/miri/genmc-sys/src/lib.rs | 55 +++++- src/tools/miri/src/bin/miri.rs | 9 +- .../miri/src/concurrency/genmc/config.rs | 17 ++ src/tools/miri/src/concurrency/genmc/dummy.rs | 12 -- src/tools/miri/src/concurrency/genmc/mod.rs | 61 +++++-- src/tools/miri/src/concurrency/genmc/run.rs | 166 +++++++++++++----- .../genmc/fail/data_race/mpu2_rels_rlx.stderr | 2 + .../data_race/weak_orderings.rel_rlx.stderr | 2 + .../data_race/weak_orderings.rlx_acq.stderr | 2 + .../data_race/weak_orderings.rlx_rlx.stderr | 2 + .../tests/genmc/fail/loom/buggy_inc.stderr | 2 + .../fail/loom/store_buffering.genmc.stderr | 2 + .../fail/simple/2w2w_weak.relaxed4.stderr | 2 + .../fail/simple/2w2w_weak.release4.stderr | 2 + .../fail/simple/2w2w_weak.sc3_rel1.stderr | 2 + .../cas_failure_ord_racy_key_init.stderr | 4 +- .../genmc/pass/atomics/cas_simple.stderr | 4 +- .../tests/genmc/pass/atomics/rmw_ops.stderr | 4 +- .../miri/tests/genmc/pass/litmus/2cowr.stderr | 4 +- .../genmc/pass/litmus/2w2w_2sc_scf.stderr | 4 +- .../pass/litmus/2w2w_3sc_1rel.release1.stderr | 4 +- .../pass/litmus/2w2w_3sc_1rel.release2.stderr | 4 +- .../genmc/pass/litmus/2w2w_4rel.sc.stderr | 4 +- .../genmc/pass/litmus/2w2w_4rel.weak.stderr | 4 +- .../tests/genmc/pass/litmus/2w2w_4sc.stderr | 4 +- .../genmc/pass/litmus/IRIW-acq-sc.stderr | 4 +- .../tests/genmc/pass/litmus/IRIWish.stderr | 4 +- .../miri/tests/genmc/pass/litmus/LB.stderr | 4 +- .../tests/genmc/pass/litmus/LB_incMPs.stderr | 4 +- .../miri/tests/genmc/pass/litmus/MP.stderr | 4 +- .../genmc/pass/litmus/MPU2_rels_acqf.stderr | 4 +- .../genmc/pass/litmus/MPU_rels_acq.stderr | 4 +- .../tests/genmc/pass/litmus/MP_incMPs.stderr | 4 +- .../genmc/pass/litmus/MP_rels_acqf.stderr | 4 +- .../miri/tests/genmc/pass/litmus/SB.stderr | 4 +- .../tests/genmc/pass/litmus/SB_2sc_scf.stderr | 4 +- .../tests/genmc/pass/litmus/Z6_U.sc.stderr | 4 +- .../tests/genmc/pass/litmus/Z6_U.weak.stderr | 4 +- .../tests/genmc/pass/litmus/Z6_acq.stderr | 4 +- .../tests/genmc/pass/litmus/atomicpo.stderr | 4 +- .../tests/genmc/pass/litmus/casdep.stderr | 4 +- .../miri/tests/genmc/pass/litmus/ccr.stderr | 4 +- .../miri/tests/genmc/pass/litmus/cii.stderr | 4 +- .../miri/tests/genmc/pass/litmus/corr.stderr | 4 +- .../miri/tests/genmc/pass/litmus/corr0.stderr | 4 +- .../miri/tests/genmc/pass/litmus/corr1.stderr | 4 +- .../miri/tests/genmc/pass/litmus/corr2.stderr | 4 +- .../miri/tests/genmc/pass/litmus/corw.stderr | 4 +- .../miri/tests/genmc/pass/litmus/cowr.stderr | 4 +- .../genmc/pass/litmus/cumul-release.stderr | 4 +- .../tests/genmc/pass/litmus/default.stderr | 4 +- .../genmc/pass/litmus/detour.join.stderr | 4 +- .../genmc/pass/litmus/detour.no_join.stderr | 4 +- .../genmc/pass/litmus/fr_w_w_w_reads.stderr | 4 +- .../miri/tests/genmc/pass/litmus/inc2w.stderr | 4 +- .../genmc/pass/litmus/inc_inc_RR_W_RR.stderr | 4 +- .../miri/tests/genmc/pass/litmus/riwi.stderr | 4 +- .../tests/genmc/pass/litmus/viktor-relseq.rs | 4 +- .../genmc/pass/litmus/viktor-relseq.stderr | 6 +- src/tools/miri/tests/ui.rs | 2 + 64 files changed, 390 insertions(+), 174 deletions(-) diff --git a/src/tools/miri/doc/genmc.md b/src/tools/miri/doc/genmc.md index 8af697be34a6..44e11dcbec44 100644 --- a/src/tools/miri/doc/genmc.md +++ b/src/tools/miri/doc/genmc.md @@ -24,6 +24,8 @@ Note that `cargo miri test` in GenMC mode is currently not supported. ### Supported Parameters - `-Zmiri-genmc`: Enable GenMC mode (not required if any other GenMC options are used). +- `-Zmiri-genmc-estimate`: This enables estimation of the concurrent execution space and verification time, before running the full verification. This should help users detect when their program is too complex to fully verify in a reasonable time. This will explore enough executions to make a good estimation, but at least 10 and at most `estimation-max` executions. +- `-Zmiri-genmc-estimation-max={MAX_ITERATIONS}`: Set the maximum number of executions that will be explored during estimation (default: 1000). - `-Zmiri-genmc-print-exec-graphs={none,explored,blocked,all}`: Make GenMC print the execution graph of the program after every explored, every blocked, or after every execution (default: None). - `-Zmiri-genmc-print-exec-graphs`: Shorthand for suffix `=explored`. - `-Zmiri-genmc-print-genmc-output`: Print the output that GenMC provides. NOTE: this output is quite verbose and the events in the printed execution graph are hard to map back to the Rust code location they originate from. @@ -36,6 +38,7 @@ Note that `cargo miri test` in GenMC mode is currently not supported. - `debug1`: Print revisits considered by GenMC. - `debug2`: Print the execution graph after every memory access. - `debug3`: Print reads-from values considered by GenMC. +- `-Zmiri-genmc-verbose`: Show more information, such as estimated number of executions, and time taken for verification. #### Regular Miri parameters useful for GenMC mode diff --git a/src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp b/src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp index 662eb0e173ca..444c9375319a 100644 --- a/src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp +++ b/src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp @@ -31,6 +31,7 @@ enum class LogLevel : std::uint8_t; struct GenmcScalar; struct SchedulingResult; +struct EstimationResult; struct LoadResult; struct StoreResult; struct ReadModifyWriteResult; @@ -66,7 +67,7 @@ struct MiriGenmcShim : private GenMCDriver { /// `logLevel`, causing a data race. The safest way to use these functions is to call /// `set_log_level_raw` once, and only then start creating handles. There should not be any /// other (safe) way to create a `MiriGenmcShim`. - /* unsafe */ static auto create_handle(const GenmcParams& params) + /* unsafe */ static auto create_handle(const GenmcParams& params, bool estimation_mode) -> std::unique_ptr; virtual ~MiriGenmcShim() {} @@ -183,6 +184,11 @@ struct MiriGenmcShim : private GenMCDriver { return nullptr; } + /**** Printing and estimation mode functionality. ****/ + + /// Get the results of a run in estimation mode. + auto get_estimation_results() const -> EstimationResult; + private: /** Increment the event index in the given thread by 1 and return the new event. */ [[nodiscard]] inline auto inc_pos(ThreadId tid) -> Event { diff --git a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp index c51b59e86517..5e7188f17e0d 100644 --- a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp +++ b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp @@ -10,7 +10,9 @@ #include "Support/Verbosity.hpp" // C++ headers: +#include #include +#include auto MiriGenmcShim::schedule_next( const int curr_thread_id, @@ -40,3 +42,15 @@ auto MiriGenmcShim::handle_execution_end() -> std::unique_ptr { GenMCDriver::handleExecutionEnd(); return {}; } + +/**** Estimation mode result ****/ + +auto MiriGenmcShim::get_estimation_results() const -> EstimationResult { + const auto& res = getResult(); + return EstimationResult { + .mean = static_cast(res.estimationMean), + .sd = static_cast(std::sqrt(res.estimationVariance)), + .explored_execs = static_cast(res.explored), + .blocked_execs = static_cast(res.exploredBlocked), + }; +} diff --git a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Setup.cpp b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Setup.cpp index a17a83aa06e1..af13f0d07746 100644 --- a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Setup.cpp +++ b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Setup.cpp @@ -58,7 +58,7 @@ static auto to_genmc_verbosity_level(const LogLevel log_level) -> VerbosityLevel logLevel = to_genmc_verbosity_level(log_level); } -/* unsafe */ auto MiriGenmcShim::create_handle(const GenmcParams& params) +/* unsafe */ auto MiriGenmcShim::create_handle(const GenmcParams& params, bool estimation_mode) -> std::unique_ptr { auto conf = std::make_shared(); @@ -82,7 +82,8 @@ static auto to_genmc_verbosity_level(const LogLevel log_level) -> VerbosityLevel // Miri. conf->warnOnGraphSize = 1024 * 1024; - // We only support the `RC11` memory model for Rust, and `SC` when weak memory emulation is disabled. + // We only support the `RC11` memory model for Rust, and `SC` when weak memory emulation is + // disabled. conf->model = params.disable_weak_memory_emulation ? ModelType::SC : ModelType::RC11; // This prints the seed that GenMC picks for randomized scheduling during estimation mode. @@ -119,12 +120,20 @@ static auto to_genmc_verbosity_level(const LogLevel log_level) -> VerbosityLevel ); conf->symmetryReduction = params.do_symmetry_reduction; - // FIXME(genmc): expose this setting to Miri (useful for testing Miri-GenMC). - conf->schedulePolicy = SchedulePolicy::WF; + // Set the scheduling policy. GenMC uses `WFR` for estimation mode. + // For normal verification, `WF` has the best performance and is the GenMC default. + // Other scheduling policies are used by GenMC for testing and for modes currently + // unsupported with Miri such as bounding, which uses LTR. + conf->schedulePolicy = estimation_mode ? SchedulePolicy::WFR : SchedulePolicy::WF; + // Set the min and max number of executions tested in estimation mode. + conf->estimationMin = 10; // default taken from GenMC + conf->estimationMax = params.estimation_max; + // Deviation threshold % under which estimation is deemed good enough. + conf->sdThreshold = 10; // default taken from GenMC // Set the mode used for this driver, either estimation or verification. - // FIXME(genmc): implement estimation mode. - const auto mode = GenMCDriver::Mode(GenMCDriver::VerificationMode {}); + const auto mode = estimation_mode ? GenMCDriver::Mode(GenMCDriver::EstimationMode {}) + : GenMCDriver::Mode(GenMCDriver::VerificationMode {}); // Running Miri-GenMC without race detection is not supported. // Disabling this option also changes the behavior of the replay scheduler to only schedule diff --git a/src/tools/miri/genmc-sys/src/lib.rs b/src/tools/miri/genmc-sys/src/lib.rs index 31bc2606adc0..733b3d780b18 100644 --- a/src/tools/miri/genmc-sys/src/lib.rs +++ b/src/tools/miri/genmc-sys/src/lib.rs @@ -27,6 +27,7 @@ static GENMC_LOG_LEVEL: OnceLock = OnceLock::new(); pub fn create_genmc_driver_handle( params: &GenmcParams, genmc_log_level: LogLevel, + do_estimation: bool, ) -> UniquePtr { // SAFETY: Only setting the GenMC log level once is guaranteed by the `OnceLock`. // No other place calls `set_log_level_raw`, so the `logLevel` value in GenMC will not change once we initialize it once. @@ -40,7 +41,7 @@ pub fn create_genmc_driver_handle( }), "Attempt to change the GenMC log level after it was already set" ); - unsafe { MiriGenmcShim::create_handle(params) } + unsafe { MiriGenmcShim::create_handle(params, do_estimation) } } impl GenmcScalar { @@ -54,6 +55,7 @@ impl GenmcScalar { impl Default for GenmcParams { fn default() -> Self { Self { + estimation_max: 1000, // default taken from GenMC print_random_schedule_seed: false, do_symmetry_reduction: false, // GenMC graphs can be quite large since Miri produces a lot of (non-atomic) events. @@ -70,6 +72,20 @@ impl Default for LogLevel { } } +impl FromStr for SchedulePolicy { + type Err = &'static str; + + fn from_str(s: &str) -> Result { + Ok(match s { + "wf" => SchedulePolicy::WF, + "wfr" => SchedulePolicy::WFR, + "arbitrary" | "random" => SchedulePolicy::Arbitrary, + "ltr" => SchedulePolicy::LTR, + _ => return Err("invalid scheduling policy"), + }) + } +} + impl FromStr for LogLevel { type Err = &'static str; @@ -92,9 +108,12 @@ mod ffi { /**** Types shared between Miri/Rust and Miri/C++ through cxx_bridge: ****/ /// Parameters that will be given to GenMC for setting up the model checker. - /// (The fields of this struct are visible to both Rust and C++) + /// The fields of this struct are visible to both Rust and C++. + /// Note that this struct is #[repr(C)], so the order of fields matters. #[derive(Clone, Debug)] struct GenmcParams { + /// Maximum number of executions explored in estimation mode. + pub estimation_max: u32, pub print_random_schedule_seed: bool, pub do_symmetry_reduction: bool, pub print_execution_graphs: ExecutiongraphPrinting, @@ -165,6 +184,19 @@ mod ffi { next_thread: i32, } + #[must_use] + #[derive(Debug)] + struct EstimationResult { + /// Expected number of total executions. + mean: f64, + /// Standard deviation of the total executions estimate. + sd: f64, + /// Number of explored executions during the estimation. + explored_execs: u64, + /// Number of encounteded blocked executions during the estimation. + blocked_execs: u64, + } + #[must_use] #[derive(Debug)] struct LoadResult { @@ -214,6 +246,14 @@ mod ffi { /**** These are GenMC types that we have to copy-paste here since cxx does not support "importing" externally defined C++ types. ****/ + #[derive(Clone, Copy, Debug)] + enum SchedulePolicy { + LTR, + WF, + WFR, + Arbitrary, + } + #[derive(Debug)] /// Corresponds to GenMC's type with the same name. /// Should only be modified if changed by GenMC. @@ -272,6 +312,7 @@ mod ffi { type ActionKind; type MemOrdering; type RMWBinOp; + type SchedulePolicy; /// Set the log level for GenMC. /// @@ -295,7 +336,10 @@ mod ffi { /// start creating handles. /// There should not be any other (safe) way to create a `MiriGenmcShim`. #[Self = "MiriGenmcShim"] - unsafe fn create_handle(params: &GenmcParams) -> UniquePtr; + unsafe fn create_handle( + params: &GenmcParams, + estimation_mode: bool, + ) -> UniquePtr; /// Get the bit mask that GenMC expects for global memory allocations. fn get_global_alloc_static_mask() -> u64; @@ -403,5 +447,10 @@ mod ffi { fn get_result_message(self: &MiriGenmcShim) -> UniquePtr; /// If an error occurred, return a string describing the error, otherwise, return `nullptr`. fn get_error_string(self: &MiriGenmcShim) -> UniquePtr; + + /**** Printing functionality. ****/ + + /// Get the results of a run in estimation mode. + fn get_estimation_results(self: &MiriGenmcShim) -> EstimationResult; } } diff --git a/src/tools/miri/src/bin/miri.rs b/src/tools/miri/src/bin/miri.rs index 731fe283a219..8b15a7863476 100644 --- a/src/tools/miri/src/bin/miri.rs +++ b/src/tools/miri/src/bin/miri.rs @@ -186,18 +186,17 @@ impl rustc_driver::Callbacks for MiriCompilerCalls { optimizations is usually marginal at best."); } - if let Some(_genmc_config) = &config.genmc_config { + // Run in GenMC mode if enabled. + if config.genmc_config.is_some() { + // This is the entry point used in GenMC mode. + // This closure will be called multiple times to explore the concurrent execution space of the program. let eval_entry_once = |genmc_ctx: Rc| { miri::eval_entry(tcx, entry_def_id, entry_type, &config, Some(genmc_ctx)) }; - - // FIXME(genmc): add estimation mode here. - let return_code = run_genmc_mode(&config, eval_entry_once, tcx).unwrap_or_else(|| { tcx.dcx().abort_if_errors(); rustc_driver::EXIT_FAILURE }); - exit(return_code); }; diff --git a/src/tools/miri/src/concurrency/genmc/config.rs b/src/tools/miri/src/concurrency/genmc/config.rs index 34933d423f06..c7cfa6012b8d 100644 --- a/src/tools/miri/src/concurrency/genmc/config.rs +++ b/src/tools/miri/src/concurrency/genmc/config.rs @@ -10,11 +10,15 @@ use crate::{IsolatedOp, MiriConfig, RejectOpWith}; pub struct GenmcConfig { /// Parameters sent to the C++ side to create a new handle to the GenMC model checker. pub(super) params: GenmcParams, + pub(super) do_estimation: bool, /// Print the output message that GenMC generates when an error occurs. /// This error message is currently hard to use, since there is no clear mapping between the events that GenMC sees and the Rust code location where this event was produced. pub(super) print_genmc_output: bool, /// The log level for GenMC. pub(super) log_level: LogLevel, + /// Enable more verbose output, such as number of executions estimate + /// and time to completion of verification step. + pub(super) verbose_output: bool, } impl GenmcConfig { @@ -57,8 +61,21 @@ impl GenmcConfig { "Invalid suffix to GenMC argument '-Zmiri-genmc-print-exec-graphs', expected '', '=none', '=explored', '=blocked' or '=all'" )), } + } else if trimmed_arg == "estimate" { + // FIXME(genmc): should this be on by default (like for GenMC)? + // Enable estimating the execution space and require time before running the actual verification. + genmc_config.do_estimation = true; + } else if let Some(estimation_max_str) = trimmed_arg.strip_prefix("estimation-max=") { + // Set the maximum number of executions to explore during estimation. + genmc_config.params.estimation_max = estimation_max_str.parse().ok().filter(|estimation_max| *estimation_max > 0).ok_or_else(|| { + format!( + "'-Zmiri-genmc-estimation-max=...' expects a positive integer argument, but got '{estimation_max_str}'" + ) + })?; } else if trimmed_arg == "print-genmc-output" { genmc_config.print_genmc_output = true; + } else if trimmed_arg == "verbose" { + genmc_config.verbose_output = true; } else { return Err(format!("Invalid GenMC argument: \"-Zmiri-genmc-{trimmed_arg}\"")); } diff --git a/src/tools/miri/src/concurrency/genmc/dummy.rs b/src/tools/miri/src/concurrency/genmc/dummy.rs index 92b34b83ee0f..c28984cef35a 100644 --- a/src/tools/miri/src/concurrency/genmc/dummy.rs +++ b/src/tools/miri/src/concurrency/genmc/dummy.rs @@ -39,18 +39,6 @@ mod run { impl GenmcCtx { // We don't provide the `new` function in the dummy module. - pub fn get_blocked_execution_count(&self) -> usize { - unreachable!() - } - - pub fn get_explored_execution_count(&self) -> usize { - unreachable!() - } - - pub fn is_exploration_done(&self) -> bool { - unreachable!() - } - /**** Memory access handling ****/ pub(super) fn set_ongoing_action_data_race_free(&self, _enable: bool) { diff --git a/src/tools/miri/src/concurrency/genmc/mod.rs b/src/tools/miri/src/concurrency/genmc/mod.rs index 7270c6681060..0086d3f2bf0b 100644 --- a/src/tools/miri/src/concurrency/genmc/mod.rs +++ b/src/tools/miri/src/concurrency/genmc/mod.rs @@ -2,8 +2,8 @@ use std::cell::{Cell, RefCell}; use std::sync::Arc; use genmc_sys::{ - GENMC_GLOBAL_ADDRESSES_MASK, GenmcScalar, MemOrdering, MiriGenmcShim, RMWBinOp, UniquePtr, - create_genmc_driver_handle, + EstimationResult, GENMC_GLOBAL_ADDRESSES_MASK, GenmcScalar, MemOrdering, MiriGenmcShim, + RMWBinOp, UniquePtr, create_genmc_driver_handle, }; use rustc_abi::{Align, Size}; use rustc_const_eval::interpret::{AllocId, InterpCx, InterpResult, interp_ok}; @@ -16,6 +16,7 @@ use self::helper::{ MAX_ACCESS_SIZE, Warnings, emit_warning, genmc_scalar_to_scalar, maybe_upgrade_compare_exchange_success_orderings, scalar_to_genmc_scalar, to_genmc_rmw_op, }; +use self::run::GenmcMode; use self::thread_id_map::ThreadIdMap; use crate::concurrency::genmc::helper::split_access; use crate::intrinsics::AtomicRmwOp; @@ -37,6 +38,16 @@ pub use genmc_sys::GenmcParams; pub use self::config::GenmcConfig; pub use self::run::run_genmc_mode; +#[derive(Debug)] +pub enum ExecutionEndResult { + /// An error occurred at the end of the execution. + Error(String), + /// No errors occurred, and there are more executions to explore. + Continue, + /// No errors occurred and we are finished. + Stop, +} + #[derive(Clone, Copy, Debug)] pub enum ExitType { MainThreadFinish, @@ -128,26 +139,33 @@ pub struct GenmcCtx { /// GenMC Context creation and administrative / query actions impl GenmcCtx { /// Create a new `GenmcCtx` from a given config. - fn new(miri_config: &MiriConfig, global_state: Arc) -> Self { + fn new(miri_config: &MiriConfig, global_state: Arc, mode: GenmcMode) -> Self { let genmc_config = miri_config.genmc_config.as_ref().unwrap(); - let handle = - RefCell::new(create_genmc_driver_handle(&genmc_config.params, genmc_config.log_level)); + let handle = RefCell::new(create_genmc_driver_handle( + &genmc_config.params, + genmc_config.log_level, + /* do_estimation: */ mode == GenmcMode::Estimation, + )); Self { handle, exec_state: Default::default(), global_state } } + fn get_estimation_results(&self) -> EstimationResult { + self.handle.borrow().get_estimation_results() + } + /// Get the number of blocked executions encountered by GenMC. - pub fn get_blocked_execution_count(&self) -> u64 { + fn get_blocked_execution_count(&self) -> u64 { self.handle.borrow().get_blocked_execution_count() } /// Get the number of explored executions encountered by GenMC. - pub fn get_explored_execution_count(&self) -> u64 { + fn get_explored_execution_count(&self) -> u64 { self.handle.borrow().get_explored_execution_count() } /// Check if GenMC encountered an error that wasn't immediately returned during execution. /// Returns a string representation of the error if one occurred. - pub fn try_get_error(&self) -> Option { + fn try_get_error(&self) -> Option { self.handle .borrow() .get_error_string() @@ -157,7 +175,7 @@ impl GenmcCtx { /// Check if GenMC encountered an error that wasn't immediately returned during execution. /// Returns a string representation of the error if one occurred. - pub fn get_result_message(&self) -> String { + fn get_result_message(&self) -> String { self.handle .borrow() .get_result_message() @@ -166,13 +184,6 @@ impl GenmcCtx { .expect("there should always be a message") } - /// This function determines if we should continue exploring executions or if we are done. - /// - /// In GenMC mode, the input program should be repeatedly executed until this function returns `true` or an error is found. - pub fn is_exploration_done(&self) -> bool { - self.handle.borrow_mut().pin_mut().is_exploration_done() - } - /// Select whether data race free actions should be allowed. This function should be used carefully! /// /// If `true` is passed, allow for data races to happen without triggering an error, until this function is called again with argument `false`. @@ -218,13 +229,25 @@ impl GenmcCtx { /// This function will also check for those, and return their error description. /// /// To get the all messages (warnings, errors) that GenMC produces, use the `get_result_message` method. - fn handle_execution_end(&self) -> Option { + fn handle_execution_end(&self) -> ExecutionEndResult { let result = self.handle.borrow_mut().pin_mut().handle_execution_end(); - result.as_ref().map(|msg| msg.to_string_lossy().to_string())?; + if let Some(error) = result.as_ref() { + return ExecutionEndResult::Error(error.to_string_lossy().to_string()); + } + + // GenMC decides if there is more to explore: + let exploration_done = self.handle.borrow_mut().pin_mut().is_exploration_done(); // GenMC currently does not return an error value immediately in all cases. + // Both `handle_execution_end` and `is_exploration_done` can produce such errors. // We manually query for any errors here to ensure we don't miss any. - self.try_get_error() + if let Some(error) = self.try_get_error() { + ExecutionEndResult::Error(error) + } else if exploration_done { + ExecutionEndResult::Stop + } else { + ExecutionEndResult::Continue + } } /**** Memory access handling ****/ diff --git a/src/tools/miri/src/concurrency/genmc/run.rs b/src/tools/miri/src/concurrency/genmc/run.rs index 7e4ed816a76a..bc2f5f7b79ec 100644 --- a/src/tools/miri/src/concurrency/genmc/run.rs +++ b/src/tools/miri/src/concurrency/genmc/run.rs @@ -1,32 +1,65 @@ use std::rc::Rc; use std::sync::Arc; +use std::time::Instant; +use genmc_sys::EstimationResult; use rustc_middle::ty::TyCtxt; use super::GlobalState; +use crate::concurrency::genmc::ExecutionEndResult; use crate::rustc_const_eval::interpret::PointerArithmetic; -use crate::{GenmcCtx, MiriConfig}; +use crate::{GenmcConfig, GenmcCtx, MiriConfig}; + +#[derive(Clone, Copy, PartialEq, Eq)] +pub(super) enum GenmcMode { + Estimation, + Verification, +} + +impl GenmcMode { + /// Return whether warnings on unsupported features should be printed in this mode. + fn print_unsupported_warnings(self) -> bool { + self == GenmcMode::Verification + } +} /// Do a complete run of the program in GenMC mode. /// This will call `eval_entry` multiple times, until either: /// - An error is detected (indicated by a `None` return value) /// - All possible executions are explored. /// -/// FIXME(genmc): add estimation mode setting. +/// Returns `None` is an error is detected, or `Some(return_value)` with the return value of the last run of the program. pub fn run_genmc_mode<'tcx>( config: &MiriConfig, eval_entry: impl Fn(Rc) -> Option, tcx: TyCtxt<'tcx>, ) -> Option { let genmc_config = config.genmc_config.as_ref().unwrap(); + // Run in Estimation mode if requested. + if genmc_config.do_estimation { + eprintln!("Estimating GenMC verification time..."); + run_genmc_mode_impl(config, &eval_entry, tcx, GenmcMode::Estimation)?; + } + // Run in Verification mode. + eprintln!("Running GenMC Verification..."); + run_genmc_mode_impl(config, &eval_entry, tcx, GenmcMode::Verification) +} + +fn run_genmc_mode_impl<'tcx>( + config: &MiriConfig, + eval_entry: &impl Fn(Rc) -> Option, + tcx: TyCtxt<'tcx>, + mode: GenmcMode, +) -> Option { + let time_start = Instant::now(); + let genmc_config = config.genmc_config.as_ref().unwrap(); // There exists only one `global_state` per full run in GenMC mode. // It is shared by all `GenmcCtx` in this run. // FIXME(genmc): implement multithreading once GenMC supports it. - // FIXME(genmc): disable warnings in estimation mode once it is added. let global_state = - Arc::new(GlobalState::new(tcx.target_usize_max(), /* print_warnings */ true)); - let genmc_ctx = Rc::new(GenmcCtx::new(config, global_state)); + Arc::new(GlobalState::new(tcx.target_usize_max(), mode.print_unsupported_warnings())); + let genmc_ctx = Rc::new(GenmcCtx::new(config, global_state, mode)); // `rep` is used to report the progress, Miri will panic on wrap-around. for rep in 0u64.. { @@ -37,46 +70,97 @@ pub fn run_genmc_mode<'tcx>( // Execute the program until completion to get the return value, or return if an error happens: let Some(return_code) = eval_entry(genmc_ctx.clone()) else { - // If requested, print the output GenMC produced: - if genmc_config.print_genmc_output { - eprintln!("== raw GenMC output ========================="); - eprintln!("{}", genmc_ctx.get_result_message()); - eprintln!("== end of raw GenMC output =================="); - } + genmc_ctx.print_genmc_output(genmc_config); return None; }; - // We inform GenMC that the execution is complete. If there was an error, we print it. - if let Some(error) = genmc_ctx.handle_execution_end() { - // This can be reached for errors that affect the entire execution, not just a specific event. - // For instance, linearizability checking and liveness checking report their errors this way. - // Neither are supported by Miri-GenMC at the moment though. However, GenMC also - // treats races on deallocation as global errors, so this code path is still reachable. - // Since we don't have any span information for the error at this point, - // we just print GenMC's error message. - eprintln!("(GenMC) Error detected: {error}"); - eprintln!(); - eprintln!("{}", genmc_ctx.get_result_message()); - return None; + // We inform GenMC that the execution is complete. + // If there was an error, we print it. + match genmc_ctx.handle_execution_end() { + ExecutionEndResult::Continue => continue, + ExecutionEndResult::Stop => { + let elapsed_time_sec = Instant::now().duration_since(time_start).as_secs_f64(); + // Print the output for the current mode. + if mode == GenmcMode::Estimation { + genmc_ctx.print_estimation_output(genmc_config, elapsed_time_sec); + } else { + genmc_ctx.print_verification_output(genmc_config, elapsed_time_sec); + } + // Return the return code of the last execution. + return Some(return_code); + } + ExecutionEndResult::Error(error) => { + // This can be reached for errors that affect the entire execution, not just a specific event. + // For instance, linearizability checking and liveness checking report their errors this way. + // Neither are supported by Miri-GenMC at the moment though. However, GenMC also + // treats races on deallocation as global errors, so this code path is still reachable. + // Since we don't have any span information for the error at this point, + // we just print GenMC's error string, and the full GenMC output if requested. + eprintln!("(GenMC) Error detected: {error}"); + genmc_ctx.print_genmc_output(genmc_config); + return None; + } } - - // Check if we've explored enough executions: - if !genmc_ctx.is_exploration_done() { - continue; - } - - eprintln!("(GenMC) Verification complete. No errors were detected."); - - let explored_execution_count = genmc_ctx.get_explored_execution_count(); - let blocked_execution_count = genmc_ctx.get_blocked_execution_count(); - - eprintln!("Number of complete executions explored: {explored_execution_count}"); - if blocked_execution_count > 0 { - eprintln!("Number of blocked executions seen: {blocked_execution_count}"); - } - - // Return the return code of the last execution. - return Some(return_code); } unreachable!() } + +impl GenmcCtx { + /// Print the full output message produced by GenMC if requested, or a hint on how to enable it. + /// + /// This message can be very verbose and is likely not useful for the average user. + /// This function should be called *after* Miri has printed all of its output. + fn print_genmc_output(&self, genmc_config: &GenmcConfig) { + if genmc_config.print_genmc_output { + eprintln!("GenMC error report:"); + eprintln!("{}", self.get_result_message()); + } else { + eprintln!( + "(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.)" + ); + } + } + + /// Given the time taken for the estimation mode run, print the expected time range for verification. + /// Verbose output also includes information about the expected number of executions and how many estimation rounds were explored or got blocked. + fn print_estimation_output(&self, genmc_config: &GenmcConfig, elapsed_time_sec: f64) { + let EstimationResult { mean, sd, explored_execs, blocked_execs } = + self.get_estimation_results(); + #[allow(clippy::as_conversions)] + let time_per_exec_sec = elapsed_time_sec / (explored_execs as f64 + blocked_execs as f64); + let estimated_mean_sec = time_per_exec_sec * mean; + let estimated_sd_sec = time_per_exec_sec * sd; + + if genmc_config.verbose_output { + eprintln!("Finished estimation in {elapsed_time_sec:.2?}s"); + if blocked_execs != 0 { + eprintln!(" Explored executions: {explored_execs}"); + eprintln!(" Blocked executions: {blocked_execs}"); + } + eprintln!("Expected number of executions: {mean:.0} ± {sd:.0}"); + } + // The estimation can be out-of-bounds of an `f64`. + if !(mean.is_finite() && mean >= 0.0 && sd.is_finite() && sd >= 0.0) { + eprintln!("WARNING: Estimation gave weird results, there may have been an overflow."); + } + eprintln!("Expected verification time: {estimated_mean_sec:.2}s ± {estimated_sd_sec:.2}s"); + } + + /// Given the time taken for the verification mode run, print the expected time range for verification. + /// Verbose output also includes information about the expected number of executions and how many estimation rounds were explored or got blocked. + fn print_verification_output(&self, genmc_config: &GenmcConfig, elapsed_time_sec: f64) { + let explored_execution_count = self.get_explored_execution_count(); + let blocked_execution_count = self.get_blocked_execution_count(); + eprintln!( + "Verification complete with {} executions. No errors found.", + explored_execution_count + blocked_execution_count + ); + if genmc_config.verbose_output { + if blocked_execution_count > 0 { + eprintln!("Number of complete executions explored: {explored_execution_count}"); + eprintln!("Number of blocked executions seen: {blocked_execution_count}"); + } + eprintln!("Verification took {elapsed_time_sec:.2?}s."); + } + } +} diff --git a/src/tools/miri/tests/genmc/fail/data_race/mpu2_rels_rlx.stderr b/src/tools/miri/tests/genmc/fail/data_race/mpu2_rels_rlx.stderr index 946d9a2124b8..00de74009d9b 100644 --- a/src/tools/miri/tests/genmc/fail/data_race/mpu2_rels_rlx.stderr +++ b/src/tools/miri/tests/genmc/fail/data_race/mpu2_rels_rlx.stderr @@ -1,3 +1,4 @@ +Running GenMC Verification... error: Undefined Behavior: Non-atomic race --> tests/genmc/fail/data_race/mpu2_rels_rlx.rs:LL:CC | @@ -15,5 +16,6 @@ note: inside `genmc::spawn_pthread_closure::thread_func::<{closure@tests/genmc/f LL | f(); | ^^^ +(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.) error: aborting due to 1 previous error diff --git a/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rel_rlx.stderr b/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rel_rlx.stderr index 121ded2a181c..501957a90d3a 100644 --- a/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rel_rlx.stderr +++ b/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rel_rlx.stderr @@ -1,3 +1,4 @@ +Running GenMC Verification... error: Undefined Behavior: Non-atomic race --> tests/genmc/fail/data_race/weak_orderings.rs:LL:CC | @@ -15,5 +16,6 @@ note: inside `genmc::spawn_pthread_closure::thread_func::<{closure@tests/genmc/f LL | f(); | ^^^ +(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.) error: aborting due to 1 previous error diff --git a/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rlx_acq.stderr b/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rlx_acq.stderr index 121ded2a181c..501957a90d3a 100644 --- a/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rlx_acq.stderr +++ b/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rlx_acq.stderr @@ -1,3 +1,4 @@ +Running GenMC Verification... error: Undefined Behavior: Non-atomic race --> tests/genmc/fail/data_race/weak_orderings.rs:LL:CC | @@ -15,5 +16,6 @@ note: inside `genmc::spawn_pthread_closure::thread_func::<{closure@tests/genmc/f LL | f(); | ^^^ +(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.) error: aborting due to 1 previous error diff --git a/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rlx_rlx.stderr b/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rlx_rlx.stderr index 121ded2a181c..501957a90d3a 100644 --- a/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rlx_rlx.stderr +++ b/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rlx_rlx.stderr @@ -1,3 +1,4 @@ +Running GenMC Verification... error: Undefined Behavior: Non-atomic race --> tests/genmc/fail/data_race/weak_orderings.rs:LL:CC | @@ -15,5 +16,6 @@ note: inside `genmc::spawn_pthread_closure::thread_func::<{closure@tests/genmc/f LL | f(); | ^^^ +(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.) error: aborting due to 1 previous error diff --git a/src/tools/miri/tests/genmc/fail/loom/buggy_inc.stderr b/src/tools/miri/tests/genmc/fail/loom/buggy_inc.stderr index 5a8948ff9b4b..9c3ba1d4c592 100644 --- a/src/tools/miri/tests/genmc/fail/loom/buggy_inc.stderr +++ b/src/tools/miri/tests/genmc/fail/loom/buggy_inc.stderr @@ -1,3 +1,4 @@ +Running GenMC Verification... error: abnormal termination: the program aborted execution --> tests/genmc/fail/loom/buggy_inc.rs:LL:CC | @@ -9,5 +10,6 @@ LL | std::process::abort(); note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace +(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.) error: aborting due to 1 previous error diff --git a/src/tools/miri/tests/genmc/fail/loom/store_buffering.genmc.stderr b/src/tools/miri/tests/genmc/fail/loom/store_buffering.genmc.stderr index a6c3ed7055e7..db92d0573fad 100644 --- a/src/tools/miri/tests/genmc/fail/loom/store_buffering.genmc.stderr +++ b/src/tools/miri/tests/genmc/fail/loom/store_buffering.genmc.stderr @@ -1,3 +1,4 @@ +Running GenMC Verification... error: abnormal termination: the program aborted execution --> tests/genmc/fail/loom/store_buffering.rs:LL:CC | @@ -9,5 +10,6 @@ LL | std::process::abort(); note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace +(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.) error: aborting due to 1 previous error diff --git a/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.relaxed4.stderr b/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.relaxed4.stderr index cbfb6ec833eb..773f86a97596 100644 --- a/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.relaxed4.stderr +++ b/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.relaxed4.stderr @@ -1,3 +1,4 @@ +Running GenMC Verification... error: abnormal termination: the program aborted execution --> tests/genmc/fail/simple/2w2w_weak.rs:LL:CC | @@ -9,5 +10,6 @@ LL | std::process::abort(); note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace +(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.) error: aborting due to 1 previous error diff --git a/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.release4.stderr b/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.release4.stderr index cbfb6ec833eb..773f86a97596 100644 --- a/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.release4.stderr +++ b/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.release4.stderr @@ -1,3 +1,4 @@ +Running GenMC Verification... error: abnormal termination: the program aborted execution --> tests/genmc/fail/simple/2w2w_weak.rs:LL:CC | @@ -9,5 +10,6 @@ LL | std::process::abort(); note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace +(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.) error: aborting due to 1 previous error diff --git a/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.sc3_rel1.stderr b/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.sc3_rel1.stderr index cbfb6ec833eb..773f86a97596 100644 --- a/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.sc3_rel1.stderr +++ b/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.sc3_rel1.stderr @@ -1,3 +1,4 @@ +Running GenMC Verification... error: abnormal termination: the program aborted execution --> tests/genmc/fail/simple/2w2w_weak.rs:LL:CC | @@ -9,5 +10,6 @@ LL | std::process::abort(); note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace +(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.) error: aborting due to 1 previous error diff --git a/src/tools/miri/tests/genmc/pass/atomics/cas_failure_ord_racy_key_init.stderr b/src/tools/miri/tests/genmc/pass/atomics/cas_failure_ord_racy_key_init.stderr index d97b8b3d92f4..31438f9352fe 100644 --- a/src/tools/miri/tests/genmc/pass/atomics/cas_failure_ord_racy_key_init.stderr +++ b/src/tools/miri/tests/genmc/pass/atomics/cas_failure_ord_racy_key_init.stderr @@ -1,3 +1,4 @@ +Running GenMC Verification... warning: GenMC currently does not model the failure ordering for `compare_exchange`. Success ordering 'Release' was upgraded to 'AcqRel' to match failure ordering 'Acquire'. Miri with GenMC might miss bugs related to this memory access. --> tests/genmc/pass/atomics/cas_failure_ord_racy_key_init.rs:LL:CC | @@ -18,5 +19,4 @@ note: inside `genmc::spawn_pthread_closure::thread_func::<{closure@tests/genmc/p LL | f(); | ^^^ -(GenMC) Verification complete. No errors were detected. -Number of complete executions explored: 2 +Verification complete with 2 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/atomics/cas_simple.stderr b/src/tools/miri/tests/genmc/pass/atomics/cas_simple.stderr index 3b22247ee44c..7867be2dbe8e 100644 --- a/src/tools/miri/tests/genmc/pass/atomics/cas_simple.stderr +++ b/src/tools/miri/tests/genmc/pass/atomics/cas_simple.stderr @@ -1,2 +1,2 @@ -(GenMC) Verification complete. No errors were detected. -Number of complete executions explored: 1 +Running GenMC Verification... +Verification complete with 1 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/atomics/rmw_ops.stderr b/src/tools/miri/tests/genmc/pass/atomics/rmw_ops.stderr index 3b22247ee44c..7867be2dbe8e 100644 --- a/src/tools/miri/tests/genmc/pass/atomics/rmw_ops.stderr +++ b/src/tools/miri/tests/genmc/pass/atomics/rmw_ops.stderr @@ -1,2 +1,2 @@ -(GenMC) Verification complete. No errors were detected. -Number of complete executions explored: 1 +Running GenMC Verification... +Verification complete with 1 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/litmus/2cowr.stderr b/src/tools/miri/tests/genmc/pass/litmus/2cowr.stderr index 0667962f99c8..a67635dee1be 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/2cowr.stderr +++ b/src/tools/miri/tests/genmc/pass/litmus/2cowr.stderr @@ -1,2 +1,2 @@ -(GenMC) Verification complete. No errors were detected. -Number of complete executions explored: 4 +Running GenMC Verification... +Verification complete with 4 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/litmus/2w2w_2sc_scf.stderr b/src/tools/miri/tests/genmc/pass/litmus/2w2w_2sc_scf.stderr index 115b1986ce55..485142e945a7 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/2w2w_2sc_scf.stderr +++ b/src/tools/miri/tests/genmc/pass/litmus/2w2w_2sc_scf.stderr @@ -1,2 +1,2 @@ -(GenMC) Verification complete. No errors were detected. -Number of complete executions explored: 3 +Running GenMC Verification... +Verification complete with 3 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/litmus/2w2w_3sc_1rel.release1.stderr b/src/tools/miri/tests/genmc/pass/litmus/2w2w_3sc_1rel.release1.stderr index 0667962f99c8..a67635dee1be 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/2w2w_3sc_1rel.release1.stderr +++ b/src/tools/miri/tests/genmc/pass/litmus/2w2w_3sc_1rel.release1.stderr @@ -1,2 +1,2 @@ -(GenMC) Verification complete. No errors were detected. -Number of complete executions explored: 4 +Running GenMC Verification... +Verification complete with 4 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/litmus/2w2w_3sc_1rel.release2.stderr b/src/tools/miri/tests/genmc/pass/litmus/2w2w_3sc_1rel.release2.stderr index 0667962f99c8..a67635dee1be 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/2w2w_3sc_1rel.release2.stderr +++ b/src/tools/miri/tests/genmc/pass/litmus/2w2w_3sc_1rel.release2.stderr @@ -1,2 +1,2 @@ -(GenMC) Verification complete. No errors were detected. -Number of complete executions explored: 4 +Running GenMC Verification... +Verification complete with 4 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/litmus/2w2w_4rel.sc.stderr b/src/tools/miri/tests/genmc/pass/litmus/2w2w_4rel.sc.stderr index 115b1986ce55..485142e945a7 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/2w2w_4rel.sc.stderr +++ b/src/tools/miri/tests/genmc/pass/litmus/2w2w_4rel.sc.stderr @@ -1,2 +1,2 @@ -(GenMC) Verification complete. No errors were detected. -Number of complete executions explored: 3 +Running GenMC Verification... +Verification complete with 3 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/litmus/2w2w_4rel.weak.stderr b/src/tools/miri/tests/genmc/pass/litmus/2w2w_4rel.weak.stderr index 0667962f99c8..a67635dee1be 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/2w2w_4rel.weak.stderr +++ b/src/tools/miri/tests/genmc/pass/litmus/2w2w_4rel.weak.stderr @@ -1,2 +1,2 @@ -(GenMC) Verification complete. No errors were detected. -Number of complete executions explored: 4 +Running GenMC Verification... +Verification complete with 4 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/litmus/2w2w_4sc.stderr b/src/tools/miri/tests/genmc/pass/litmus/2w2w_4sc.stderr index 115b1986ce55..485142e945a7 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/2w2w_4sc.stderr +++ b/src/tools/miri/tests/genmc/pass/litmus/2w2w_4sc.stderr @@ -1,2 +1,2 @@ -(GenMC) Verification complete. No errors were detected. -Number of complete executions explored: 3 +Running GenMC Verification... +Verification complete with 3 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/litmus/IRIW-acq-sc.stderr b/src/tools/miri/tests/genmc/pass/litmus/IRIW-acq-sc.stderr index c760b4460511..d6ec73a8c667 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/IRIW-acq-sc.stderr +++ b/src/tools/miri/tests/genmc/pass/litmus/IRIW-acq-sc.stderr @@ -1,2 +1,2 @@ -(GenMC) Verification complete. No errors were detected. -Number of complete executions explored: 16 +Running GenMC Verification... +Verification complete with 16 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/litmus/IRIWish.stderr b/src/tools/miri/tests/genmc/pass/litmus/IRIWish.stderr index 4fc77b63f380..7ea2dd508513 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/IRIWish.stderr +++ b/src/tools/miri/tests/genmc/pass/litmus/IRIWish.stderr @@ -1,3 +1,4 @@ +Running GenMC Verification... [1, 1, 1, 1, 1] [1, 1, 1, 0, 1] [1, 1, 1, 0, 0] @@ -26,5 +27,4 @@ [0, 0, 0, 0, 0] [0, 0, 0, 0, 1] [0, 0, 0, 0, 0] -(GenMC) Verification complete. No errors were detected. -Number of complete executions explored: 28 +Verification complete with 28 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/litmus/LB.stderr b/src/tools/miri/tests/genmc/pass/litmus/LB.stderr index 115b1986ce55..485142e945a7 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/LB.stderr +++ b/src/tools/miri/tests/genmc/pass/litmus/LB.stderr @@ -1,2 +1,2 @@ -(GenMC) Verification complete. No errors were detected. -Number of complete executions explored: 3 +Running GenMC Verification... +Verification complete with 3 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/litmus/LB_incMPs.stderr b/src/tools/miri/tests/genmc/pass/litmus/LB_incMPs.stderr index c879e95a1708..e414cd5e064d 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/LB_incMPs.stderr +++ b/src/tools/miri/tests/genmc/pass/litmus/LB_incMPs.stderr @@ -1,2 +1,2 @@ -(GenMC) Verification complete. No errors were detected. -Number of complete executions explored: 15 +Running GenMC Verification... +Verification complete with 15 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/litmus/MP.stderr b/src/tools/miri/tests/genmc/pass/litmus/MP.stderr index 115b1986ce55..485142e945a7 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/MP.stderr +++ b/src/tools/miri/tests/genmc/pass/litmus/MP.stderr @@ -1,2 +1,2 @@ -(GenMC) Verification complete. No errors were detected. -Number of complete executions explored: 3 +Running GenMC Verification... +Verification complete with 3 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/litmus/MPU2_rels_acqf.stderr b/src/tools/miri/tests/genmc/pass/litmus/MPU2_rels_acqf.stderr index 4551c00b0575..29b59ce3bc1a 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/MPU2_rels_acqf.stderr +++ b/src/tools/miri/tests/genmc/pass/litmus/MPU2_rels_acqf.stderr @@ -1,3 +1,4 @@ +Running GenMC Verification... X=1, Y=2, a=Err(1), b=Ok(1), c=2 X=1, Y=2, a=Err(1), b=Ok(1), c=1 X=1, Y=2, a=Err(1), b=Ok(1), c=0 @@ -34,5 +35,4 @@ X=1, Y=1, a=Err(0), b=Err(0), c=0 X=1, Y=1, a=Err(0), b=Err(0), c=1 X=1, Y=1, a=Err(0), b=Err(0), c=0 X=1, Y=1, a=Err(0), b=Err(0), c=0 -(GenMC) Verification complete. No errors were detected. -Number of complete executions explored: 36 +Verification complete with 36 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/litmus/MPU_rels_acq.stderr b/src/tools/miri/tests/genmc/pass/litmus/MPU_rels_acq.stderr index c5e34b00642a..423ee6dc3999 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/MPU_rels_acq.stderr +++ b/src/tools/miri/tests/genmc/pass/litmus/MPU_rels_acq.stderr @@ -1,2 +1,2 @@ -(GenMC) Verification complete. No errors were detected. -Number of complete executions explored: 13 +Running GenMC Verification... +Verification complete with 13 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/litmus/MP_incMPs.stderr b/src/tools/miri/tests/genmc/pass/litmus/MP_incMPs.stderr index 2be9a6c7fbde..f527b6120232 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/MP_incMPs.stderr +++ b/src/tools/miri/tests/genmc/pass/litmus/MP_incMPs.stderr @@ -1,2 +1,2 @@ -(GenMC) Verification complete. No errors were detected. -Number of complete executions explored: 7 +Running GenMC Verification... +Verification complete with 7 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/litmus/MP_rels_acqf.stderr b/src/tools/miri/tests/genmc/pass/litmus/MP_rels_acqf.stderr index 0667962f99c8..a67635dee1be 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/MP_rels_acqf.stderr +++ b/src/tools/miri/tests/genmc/pass/litmus/MP_rels_acqf.stderr @@ -1,2 +1,2 @@ -(GenMC) Verification complete. No errors were detected. -Number of complete executions explored: 4 +Running GenMC Verification... +Verification complete with 4 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/litmus/SB.stderr b/src/tools/miri/tests/genmc/pass/litmus/SB.stderr index 0667962f99c8..a67635dee1be 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/SB.stderr +++ b/src/tools/miri/tests/genmc/pass/litmus/SB.stderr @@ -1,2 +1,2 @@ -(GenMC) Verification complete. No errors were detected. -Number of complete executions explored: 4 +Running GenMC Verification... +Verification complete with 4 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/litmus/SB_2sc_scf.stderr b/src/tools/miri/tests/genmc/pass/litmus/SB_2sc_scf.stderr index 115b1986ce55..485142e945a7 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/SB_2sc_scf.stderr +++ b/src/tools/miri/tests/genmc/pass/litmus/SB_2sc_scf.stderr @@ -1,2 +1,2 @@ -(GenMC) Verification complete. No errors were detected. -Number of complete executions explored: 3 +Running GenMC Verification... +Verification complete with 3 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/litmus/Z6_U.sc.stderr b/src/tools/miri/tests/genmc/pass/litmus/Z6_U.sc.stderr index 8dd2fbe1b975..c8fbb8951a38 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/Z6_U.sc.stderr +++ b/src/tools/miri/tests/genmc/pass/litmus/Z6_U.sc.stderr @@ -1,3 +1,4 @@ +Running GenMC Verification... a=2, b=1, X=1, Y=3 a=4, b=1, X=1, Y=4 a=3, b=1, X=1, Y=3 @@ -16,5 +17,4 @@ a=3, b=0, X=1, Y=1 a=1, b=1, X=1, Y=3 a=1, b=1, X=1, Y=1 a=1, b=0, X=1, Y=1 -(GenMC) Verification complete. No errors were detected. -Number of complete executions explored: 18 +Verification complete with 18 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/litmus/Z6_U.weak.stderr b/src/tools/miri/tests/genmc/pass/litmus/Z6_U.weak.stderr index 65622575de21..72c59d33f77c 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/Z6_U.weak.stderr +++ b/src/tools/miri/tests/genmc/pass/litmus/Z6_U.weak.stderr @@ -1,3 +1,4 @@ +Running GenMC Verification... a=2, b=1, X=1, Y=3 a=4, b=1, X=1, Y=4 a=4, b=0, X=1, Y=4 @@ -20,5 +21,4 @@ a=1, b=1, X=1, Y=3 a=1, b=0, X=1, Y=3 a=1, b=1, X=1, Y=1 a=1, b=0, X=1, Y=1 -(GenMC) Verification complete. No errors were detected. -Number of complete executions explored: 22 +Verification complete with 22 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/litmus/Z6_acq.stderr b/src/tools/miri/tests/genmc/pass/litmus/Z6_acq.stderr index 2be9a6c7fbde..f527b6120232 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/Z6_acq.stderr +++ b/src/tools/miri/tests/genmc/pass/litmus/Z6_acq.stderr @@ -1,2 +1,2 @@ -(GenMC) Verification complete. No errors were detected. -Number of complete executions explored: 7 +Running GenMC Verification... +Verification complete with 7 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/litmus/atomicpo.stderr b/src/tools/miri/tests/genmc/pass/litmus/atomicpo.stderr index 0667962f99c8..a67635dee1be 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/atomicpo.stderr +++ b/src/tools/miri/tests/genmc/pass/litmus/atomicpo.stderr @@ -1,2 +1,2 @@ -(GenMC) Verification complete. No errors were detected. -Number of complete executions explored: 4 +Running GenMC Verification... +Verification complete with 4 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/litmus/casdep.stderr b/src/tools/miri/tests/genmc/pass/litmus/casdep.stderr index 01701dfe6918..bde951866d01 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/casdep.stderr +++ b/src/tools/miri/tests/genmc/pass/litmus/casdep.stderr @@ -1,2 +1,2 @@ -(GenMC) Verification complete. No errors were detected. -Number of complete executions explored: 2 +Running GenMC Verification... +Verification complete with 2 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/litmus/ccr.stderr b/src/tools/miri/tests/genmc/pass/litmus/ccr.stderr index 01701dfe6918..bde951866d01 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/ccr.stderr +++ b/src/tools/miri/tests/genmc/pass/litmus/ccr.stderr @@ -1,2 +1,2 @@ -(GenMC) Verification complete. No errors were detected. -Number of complete executions explored: 2 +Running GenMC Verification... +Verification complete with 2 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/litmus/cii.stderr b/src/tools/miri/tests/genmc/pass/litmus/cii.stderr index be75e68fde77..b9bdf2245aed 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/cii.stderr +++ b/src/tools/miri/tests/genmc/pass/litmus/cii.stderr @@ -1,2 +1,2 @@ -(GenMC) Verification complete. No errors were detected. -Number of complete executions explored: 6 +Running GenMC Verification... +Verification complete with 6 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/litmus/corr.stderr b/src/tools/miri/tests/genmc/pass/litmus/corr.stderr index be75e68fde77..b9bdf2245aed 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/corr.stderr +++ b/src/tools/miri/tests/genmc/pass/litmus/corr.stderr @@ -1,2 +1,2 @@ -(GenMC) Verification complete. No errors were detected. -Number of complete executions explored: 6 +Running GenMC Verification... +Verification complete with 6 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/litmus/corr0.stderr b/src/tools/miri/tests/genmc/pass/litmus/corr0.stderr index 0667962f99c8..a67635dee1be 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/corr0.stderr +++ b/src/tools/miri/tests/genmc/pass/litmus/corr0.stderr @@ -1,2 +1,2 @@ -(GenMC) Verification complete. No errors were detected. -Number of complete executions explored: 4 +Running GenMC Verification... +Verification complete with 4 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/litmus/corr1.stderr b/src/tools/miri/tests/genmc/pass/litmus/corr1.stderr index f6d07e9c77b2..384425fc43c6 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/corr1.stderr +++ b/src/tools/miri/tests/genmc/pass/litmus/corr1.stderr @@ -1,2 +1,2 @@ -(GenMC) Verification complete. No errors were detected. -Number of complete executions explored: 36 +Running GenMC Verification... +Verification complete with 36 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/litmus/corr2.stderr b/src/tools/miri/tests/genmc/pass/litmus/corr2.stderr index 78a90b63feab..07fd2d4de180 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/corr2.stderr +++ b/src/tools/miri/tests/genmc/pass/litmus/corr2.stderr @@ -1,2 +1,2 @@ -(GenMC) Verification complete. No errors were detected. -Number of complete executions explored: 72 +Running GenMC Verification... +Verification complete with 72 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/litmus/corw.stderr b/src/tools/miri/tests/genmc/pass/litmus/corw.stderr index 115b1986ce55..485142e945a7 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/corw.stderr +++ b/src/tools/miri/tests/genmc/pass/litmus/corw.stderr @@ -1,2 +1,2 @@ -(GenMC) Verification complete. No errors were detected. -Number of complete executions explored: 3 +Running GenMC Verification... +Verification complete with 3 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/litmus/cowr.stderr b/src/tools/miri/tests/genmc/pass/litmus/cowr.stderr index 115b1986ce55..485142e945a7 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/cowr.stderr +++ b/src/tools/miri/tests/genmc/pass/litmus/cowr.stderr @@ -1,2 +1,2 @@ -(GenMC) Verification complete. No errors were detected. -Number of complete executions explored: 3 +Running GenMC Verification... +Verification complete with 3 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/litmus/cumul-release.stderr b/src/tools/miri/tests/genmc/pass/litmus/cumul-release.stderr index 00394048ec5c..a031dfc8977a 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/cumul-release.stderr +++ b/src/tools/miri/tests/genmc/pass/litmus/cumul-release.stderr @@ -1,2 +1,2 @@ -(GenMC) Verification complete. No errors were detected. -Number of complete executions explored: 8 +Running GenMC Verification... +Verification complete with 8 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/litmus/default.stderr b/src/tools/miri/tests/genmc/pass/litmus/default.stderr index e0313930282e..87d38d250411 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/default.stderr +++ b/src/tools/miri/tests/genmc/pass/litmus/default.stderr @@ -1,2 +1,2 @@ -(GenMC) Verification complete. No errors were detected. -Number of complete executions explored: 12 +Running GenMC Verification... +Verification complete with 12 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/litmus/detour.join.stderr b/src/tools/miri/tests/genmc/pass/litmus/detour.join.stderr index 15017249dc3a..5006f11fefb1 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/detour.join.stderr +++ b/src/tools/miri/tests/genmc/pass/litmus/detour.join.stderr @@ -1,2 +1,2 @@ -(GenMC) Verification complete. No errors were detected. -Number of complete executions explored: 9 +Running GenMC Verification... +Verification complete with 9 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/litmus/detour.no_join.stderr b/src/tools/miri/tests/genmc/pass/litmus/detour.no_join.stderr index 15017249dc3a..5006f11fefb1 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/detour.no_join.stderr +++ b/src/tools/miri/tests/genmc/pass/litmus/detour.no_join.stderr @@ -1,2 +1,2 @@ -(GenMC) Verification complete. No errors were detected. -Number of complete executions explored: 9 +Running GenMC Verification... +Verification complete with 9 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/litmus/fr_w_w_w_reads.stderr b/src/tools/miri/tests/genmc/pass/litmus/fr_w_w_w_reads.stderr index 3b6ba238f534..c09b50e282f1 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/fr_w_w_w_reads.stderr +++ b/src/tools/miri/tests/genmc/pass/litmus/fr_w_w_w_reads.stderr @@ -1,2 +1,2 @@ -(GenMC) Verification complete. No errors were detected. -Number of complete executions explored: 210 +Running GenMC Verification... +Verification complete with 210 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/litmus/inc2w.stderr b/src/tools/miri/tests/genmc/pass/litmus/inc2w.stderr index be75e68fde77..b9bdf2245aed 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/inc2w.stderr +++ b/src/tools/miri/tests/genmc/pass/litmus/inc2w.stderr @@ -1,2 +1,2 @@ -(GenMC) Verification complete. No errors were detected. -Number of complete executions explored: 6 +Running GenMC Verification... +Verification complete with 6 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/litmus/inc_inc_RR_W_RR.stderr b/src/tools/miri/tests/genmc/pass/litmus/inc_inc_RR_W_RR.stderr index b5f8cd15b683..770fb7ef8804 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/inc_inc_RR_W_RR.stderr +++ b/src/tools/miri/tests/genmc/pass/litmus/inc_inc_RR_W_RR.stderr @@ -1,2 +1,2 @@ -(GenMC) Verification complete. No errors were detected. -Number of complete executions explored: 600 +Running GenMC Verification... +Verification complete with 600 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/litmus/riwi.stderr b/src/tools/miri/tests/genmc/pass/litmus/riwi.stderr index 115b1986ce55..485142e945a7 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/riwi.stderr +++ b/src/tools/miri/tests/genmc/pass/litmus/riwi.stderr @@ -1,2 +1,2 @@ -(GenMC) Verification complete. No errors were detected. -Number of complete executions explored: 3 +Running GenMC Verification... +Verification complete with 3 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/litmus/viktor-relseq.rs b/src/tools/miri/tests/genmc/pass/litmus/viktor-relseq.rs index a193dcf0683e..3256c9f42119 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/viktor-relseq.rs +++ b/src/tools/miri/tests/genmc/pass/litmus/viktor-relseq.rs @@ -1,6 +1,8 @@ -//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows +//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows -Zmiri-genmc-estimate // Translated from GenMC's "litmus/viktor-relseq" test. +// +// This test also checks that we can run the GenMC estimation mode. #![no_main] diff --git a/src/tools/miri/tests/genmc/pass/litmus/viktor-relseq.stderr b/src/tools/miri/tests/genmc/pass/litmus/viktor-relseq.stderr index d63ac5199d5d..c53d5c569b9c 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/viktor-relseq.stderr +++ b/src/tools/miri/tests/genmc/pass/litmus/viktor-relseq.stderr @@ -1,2 +1,4 @@ -(GenMC) Verification complete. No errors were detected. -Number of complete executions explored: 180 +Estimating GenMC verification time... +Expected verification time: [MEAN] ± [SD] +Running GenMC Verification... +Verification complete with 180 executions. No errors found. diff --git a/src/tools/miri/tests/ui.rs b/src/tools/miri/tests/ui.rs index b7286d9a3673..efaaf9fc8417 100644 --- a/src/tools/miri/tests/ui.rs +++ b/src/tools/miri/tests/ui.rs @@ -277,6 +277,8 @@ regexes! { r"\bsys/([a-z_]+)/[a-z]+\b" => "sys/$1/PLATFORM", // erase paths into the crate registry r"[^ ]*/\.?cargo/registry/.*/(.*\.rs)" => "CARGO_REGISTRY/.../$1", + // remove time print from GenMC estimation mode output. + "\nExpected verification time: .* ± .*" => "\nExpected verification time: [MEAN] ± [SD]", } enum Dependencies { From 00bfe9ce6ed3d21b39a40309974dda5c19dc6fb0 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Thu, 18 Sep 2025 20:41:06 +0200 Subject: [PATCH 2/2] tweak genmc error report note --- src/tools/miri/src/concurrency/genmc/run.rs | 10 +++++----- .../tests/genmc/fail/data_race/mpu2_rels_rlx.stderr | 3 ++- .../genmc/fail/data_race/weak_orderings.rel_rlx.stderr | 3 ++- .../genmc/fail/data_race/weak_orderings.rlx_acq.stderr | 3 ++- .../genmc/fail/data_race/weak_orderings.rlx_rlx.stderr | 3 ++- src/tools/miri/tests/genmc/fail/loom/buggy_inc.stderr | 3 ++- .../tests/genmc/fail/loom/store_buffering.genmc.stderr | 3 ++- .../tests/genmc/fail/simple/2w2w_weak.relaxed4.stderr | 3 ++- .../tests/genmc/fail/simple/2w2w_weak.release4.stderr | 3 ++- .../tests/genmc/fail/simple/2w2w_weak.sc3_rel1.stderr | 3 ++- 10 files changed, 23 insertions(+), 14 deletions(-) diff --git a/src/tools/miri/src/concurrency/genmc/run.rs b/src/tools/miri/src/concurrency/genmc/run.rs index bc2f5f7b79ec..33c5b6b0a005 100644 --- a/src/tools/miri/src/concurrency/genmc/run.rs +++ b/src/tools/miri/src/concurrency/genmc/run.rs @@ -70,7 +70,7 @@ fn run_genmc_mode_impl<'tcx>( // Execute the program until completion to get the return value, or return if an error happens: let Some(return_code) = eval_entry(genmc_ctx.clone()) else { - genmc_ctx.print_genmc_output(genmc_config); + genmc_ctx.print_genmc_output(genmc_config, tcx); return None; }; @@ -97,7 +97,7 @@ fn run_genmc_mode_impl<'tcx>( // Since we don't have any span information for the error at this point, // we just print GenMC's error string, and the full GenMC output if requested. eprintln!("(GenMC) Error detected: {error}"); - genmc_ctx.print_genmc_output(genmc_config); + genmc_ctx.print_genmc_output(genmc_config, tcx); return None; } } @@ -110,13 +110,13 @@ impl GenmcCtx { /// /// This message can be very verbose and is likely not useful for the average user. /// This function should be called *after* Miri has printed all of its output. - fn print_genmc_output(&self, genmc_config: &GenmcConfig) { + fn print_genmc_output(&self, genmc_config: &GenmcConfig, tcx: TyCtxt<'_>) { if genmc_config.print_genmc_output { eprintln!("GenMC error report:"); eprintln!("{}", self.get_result_message()); } else { - eprintln!( - "(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.)" + tcx.dcx().note( + "add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report" ); } } diff --git a/src/tools/miri/tests/genmc/fail/data_race/mpu2_rels_rlx.stderr b/src/tools/miri/tests/genmc/fail/data_race/mpu2_rels_rlx.stderr index 00de74009d9b..1ffb55f22e6e 100644 --- a/src/tools/miri/tests/genmc/fail/data_race/mpu2_rels_rlx.stderr +++ b/src/tools/miri/tests/genmc/fail/data_race/mpu2_rels_rlx.stderr @@ -16,6 +16,7 @@ note: inside `genmc::spawn_pthread_closure::thread_func::<{closure@tests/genmc/f LL | f(); | ^^^ -(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.) +note: add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report + error: aborting due to 1 previous error diff --git a/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rel_rlx.stderr b/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rel_rlx.stderr index 501957a90d3a..b0037c211c69 100644 --- a/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rel_rlx.stderr +++ b/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rel_rlx.stderr @@ -16,6 +16,7 @@ note: inside `genmc::spawn_pthread_closure::thread_func::<{closure@tests/genmc/f LL | f(); | ^^^ -(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.) +note: add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report + error: aborting due to 1 previous error diff --git a/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rlx_acq.stderr b/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rlx_acq.stderr index 501957a90d3a..b0037c211c69 100644 --- a/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rlx_acq.stderr +++ b/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rlx_acq.stderr @@ -16,6 +16,7 @@ note: inside `genmc::spawn_pthread_closure::thread_func::<{closure@tests/genmc/f LL | f(); | ^^^ -(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.) +note: add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report + error: aborting due to 1 previous error diff --git a/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rlx_rlx.stderr b/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rlx_rlx.stderr index 501957a90d3a..b0037c211c69 100644 --- a/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rlx_rlx.stderr +++ b/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rlx_rlx.stderr @@ -16,6 +16,7 @@ note: inside `genmc::spawn_pthread_closure::thread_func::<{closure@tests/genmc/f LL | f(); | ^^^ -(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.) +note: add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report + error: aborting due to 1 previous error diff --git a/src/tools/miri/tests/genmc/fail/loom/buggy_inc.stderr b/src/tools/miri/tests/genmc/fail/loom/buggy_inc.stderr index 9c3ba1d4c592..290cdf90a084 100644 --- a/src/tools/miri/tests/genmc/fail/loom/buggy_inc.stderr +++ b/src/tools/miri/tests/genmc/fail/loom/buggy_inc.stderr @@ -10,6 +10,7 @@ LL | std::process::abort(); note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace -(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.) +note: add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report + error: aborting due to 1 previous error diff --git a/src/tools/miri/tests/genmc/fail/loom/store_buffering.genmc.stderr b/src/tools/miri/tests/genmc/fail/loom/store_buffering.genmc.stderr index db92d0573fad..7742790e3330 100644 --- a/src/tools/miri/tests/genmc/fail/loom/store_buffering.genmc.stderr +++ b/src/tools/miri/tests/genmc/fail/loom/store_buffering.genmc.stderr @@ -10,6 +10,7 @@ LL | std::process::abort(); note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace -(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.) +note: add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report + error: aborting due to 1 previous error diff --git a/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.relaxed4.stderr b/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.relaxed4.stderr index 773f86a97596..80ac7206644c 100644 --- a/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.relaxed4.stderr +++ b/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.relaxed4.stderr @@ -10,6 +10,7 @@ LL | std::process::abort(); note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace -(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.) +note: add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report + error: aborting due to 1 previous error diff --git a/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.release4.stderr b/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.release4.stderr index 773f86a97596..80ac7206644c 100644 --- a/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.release4.stderr +++ b/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.release4.stderr @@ -10,6 +10,7 @@ LL | std::process::abort(); note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace -(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.) +note: add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report + error: aborting due to 1 previous error diff --git a/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.sc3_rel1.stderr b/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.sc3_rel1.stderr index 773f86a97596..80ac7206644c 100644 --- a/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.sc3_rel1.stderr +++ b/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.sc3_rel1.stderr @@ -10,6 +10,7 @@ LL | std::process::abort(); note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace -(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.) +note: add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report + error: aborting due to 1 previous error