Use Github URL to fetch GenMC

genmc-sys/build.rs

@@ -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://gitlab.inf.ethz.ch/public-plf/genmc.git";
+    pub(crate) const GENMC_GITHUB_URL: &str = "https://github.com/MPI-SWS/genmc.git";
     /// The GenMC commit we depend on. It must be available on the specified GenMC repository.
-    pub(crate) const GENMC_COMMIT: &str = "ce775ccd7866db820fa12ffca66463087a11dd96";
+    pub(crate) const GENMC_COMMIT: &str = "d9527280bb99f1cef64326b1803ffd952e3880df";
 
     /// 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.

genmc-sys/cpp/include/MiriInterface.hpp

@@ -261,27 +261,27 @@ namespace GenmcScalarExt {
 inline GenmcScalar uninit() {
     return GenmcScalar {
         .value = 0,
-        .extra = 0,
+        .provenance = 0,
         .is_init = false,
     };
 }
 
 inline GenmcScalar from_sval(SVal sval) {
     return GenmcScalar {
         .value = sval.get(),
-        .extra = sval.getExtra(),
+        .provenance = sval.getProvenance(),
         .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, scalar.extra);
+    return SVal(scalar.value, scalar.provenance);
 }
 
 inline std::optional<SVal> try_to_sval(GenmcScalar scalar) {
     if (scalar.is_init)
-        return { SVal(scalar.value, scalar.extra) };
+        return { SVal(scalar.value, scalar.provenance) };
     return std::nullopt;
 }
 } // namespace GenmcScalarExt

genmc-sys/src/lib.rs

@@ -45,14 +45,14 @@ pub fn create_genmc_driver_handle(
 }
 
 impl GenmcScalar {
-    pub const UNINIT: Self = Self { value: 0, extra: 0, is_init: false };
+    pub const UNINIT: Self = Self { value: 0, provenance: 0, is_init: false };
 
     pub const fn from_u64(value: u64) -> Self {
-        Self { value, extra: 0, is_init: true }
+        Self { value, provenance: 0, is_init: true }
     }
 
     pub const fn has_provenance(&self) -> bool {
-        self.extra != 0
+        self.provenance != 0
     }
 }
 
@@ -172,8 +172,9 @@ mod ffi {
         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,
+        /// Operations on `SVal` in GenMC (e.g., `fetch_add`) preserve the `provenance` of the left
+        /// argument (`left.fetch_add(right, ...)`).
+        provenance: 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,

src/concurrency/genmc/helper.rs

@@ -55,7 +55,7 @@ pub fn scalar_to_genmc_scalar<'tcx>(
         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, extra: 0, is_init: true }
+            GenmcScalar { value, provenance: 0, is_init: true }
         }
         rustc_const_eval::interpret::Scalar::Ptr(pointer, size) => {
             // FIXME(genmc,borrow tracking): Borrow tracking information is lost.
@@ -69,7 +69,7 @@ pub fn scalar_to_genmc_scalar<'tcx>(
             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 }
+            GenmcScalar { value: addr.bytes(), provenance: base_addr, is_init: true }
         }
     })
 }
@@ -84,16 +84,17 @@ pub fn genmc_scalar_to_scalar<'tcx>(
     scalar: GenmcScalar,
     size: Size,
 ) -> InterpResult<'tcx, Scalar> {
-    // If `extra` is zero, we have a regular integer.
-    if scalar.extra == 0 {
+    // If `provenance` is zero, we have a regular integer.
+    if scalar.provenance == 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];
+    // `provenance` 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.provenance];
     // 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));