Merge pull request #4609 from RalfJung/genmc-targets

genmc: bail out for non-64bit-little-endian targets

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<GenmcCtx>| {
@@ -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"

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<GenmcConfig>,
         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");

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(())
     }