Simplify mutex lock annotation id.

Author: Patrick-6

genmc-sys/cpp/include/MiriInterface.hpp

@@ -12,7 +12,6 @@
 
 // GenMC headers:
 #include "ExecutionGraph/EventLabel.hpp"
-#include "Static/ModuleID.hpp"
 #include "Support/MemOrdering.hpp"
 #include "Support/RMWOps.hpp"
 #include "Verification/Config.hpp"
@@ -41,10 +40,6 @@ struct MutexLockResult;
 // GenMC uses `int` for its thread IDs.
 using ThreadId = int;
 
-// Types used for GenMC annotations, e.g., in `handle_mutex_lock`.
-using AnnotID = ModuleID::ID;
-using AnnotT = SExpr<AnnotID>;
-
 /// Set the log level for GenMC.
 ///
 /// # Safety
@@ -245,14 +240,6 @@ struct MiriGenmcShim : private GenMCDriver {
      * indices, since GenMC expects us to do that.
      */
     std::vector<Action> threads_action_;
-
-    /**
-     * Map of already used annotation ids (e.g., for mutexes).
-     * FIXME(GenMC): Ensure that these are consistent with how GenMC expects them once Miri supports
-     * multithreading in GenMC mode.
-     */
-    std::unordered_map<uint64_t, ModuleID::ID> annotation_id {};
-    ModuleID::ID annotation_id_counter = 0;
 };
 
 /// Get the bit mask that GenMC expects for global memory allocations.

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

@@ -2,6 +2,9 @@
 
 #include "MiriInterface.hpp"
 
+// GenMC headers:
+#include "Static/ModuleID.hpp"
+
 // CXX.rs generated headers:
 #include "genmc-sys/src/lib.rs.h"
 
@@ -10,24 +13,20 @@
 
 auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint64_t size)
     -> MutexLockResult {
-    // FIXME(genmc,multithreading): ensure this annotation id is unique even if Miri runs GenMC mode
-    // multithreaded. We cannot use the address directly, since it is 64 bits, and `ID` is an
-    // `unsigned int`.
-    ModuleID::ID annot_id;
-    auto [it, inserted] = annotation_id.try_emplace(address, annotation_id_counter);
-    if (inserted) {
-        annot_id = annotation_id_counter++;
-    } else {
-        annot_id = it->second;
-    }
+    // This annotation informs GenMC about the condition required to make this lock call succeed.
+    // It stands for `value_read_by_load != MUTEX_LOCKED`.
     const auto size_bits = size * 8;
     const auto annot = std::move(Annotation(
         AssumeType::Spinloop,
-        Annotation::ExprVP(NeExpr<AnnotID>::create(
-                               RegisterExpr<AnnotID>::create(size_bits, annot_id),
-                               ConcreteExpr<AnnotID>::create(size_bits, MUTEX_LOCKED)
+        Annotation::ExprVP(
+            NeExpr<ModuleID::ID>::create(
+                // `RegisterExpr` marks the value of the current expression, i.e., the loaded value.
+                // The id is zero, since this annotation only uses one input variable.
+                RegisterExpr<ModuleID::ID>::create(size_bits, /* id */ 0),
+                ConcreteExpr<ModuleID::ID>::create(size_bits, MUTEX_LOCKED)
+            )
+                .release()
         )
-                               .release())
     ));
 
     // Mutex starts out unlocked, so we always say the previous value is "unlocked".