Implement basic support for running Miri with GenMC.

- Implement memory allocation compatible with GenMC.
  - Extract address generator struct from Miri's allocator.
- Support thread creation and joining.
- Support atomic load and store.
- Support scheduling through GenMC.
- Add tests for GenMC mode.
- Add clang-format file for C++ code in Miri.
- Update genmc-sys crate license to MIT/Apache to match GenMC dependency.
- Add documentation for GenMC mode.

Note: this commit depends on changes to GenMC not yet upstreamed to its official repository.

Co-authored-by: Ralf Jung <[email protected]>

Author: Patrick-6

Cargo.lock

@@ -70,7 +70,7 @@ harness = false
 
 [features]
 default = ["stack-cache", "native-lib"]
-genmc = ["dep:genmc-sys"] # this enables a GPL dependency!
+genmc = ["dep:genmc-sys"]
 stack-cache = []
 stack-cache-consistency-check = ["stack-cache"]
 tracing = ["serde_json"]

Cargo.toml

@@ -9,9 +9,7 @@ Miri-GenMC integrates that model checker into Miri.
 
 ## Usage
 
-**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):
+For testing/developing Miri-GenMC:
 - clone the Miri repo.
 - build Miri-GenMC with `./miri build --features=genmc`.
 - OR: install Miri-GenMC in the current system with `./miri install --features=genmc`
@@ -21,6 +19,21 @@ Basic usage:
 MIRIFLAGS="-Zmiri-genmc" cargo miri run
 ```
 
+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-log=LOG_LEVEL`: Change the log level for GenMC. Default: `warning`.
+  - `quiet`:    Disable logging.
+  - `error`:    Print errors.
+  - `warning`:  Print errors and warnings.
+  - `tip`:      Print errors, warnings and tips.
+  - If Miri is built with debug assertions, there are additional log levels available (downgraded to `tip` without debug assertions):
+    - `debug1`:   Print revisits considered by GenMC.
+    - `debug2`:   Print the execution graph after every memory access.
+    - `debug3`:   Print reads-from values considered by GenMC.
+
 <!-- FIXME(genmc): explain options. -->
 
 <!-- FIXME(genmc): explain Miri-GenMC specific functions. -->
@@ -57,6 +70,15 @@ The process for obtaining them is as follows:
   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.
 
+### Formatting the C++ code
+
+For formatting the C++ code we provide a `.clang-format` file in the `genmc-sys` directory.
+With `clang-format` installed, run this command to format the c++ files (replace the `-i` with `--dry-run` to just see the changes.):
+```
+find ./genmc-sys/cpp/ -name "*.cpp" -o -name "*.hpp" | xargs clang-format --style=file:"./genmc-sys/.clang-format" -i
+```
+NOTE: this is currently not done automatically on pull requests to Miri.
+
 <!-- FIXME(genmc): explain how submitting code to GenMC should be handled. -->
 
 <!-- FIXME(genmc): explain development. -->

doc/genmc.md

@@ -0,0 +1,52 @@
+# .clang-format
+
+BasedOnStyle: LLVM
+Standard: c++20
+
+ColumnLimit: 100
+AllowShortFunctionsOnASingleLine: Empty
+AllowShortIfStatementsOnASingleLine: false
+AllowShortLoopsOnASingleLine: false
+AllowShortBlocksOnASingleLine: Empty
+BreakBeforeBraces: Attach
+
+BinPackArguments: false
+BinPackParameters: false
+AllowAllParametersOfDeclarationOnNextLine: false
+AlwaysBreakAfterReturnType: None
+
+# Force parameters to break and align
+AlignAfterOpenBracket: BlockIndent
+AllowAllArgumentsOnNextLine: false
+
+# Spacing around braces and parentheses
+SpaceBeforeCtorInitializerColon: true
+SpaceBeforeInheritanceColon: true
+SpaceInEmptyBlock: false
+SpacesInContainerLiterals: true
+SpacesInParensOptions:
+  InCStyleCasts: false
+  InConditionalStatements: false
+  InEmptyParentheses: false
+  Other: false
+SpacesInSquareBrackets: false
+
+# Brace spacing for initializers
+Cpp11BracedListStyle: false
+SpaceBeforeCpp11BracedList: true
+
+# Import grouping: group standard, external, and project includes.
+IncludeBlocks: Regroup
+SortIncludes: true
+
+# Granularity: sort includes per module/file.
+IncludeIsMainRegex: '([-_](test|unittest))?$'
+
+# Miscellaneous
+SpaceAfterCStyleCast: true
+SpaceBeforeParens: ControlStatements
+PointerAlignment: Left
+IndentCaseLabels: true
+IndentWidth: 4
+TabWidth: 4
+UseTab: Never

genmc-sys/.clang-format

@@ -1,17 +1,15 @@
 [package]
 authors = ["Miri Team"]
-# The parts in this repo are MIT OR Apache-2.0, but we are linking in
-# code from https://github.com/MPI-SWS/genmc which is GPL-3.0-or-later.
-license = "(MIT OR Apache-2.0) AND GPL-3.0-or-later"
+license = "MIT OR Apache-2.0"
 name = "genmc-sys"
 version = "0.1.0"
 edition = "2024"
 
 [dependencies]
