miri subtree update

src/tools/miri/Cargo.lock

@@ -1162,9 +1162,9 @@ checksum = "69cdb34c158ceb288df11e18b4bd39de994f6657d83847bdffdbd7f346754b0f"
 
 [[package]]
 name = "rand"
-version = "0.9.2"
+version = "0.9.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6db2770f06117d490610c7488547d543617b21bfa07796d7a12f6f1bd53850d1"
+checksum = "7ec095654a25171c2124e9e3393a930bddbffdc939556c914957a4c3e0a87166"
 dependencies = [
  "rand_chacha",
  "rand_core",

src/tools/miri/cargo-miri/src/phases.rs

@@ -87,7 +87,9 @@ pub fn phase_cargo_miri(mut args: impl Iterator<Item = String>) {
                 println!("`cargo miri {verb}` supports the same flags as `cargo {verb}`:\n");
                 let mut cmd = cargo();
                 cmd.arg(verb);
-                cmd.arg("--help");
+                // Forward all arguments (some of them can influence the help output, e.g.
+                // the nextest verb).
+                cmd.args(args);
                 exec(cmd);
             }
             _ => {

src/tools/miri/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://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 = "22d3d0b44dedb4e8e1aae3330e546465e4664529";
+    pub(crate) const GENMC_COMMIT: &str = "29b03a66402c4453fc77901ef3be90bb55707cd4";
 
     /// Ensure that a local GenMC repo is present and set to the correct commit.
     /// Return the path of the GenMC repo clone.
@@ -159,6 +159,7 @@ fn compile_cpp_dependencies(genmc_path: &Path) {
         .out_dir(genmc_build_dir)
         .profile(GENMC_CMAKE_PROFILE)
         .define("BUILD_LLI", "OFF")
+        .define("EMIT_NA_LABELS", "OFF")
         .define("GENMC_DEBUG", if enable_genmc_debug { "ON" } else { "OFF" });
 
     // The actual compilation happens here:
@@ -172,7 +173,7 @@ fn compile_cpp_dependencies(genmc_path: &Path) {
     // Part 2:
     // Compile the cxx_bridge (the link between the Rust and C++ code).
 
-    let genmc_include_dir = genmc_install_dir.join("include").join("genmc");
+    let genmc_include_dir = genmc_install_dir.join("include");
 
     // 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.
@@ -181,10 +182,6 @@ fn compile_cpp_dependencies(genmc_path: &Path) {
         .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.
-    if enable_genmc_debug {
-        bridge.define("ENABLE_GENMC_DEBUG", None);
-    }
     bridge
         .opt_level(2)
         .debug(true) // Same settings that GenMC uses (default for cmake `RelWithDebInfo`)

src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp

@@ -5,17 +5,17 @@
 #include "rust/cxx.h"
 
 // GenMC generated headers:
-#include "config.h"
+#include "genmc/config.h"
 
 // Miri `genmc-sys/src_cpp` headers:
 #include "ResultHandling.hpp"
 
 // GenMC headers:
-#include "ExecutionGraph/EventLabel.hpp"
-#include "Support/MemOrdering.hpp"
-#include "Support/RMWOps.hpp"
-#include "Verification/Config.hpp"
-#include "Verification/GenMCDriver.hpp"
+#include "genmc/Execution/EventLabel.hpp"
+#include "genmc/Support/MemOrdering.hpp"
+#include "genmc/Support/RMWOps.hpp"
+#include "genmc/Verification/Config.hpp"
+#include "genmc/Verification/GenMCDriver.hpp"
 
 // C++ headers:
 #include <cstdint>
@@ -36,6 +36,7 @@ struct StoreResult;
 struct ReadModifyWriteResult;
 struct CompareExchangeResult;
 struct MutexLockResult;
+struct MallocResult;
 
 // GenMC uses `int` for its thread IDs.
 using ThreadId = int;
@@ -86,13 +87,15 @@ struct MiriGenmcShim : private GenMCDriver {
 
     /**** Memory access handling ****/
 
-    [[nodiscard]] LoadResult handle_load(
+    [[nodiscard]] LoadResult handle_atomic_load(
         ThreadId thread_id,
         uint64_t address,
         uint64_t size,
         MemOrdering ord,
         GenmcScalar old_val
     );
+    [[nodiscard]] LoadResult
+    handle_non_atomic_load(ThreadId thread_id, uint64_t address, uint64_t size);
     [[nodiscard]] ReadModifyWriteResult handle_read_modify_write(
         ThreadId thread_id,
         uint64_t address,
@@ -113,20 +116,22 @@ struct MiriGenmcShim : private GenMCDriver {
         MemOrdering fail_load_ordering,
         bool can_fail_spuriously
     );
-    [[nodiscard]] StoreResult handle_store(
+    [[nodiscard]] StoreResult handle_atomic_store(
         ThreadId thread_id,
         uint64_t address,
         uint64_t size,
         GenmcScalar value,
         GenmcScalar old_val,
         MemOrdering ord
     );
+    [[nodiscard]] StoreResult
+    handle_non_atomic_store(ThreadId thread_id, uint64_t address, uint64_t size);
 
     void handle_fence(ThreadId thread_id, MemOrdering ord);
 
     /**** Memory (de)allocation ****/
 
-    auto handle_malloc(ThreadId thread_id, uint64_t size, uint64_t alignment) -> uint64_t;
+    auto handle_malloc(ThreadId thread_id, uint64_t size, uint64_t alignment) -> MallocResult;
 
     /** Returns null on success, or an error string if an error occurs. */
     auto handle_free(ThreadId thread_id, uint64_t address) -> std::unique_ptr<std::string>;
@@ -203,33 +208,15 @@ struct MiriGenmcShim : private GenMCDriver {
     auto get_estimation_results() const -> EstimationResult;
 
   private:
-    /** Increment the event index in the given thread by 1 and return the new event. */
-    [[nodiscard]] inline auto inc_pos(ThreadId tid) -> Event {
+    /** Returns the current event for a given thread. */
+    inline auto curr_pos(ThreadId tid) -> Event {
         ERROR_ON(tid >= threads_action_.size(), "ThreadId out of bounds");
-        return ++threads_action_[tid].event;
+        return threads_action_[tid].event;
     }
-    /** Decrement the event index in the given thread by 1 and return the new event. */
-    inline auto dec_pos(ThreadId tid) -> Event {
+    /** Increment the event index in the given thread by `count`. */
+    inline void inc_pos(ThreadId tid, unsigned int count) {
         ERROR_ON(tid >= threads_action_.size(), "ThreadId out of bounds");
-        return --threads_action_[tid].event;
-    }
-
-    /**
-     * Helper function for loads that need to reset the event counter when no value is returned.
-     * Same syntax as `GenMCDriver::handleLoad`, but this takes a thread id instead of an Event.
-     * Automatically calls `inc_pos` and `dec_pos` where needed for the given thread.
-     */
-    template <EventLabel::EventLabelKind k, typename... Ts>
-    auto handle_load_reset_if_none(ThreadId tid, std::optional<SVal> old_val, Ts&&... params)
-        -> HandleResult<SVal> {
-        const auto pos = inc_pos(tid);
-        const auto ret =
-            GenMCDriver::handleLoad<k>(nullptr, pos, old_val, std::forward<Ts>(params)...);
-        // If we didn't get a value, we have to reset the index of the current thread.
-        if (!std::holds_alternative<SVal>(ret)) {
-            dec_pos(tid);
-        }
-        return ret;
+        threads_action_[tid].event.index += count;
     }
 
     /**
@@ -293,48 +280,72 @@ inline std::optional<SVal> try_to_sval(GenmcScalar scalar) {
 namespace LoadResultExt {
 inline LoadResult no_value() {
     return LoadResult {
+        .invalid = false,
         .error = std::unique_ptr<std::string>(nullptr),
-        .has_value = false,
         .read_value = GenmcScalarExt::uninit(),
     };
 }
 
 inline LoadResult from_value(SVal read_value) {
-    return LoadResult { .error = std::unique_ptr<std::string>(nullptr),
-                        .has_value = true,
+    return LoadResult { .invalid = false,
+                        .error = std::unique_ptr<std::string>(nullptr),
                         .read_value = GenmcScalarExt::from_sval(read_value) };
 }
 
 inline LoadResult from_error(std::unique_ptr<std::string> error) {
-    return LoadResult { .error = std::move(error),
-                        .has_value = false,
+    return LoadResult { .invalid = false,
+                        .error = std::move(error),
                         .read_value = GenmcScalarExt::uninit() };
 }
+
+inline LoadResult from_invalid() {
+    return LoadResult { .invalid = true, .error = nullptr, .read_value = GenmcScalarExt::uninit() };
+}
+
 } // namespace LoadResultExt
 
 namespace StoreResultExt {
 inline StoreResult ok(bool is_coherence_order_maximal_write) {
-    return StoreResult { /* error: */ std::unique_ptr<std::string>(nullptr),
-                         is_coherence_order_maximal_write };
+    return StoreResult { .invalid = false,
+                         .error = std::unique_ptr<std::string>(nullptr),
+                         .is_coherence_order_maximal_write = is_coherence_order_maximal_write };
 }
 
 inline StoreResult from_error(std::unique_ptr<std::string> error) {
-    return StoreResult { .error = std::move(error), .is_coherence_order_maximal_write = false };
+    return StoreResult { .invalid = false,
+                         .error = std::move(error),
+                         .is_coherence_order_maximal_write = false };
+}
+
+inline StoreResult from_invalid() {
+    return StoreResult { .invalid = true,
+                         .error = nullptr,
+                         .is_coherence_order_maximal_write = false };
 }
 } // namespace StoreResultExt
 
 namespace ReadModifyWriteResultExt {
 inline ReadModifyWriteResult
 ok(SVal old_value, SVal new_value, bool is_coherence_order_maximal_write) {
-    return ReadModifyWriteResult { .error = std::unique_ptr<std::string>(nullptr),
+    return ReadModifyWriteResult { .invalid = false,
+                                   .error = std::unique_ptr<std::string>(nullptr),
                                    .old_value = GenmcScalarExt::from_sval(old_value),
                                    .new_value = GenmcScalarExt::from_sval(new_value),
                                    .is_coherence_order_maximal_write =
                                        is_coherence_order_maximal_write };
 }
 
 inline ReadModifyWriteResult from_error(std::unique_ptr<std::string> error) {
-    return ReadModifyWriteResult { .error = std::move(error),
+    return ReadModifyWriteResult { .invalid = false,
+                                   .error = std::move(error),
+                                   .old_value = GenmcScalarExt::uninit(),
+                                   .new_value = GenmcScalarExt::uninit(),
+                                   .is_coherence_order_maximal_write = false };
+}
+
+inline ReadModifyWriteResult from_invalid() {
+    return ReadModifyWriteResult { .invalid = true,
+                                   .error = nullptr,
                                    .old_value = GenmcScalarExt::uninit(),
                                    .new_value = GenmcScalarExt::uninit(),
                                    .is_coherence_order_maximal_write = false };
@@ -343,22 +354,33 @@ inline ReadModifyWriteResult from_error(std::unique_ptr<std::string> error) {
 
 namespace CompareExchangeResultExt {
 inline CompareExchangeResult success(SVal old_value, bool is_coherence_order_maximal_write) {
-    return CompareExchangeResult { .error = nullptr,
+    return CompareExchangeResult { .invalid = false,
+                                   .error = nullptr,
                                    .old_value = GenmcScalarExt::from_sval(old_value),
                                    .is_success = true,
                                    .is_coherence_order_maximal_write =
                                        is_coherence_order_maximal_write };
 }
 
 inline CompareExchangeResult failure(SVal old_value) {
-    return CompareExchangeResult { .error = nullptr,
+    return CompareExchangeResult { .invalid = false,
+                                   .error = nullptr,
                                    .old_value = GenmcScalarExt::from_sval(old_value),
                                    .is_success = false,
                                    .is_coherence_order_maximal_write = false };
 }
 
 inline CompareExchangeResult from_error(std::unique_ptr<std::string> error) {
-    return CompareExchangeResult { .error = std::move(error),
+    return CompareExchangeResult { .invalid = false,
+                                   .error = std::move(error),
+                                   .old_value = GenmcScalarExt::uninit(),
+                                   .is_success = false,
+                                   .is_coherence_order_maximal_write = false };
+}
+
+inline CompareExchangeResult from_invalid() {
+    return CompareExchangeResult { .invalid = true,
+                                   .error = nullptr,
                                    .old_value = GenmcScalarExt::uninit(),
                                    .is_success = false,
                                    .is_coherence_order_maximal_write = false };
@@ -367,20 +389,42 @@ inline CompareExchangeResult from_error(std::unique_ptr<std::string> error) {
 
 namespace MutexLockResultExt {
 inline MutexLockResult ok(bool is_lock_acquired) {
-    return MutexLockResult { /* error: */ nullptr, /* is_reset: */ false, is_lock_acquired };
+    return MutexLockResult { .invalid = false,
+                             .error = nullptr,
+                             .is_reset = false,
+                             .is_lock_acquired = is_lock_acquired };
 }
 
 inline MutexLockResult reset() {
-    return MutexLockResult { /* error: */ nullptr,
-                             /* is_reset: */ true,
-                             /* is_lock_acquired: */ false };
+    return MutexLockResult { .invalid = false,
+                             .error = nullptr,
+                             .is_reset = true,
+                             .is_lock_acquired = false };
 }
 
 inline MutexLockResult from_error(std::unique_ptr<std::string> error) {
-    return MutexLockResult { /* error: */ std::move(error),
-                             /* is_reset: */ false,
-                             /* is_lock_acquired: */ false };
+    return MutexLockResult { .invalid = false,
+                             .error = std::move(error),
+                             .is_reset = false,
+                             .is_lock_acquired = false };
+}
+
+inline MutexLockResult from_invalid() {
+    return MutexLockResult { .invalid = true,
+                             .error = nullptr,
+                             .is_reset = false,
+                             .is_lock_acquired = false };
 }
 } // namespace MutexLockResultExt
 
+namespace MallocResultExt {
+inline MallocResult ok(SVal addr) {
+    return MallocResult { .error = nullptr, .address = addr.get() };
+}
+
+inline MallocResult from_error(std::unique_ptr<std::string> error) {
+    return MallocResult { .error = std::move(error), .address = 0UL };
+}
+} // namespace MallocResultExt
+
 #endif /* GENMC_MIRI_INTERFACE_HPP */

src/tools/miri/genmc-sys/cpp/include/ResultHandling.hpp

@@ -5,7 +5,7 @@
 #include "rust/cxx.h"
 
 // GenMC headers:
-#include "Verification/VerificationError.hpp"
+#include "genmc/Verification/VerificationError.hpp"
 
 #include <format>
 #include <memory>