Implement building GenMC C++ code

Cargo.toml

@@ -47,6 +47,9 @@ ipc-channel = "0.19.0"
 serde = { version = "1.0.219", features = ["derive"] }
 capstone = "0.13"
 
+[target.'cfg(all(any(target_os = "linux", target_os = "macos"), target_pointer_width = "64"))'.dependencies]
+genmc-sys = { path = "./genmc-sys/", version = "0.11.0", optional = true }
+
 [dev-dependencies]
 ui_test = "0.29.1"
 colored = "2"
@@ -65,7 +68,7 @@ harness = false
 
 [features]
 default = ["stack-cache"]
-genmc = []
+genmc = ["dep:genmc-sys"]
 stack-cache = []
 stack-cache-consistency-check = ["stack-cache"]
 tracing = ["serde_json"]

genmc-sys/.gitignore

@@ -0,0 +1,3 @@
+genmc/
+genmc-*/
+downloaded/

genmc-sys/Cargo.toml

@@ -0,0 +1,18 @@
+[package]
+name = "genmc-sys"
+version = "0.11.0" # NOTE: should match the GenMC version
+edition = "2024"
+
+[features]
+default = ["download_genmc"]
+# If downloading is disabled, a local GenMC repo must be available in the "./genmc" path.
+download_genmc = ["dep:git2"]
+
+[dependencies]
+# cxx = { version = "1.0.160", features = ["c++20"] }
+cxx = { git = "https://github.com/Patrick-6/cxx.git", rev = "e16e210970fe1a5d17e5f9651f2f1d83590586eb" }
+
+[build-dependencies]
+cmake = "0.1.54"
+git2 = { version = "0.20.2", optional = true }
+cxx-build = { version = "1.0.160", features = ["parallel"] }

genmc-sys/build.rs

