From cfefa9bc883dda6fe09a5041e35b33d17aa0969e Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Mon, 29 Sep 2025 19:07:01 +0200 Subject: [PATCH] genmc: bail out for non-64bit-little-endian targets --- src/tools/miri/src/bin/miri.rs | 10 +++++----- src/tools/miri/src/concurrency/genmc/config.rs | 11 ++++++++--- src/tools/miri/src/concurrency/genmc/dummy.rs | 4 +++- 3 files changed, 16 insertions(+), 9 deletions(-) diff --git a/src/tools/miri/src/bin/miri.rs b/src/tools/miri/src/bin/miri.rs index 40ac5c3ff385..3c759521c6ca 100644 --- a/src/tools/miri/src/bin/miri.rs +++ b/src/tools/miri/src/bin/miri.rs @@ -188,6 +188,11 @@ impl rustc_driver::Callbacks for MiriCompilerCalls { // Run in GenMC mode if enabled. if config.genmc_config.is_some() { + // Validate GenMC settings. + if let Err(err) = GenmcConfig::validate(&mut config, tcx) { + fatal_error!("Invalid settings: {err}"); + } + // 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| { @@ -745,11 +750,6 @@ fn main() { let many_seeds = many_seeds.map(|seeds| ManySeedsConfig { seeds, keep_going: many_seeds_keep_going }); - // Validate settings for data race detection and GenMC mode. - if let Err(err) = GenmcConfig::validate_genmc_mode_settings(&mut miri_config) { - fatal_error!("Invalid settings: {err}"); - } - 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" diff --git a/src/tools/miri/src/concurrency/genmc/config.rs b/src/tools/miri/src/concurrency/genmc/config.rs index c7cfa6012b8d..a05cda46f3e7 100644 --- a/src/tools/miri/src/concurrency/genmc/config.rs +++ b/src/tools/miri/src/concurrency/genmc/config.rs @@ -1,4 +1,6 @@ use genmc_sys::LogLevel; +use rustc_abi::Endian; +use rustc_middle::ty::TyCtxt; use super::GenmcParams; use crate::{IsolatedOp, MiriConfig, RejectOpWith}; @@ -32,8 +34,6 @@ impl GenmcConfig { genmc_config: &mut Option, trimmed_arg: &str, ) -> Result<(), String> { - // FIXME(genmc): Ensure host == target somewhere. - if genmc_config.is_none() { *genmc_config = Some(Default::default()); } @@ -86,11 +86,16 @@ impl GenmcConfig { /// /// Unsupported configurations return an error. /// Adjusts Miri settings where required, printing a warnings if the change might be unexpected for the user. - pub fn validate_genmc_mode_settings(miri_config: &mut MiriConfig) -> Result<(), &'static str> { + pub fn validate(miri_config: &mut MiriConfig, tcx: TyCtxt<'_>) -> Result<(), &'static str> { let Some(genmc_config) = miri_config.genmc_config.as_mut() else { return Ok(()); }; + // Check for supported target. + if tcx.data_layout.endian != Endian::Little || tcx.data_layout.pointer_size().bits() != 64 { + return Err("GenMC only supports 64bit little-endian targets"); + } + // Check for disallowed configurations. if !miri_config.data_race_detector { return Err("Cannot disable data race detection in GenMC mode"); diff --git a/src/tools/miri/src/concurrency/genmc/dummy.rs b/src/tools/miri/src/concurrency/genmc/dummy.rs index e260af7c4a16..ef5b24d5abad 100644 --- a/src/tools/miri/src/concurrency/genmc/dummy.rs +++ b/src/tools/miri/src/concurrency/genmc/dummy.rs @@ -1,5 +1,6 @@ use rustc_abi::{Align, Size}; use rustc_const_eval::interpret::{AllocId, InterpCx, InterpResult}; +use rustc_middle::ty::TyCtxt; pub use self::intercept::EvalContextExt as GenmcEvalContextExt; pub use self::run::run_genmc_mode; @@ -230,8 +231,9 @@ impl GenmcConfig { } } - pub fn validate_genmc_mode_settings( + pub fn validate( _miri_config: &mut crate::MiriConfig, + _tcx: TyCtxt<'_>, ) -> Result<(), &'static str> { Ok(()) }