Add minimal functionality for using GenMC mode

genmc-sys/cpp/include/MiriInterface.hpp

@@ -39,7 +39,8 @@ using ThreadId = int;
 
 /// Set the log level for GenMC.
 ///
-/// # SAFETY
+/// # Safety
+///
 /// This function is not thread safe, since it writes to the global, mutable, non-atomic `logLevel`
 /// variable. Any GenMC function may read from `logLevel` unsynchronized.
 /// The safest way to use this function is to set the log level exactly once before first calling
@@ -55,7 +56,8 @@ struct MiriGenmcShim : private GenMCDriver {
 
     /// Create a new `MiriGenmcShim`, which wraps a `GenMCDriver`.
     ///
-    /// # SAFETY
+    /// # Safety
+    ///
     /// This function is marked as unsafe since the `logLevel` global variable is non-atomic.
     /// This function should not be called in an unsynchronized way with `set_log_level_raw`, since
     /// this function and any methods on the returned `MiriGenmcShim` may read the `logLevel`,

genmc-sys/src/lib.rs

@@ -1,12 +1,10 @@
 use std::str::FromStr;
+use std::sync::OnceLock;
 
 pub use cxx::UniquePtr;
 
 pub use self::ffi::*;
 
-mod genmc;
-pub use genmc::Genmc;
-
 /// Defined in "genmc/src/Support/SAddr.hpp".
 /// The first bit of all global addresses must be set to `1`.
 /// This means the mask, interpreted as an address, is the lower bound of where the global address space starts.
@@ -20,6 +18,33 @@ pub const GENMC_GLOBAL_ADDRESSES_MASK: u64 = 1 << 63;
 /// The main thread always has thread id 0.
 pub const GENMC_MAIN_THREAD_ID: i32 = 0;
 
+/// Changing GenMC's log level is not thread safe, so we limit it to only be set once to prevent any data races.
+/// This value will be initialized when the first `MiriGenmcShim` is created.
+static GENMC_LOG_LEVEL: OnceLock<LogLevel> = OnceLock::new();
+
+// Create a new handle to the GenMC model checker.
+// The first call to this function determines the log level of GenMC, any future call with a different log level will panic.
+pub fn create_genmc_driver_handle(
+    params: &GenmcParams,
+    genmc_log_level: LogLevel,
+) -> UniquePtr<MiriGenmcShim> {
+    // # Safety
+    //
+    // Only setting the GenMC log level once is guaranteed by the `OnceLock`.
+    // No other place calls `set_log_level_raw`, so the `logLevel` value in GenMC will not change once we initialize it once.
+    // All functions that use GenMC's `logLevel` can only be accessed in safe Rust through a `MiriGenmcShim`.
+    // There is no way to get `MiriGenmcShim` other than through `create_handle`, and we only call it *after* setting the log level, preventing any possible data races.
+    assert_eq!(
+        &genmc_log_level,
+        GENMC_LOG_LEVEL.get_or_init(|| {
+            unsafe { set_log_level_raw(genmc_log_level) };
+            genmc_log_level
+        }),
+        "Attempt to change the GenMC log level after it was already set"
+    );
+    unsafe { MiriGenmcShim::create_handle(params) }
+}
+
 impl GenmcScalar {
     pub const UNINIT: Self = Self { value: 0, is_init: false };
 
@@ -166,7 +191,8 @@ mod ffi {
         SequentiallyConsistent = 6,
     }
 
-    // # SAFETY
+    // # Safety
+    //
     // This block is unsafe to allow defining safe methods inside.
     //
     // `get_global_alloc_static_mask` is safe since it just returns a constant.
@@ -185,7 +211,8 @@ mod ffi {
 
         /// Set the log level for GenMC.
         ///
-        /// # SAFETY
+        /// # Safety
+        ///
         /// This function is not thread safe, since it writes to the global, mutable, non-atomic `logLevel` variable.
         /// Any GenMC function may read from `logLevel` unsynchronized.
         /// The safest way to use this function is to set the log level exactly once before first calling `create_handle`.
@@ -194,7 +221,8 @@ mod ffi {
 
         /// Create a new `MiriGenmcShim`, which wraps a `GenMCDriver`.
         ///
-        /// # SAFETY
+        /// # Safety
+        ///
         /// This function is marked as unsafe since the `logLevel` global variable is non-atomic.
         /// This function should not be called in an unsynchronized way with `set_log_level_raw`, since
         /// this function and any methods on the returned `MiriGenmcShim` may read the `logLevel`,

src/bin/miri.rs

@@ -39,8 +39,7 @@ use std::sync::atomic::{AtomicI32, AtomicU32, Ordering};
 
 use miri::{
     BacktraceStyle, BorrowTrackerMethod, GenmcConfig, GenmcCtx, MiriConfig, MiriEntryFnType,
-    ProvenanceMode, RetagFields, TreeBorrowsParams, ValidationMode, initialize_genmc,
-    run_genmc_mode,
+    ProvenanceMode, RetagFields, TreeBorrowsParams, ValidationMode, run_genmc_mode,
 };
 use rustc_abi::ExternAbi;
 use rustc_data_structures::sync;
@@ -187,21 +186,17 @@ impl rustc_driver::Callbacks for MiriCompilerCalls {
                     optimizations is usually marginal at best.");
         }
 
-        if let Some(genmc_config) = &config.genmc_config {
+        if let Some(_genmc_config) = &config.genmc_config {
             let eval_entry_once = |genmc_ctx: Rc<GenmcCtx>| {
                 miri::eval_entry(tcx, entry_def_id, entry_type, &config, Some(genmc_ctx))
             };
 
-            // Initialize GenMC by setting the log level for the entire program duration.
-            let genmc = initialize_genmc(genmc_config);
-
             // FIXME(genmc): add estimation mode here.
 
-            let return_code =
-                run_genmc_mode(genmc, &config, eval_entry_once, tcx).unwrap_or_else(|| {
-                    tcx.dcx().abort_if_errors();
-                    rustc_driver::EXIT_FAILURE
-                });
+            let return_code = run_genmc_mode(&config, eval_entry_once, tcx).unwrap_or_else(|| {
+                tcx.dcx().abort_if_errors();
+                rustc_driver::EXIT_FAILURE
+            });
 
             exit(return_code);
         };

src/concurrency/genmc/dummy.rs

@@ -8,13 +8,6 @@ use crate::{
     ThreadId, ThreadManager, VisitProvenance, VisitWith,
 };
 
-#[derive(Clone, Copy)]
-pub struct Genmc {}
-
-pub fn initialize_genmc(_genmc_config: &GenmcConfig) -> Genmc {
-    unreachable!();
-}
-
 #[derive(Clone, Copy, Debug)]
 pub enum ExitType {
     MainThreadFinish,
@@ -32,11 +25,9 @@ mod run {
 
     use rustc_middle::ty::TyCtxt;
 
-    use super::Genmc;
     use crate::{GenmcCtx, MiriConfig};
 
     pub fn run_genmc_mode<'tcx>(
-        _genmc: Genmc,
         _config: &MiriConfig,
         _eval_entry: impl Fn(Rc<GenmcCtx>) -> Option<i32>,
         _tcx: TyCtxt<'tcx>,

src/concurrency/genmc/mod.rs

@@ -1,7 +1,10 @@
 use std::cell::{Cell, RefCell};
 use std::sync::Arc;
 
-use genmc_sys::{GENMC_GLOBAL_ADDRESSES_MASK, GenmcScalar, MemOrdering, MiriGenmcShim, UniquePtr};
+use genmc_sys::{
+    GENMC_GLOBAL_ADDRESSES_MASK, GenmcScalar, MemOrdering, MiriGenmcShim, UniquePtr,
+    create_genmc_driver_handle,
+};
 use rustc_abi::{Align, Size};
 use rustc_const_eval::interpret::{AllocId, InterpCx, InterpResult, interp_ok};
 use rustc_middle::{mir, throw_machine_stop, throw_ub_format, throw_unsup_format};
@@ -24,17 +27,9 @@ mod run;
 pub(crate) mod scheduling;
 mod thread_id_map;
 
-pub use genmc_sys::Genmc;
-
 pub use self::config::GenmcConfig;
 pub use self::run::run_genmc_mode;
 
-/// Initialize GenMC by setting everything required.
-/// The returned `Genmc` struct is used to interact with GenMC in a safe way.
-pub fn initialize_genmc(genmc_config: &GenmcConfig) -> Genmc {
-    Genmc::new(genmc_config.log_level)
-}
-
 #[derive(Clone, Copy, Debug)]
 pub enum ExitType {
     MainThreadFinish,
@@ -120,9 +115,10 @@ pub struct GenmcCtx {
 /// GenMC Context creation and administrative / query actions
 impl GenmcCtx {
     /// Create a new `GenmcCtx` from a given config.
-    fn new(genmc: Genmc, miri_config: &MiriConfig, global_state: Arc<GlobalState>) -> Self {
+    fn new(miri_config: &MiriConfig, global_state: Arc<GlobalState>) -> Self {
         let genmc_config = miri_config.genmc_config.as_ref().unwrap();
-        let handle = RefCell::new(genmc.create_driver_handle(&genmc_config.params));
+        let handle =
+            RefCell::new(create_genmc_driver_handle(&genmc_config.params, genmc_config.log_level));
         Self { handle, exec_state: Default::default(), global_state }
     }
 

src/concurrency/genmc/run.rs

@@ -1,7 +1,6 @@
 use std::rc::Rc;
 use std::sync::Arc;
 
-use genmc_sys::Genmc;
 use rustc_middle::ty::TyCtxt;
 
 use super::GlobalState;
@@ -15,7 +14,6 @@ use crate::{GenmcCtx, MiriConfig};
 ///
 /// FIXME(genmc): add estimation mode setting.
 pub fn run_genmc_mode<'tcx>(
-    genmc: Genmc,
     config: &MiriConfig,
     eval_entry: impl Fn(Rc<GenmcCtx>) -> Option<i32>,
     tcx: TyCtxt<'tcx>,
@@ -24,7 +22,7 @@ pub fn run_genmc_mode<'tcx>(
     // It is shared by all `GenmcCtx` in this run.
     // FIXME(genmc): implement multithreading once GenMC supports it.
     let global_state = Arc::new(GlobalState::new(tcx.target_usize_max()));
-    let genmc_ctx = Rc::new(GenmcCtx::new(genmc, config, global_state));
+    let genmc_ctx = Rc::new(GenmcCtx::new(config, global_state));
 
     // `rep` is used to report the progress, Miri will panic on wrap-around.
     for rep in 0u64.. {

src/concurrency/mod.rs

@@ -22,5 +22,5 @@ pub mod weak_memory;
 mod genmc;
 
 pub use self::data_race_handler::{AllocDataRaceHandler, GlobalDataRaceHandler};
-pub use self::genmc::{ExitType, GenmcConfig, GenmcCtx, initialize_genmc, run_genmc_mode};
+pub use self::genmc::{ExitType, GenmcConfig, GenmcCtx, run_genmc_mode};
 pub use self::vector_clock::VClock;

src/lib.rs

@@ -133,7 +133,7 @@ pub use crate::concurrency::thread::{
     BlockReason, DynUnblockCallback, EvalContextExt as _, StackEmptyCallback, ThreadId,
     ThreadManager, TimeoutAnchor, TimeoutClock, UnblockKind,
 };
-pub use crate::concurrency::{GenmcConfig, GenmcCtx, initialize_genmc, run_genmc_mode};
+pub use crate::concurrency::{GenmcConfig, GenmcCtx, run_genmc_mode};
 pub use crate::data_structures::dedup_range_map::DedupRangeMap;
 pub use crate::data_structures::mono_hash_map::MonoHashMap;
 pub use crate::diagnostics::{