@@ -0,0 +1,183 @@
+use std::path::{Path, PathBuf};
+use std::str::FromStr;
+
+const GENMC_LOCAL_PATH_STR: &str = "./genmc/";
+
+/// Name of the library of the GenMC model checker.
+const GENMC_MODEL_CHECKER: &str = "model_checker";
+
+const RUST_CXX_BRIDGE_FILE_PATH: &str = "src/lib.rs";
+
+// FIXME(GenMC, build): decide whether to keep debug enabled or not (without this: calling BUG() ==> UB)
+const ENABLE_GENMC_DEBUG: bool = true;
+
+#[cfg(feature = "download_genmc")]
+mod downloading {
+    use std::path::PathBuf;
+    use std::str::FromStr;
+
+    use git2::{Oid, Repository};
+
+    use super::GENMC_LOCAL_PATH_STR;
+
+    pub(crate) const GENMC_GITHUB_URL: &str = "https://github.com/Patrick-6/genmc.git";
+    pub(crate) const GENMC_COMMIT: &str = "bd4496acaf0994b2515f58f75d21ad8dd15f6603";
+    pub(crate) const GENMC_DOWNLOAD_PATH_STR: &str = "./downloaded/genmc/";
+
+    pub(crate) fn download_genmc() -> PathBuf {
+        let Ok(genmc_download_path) = PathBuf::from_str(GENMC_DOWNLOAD_PATH_STR);
+
+        let repo = Repository::open(&genmc_download_path).unwrap_or_else(|open_err| {
+            match Repository::clone(GENMC_GITHUB_URL, &genmc_download_path) {
+                Ok(repo) => {
+                    repo
+                }
+                Err(clone_err) => {
+                    println!("cargo::error=Cannot open GenMC repo at path '{GENMC_LOCAL_PATH_STR}': {open_err:?}");
+                    println!("cargo::error=Cannot clone GenMC repo from '{GENMC_GITHUB_URL}': {clone_err:?}");
+                    std::process::exit(1);
+                }
+            }
+        });
+
+        // Check if there are any updates:
+        let commit = if let Ok(oid) = Oid::from_str(GENMC_COMMIT)
+            && let Ok(commit) = repo.find_commit(oid)
+        {
+            commit
+        } else {
+            match repo.find_remote("origin") {
+                Ok(mut remote) =>
+                    match remote.fetch(&[GENMC_COMMIT], None, None) {
+                        Ok(_) =>
+                            println!(
+                                "cargo::warning=Successfully fetched commit '{GENMC_COMMIT:?}'"
+                            ),
+                        Err(e) => panic!("Failed to fetch from remote: {e}"),
+                    },
+                Err(e) => println!("cargo::warning=Could not find remote 'origin': {e}"),
+            }
+            let oid = Oid::from_str(GENMC_COMMIT).unwrap();
+            repo.find_commit(oid).unwrap()
+        };
+
+        // Set the repo to the correct branch:
+        checkout_commit(&repo, GENMC_COMMIT);
+
+        let head_commit = repo.head().unwrap().peel_to_commit().unwrap();
+        assert_eq!(head_commit.id(), commit.id());
+        println!("cargo::warning=Successfully set checked out commit {head_commit:?}");
+
+        genmc_download_path
+    }
+
+    fn checkout_commit(repo: &Repository, refname: &str) {
+        let (object, reference) = repo.revparse_ext(refname).expect("Object not found");
+
+        repo.checkout_tree(&object, None).expect("Failed to checkout");
+
+        match reference {
+            // `gref` is an actual reference like branches or tags.
+            Some(gref) => repo.set_head(gref.name().unwrap()),
+            // This is a commit, not a reference.
+            None => repo.set_head_detached(object.id()),
+        }
+        .expect("Failed to set HEAD");
+    }
+}
+
+/// Build the Rust-C++ interop library with cxx.rs
+fn build_cxx_bridge(genmc_path: &Path) {
+    // Paths for include directories:
+    let model_checker_include_path = genmc_path.join(GENMC_MODEL_CHECKER).join("include");
+    let genmc_common_include_path = genmc_path.join("common").join("include");
+
+    let mut bridge = cxx_build::bridge("src/lib.rs");
+
+    // FIXME(GenMC, build): make sure GenMC uses the same compiler / settings as the cxx_bridge
+    // FIXME(GenMC, build): can we use c++23? Does CXX support that? Does rustc CI support that?
+    bridge
+        .opt_level(2)
+        .debug(true) // Same settings that GenMC uses ("-O2 -g")
+        .warnings(false) // NOTE: enabling this produces a lot of warnings.
+        .std("c++20")
+        .include(genmc_common_include_path)
+        .include(model_checker_include_path)
+        .include("./src_cpp")
+        .define("PACKAGE_BUGREPORT", "\"FIXME(GenMC) determine what to do with this!!\"") // FIXME(GenMC): HACK to get stuff to compile (this is normally defined by cmake)
+        .file("./src_cpp/MiriInterface.hpp")
+        .file("./src_cpp/MiriInterface.cpp");
+
+    // NOTE: It is very important to ensure that this and similar flags are set/unset both here and
+    // for the cmake build below, otherwise, certain structs/classes can have different
+    // sizes and field offsets in the cxx bridge library compared to the model_checker library.
+    // This will lead to data corruption in these fields, which can be hard to debug (fields change values randomly).
+    if ENABLE_GENMC_DEBUG {
+        bridge.define("ENABLE_GENMC_DEBUG", "1");
+    }
+
+    bridge.compile("genmc_interop");
+
+    // Link the Rust-C++ interface library generated by cxx_build:
+    println!("cargo::rustc-link-lib=static=genmc_interop");
+}
+
+/// Build the GenMC model checker library.
+/// Returns the path
+fn build_genmc_model_checker(genmc_path: &Path) {
+    let cmakelists_path = genmc_path.join("CMakeLists.txt");
+
+    let mut config = cmake::Config::new(cmakelists_path);
+    config.profile("RelWithDebInfo"); // FIXME(GenMC,cmake): decide on profile to use
+    if ENABLE_GENMC_DEBUG {
+        config.define("GENMC_DEBUG", "ON");
+    }
+
+    // FIXME(GenMC,HACK): Required for unknown reasons on older cmake (version 3.22.1, works without this with version 3.31.6)
+    //              Without this, the files are written into the source directory by the cmake configure step, and then
+    //              the build step cannot find these files, because it correctly tries using the `target` directory.
+    let out_dir = std::env::var("OUT_DIR").unwrap();
+    config.configure_arg(format!("-B {out_dir}/build"));
+
+    // Enable only the components of GenMC that we need:
+    config.define("BUILD_LLI", "OFF");
+    config.define("BUILD_INSTRUMENTATION", "OFF");
+    config.define("BUILD_MODEL_CHECKER", "ON");
+
+    config.build_target(GENMC_MODEL_CHECKER);
+    let dst = config.build();
+
+    println!("cargo::rustc-link-search=native={}/build/{GENMC_MODEL_CHECKER}", dst.display());
+    println!("cargo::rustc-link-lib=static={GENMC_MODEL_CHECKER}");
+}
+
+fn main() {
+    // Select between local GenMC repo, or downloading GenMC from a specific commit.
+    let Ok(genmc_local_path) = PathBuf::from_str(GENMC_LOCAL_PATH_STR);
+    let genmc_path = if genmc_local_path.exists() {
+        genmc_local_path
+    } else {
+        #[cfg(not(feature = "download_genmc"))]
+        panic!(
+            "GenMC not found in path '{GENMC_LOCAL_PATH_STR}', and downloading GenMC is disabled."
+        );
+
+        #[cfg(feature = "download_genmc")]
+        downloading::download_genmc()
+    };
+
+    // FIXME(GenMC, performance): these *should* be able to build in parallel:
+    // Build all required components:
+    build_cxx_bridge(&genmc_path);
+    build_genmc_model_checker(&genmc_path);
+
+    // FIXME(GenMC, build): Cloning the GenMC repo triggers a rebuild on the next build (since the directory changed during the first build)
+
+    // Only rebuild if anything changes:
+    println!("cargo::rerun-if-changed={RUST_CXX_BRIDGE_FILE_PATH}");
+    println!("cargo::rerun-if-changed=./src_cpp");
+    let genmc_src_paths = [genmc_path.join("model_checker"), genmc_path.join("common")];
+    for genmc_src_path in genmc_src_paths {
+        println!("cargo::rerun-if-changed={}", genmc_src_path.display());
+    }
+}

