various minor adjustments

7 files changed, 49 insertions, 79 deletions

diff --git a/src/tools/miri/doc/genmc.md b/src/tools/miri/doc/genmc.md
index 4839919557e..5aabe90b5da 100644
--- a/src/tools/miri/doc/genmc.md
+++ b/src/tools/miri/doc/genmc.md
@@ -1,5 +1,7 @@
 # **(WIP)** Documentation for Miri-GenMC
+
 [GenMC](https://github.com/MPI-SWS/genmc) is a stateless model checker for exploring concurrent executions of a program.
+Miri-GenMC integrates that model checker into Miri.
 
 **NOTE: Currently, no actual GenMC functionality is part of Miri, this is still WIP.**
 
@@ -7,9 +9,7 @@
 
 ## Usage
 
-**IMPORTANT: The license of GenMC and thus the `genmc-sys` crate in the Miri repo is currently "GPL-3.0-or-later", which is NOT compatible with Miri's "MIT OR Apache" license.**
-
-**IMPORTANT: There should be no distribution of Miri-GenMC until all licensing questions are clarified (the `genmc` feature of Miri is OFF-BY-DEFAULT and should be OFF for all Miri releases).**
+**IMPORTANT: The license of GenMC and thus the `genmc-sys` crate in the Miri repo is currently "GPL-3.0-or-later", so a binary produced with the `genmc` feature is subject to the requirements of the GPL. As long as that remains the case, the `genmc` feature of Miri is OFF-BY-DEFAULT and must be OFF for all Miri releases.**
 
 For testing/developing Miri-GenMC (while keeping in mind the licensing issues):
 - clone the Miri repo.
@@ -35,44 +35,28 @@ Some or all of these limitations might get removed in the future:
 
 - Borrow tracking is currently incompatible (stacked/tree borrows).
 - Only Linux is supported for now.
-- No 32-bit platform support.
-- No cross-platform interpretation.
+- No support for 32-bit or big-endian targets.
+- No cross-target interpretation.
 
 <!-- FIXME(genmc): document remaining limitations -->
 
 ## Development
 
 GenMC is written in C++, which complicates development a bit.
-For Rust-C++ interop, Miri uses [CXX.rs](https://cxx.rs/), and all handling of C++ code is contained in the `genmc-sys` crate (located in the Miri repository root directory: `miri/genmc-sys/`).
-
-Building GenMC requires a compiler with C++23 support.
-<!-- FIXME(genmc,llvm): remove once LLVM dependency is no longer required. -->
-Currently, building GenMC also requires linking to LLVM, which needs to be installed manually.
-
-The actual code for GenMC is not contained in the Miri repo itself, but in a [separate GenMC repo](https://github.com/MPI-SWS/genmc) (with different maintainers).
-Note that this repo is just a mirror repo.
-<!-- FIXME(genmc): define how submitting code to GenMC should be handled. -->
+The prerequisites for building Miri-GenMC are:
+- A compiler with C++23 support.
+- LLVM developments headers and clang.
+  <!-- FIXME(genmc,llvm): remove once LLVM dependency is no longer required. -->
+
+The actual code for GenMC is not contained in the Miri repo itself, but in a [separate GenMC repo](https://github.com/MPI-SWS/genmc) (with its own maintainers).
+These sources need to be available to build Miri-GenMC.
+The process for obtaining them is as follows:
+- By default, a fixed commit of GenMC is downloaded to `genmc-sys/genmc-src` and built automatically.
+  (The commit is determined by `GENMC_COMMIT` in `genmc-sys/build.rs`.)
+- If you want to overwrite that, set the `GENMC_SRC_PATH` environment variable to a path that contains the GenMC sources.
+  If you place this directory inside the Miri folder, it is recommended to call it `genmc-src` as that tells `./miri fmt` to avoid
+  formatting the Rust files inside that folder.
+
+<!-- FIXME(genmc): explain how submitting code to GenMC should be handled. -->
 
 <!-- FIXME(genmc): explain development. -->
-
-### Building the GenMC Library
-The build script in the `genmc-sys` crate handles locating, downloading, building and linking the GenMC library.
-
-To determine which GenMC repo path will be used, the following steps are taken:
-- If the env var `GENMC_SRC_PATH` is set, it's value is used as a path to a directory with a GenMC repo (e.g., `GENMC_SRC_PATH="path/to/miri/genmc-sys/genmc-sys-local"`).
-  - Note that this variable must be set wherever Miri is built, e.g., in the terminal, or in the Rust Analyzer settings.
-- If the path `genmc-sys/genmc-src/genmc` exists, try to set the GenMC repo there to the commit we need.
-- If the downloaded repo doesn't exist or is missing the commit, the build script will fetch the commit over the network.
-  - Note that the build script will *not* access the network if any of the steps previous steps succeeds.
-
-Once we get the path to the repo, the compilation proceeds in two steps:
-- Compile GenMC into a library (using cmake).
-- Compile the cxx.rs bridge to connect the library to the Rust code.
-The first step is where all build settings are made, the relevant ones are then stored in a `config.h` file that can be included in the second compilation step.
-
-#### Code Formatting
-Note that all directories with names starting with `genmc-src` are ignored by `./miri fmt` on purpose.
-GenMC also contains Rust files, but they should not be formatted with Miri's formatting rules.
-For working on Miri-GenMC locally, placing the GenMC repo into such a path (e.g., `miri/genmc-sys/genmc-src-local`) ensures that it is also exempt from formatting.
-
-<!-- FIXME(genmc): Decide on formatting rules for Miri-GenMC interface C++ code. -->
diff --git a/src/tools/miri/genmc-sys/build.rs b/src/tools/miri/genmc-sys/build.rs
index 16f7b69cc21..f20e0e8d525 100644
--- a/src/tools/miri/genmc-sys/build.rs
+++ b/src/tools/miri/genmc-sys/build.rs
@@ -6,7 +6,7 @@ use std::str::FromStr;
 
 /// Path where the downloaded GenMC repository will be stored (relative to the `genmc-sys` directory).
 /// Note that this directory is *not* cleaned up automatically by `cargo clean`.
-const GENMC_DOWNLOAD_PATH: &str = "./genmc-src/genmc/";
+const GENMC_DOWNLOAD_PATH: &str = "./genmc-src/";
 
 /// Name of the library of the GenMC model checker.
 const GENMC_MODEL_CHECKER: &str = "genmc_lib";
@@ -122,11 +122,9 @@ mod downloading {
             return;
         }
 
-        println!(
-            "HINT: For local development, set the environment variable 'GENMC_SRC_PATH' to the path of a GenMC repository.",
-        );
         panic!(
-            "Downloaded GenMC repository at path '{GENMC_DOWNLOAD_PATH}' has been modified. Please undo any changes made, or delete the '{GENMC_DOWNLOAD_PATH}' directory to have it downloaded again."
+            "Downloaded GenMC repository at path '{GENMC_DOWNLOAD_PATH}' has been modified. Please undo any changes made, or delete the '{GENMC_DOWNLOAD_PATH}' directory to have it downloaded again.\n\
+            HINT: For local development, set the environment variable 'GENMC_SRC_PATH' to the path of a GenMC repository."
         );
     }
 }
@@ -194,7 +192,7 @@ fn compile_cpp_dependencies(genmc_path: &Path) {
     // The actual compilation happens here:
     let genmc_install_dir = config.build();
 
-    // Add the model checker library to be linked and tell GenMC where to find it:
+    // Add the model checker library to be linked and tell rustc where to find it:
     let cmake_lib_dir = genmc_install_dir.join("lib").join("genmc");
     println!("cargo::rustc-link-search=native={}", cmake_lib_dir.display());
     println!("cargo::rustc-link-lib=static={GENMC_MODEL_CHECKER}");
@@ -260,9 +258,10 @@ fn main() {
     compile_cpp_dependencies(&genmc_path);
 
     // Only rebuild if anything changes:
-    // Note that we don't add the downloaded GenMC repo, since that should never be modified manually.
-    // Adding that path here would also trigger an unnecessary rebuild after the repo is cloned (since cargo detects that as a file modification).
+    // Note that we don't add the downloaded GenMC repo, since that should never be modified
+    // manually. Adding that path here would also trigger an unnecessary rebuild after the repo is
+    // cloned (since cargo detects that as a file modification).
     println!("cargo::rerun-if-changed={RUST_CXX_BRIDGE_FILE_PATH}");
+    println!("cargo::rerun-if-changed=./src");
     println!("cargo::rerun-if-changed=./src_cpp");
-    println!("cargo::rerun-if-env-changed=GENMC_SRC_PATH");
 }
diff --git a/src/tools/miri/src/bin/miri.rs b/src/tools/miri/src/bin/miri.rs
index 11d17994cc2..ae1b25f8857 100644
--- a/src/tools/miri/src/bin/miri.rs
+++ b/src/tools/miri/src/bin/miri.rs
@@ -596,7 +596,9 @@ fn main() {
         } else if arg == "-Zmiri-many-seeds-keep-going" {
             many_seeds_keep_going = true;
         } else if let Some(trimmed_arg) = arg.strip_prefix("-Zmiri-genmc") {
-            GenmcConfig::parse_arg(&mut miri_config.genmc_config, trimmed_arg);
+            if let Err(msg) = GenmcConfig::parse_arg(&mut miri_config.genmc_config, trimmed_arg) {
+                fatal_error!("{msg}");
+            }
         } else if let Some(param) = arg.strip_prefix("-Zmiri-env-forward=") {
             miri_config.forwarded_env_vars.push(param.to_owned());
         } else if let Some(param) = arg.strip_prefix("-Zmiri-env-set=") {
@@ -732,18 +734,15 @@ fn main() {
 
     // Validate settings for data race detection and GenMC mode.
     if miri_config.genmc_config.is_some() {
-        // FIXME(genmc): Add checks for currently supported platforms (64bit, target == host)
         if !miri_config.data_race_detector {
             fatal_error!("Cannot disable data race detection in GenMC mode (currently)");
         } else if !miri_config.weak_memory_emulation {
             fatal_error!("Cannot disable weak memory emulation in GenMC mode");
         }
-        // FIXME(genmc): Remove once GenMC mode is compatible with borrow tracking:
         if miri_config.borrow_tracker.is_some() {
             eprintln!(
-                "warning: Borrow tracking has been disabled, it is not (yet) supported in GenMC mode."
+                "warning: borrow tracking has been disabled, it is not (yet) supported in GenMC mode."
             );
-            eprintln!();
             miri_config.borrow_tracker = None;
         }
     } else if miri_config.weak_memory_emulation && !miri_config.data_race_detector {
diff --git a/src/tools/miri/src/concurrency/genmc/config.rs b/src/tools/miri/src/concurrency/genmc/config.rs
index 42591c9ac25..c56adab90fe 100644
--- a/src/tools/miri/src/concurrency/genmc/config.rs
+++ b/src/tools/miri/src/concurrency/genmc/config.rs
@@ -17,23 +17,17 @@ impl GenmcConfig {
     /// Passing any GenMC argument will enable GenMC mode.
     ///
     /// `trimmed_arg` should be the argument to be parsed, with the suffix "-Zmiri-genmc" removed.
-    pub fn parse_arg(genmc_config: &mut Option<GenmcConfig>, trimmed_arg: &str) {
-        // FIXME(genmc,macos): Add `target_os = "macos"` once `https://github.com/dtolnay/cxx/issues/1535` is fixed.
-        if !cfg!(all(
-            feature = "genmc",
-            any(target_os = "linux", target_os = "macos"),
-            target_pointer_width = "64",
-            target_endian = "little"
-        )) {
-            unimplemented!(
-                "GenMC mode is not supported on this platform, cannot handle argument: \"-Zmiri-genmc{trimmed_arg}\""
-            );
-        }
+    pub fn parse_arg(
+        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());
         }
         if trimmed_arg.is_empty() {
-            return; // this corresponds to "-Zmiri-genmc"
+            return Ok(()); // this corresponds to "-Zmiri-genmc"
         }
         // FIXME(GenMC): implement remaining parameters.
         todo!();
diff --git a/src/tools/miri/src/concurrency/genmc/dummy.rs b/src/tools/miri/src/concurrency/genmc/dummy.rs
index 7570f8ba362..79d27c4be15 100644
--- a/src/tools/miri/src/concurrency/genmc/dummy.rs
+++ b/src/tools/miri/src/concurrency/genmc/dummy.rs
@@ -227,21 +227,14 @@ impl VisitProvenance for GenmcCtx {
 }
 
 impl GenmcConfig {
-    pub fn parse_arg(_genmc_config: &mut Option<GenmcConfig>, trimmed_arg: &str) {
-        // FIXME(genmc,macos): Add `target_os = "macos"` once `https://github.com/dtolnay/cxx/issues/1535` is fixed.
-        if cfg!(all(
-            feature = "genmc",
-            any(target_os = "linux", target_os = "macos"),
-            target_pointer_width = "64",
-            target_endian = "little"
-        )) {
-            unimplemented!(
-                "GenMC is disabled, cannot handle argument: \"-Zmiri-genmc{trimmed_arg}\""
-            );
+    pub fn parse_arg(
+        _genmc_config: &mut Option<GenmcConfig>,
+        trimmed_arg: &str,
+    ) -> Result<(), String> {
+        if cfg!(feature = "genmc") {
+            Err(format!("GenMC is disabled in this build of Miri"))
         } else {
-            unimplemented!(
-                "GenMC mode is not supported on this platform, cannot handle argument: \"-Zmiri-genmc{trimmed_arg}\""
-            );
+            Err(format!("GenMC is not supported on this target"))
         }
     }
 
diff --git a/src/tools/miri/src/concurrency/thread.rs b/src/tools/miri/src/concurrency/thread.rs
index abfee0ee874..878afdf2517 100644
--- a/src/tools/miri/src/concurrency/thread.rs
+++ b/src/tools/miri/src/concurrency/thread.rs
@@ -677,6 +677,8 @@ trait EvalContextPrivExt<'tcx>: MiriInterpCxExt<'tcx> {
     fn run_on_stack_empty(&mut self) -> InterpResult<'tcx, Poll<()>> {
         let this = self.eval_context_mut();
         // Inform GenMC that a thread has finished all user code. GenMC needs to know this for scheduling.
+        // FIXME(GenMC): Thread-local destructors *are* user code, so this is odd. Also now that we
+        // support pre-main constructors, it can get called there as well.
         if let Some(genmc_ctx) = this.machine.data_race.as_genmc_ref() {
             let thread_id = this.active_thread();
             genmc_ctx.handle_thread_stack_empty(thread_id);
diff --git a/src/tools/miri/tests/genmc/pass/test_cxx_build.stderr b/src/tools/miri/tests/genmc/pass/test_cxx_build.stderr
index 3773dbeff3b..4b7aa824bd1 100644
--- a/src/tools/miri/tests/genmc/pass/test_cxx_build.stderr
+++ b/src/tools/miri/tests/genmc/pass/test_cxx_build.stderr
@@ -1,5 +1,4 @@
-warning: Borrow tracking has been disabled, it is not (yet) supported in GenMC mode.
-
+warning: borrow tracking has been disabled, it is not (yet) supported in GenMC mode.
 C++: GenMC handle created!
 Miri: GenMC handle creation successful!
 C++: GenMC handle destroyed!