miri subtree update

src/tools/miri/.github/workflows/ci.yml

@@ -231,6 +231,9 @@ jobs:
             exit ${exitcode}
           fi
 
+          # Store merge commit message          
+          git log -1 --pretty=%B > message.txt
+
           # Format changes
           ./miri toolchain
           ./miri fmt --check || (./miri fmt && git commit -am "fmt")
@@ -239,7 +242,7 @@ jobs:
           BRANCH="rustup-$(date -u +%Y-%m-%d)"
           git switch -c $BRANCH
           git push -u origin $BRANCH
-          gh pr create -B master --title 'Automatic Rustup' --body "Update \`rustc\` to https://github.com/rust-lang/rust/commit/$(cat rust-version)."
+          gh pr create -B master --title 'Automatic Rustup' --body-file message.txt
         env:
           GITHUB_TOKEN: ${{ steps.app-token.outputs.token }}
 

src/tools/miri/README.md

@@ -246,6 +246,21 @@ such races.
 
 Note: `cargo-nextest` does not support doctests, see https://github.com/nextest-rs/nextest/issues/16
 
+### Directly invoking the `miri` driver
+
+The recommended way to invoke Miri is via `cargo miri`. Directly invoking the underlying `miri`
+driver is not supported, which is why that binary is not even installed into the PATH. However, if
+you need to run Miri on many small tests and want to invoke it directly like you would invoke
+`rustc`, that is still possible with a bit of extra effort:
+
+```sh
+# one-time setup
+cargo +nightly miri setup
+SYSROOT=$(cargo +nightly miri setup --print-sysroot)
+# per file
+~/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/bin/miri --sysroot "$SYSROOT" file.rs
+```
+
 ### Common Problems
 
 When using the above instructions, you may encounter a number of confusing compiler

src/tools/miri/doc/genmc.md

@@ -1,15 +1,26 @@
 # **(WIP)** Documentation for Miri-GenMC
 