genmc-sys/src/lib.rs

@@ -0,0 +1,30 @@
+pub use self::ffi::*;
+
+impl Default for GenmcParams {
+    fn default() -> Self {
+        Self {
+            print_random_schedule_seed: false,
+            do_symmetry_reduction: false,
+            // FIXME(GenMC): Add defaults for remaining parameters
+        }
+    }
+}
+
+#[cxx::bridge]
+mod ffi {
+    /// 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++)
+    #[derive(Clone, Debug)]
+    struct GenmcParams {
+        pub print_random_schedule_seed: bool,
+        pub do_symmetry_reduction: bool,
+        // FIXME(GenMC): Add remaining parameters.
+    }
+    unsafe extern "C++" {
+        include!("MiriInterface.hpp");
+
+        type MiriGenMCShim;
+
+        fn createGenmcHandle(config: &GenmcParams) -> UniquePtr<MiriGenMCShim>;
+    }
+}

genmc-sys/src_cpp/MiriInterface.cpp

@@ -0,0 +1,49 @@
+#include "MiriInterface.hpp"
+
+#include "genmc-sys/src/lib.rs.h"
+
+auto MiriGenMCShim::createHandle(const GenmcParams &config)
+	-> std::unique_ptr<MiriGenMCShim>
+{
+	auto vConf = std::make_shared<VerificationConfig>();
+
+	// Miri needs all threads to be replayed, even fully completed ones.
+	vConf->replayCompletedThreads = true;
+
+	// We only support the RC11 memory model for Rust.
+	vConf->model = ModelType::RC11;
+
+	vConf->printRandomScheduleSeed = config.print_random_schedule_seed;
+
+	// FIXME(GenMC): disable any options we don't support currently:
+	vConf->ipr = false;
+	vConf->disableBAM = true;
+	vConf->instructionCaching = false;
+
+	ERROR_ON(config.do_symmetry_reduction, "Symmetry reduction is currently unsupported in GenMC mode.");
+	vConf->symmetryReduction = config.do_symmetry_reduction;
+
+	// FIXME(GenMC): Should there be a way to change this option from Miri?
+	vConf->schedulePolicy = SchedulePolicy::WF;
+
+	// FIXME(GenMC): implement estimation mode:
+	vConf->estimate = false;
+	vConf->estimationMax = 1000;
+	const auto mode = vConf->estimate ? 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 at atomic operations, which is required with Miri.
+	// This happens because Miri can generate multiple GenMC events for a single MIR terminator. Without this option,
+	// the scheduler might incorrectly schedule an atomic MIR terminator because the first event it creates is a non-atomic (e.g., `StorageLive`).
+	vConf->disableRaceDetection = false;
+
+	// Miri can already check for unfreed memory. Also, GenMC cannot distinguish between memory
+	// that is allowed to leak and memory that is not.
+	vConf->warnUnfreedMemory = false;
+
+	checkVerificationConfigOptions(*vConf);
+
+	auto driver = std::make_unique<MiriGenMCShim>(std::move(vConf), mode);
+	return driver;
+}

