WIP: Start working on Miri-GenMC interop.

- Add genmc-sys crate for building GenMC C++ code.
- Implemented program features:
  - Handling of atomic loads, stores, allocations and deallocations.
    - Implement consistent address allocations for globals
    - Non-global addresses allocated by GenMC.
      - Limitation: No address randomization.
      - Limitation: No address reuse.
  - Handling of non-atomic memory accesses.
    - Limitation: need to split up NA reads and stores into max 8 byte chunks.
    - Limitation: no mixed size access support.
  - Limitation: Incomplete (unsound) handling of uninitialized memory.
  - Implement Pointer conversions to and from GenMC
    - Limitation: Aliasing model checking must be disabled.
  - Handling of Read-Modify-Write, Compare-Exchange and Atomic Exchange operations.
    - Limitation: Compare-Exchange currently ignores possibility of spurious failures.
    - Limitation: Compare-Exchange failure memory ordering is ignored.
  - Handling of thread creation and finishing.
    - Added Miri to GenMC thread id mapping.
  - Implement mutex lock, try_lock and unlock.
    - Make use of annotations to reduce number of blocked executions for programs with mutexes.
- Add estimation mode for Miri-GenMC.
  - Limitation: Printing currently handled on C++ side (Should be moved once VerificationResult is available to Rust code)
- Thread scheduling in Miri done through GenMC, add loop over eval_entry function.
  - Rebase GenMC to use new scheduler.
- Added GenMC `__VERIFIER_assume` equivalent for Miri (`miri_genmc_verifier_assume`)
- Add warnings for GenMC mode for unsupported features.
- Add a lot of test, including translation of GenMC litmus tests.
  - Only run tests if 'genmc' feature enabled.
- WIP: try implementing NonNullUniquePtr wrapper for CXX.
- WIP: work on mixed atomic/non-atomics.
  - Partially working, some issues with globals
- FIX: Make naming consistent with GenMC for blocked execution

Squashed changes:
- Add git support to build, move C++ files into genmc-sys crate
- Implement building GenMC-Miri after GenMC codebase split.
- Cleanup genmc-sys build, remove walkdir dependency.
- Fix printing after LLVM IO removal.
- WIP: temporarily point GenMC repo to private branch.
- WIP: Work on building without LLVM dependency.
- Fix build for Ubuntu 22
- Disable stacked borrows for GenMC tests
- Get Miri-GenMC building again after rebasing onto GenMC release 0.12.0
- Translate some Loom tests for Miri-GenMC.
- Add error for using native-lib with GenMC mode.
- Remove on_stack_empty handling except for main thread.
- Rename 'stuck' to 'blocked' to be in line with GenMC terminology.
- Enable tests that were blocked on rust-lang #116707
- Remove redundant file in compilation step.
- Clean up InterpResult<'tcx, ()>
- Improve program exit handling, remove 'thread_stack_empty' hack, clean up terminator cache leftovers.

Author: Patrick-6

Cargo.toml

@@ -72,7 +72,8 @@ name = "ui"
 harness = false
 
 [features]
-default = ["stack-cache", "native-lib"]
+# TODO GENMC (DEBUGGING): `genmc` feature should be turned off in upstream repo for now
+default = ["stack-cache", "native-lib", "genmc"]
 genmc = ["dep:genmc-sys"] # this enables a GPL dependency!
 stack-cache = []
 stack-cache-consistency-check = ["stack-cache"]

genmc-sys/.gitignore

@@ -1 +1,2 @@
 genmc-src*/
+genmc*/

genmc-sys/build.rs