+**NOTE: GenMC mode is not yet fully implemented, and has [several correctness issues](https://github.com/rust-lang/miri/issues/4572). Using GenMC mode currently requires manually compiling Miri, see [Usage](#usage).**
+
+
 [GenMC](https://github.com/MPI-SWS/genmc) is a stateless model checker for exploring concurrent executions of a program.
 Miri-GenMC integrates that model checker into Miri.
 
-**NOTE: Currently, no actual GenMC functionality is part of Miri, this is still WIP.**
+Miri in GenMC mode takes a program as input like regular Miri, but instead of running it once, the program is executed repeatedly, until all possible executions allowed by the Rust memory model are explored.
+This includes all possible thread interleavings and all allowed return values for atomic operations, including cases that are very rare to encounter on actual hardware.
+(However, this does not include other sources of non-determinism, such as the absolute addresses of allocations.
+It is hence still possible to have latent bugs in a test case even if they passed GenMC.)
 
-<!-- FIXME(genmc): add explanation. -->
+GenMC requires the input program to be bounded, i.e., have finitely many possible executions, otherwise it will not terminate.
+Any loops that may run infinitely must be replaced or bounded (see below).
+
+GenMC makes use of Dynamic Partial Order Reduction (DPOR) to reduce the number of executions that must be explored, but the runtime can still be super-exponential in the size of the input program (number of threads and amount of interaction between threads).
+Large programs may not be verifiable in a reasonable amount of time.
 
 ## Usage
 
 For testing/developing Miri-GenMC:
+- install all [dependencies required by GenMC](https://github.com/MPI-SWS/genmc?tab=readme-ov-file#dependencies)
 - clone the Miri repo.
 - build Miri-GenMC with `./miri build --features=genmc`.
 - OR: install Miri-GenMC in the current system with `./miri install --features=genmc`
@@ -50,6 +61,66 @@ Note that `cargo miri test` in GenMC mode is currently not supported.
 
 <!-- FIXME(genmc): add tips for using Miri-GenMC more efficiently. -->
 
+### Eliminating unbounded loops
+
+As mentioned above, GenMC requires all loops to be bounded.
+Otherwise, it is not possible to exhaustively explore all executions.
+Currently, Miri-GenMC has no support for automatically bounding loops, so this needs to be done manually.
+
+#### Bounding loops without side effects
+
+The easiest case is that of a loop that simply spins until it observes a certain condition, without any side effects.
+Such loops can be limited to one iteration, as demonstrated by the following example:
+
+```rust
+#[cfg(miri)]
+unsafe extern "Rust" {
+  // This is a special function that Miri provides.
+  // It blocks the thread calling this function if the condition is false.
+  pub unsafe fn miri_genmc_assume(condition: bool);
+}
+
+// This functions loads an atomic boolean in a loop until it is true.
+// GenMC will explore all executions where this does 1, 2, ..., ∞ loads, which means the verification will never terminate.
+fn spin_until_true(flag: &AtomicBool) {
+  while !flag.load(Relaxed) {
+    std::hint::spin_loop();
+  }
+}
+
+// By replacing this loop with an assume statement, the only executions that will be explored are those with exactly 1 load that observes the expected value.
+// Incorrect use of assume statements can lead GenMC to miss important executions, so it is marked `unsafe`.
+fn spin_until_true_genmc(flag: &AtomicBool) {
+  unsafe { miri_genmc_assume(flag.load(Relaxed)) };
+}
+```
+
+#### Bounding loops with side effects
+
+Some loops do contain side effects, meaning the number of explored iterations affects the rest of the program.
+Replacing the loop with one iteration like we did above would mean we miss all those possible executions.
+
+In such a case, the loop can be limited to a fixed number of iterations instead.
+The choice of iteration limit trades off verification time for possibly missing bugs requiring more iterations.
+
+```rust
+/// The loop in this function has a side effect, which is to increment the counter for the number of iterations.
+/// Instead of replacing the loop entirely (which would miss all executions with `count > 0`), we limit the loop to at most 3 iterations.
+fn count_until_true_genmc(flag: &AtomicBool) -> u64 {
+  let mut count = 0;
+  while !flag.load(Relaxed) {
+    count += 1;
+    std::hint::spin_loop();
+    // Any execution that takes more than 3 iterations will not be explored.
+    unsafe { miri_genmc_assume(count <= 3) };
+  }
+  count
+}
+```
+
+<!-- FIXME: update the code above once Miri supports a loop bounding features like GenMC's `--unroll=N`. -->
+<!-- FIXME: update this section once Miri-GenMC supports automatic program transformations (like spinloop-assume replacement). -->
+
 ## Limitations
 
 Some or all of these limitations might get removed in the future:

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://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 = "ce775ccd7866db820fa12ffca66463087a11dd96";
 
     /// 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,17 @@ 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/Mutex.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.

src/tools/miri/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"
@@ -36,6 +35,7 @@ struct LoadResult;
 struct StoreResult;
 struct ReadModifyWriteResult;
 struct CompareExchangeResult;
+struct MutexLockResult;
 
 // GenMC uses `int` for its thread IDs.
 using ThreadId = int;
@@ -126,14 +126,24 @@ 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);
     void handle_thread_join(ThreadId thread_id, ThreadId child_id);
     void handle_thread_finish(ThreadId thread_id, uint64_t ret_val);
     void handle_thread_kill(ThreadId thread_id);
 
+    /**** Blocking instructions ****/
+    /// Inform GenMC that the thread should be blocked.
+    void handle_assume_block(ThreadId thread_id, AssumeType assume_type);
+
+    /**** Mutex handling ****/
+    auto handle_mutex_lock(ThreadId thread_id, uint64_t address, uint64_t size) -> MutexLockResult;
+    auto handle_mutex_try_lock(ThreadId thread_id, uint64_t address, uint64_t size)
+        -> MutexLockResult;
+    auto handle_mutex_unlock(ThreadId thread_id, uint64_t address, uint64_t size) -> StoreResult;
+
     /***** Exploration related functionality *****/
 
     /** Ask the GenMC scheduler for a new thread to schedule and return whether the execution is
@@ -207,9 +217,10 @@ struct MiriGenmcShim : private GenMCDriver {
      * 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, Ts&&... params) -> HandleResult<SVal> {
+    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>(pos, std::forward<Ts>(params)...);
+        const auto ret = GenMCDriver::handleLoad<k>(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);
@@ -250,20 +261,28 @@ 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);
+}
+
+inline std::optional<SVal> try_to_sval(GenmcScalar scalar) {
+    if (scalar.is_init)
+        return { SVal(scalar.value, scalar.extra) };
+    return std::nullopt;
 }
 } // namespace GenmcScalarExt
 
@@ -342,4 +361,22 @@ inline CompareExchangeResult from_error(std::unique_ptr<std::string> error) {
 }
 } // namespace CompareExchangeResultExt
 
+namespace MutexLockResultExt {
+inline MutexLockResult ok(bool is_lock_acquired) {
+    return MutexLockResult { /* error: */ nullptr, /* is_reset: */ false, is_lock_acquired };
+}
+
+inline MutexLockResult reset() {
+    return MutexLockResult { /* 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 };
+}
+} // namespace MutexLockResultExt
+
 #endif /* GENMC_MIRI_INTERFACE_HPP */