-cxx = { version = "1.0.160", features = ["c++20"] }
+cxx = { version = "1.0.173", features = ["c++20"] }
 
 [build-dependencies]
 cc = "1.2.30"
 cmake = "0.1.54"
 git2 = { version = "0.20.2", default-features = false, features = ["https"] }
-cxx-build = { version = "1.0.160", features = ["parallel"] }
+cxx-build = { version = "1.0.173", features = ["parallel"] }

genmc-sys/Cargo.toml

@@ -26,9 +26,9 @@ mod downloading {
     use super::GENMC_DOWNLOAD_PATH;
 
     /// The GenMC repository the we get our commit from.
-    pub(crate) const GENMC_GITHUB_URL: &str = "https://github.com/MPI-SWS/genmc.git";
+    pub(crate) const GENMC_GITHUB_URL: &str = "https://gitlab.inf.ethz.ch/public-plf/genmc.git";
     /// The GenMC commit we depend on. It must be available on the specified GenMC repository.
-    pub(crate) const GENMC_COMMIT: &str = "3438dd2c1202cd4a47ed7881d099abf23e4167ab";
+    pub(crate) const GENMC_COMMIT: &str = "af9cc9ccd5d412b16defc35dbf36571c63a19c76";
 
     pub(crate) fn download_genmc() -> PathBuf {
         let Ok(genmc_download_path) = PathBuf::from_str(GENMC_DOWNLOAD_PATH);
@@ -176,6 +176,11 @@ fn link_to_llvm(config_file: &Path) -> (String, String) {
 
 /// Build the GenMC model checker library and the Rust-C++ interop library with cxx.rs
 fn compile_cpp_dependencies(genmc_path: &Path) {
+    // Give each step a separate build directory to prevent interference.
+    let out_dir = PathBuf::from(std::env::var("OUT_DIR").as_deref().unwrap());
+    let genmc_build_dir = out_dir.join("genmc");
+    let interface_build_dir = out_dir.join("miri_genmc");
+
     // Part 1:
     // Compile the GenMC library using cmake.
 
@@ -186,8 +191,11 @@ fn compile_cpp_dependencies(genmc_path: &Path) {
     let enable_genmc_debug = matches!(std::env::var("PROFILE").as_deref().unwrap(), "debug");
 
     let mut config = cmake::Config::new(cmakelists_path);
-    config.profile(GENMC_CMAKE_PROFILE);
-    config.define("GENMC_DEBUG", if enable_genmc_debug { "ON" } else { "OFF" });
+    config
+        .always_configure(false) // We don't need to reconfigure on subsequent compilation runs.
+        .out_dir(genmc_build_dir)
+        .profile(GENMC_CMAKE_PROFILE)
+        .define("GENMC_DEBUG", if enable_genmc_debug { "ON" } else { "OFF" });
 
     // The actual compilation happens here:
     let genmc_install_dir = config.build();
@@ -210,6 +218,13 @@ fn compile_cpp_dependencies(genmc_path: &Path) {
     // These definitions are parsed into a cmake list and then printed to the config.h file, so they are ';' separated.
     let definitions = llvm_definitions.split(";");
 
+    let cpp_files = [
+        "./cpp/src/MiriInterface/EventHandling.cpp",
+        "./cpp/src/MiriInterface/Exploration.cpp",
+        "./cpp/src/MiriInterface/Setup.cpp",
+        "./cpp/src/MiriInterface/ThreadManagement.cpp",
+    ];
+
     let mut bridge = cxx_build::bridge("src/lib.rs");
     // FIXME(genmc,cmake): Remove once the GenMC debug setting is available in the config.h file.
     if enable_genmc_debug {
@@ -223,32 +238,27 @@ fn compile_cpp_dependencies(genmc_path: &Path) {
         .std("c++23")
         .include(genmc_include_dir)
         .include(llvm_include_dirs)
-        .include("./src_cpp")
-        .file("./src_cpp/MiriInterface.hpp")
-        .file("./src_cpp/MiriInterface.cpp")
+        .include("./cpp/include")
+        .files(&cpp_files)
+        .out_dir(interface_build_dir)
         .compile("genmc_interop");
 
     // Link the Rust-C++ interface library generated by cxx_build:
     println!("cargo::rustc-link-lib=static=genmc_interop");
 }
 
 fn main() {
-    // Make sure we don't accidentally distribute a binary with GPL code.
-    if option_env!("RUSTC_STAGE").is_some() {
-        panic!(
-            "genmc should not be enabled in the rustc workspace since it includes a GPL dependency"
-        );
-    }
-
     // Select which path to use for the GenMC repo:
-    let genmc_path = if let Ok(genmc_src_path) = std::env::var("GENMC_SRC_PATH") {
+    let genmc_path = if let Some(genmc_src_path) = option_env!("GENMC_SRC_PATH") {
         let genmc_src_path =
             PathBuf::from_str(&genmc_src_path).expect("GENMC_SRC_PATH should contain a valid path");
         assert!(
             genmc_src_path.exists(),
             "GENMC_SRC_PATH={} does not exist!",
             genmc_src_path.display()
         );
+        // Rebuild files in the given path change.
+        println!("cargo::rerun-if-changed={}", genmc_src_path.display());
         genmc_src_path
     } else {
         downloading::download_genmc()
@@ -263,5 +273,5 @@ fn main() {
     // 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-changed=./cpp");
 }