@@ -224,7 +224,6 @@ fn compile_cpp_dependencies(genmc_path: &Path) {
         .include(genmc_include_dir)
         .include(llvm_include_dirs)
         .include("./src_cpp")
-        .file("./src_cpp/MiriInterface.hpp")
         .file("./src_cpp/MiriInterface.cpp")
         .compile("genmc_interop");
 

genmc-sys/src/cxx_extra.rs

@@ -0,0 +1,48 @@
+#![allow(unused)] // TODO GENMC
+
+use std::pin::Pin;
+
+use cxx::UniquePtr;
+use cxx::memory::UniquePtrTarget;
+
+#[repr(transparent)]
+pub struct NonNullUniquePtr<T: UniquePtrTarget> {
+    /// SAFETY: `inner` is never `null`
+    inner: UniquePtr<T>,
+}
+
+impl<T: UniquePtrTarget> NonNullUniquePtr<T> {
+    pub fn new(input: UniquePtr<T>) -> Option<Self> {
+        if input.is_null() {
+            None
+        } else {
+            // SAFETY: `input` is not `null`
+            Some(unsafe { Self::new_unchecked(input) })
+        }
+    }
+
+    /// SAFETY: caller must ensure that `input` is not `null`
+    pub unsafe fn new_unchecked(input: UniquePtr<T>) -> Self {
+        Self { inner: input }
+    }
+
+    pub fn into_inner(self) -> UniquePtr<T> {
+        self.inner
+    }
+
+    pub fn as_mut(&mut self) -> Pin<&mut T> {
+        let ptr = self.inner.as_mut_ptr();
+
+        // SAFETY: `inner` is not `null` (type invariant)
+        let mut_reference = unsafe { ptr.as_mut().unwrap_unchecked() };
+        // SAFETY: TODO GENMC (should be the same reason as in CXX crate, but there is no safety comment there)
+        unsafe { Pin::new_unchecked(mut_reference) }
+    }
+}
+
+impl<T: UniquePtrTarget> AsRef<T> for NonNullUniquePtr<T> {
+    fn as_ref(&self) -> &T {
+        // SAFETY: `inner` is not `null` (type invariant)
+        unsafe { self.inner.as_ref().unwrap_unchecked() }
+    }
+}

genmc-sys/src/lib.rs

@@ -1,11 +1,38 @@
 pub use self::ffi::*;
 
+pub mod cxx_extra;
+
+/// Defined in "genmc/src/Support/SAddr.hpp"
+/// FIXME: currently we use `getGlobalAllocStaticMask()` to ensure the constant is consistent between Miri and GenMC,
+///   but if https://github.com/dtolnay/cxx/issues/1051 is fixed we could share the constant directly.
+pub const GENMC_GLOBAL_ADDRESSES_MASK: u64 = 1 << 63;
+
+#[repr(transparent)]
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+pub struct GenmcThreadId(pub i32);
+
+pub const GENMC_MAIN_THREAD_ID: GenmcThreadId = GenmcThreadId(0);
+
+impl GenmcScalar {
+    pub const UNINIT: Self = Self { value: 0, extra: 0, is_init: false };
+    pub const DUMMY: Self = Self::from_u64(0xDEADBEEF);
+
+    pub const MUTEX_LOCKED_STATE: Self = Self::from_u64(1);
+    pub const MUTEX_UNLOCKED_STATE: Self = Self::from_u64(0);
+
+    pub const fn from_u64(value: u64) -> Self {
+        Self { value, extra: 0, is_init: true }
+    }
+}
+
 impl Default for GenmcParams {
     fn default() -> Self {
         Self {
             print_random_schedule_seed: false,
-            do_symmetry_reduction: false,
-            // FIXME(GenMC): Add defaults for remaining parameters
+            quiet: true,
+            log_level_trace: false,
+            do_symmetry_reduction: false, // TODO GENMC (PERFORMANCE): maybe make this default `true`
+            estimation_max: 1000,
         }
     }
 }
@@ -16,15 +43,268 @@ mod ffi {
     /// (The fields of this struct are visible to both Rust and C++)
     #[derive(Clone, Debug)]
     struct GenmcParams {
+        // pub genmc_seed: u64; // OR: Option<u64>
         pub print_random_schedule_seed: bool,
+        pub quiet: bool, // TODO GENMC: maybe make log-level more fine grained
+        pub log_level_trace: bool,
         pub do_symmetry_reduction: bool,
-        // FIXME(GenMC): Add remaining parameters.
+        pub estimation_max: u32,
+    }
+
+    #[derive(Debug)]
+    enum ActionKind {
+        /// Any Mir terminator that's atomic and has load semantics.
+        Load,
+        /// Anything that's not a `Load`.
+        NonLoad,
+    }
+
+    #[derive(Debug)]
+    enum MemOrdering {
+        NotAtomic = 0,
+        Relaxed = 1,
+        // In case we support consume
+        Acquire = 3,
+        Release = 4,
+        AcquireRelease = 5,
+        SequentiallyConsistent = 6,
+    }
+
+    #[derive(Debug)]
+    enum RMWBinOp {
+        Xchg = 0,
+        Add = 1,
+        Sub = 2,
+        And = 3,
+        Nand = 4,
+        Or = 5,
+        Xor = 6,
+        Max = 7,
+        Min = 8,
+        UMax = 9,
+        UMin = 10,
+    }
+
+    // TODO GENMC: do these have to be shared with the Rust side?
+    #[derive(Debug)]
+    enum StoreEventType {
+        Normal,
+        ReadModifyWrite,
+        CompareExchange,
+        MutexUnlockWrite,
+    }
+
+    #[derive(Debug, Clone, Copy)]
+    struct GenmcScalar {
+        value: u64,
+        extra: u64,
+        is_init: bool,
+    }
+
+    /**** \/ Result & Error types \/ ****/
+
+    #[must_use]
+    #[derive(Debug)]
+    struct ReadModifyWriteResult {
+        old_value: GenmcScalar,
+        new_value: GenmcScalar,
+        isCoMaxWrite: bool,
+        error: UniquePtr<CxxString>, // TODO GENMC: pass more error info here
+    }
+
+    #[must_use]
+    #[derive(Debug)]
+    struct MutexLockResult {
+        is_lock_acquired: bool,
+        error: UniquePtr<CxxString>, // TODO GENMC: pass more error info here
+    }
+
+    #[must_use]
+    #[derive(Debug)]
+    struct CompareExchangeResult {
+        old_value: GenmcScalar, // TODO GENMC: handle bigger values
+        is_success: bool,
+        isCoMaxWrite: bool,
+        error: UniquePtr<CxxString>, // TODO GENMC: pass more error info here
     }
+
+    #[must_use]
+    #[derive(Debug)]
+    struct LoadResult {
+        is_read_opt: bool,
+        read_value: GenmcScalar,     // TODO GENMC: handle bigger values
+        error: UniquePtr<CxxString>, // TODO GENMC: pass more error info here
+    }
+
+    #[must_use]
+    #[derive(Debug)]
+    struct StoreResult {
+        error: UniquePtr<CxxString>, // TODO GENMC: pass more error info here
+        isCoMaxWrite: bool,
+    }
+
+    #[must_use]
+    #[derive(Debug)]
+    enum VerificationError {
+        VE_NonErrorBegin,
+        VE_OK,
+        VE_WWRace,
+        VE_UnfreedMemory,
+        VE_NonErrorLast,
+
+        VE_Safety,
+        VE_Recovery,
+        VE_Liveness,
+        VE_RaceNotAtomic,
+        VE_RaceFreeMalloc,
+        VE_FreeNonMalloc,
+        VE_DoubleFree,
+        VE_Allocation,
+
+        VE_InvalidAccessBegin,
+        VE_UninitializedMem,
+        VE_AccessNonMalloc,
+        VE_AccessFreed,
+        VE_InvalidAccessEnd,
+
+        VE_InvalidCreate,
+        VE_InvalidJoin,
+        VE_InvalidUnlock,
+        VE_InvalidBInit,
+        VE_BarrierWellFormedness,
+        VE_Annotation,
+        VE_MixedSize,
+        VE_LinearizabilityError,
+        VE_SystemError,
+    }
+
+    /**** /\ Result & Error types /\ ****/
+
     unsafe extern "C++" {
         include!("MiriInterface.hpp");
 
+        type MemOrdering;
+        type RMWBinOp;
+        type StoreEventType;
+
+        // Types for Scheduling queries:
+        type ActionKind;
+
+        // Result / Error types:
+        type LoadResult;
+        type StoreResult;
+        type ReadModifyWriteResult;
+        type CompareExchangeResult;
+        type MutexLockResult;
+        type VerificationError;
+
+        type GenmcScalar;
+
+        // type OperatingMode; // Estimation(budget) or Verification
+
         type MiriGenMCShim;
 
-        fn createGenmcHandle(config: &GenmcParams) -> UniquePtr<MiriGenMCShim>;
+        fn createGenmcHandle(config: &GenmcParams, do_estimation: bool)
+        -> UniquePtr<MiriGenMCShim>;
+        fn getGlobalAllocStaticMask() -> u64;
+
+        fn handleExecutionStart(self: Pin<&mut MiriGenMCShim>);
+        fn handleExecutionEnd(self: Pin<&mut MiriGenMCShim>) -> UniquePtr<CxxString>;
+
+        fn handleLoad(
+            self: Pin<&mut MiriGenMCShim>,
+            thread_id: i32,
+            address: u64,
+            size: u64,
+            memory_ordering: MemOrdering,
+            old_value: GenmcScalar,
+        ) -> LoadResult;
+        fn handleReadModifyWrite(
+            self: Pin<&mut MiriGenMCShim>,
+            thread_id: i32,
+            address: u64,
+            size: u64,
+            load_ordering: MemOrdering,
+            store_ordering: MemOrdering,
+            rmw_op: RMWBinOp,
+            rhs_value: GenmcScalar,
+            old_value: GenmcScalar,
+        ) -> ReadModifyWriteResult;
+        fn handleCompareExchange(
+            self: Pin<&mut MiriGenMCShim>,
+            thread_id: i32,
+            address: u64,
+            size: u64,
+            expected_value: GenmcScalar,
+            new_value: GenmcScalar,
+            old_value: GenmcScalar,
+            success_load_ordering: MemOrdering,
+            success_store_ordering: MemOrdering,
+            fail_load_ordering: MemOrdering,
+            can_fail_spuriously: bool,
+        ) -> CompareExchangeResult;
+        fn handleStore(
+            self: Pin<&mut MiriGenMCShim>,
+            thread_id: i32,
+            address: u64,
+            size: u64,
+            value: GenmcScalar,
+            old_value: GenmcScalar,
+            memory_ordering: MemOrdering,
+            store_event_type: StoreEventType,
+        ) -> StoreResult;
+        fn handleFence(self: Pin<&mut MiriGenMCShim>, thread_id: i32, memory_ordering: MemOrdering);
+
+        fn handleMalloc(
+            self: Pin<&mut MiriGenMCShim>,
+            thread_id: i32,
+            size: u64,
+            alignment: u64,
+        ) -> u64;
+        fn handleFree(self: Pin<&mut MiriGenMCShim>, thread_id: i32, address: u64, size: u64);
+
+        fn handleThreadCreate(self: Pin<&mut MiriGenMCShim>, thread_id: i32, parent_id: i32);
+        fn handleThreadJoin(self: Pin<&mut MiriGenMCShim>, thread_id: i32, child_id: i32);
+        fn handleThreadFinish(self: Pin<&mut MiriGenMCShim>, thread_id: i32, ret_val: u64);
+
+        /**** Blocking instructions ****/
+        fn handleUserBlock(self: Pin<&mut MiriGenMCShim>, thread_id: i32);
+
+        /**** Mutex handling ****/
+        fn handleMutexLock(
+            self: Pin<&mut MiriGenMCShim>,
+            thread_id: i32,
+            address: u64,
+            size: u64,
+        ) -> MutexLockResult;
+        fn handleMutexTryLock(
+            self: Pin<&mut MiriGenMCShim>,
+            thread_id: i32,
+            address: u64,
+            size: u64,
+        ) -> MutexLockResult;
+        fn handleMutexUnlock(
+            self: Pin<&mut MiriGenMCShim>,
+            thread_id: i32,
+            address: u64,
+            size: u64,
+        ) -> StoreResult;
+
+        /**** Scheduling ****/
+        fn scheduleNext(
+            self: Pin<&mut MiriGenMCShim>,
+            curr_thread_id: i32,
+            curr_thread_next_instr_kind: ActionKind,
+        ) -> i64;
+
+        fn getBlockedExecutionCount(self: &MiriGenMCShim) -> u64;
+        fn getExploredExecutionCount(self: &MiriGenMCShim) -> u64;
+
+        /// Check whether there are more executions to explore.
+        /// If there are more executions, this method prepares for the next execution and returns `true`.
+        fn isExplorationDone(self: Pin<&mut MiriGenMCShim>) -> bool;
+
+        fn printGraph(self: Pin<&mut MiriGenMCShim>);
+        fn printEstimationResults(self: &MiriGenMCShim, elapsed_time_sec: f64);
     }
 }