genmc-sys/src_cpp/MiriInterface.hpp

@@ -0,0 +1,42 @@
+#ifndef GENMC_MIRI_INTERFACE_HPP
+#define GENMC_MIRI_INTERFACE_HPP
+
+#include "rust/cxx.h"
+
+#include "Verification/GenMCDriver.hpp"
+#include "Verification/VerificationConfig.hpp"
+
+#include <iostream>
+
+/**** Types available to Miri ****/
+
+// Config struct defined on the Rust side and translated to C++ by cxx.rs:
+struct GenmcParams;
+
+struct MiriGenMCShim : private GenMCDriver
+{
+
+public:
+	MiriGenMCShim(std::shared_ptr<const VerificationConfig> vConf, Mode mode /* = VerificationMode{} */)
+		: GenMCDriver(std::move(vConf), nullptr, mode)
+	{
+		std::cerr << "C++: GenMC handle created!" << std::endl;
+	}
+
+	virtual ~MiriGenMCShim()
+	{
+		std::cerr << "C++: GenMC handle destroyed!" << std::endl;
+	}
+
+	static std::unique_ptr<MiriGenMCShim> createHandle(const GenmcParams &config);
+};
+
+/**** Functions available to Miri ****/
+
+// NOTE: CXX doesn't support exposing static methods to Rust currently, so we expose this function instead.
+static inline auto createGenmcHandle(const GenmcParams &config) -> std::unique_ptr<MiriGenMCShim>
+{
+	return MiriGenMCShim::createHandle(config);
+}
+
+#endif /* GENMC_MIRI_INTERFACE_HPP */

src/bin/miri.rs

@@ -598,7 +598,11 @@ 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") {
-            // FIXME(GenMC): Currently, GenMC mode is incompatible with aliasing model checking.
+            if !miri_config.genmc_mode {
+                miri_config.genmc_mode = true;
+                // FIXME(GenMC): Currently, GenMC mode is incompatible with aliasing model checking.
+                miri_config.borrow_tracker = None;
+            }
             miri_config.borrow_tracker = None;
             GenmcConfig::parse_arg(&mut genmc_config, trimmed_arg);
         } else if let Some(param) = arg.strip_prefix("-Zmiri-env-forward=") {

src/concurrency/genmc/config.rs

@@ -1,19 +1,30 @@
-use crate::MiriConfig;
+use super::GenmcParams;
 
+/// Configuration for GenMC mode.
+/// The `params` field is shared with the C++ side.
+/// The remaining options are kept on the Rust side.
 #[derive(Debug, Default, Clone)]
 pub struct GenmcConfig {
-    // TODO: add fields
+    pub(super) params: GenmcParams,
+    do_estimation: bool,
+    // FIXME(GenMC): add remaining options.
 }
 
 impl GenmcConfig {
     /// Function for parsing command line options for GenMC mode.
+    ///
     /// All GenMC arguments start with the string "-Zmiri-genmc".
+    /// Passing any GenMC argument will enable GenMC mode.
     ///
-    /// `trimmed_arg` should be the argument to be parsed, with the suffix "-Zmiri-genmc" removed
+    /// `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) {
         if genmc_config.is_none() {
             *genmc_config = Some(Default::default());
         }
-        todo!("implement parsing of GenMC options")
+        if trimmed_arg.is_empty() {
+            return; // this corresponds to "-Zmiri-genmc"
+        }
+        // FIXME(GenMC): implement remaining parameters.
+        todo!();
     }
 }