Implement Pointer conversions to and from GenMC. Limitation: Borrow tracking must be disabled. Remove hacks for keeping all memory allocations in GenMC mode.

Author: Patrick-6

genmc-sys/build.rs

@@ -28,7 +28,7 @@ mod downloading {
     /// The GenMC repository the we get our commit from.
     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 = "af9cc9ccd5d412b16defc35dbf36571c63a19c76";
+    pub(crate) const GENMC_COMMIT: &str = "cd01c12032bdd71df742b41c7817f99acc72e7ab";
 
     /// Ensure that a local GenMC repo is present and set to the correct commit.
     /// Return the path of the GenMC repo and whether the checked out commit was changed.
@@ -227,12 +227,16 @@ fn compile_cpp_dependencies(genmc_path: &Path, always_configure: bool) {
     // 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(";");
 
+    // These are all the C++ files we need to compile, which needs to be updated if more C++ files are added to Miri.
+    // We use absolute paths since relative paths can confuse IDEs when attempting to go-to-source on a path in a compiler error.
+    let cpp_files_base_path = Path::new("cpp/src/");
     let cpp_files = [
-        "./cpp/src/MiriInterface/EventHandling.cpp",
-        "./cpp/src/MiriInterface/Exploration.cpp",
-        "./cpp/src/MiriInterface/Setup.cpp",
-        "./cpp/src/MiriInterface/ThreadManagement.cpp",
-    ];
+        "MiriInterface/EventHandling.cpp",
+        "MiriInterface/Exploration.cpp",
+        "MiriInterface/Setup.cpp",
+        "MiriInterface/ThreadManagement.cpp",
+    ]
+    .map(|file| std::path::absolute(cpp_files_base_path.join(file)).unwrap());
 
     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.

genmc-sys/cpp/include/MiriInterface.hpp

@@ -126,7 +126,7 @@ struct MiriGenmcShim : private GenMCDriver {
 
     /**** Memory (de)allocation ****/
     auto handle_malloc(ThreadId thread_id, uint64_t size, uint64_t alignment) -> uint64_t;
-    void handle_free(ThreadId thread_id, uint64_t address);
+    auto handle_free(ThreadId thread_id, uint64_t address) -> bool;
 
     /**** Thread management ****/
     void handle_thread_create(ThreadId thread_id, ThreadId parent_id);
@@ -257,20 +257,22 @@ namespace GenmcScalarExt {
 inline GenmcScalar uninit() {
     return GenmcScalar {
         .value = 0,
+        .extra = 0,
         .is_init = false,
     };
 }
 
 inline GenmcScalar from_sval(SVal sval) {
     return GenmcScalar {
         .value = sval.get(),
+        .extra = sval.getExtra(),
         .is_init = true,
     };
 }
 
 inline SVal to_sval(GenmcScalar scalar) {
     ERROR_ON(!scalar.is_init, "Cannot convert an uninitialized `GenmcScalar` into an `SVal`\n");
-    return SVal(scalar.value);
+    return SVal(scalar.value, scalar.extra);
 }
 } // namespace GenmcScalarExt
 

genmc-sys/cpp/src/MiriInterface/EventHandling.cpp

@@ -250,8 +250,9 @@ auto MiriGenmcShim::handle_malloc(ThreadId thread_id, uint64_t size, uint64_t al
     return ret_val.get();
 }
 
-void MiriGenmcShim::handle_free(ThreadId thread_id, uint64_t address) {
+auto MiriGenmcShim::handle_free(ThreadId thread_id, uint64_t address) -> bool {
     const auto pos = inc_pos(thread_id);
     GenMCDriver::handleFree(pos, SAddr(address), EventDeps());
-    // FIXME(genmc): add error handling once GenMC returns errors from `handleFree`
+    // FIXME(genmc): use returned error from `handleFree` once implemented in GenMC.
+    return getResult().status.has_value();
 }

genmc-sys/cpp/src/MiriInterface/Exploration.cpp

@@ -24,8 +24,10 @@ auto MiriGenmcShim::schedule_next(
 
     if (const auto result = GenMCDriver::scheduleNext(threads_action_))
         return SchedulingResult { ExecutionState::Ok, static_cast<int32_t>(result.value()) };
-    if (GenMCDriver::isExecutionBlocked())
+    if (getExec().getGraph().isBlocked())
         return SchedulingResult { ExecutionState::Blocked, 0 };
+    if (getResult().status.has_value()) // the "value" here is a `VerificationError`
+        return SchedulingResult { ExecutionState::Error, 0 };
     return SchedulingResult { ExecutionState::Finished, 0 };
 }
 

genmc-sys/cpp/src/MiriInterface/Setup.cpp

@@ -170,9 +170,8 @@ static auto to_genmc_verbosity_level(const LogLevel log_level) -> VerbosityLevel
         // From a Miri perspective, this API doesn't work very well: most memory starts out
         // "uninitialized";
         // only statics have an initial value. And their initial value is just a sequence of bytes,
-        // but GenMC
-        // expect this to be already split into separate atomic variables. So we return a dummy
-        // value.
+        // but GenMC expect this to be already split into separate atomic variables. So we return a
+        // dummy value.
         // This value should never be visible to the interpreted program.
         // GenMC does not understand uninitialized memory the same way Miri does, which may cause
         // this function to be called. The returned value can be visible to Miri or the user:
@@ -183,13 +182,14 @@ static auto to_genmc_verbosity_level(const LogLevel log_level) -> VerbosityLevel
         //   Currently, atomic loads can see this value, unless initialized by an *atomic* store.
         //   FIXME(genmc): update this comment once mixed atomic-non-atomic support is added.
         //
-        // FIXME(genmc): implement proper support for uninitialized memory in GenMC. Ideally, the
-        // initial value getter would return an `optional<SVal>`, since the memory location may be
-        // uninitialized.
+        // FIXME(genmc): implement proper support for uninitialized memory in GenMC.
+        // Ideally, the initial value getter would return an `optional<SVal>`, since the memory
+        // location may be uninitialized.
         .initValGetter = [](const AAccess& a) { return SVal(0xDEAD); },
-        // Miri serves non-atomic loads from its own memory and these GenMC checks are wrong in
-        // that case. This should no longer be required with proper mixed-size access support.
-        .skipUninitLoadChecks = [](MemOrdering ord) { return ord == MemOrdering::NotAtomic; },
+        // Miri serves non-atomic loads from its own memory and these GenMC checks are wrong in that
+        // case. This should no longer be required with proper mixed-size access support.
+        .skipUninitLoadChecks = [](const MemAccessLabel* access_label
+                                ) { return access_label->getOrdering() == MemOrdering::NotAtomic; },
     };
     driver->setInterpCallbacks(std::move(interpreter_callbacks));
 

genmc-sys/src/lib.rs

@@ -45,10 +45,14 @@ pub fn create_genmc_driver_handle(
 }
 
 impl GenmcScalar {
-    pub const UNINIT: Self = Self { value: 0, is_init: false };
+    pub const UNINIT: Self = Self { value: 0, extra: 0, is_init: false };
 
     pub const fn from_u64(value: u64) -> Self {
-        Self { value, is_init: true }
+        Self { value, extra: 0, is_init: true }
+    }
+
+    pub const fn has_provenance(&self) -> bool {
+        self.extra != 0
     }
 }
 
@@ -162,17 +166,24 @@ mod ffi {
     }
 
     /// This type corresponds to `Option<SVal>` (or `std::optional<SVal>`), where `SVal` is the type that GenMC uses for storing values.
-    /// CXX doesn't support `std::optional` currently, so we need to use an extra `bool` to define whether this value is initialized or not.
     #[derive(Debug, Clone, Copy)]
     struct GenmcScalar {
+        /// The raw byte-level value (discarding provenance, if any) of this scalar.
         value: u64,
+        /// This is zero for integer values. For pointers, this encodes the provenance by
+        /// storing the base address of the allocation that this pointer belongs to.
+        /// Operations on `SVal` in GenMC (e.g., `fetch_add`) preserve the `extra` of the left argument (`left.fetch_add(right, ...)`).
+        extra: u64,
+        /// Indicates whether this value is initialized. If this is `false`, the other fields do not matter.
+        /// (Ideally we'd use `std::optional` but CXX does not support that.)
         is_init: bool,
     }
 
     #[must_use]
     #[derive(Debug, Clone, Copy)]
     enum ExecutionState {
         Ok,
+        Error,
         Blocked,
         Finished,
     }
@@ -406,7 +417,8 @@ mod ffi {
             size: u64,
             alignment: u64,
         ) -> u64;
-        fn handle_free(self: Pin<&mut MiriGenmcShim>, thread_id: i32, address: u64);
+        /// Returns true if an error was found.
+        fn handle_free(self: Pin<&mut MiriGenmcShim>, thread_id: i32, address: u64) -> bool;
 
         /**** Thread management ****/
         fn handle_thread_create(self: Pin<&mut MiriGenmcShim>, thread_id: i32, parent_id: i32);

src/alloc_addresses/mod.rs

@@ -207,13 +207,7 @@ impl<'tcx> EvalContextExt<'tcx> for crate::MiriInterpCx<'tcx> {}
 pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
     // Returns the `AllocId` that corresponds to the specified addr,
     // or `None` if the addr is out of bounds.
-    // Setting `only_exposed_allocations` selects whether only exposed allocations are considered.
-    fn alloc_id_from_addr(
-        &self,
-        addr: u64,
-        size: i64,
-        only_exposed_allocations: bool,
-    ) -> Option<AllocId> {
+    fn alloc_id_from_addr(&self, addr: u64, size: i64) -> Option<AllocId> {
         let this = self.eval_context_ref();
         let global_state = this.machine.alloc_addresses.borrow();
         assert!(global_state.provenance_mode != ProvenanceMode::Strict);
@@ -242,13 +236,10 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
             }
         }?;
 
-        // We only use this provenance if it has been exposed, or if the caller requested also non-exposed allocations
-        if !only_exposed_allocations || global_state.exposed.contains(&alloc_id) {
+        // We only use this provenance if it has been exposed.
+        if global_state.exposed.contains(&alloc_id) {
             // This must still be live, since we remove allocations from `int_to_ptr_map` when they get freed.
-            // In GenMC mode, we keep all allocations, so this check doesn't apply there.
-            if this.machine.data_race.as_genmc_ref().is_none() {
-                debug_assert!(this.is_alloc_live(alloc_id));
-            }
+            debug_assert!(this.is_alloc_live(alloc_id));
             Some(alloc_id)
         } else {
             None
@@ -443,8 +434,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
             alloc_id
         } else {
             // A wildcard pointer.
-            let only_exposed_allocations = true;
-            this.alloc_id_from_addr(addr.bytes(), size, only_exposed_allocations)?
+            this.alloc_id_from_addr(addr.bytes(), size)?
         };
 
         // This cannot fail: since we already have a pointer with that provenance, adjust_alloc_root_pointer
@@ -465,13 +455,6 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
 
 impl<'tcx> MiriMachine<'tcx> {
     pub fn free_alloc_id(&mut self, dead_id: AllocId, size: Size, align: Align, kind: MemoryKind) {
-        // In GenMC mode, we can't remove dead allocation info since such pointers can
-        // still be stored in atomics and we need this info to convert GenMC pointers to Miri pointers.
-        // `global_state.reuse` is also unused so we can just skip this entire function.
-        if self.data_race.as_genmc_ref().is_some() {
-            return;
-        }
-
         let global_state = self.alloc_addresses.get_mut();
         let rng = self.rng.get_mut();
 

src/concurrency/genmc/helper.rs

@@ -5,16 +5,18 @@ use rustc_abi::Size;
 use rustc_const_eval::interpret::{InterpResult, interp_ok};
 use rustc_data_structures::fx::FxHashSet;
 use rustc_middle::mir;
+use rustc_middle::mir::interpret;
 use rustc_middle::ty::ScalarInt;
 use rustc_span::Span;
 use tracing::debug;
 
 use super::GenmcScalar;
-use crate::diagnostics::EvalContextExt;
+use crate::alloc_addresses::EvalContextExt as _;
+use crate::diagnostics::EvalContextExt as _;
 use crate::intrinsics::AtomicRmwOp;
 use crate::{
-    AtomicFenceOrd, AtomicReadOrd, AtomicRwOrd, AtomicWriteOrd, InterpCx, MiriInterpCx,
-    MiriMachine, NonHaltingDiagnostic, Scalar, throw_unsup_format,
+    AtomicFenceOrd, AtomicReadOrd, AtomicRwOrd, AtomicWriteOrd, BorTag, GenmcCtx, InterpCx,
+    MiriInterpCx, MiriMachine, NonHaltingDiagnostic, Scalar, machine, throw_unsup_format,
 };
 
 /// Maximum size memory access in bytes that GenMC supports.
@@ -80,19 +82,30 @@ pub fn split_access(address: Size, size: Size) -> impl Iterator<Item = (u64, u64
 /// We cannot use the `AllocId` instead of the base address, since Miri has no control over the `AllocId`, and it may change across executions.
 /// Pointers with `Wildcard` provenance are not supported.
 pub fn scalar_to_genmc_scalar<'tcx>(
-    _ecx: &MiriInterpCx<'tcx>,
+    ecx: &MiriInterpCx<'tcx>,
+    genmc_ctx: &GenmcCtx,
     scalar: Scalar,
 ) -> InterpResult<'tcx, GenmcScalar> {
     interp_ok(match scalar {
         rustc_const_eval::interpret::Scalar::Int(scalar_int) => {
             // FIXME(genmc): Add u128 support once GenMC supports it.
             let value: u64 = scalar_int.to_uint(scalar_int.size()).try_into().unwrap();
-            GenmcScalar { value, is_init: true }
+            GenmcScalar { value, extra: 0, is_init: true }
+        }
+        rustc_const_eval::interpret::Scalar::Ptr(pointer, size) => {
+            // FIXME(genmc,borrow tracking): Borrow tracking information is lost.
+            let addr = crate::Pointer::from(pointer).addr();
+            if let crate::Provenance::Wildcard = pointer.provenance {
+                throw_unsup_format!("Pointers with wildcard provenance not allowed in GenMC mode");
+            }
+            let (alloc_id, _size, _prov_extra) =
+                rustc_const_eval::interpret::Machine::ptr_get_alloc(ecx, pointer, size.into())
+                    .unwrap();
+            let base_addr = ecx.addr_from_alloc_id(alloc_id, None)?;
+            // Add the base_addr alloc_id pair to the map.
+            genmc_ctx.exec_state.genmc_shared_allocs_map.borrow_mut().insert(base_addr, alloc_id);
+            GenmcScalar { value: addr.bytes(), extra: base_addr, is_init: true }
         }
-        rustc_const_eval::interpret::Scalar::Ptr(_pointer, _size) =>
-            throw_unsup_format!(
-                "FIXME(genmc): Implement sending pointers (with provenance) to GenMC."
-            ),
     })
 }
 
@@ -101,16 +114,25 @@ pub fn scalar_to_genmc_scalar<'tcx>(
 /// Convert a `GenmcScalar` back into a Miri `Scalar`.
 /// For pointers, attempt to convert the stored base address of their allocation back into an `AllocId`.
 pub fn genmc_scalar_to_scalar<'tcx>(
-    _ecx: &MiriInterpCx<'tcx>,
+    ecx: &MiriInterpCx<'tcx>,
+    genmc_ctx: &GenmcCtx,
     scalar: GenmcScalar,
     size: Size,
 ) -> InterpResult<'tcx, Scalar> {
-    // FIXME(genmc): Add GenmcScalar to Miri Pointer conversion.
-
-    // NOTE: GenMC always returns 64 bit values, and the upper bits are not yet truncated.
-    // FIXME(genmc): GenMC should be doing the truncation, not Miri.
-    let (value_scalar_int, _got_truncated) = ScalarInt::truncate_from_uint(scalar.value, size);
-    interp_ok(Scalar::Int(value_scalar_int))
+    // If `extra` is zero, we have a regular integer.
+    if scalar.extra == 0 {
+        // NOTE: GenMC always returns 64 bit values, and the upper bits are not yet truncated.
+        // FIXME(genmc): GenMC should be doing the truncation, not Miri.
+        let (value_scalar_int, _got_truncated) = ScalarInt::truncate_from_uint(scalar.value, size);
+        return interp_ok(Scalar::from(value_scalar_int));
+    }
+    // `extra` is non-zero, we have a pointer.
+    // When we get a pointer from GenMC, then we must have sent it to GenMC before in the same execution (since the reads-from relation is always respected).
+    let alloc_id = genmc_ctx.exec_state.genmc_shared_allocs_map.borrow()[&scalar.extra];
+    // FIXME(genmc,borrow tracking): Borrow tracking not yet supported.
+    let provenance = machine::Provenance::Concrete { alloc_id, tag: BorTag::default() };
+    let ptr = interpret::Pointer::new(provenance, Size::from_bytes(scalar.value));
+    interp_ok(Scalar::from_pointer(ptr, &ecx.tcx))
 }
 
 impl AtomicReadOrd {