From c357b65324e9bb50e72bb15bb159be1df802c360 Mon Sep 17 00:00:00 2001 From: Michalis Kokologiannakis Date: Thu, 27 Nov 2025 20:10:45 +0100 Subject: [PATCH 01/10] genmc/build,api: Move wrappers around GenMC API to single file GenMC has a single API that was handled in a collection of different files. This commit collects all API wrappers to Exploration.cpp. (The Setup.cpp file remains intact as it contains setting translation and setup functions.) --- src/tools/miri/genmc-sys/build.rs | 10 +- .../cpp/src/MiriInterface/EventHandling.cpp | 265 ---------- .../cpp/src/MiriInterface/Exploration.cpp | 458 +++++++++++++++++- .../genmc-sys/cpp/src/MiriInterface/Mutex.cpp | 163 ------- .../src/MiriInterface/ThreadManagement.cpp | 56 --- 5 files changed, 457 insertions(+), 495 deletions(-) delete mode 100644 src/tools/miri/genmc-sys/cpp/src/MiriInterface/EventHandling.cpp delete mode 100644 src/tools/miri/genmc-sys/cpp/src/MiriInterface/Mutex.cpp delete mode 100644 src/tools/miri/genmc-sys/cpp/src/MiriInterface/ThreadManagement.cpp diff --git a/src/tools/miri/genmc-sys/build.rs b/src/tools/miri/genmc-sys/build.rs index 9e956449a13d..1c06387ac928 100644 --- a/src/tools/miri/genmc-sys/build.rs +++ b/src/tools/miri/genmc-sys/build.rs @@ -178,14 +178,8 @@ fn compile_cpp_dependencies(genmc_path: &Path, always_configure: bool) { // 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 = [ - "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 cpp_files = ["MiriInterface/Exploration.cpp", "MiriInterface/Setup.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. diff --git a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/EventHandling.cpp b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/EventHandling.cpp deleted file mode 100644 index 96fb803bcc4e..000000000000 --- a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/EventHandling.cpp +++ /dev/null @@ -1,265 +0,0 @@ -/** This file contains functionality related to handling events encountered - * during an execution, such as loads, stores or memory (de)allocation. */ - -#include "MiriInterface.hpp" - -// CXX.rs generated headers: -#include "genmc-sys/src/lib.rs.h" - -// GenMC headers: -#include "ADT/value_ptr.hpp" -#include "ExecutionGraph/EventLabel.hpp" -#include "ExecutionGraph/LoadAnnotation.hpp" -#include "Runtime/InterpreterEnumAPI.hpp" -#include "Static/ModuleID.hpp" -#include "Support/ASize.hpp" -#include "Support/Error.hpp" -#include "Support/Logger.hpp" -#include "Support/MemAccess.hpp" -#include "Support/RMWOps.hpp" -#include "Support/SAddr.hpp" -#include "Support/SVal.hpp" -#include "Support/ThreadInfo.hpp" -#include "Support/Verbosity.hpp" -#include "Verification/GenMCDriver.hpp" -#include "Verification/MemoryModel.hpp" - -// C++ headers: -#include -#include -#include -#include - -/**** Blocking instructions ****/ - -void MiriGenmcShim::handle_assume_block(ThreadId thread_id, AssumeType assume_type) { - BUG_ON(getExec().getGraph().isThreadBlocked(thread_id)); - GenMCDriver::handleAssume(nullptr, inc_pos(thread_id), assume_type); -} - -/**** Memory access handling ****/ - -[[nodiscard]] auto MiriGenmcShim::handle_load( - ThreadId thread_id, - uint64_t address, - uint64_t size, - MemOrdering ord, - GenmcScalar old_val -) -> LoadResult { - // `type` is only used for printing. - const auto type = AType::Unsigned; - const auto ret = handle_load_reset_if_none( - thread_id, - GenmcScalarExt::try_to_sval(old_val), - ord, - SAddr(address), - ASize(size), - type - ); - - if (const auto* err = std::get_if(&ret)) - return LoadResultExt::from_error(format_error(*err)); - const auto* ret_val = std::get_if(&ret); - // FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values. - if (ret_val == nullptr) - ERROR("Unimplemented: load returned unexpected result."); - return LoadResultExt::from_value(*ret_val); -} - -[[nodiscard]] auto MiriGenmcShim::handle_store( - ThreadId thread_id, - uint64_t address, - uint64_t size, - GenmcScalar value, - GenmcScalar old_val, - MemOrdering ord -) -> StoreResult { - const auto pos = inc_pos(thread_id); - const auto ret = GenMCDriver::handleStore( - nullptr, - pos, - GenmcScalarExt::try_to_sval(old_val), - ord, - SAddr(address), - ASize(size), - /* type */ AType::Unsigned, // `type` is only used for printing. - GenmcScalarExt::to_sval(value), - EventDeps() - ); - - if (const auto* err = std::get_if(&ret)) - return StoreResultExt::from_error(format_error(*err)); - - const bool* is_coherence_order_maximal_write = std::get_if(&ret); - // FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values. - ERROR_ON( - nullptr == is_coherence_order_maximal_write, - "Unimplemented: Store returned unexpected result." - ); - return StoreResultExt::ok(*is_coherence_order_maximal_write); -} - -void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) { - const auto pos = inc_pos(thread_id); - GenMCDriver::handleFence(nullptr, pos, ord, EventDeps()); -} - -[[nodiscard]] auto MiriGenmcShim::handle_read_modify_write( - ThreadId thread_id, - uint64_t address, - uint64_t size, - RMWBinOp rmw_op, - MemOrdering ordering, - GenmcScalar rhs_value, - GenmcScalar old_val -) -> ReadModifyWriteResult { - // NOTE: Both the store and load events should get the same `ordering`, it should not be split - // into a load and a store component. This means we can have for example `AcqRel` loads and - // stores, but this is intended for RMW operations. - - // Somewhat confusingly, the GenMC term for RMW read/write labels is - // `FaiRead` and `FaiWrite`. - const auto load_ret = handle_load_reset_if_none( - thread_id, - GenmcScalarExt::try_to_sval(old_val), - ordering, - SAddr(address), - ASize(size), - AType::Unsigned, // The type is only used for printing. - rmw_op, - GenmcScalarExt::to_sval(rhs_value), - EventDeps() - ); - if (const auto* err = std::get_if(&load_ret)) - return ReadModifyWriteResultExt::from_error(format_error(*err)); - - const auto* ret_val = std::get_if(&load_ret); - // FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values. - if (nullptr == ret_val) { - ERROR("Unimplemented: read-modify-write returned unexpected result."); - } - const auto read_old_val = *ret_val; - const auto new_value = - executeRMWBinOp(read_old_val, GenmcScalarExt::to_sval(rhs_value), size, rmw_op); - - const auto storePos = inc_pos(thread_id); - const auto store_ret = GenMCDriver::handleStore( - nullptr, - storePos, - GenmcScalarExt::try_to_sval(old_val), - ordering, - SAddr(address), - ASize(size), - AType::Unsigned, // The type is only used for printing. - new_value - ); - if (const auto* err = std::get_if(&store_ret)) - return ReadModifyWriteResultExt::from_error(format_error(*err)); - - const bool* is_coherence_order_maximal_write = std::get_if(&store_ret); - // FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values. - ERROR_ON( - nullptr == is_coherence_order_maximal_write, - "Unimplemented: RMW store returned unexpected result." - ); - return ReadModifyWriteResultExt::ok( - /* old_value: */ read_old_val, - new_value, - *is_coherence_order_maximal_write - ); -} - -[[nodiscard]] auto MiriGenmcShim::handle_compare_exchange( - ThreadId thread_id, - uint64_t address, - uint64_t size, - GenmcScalar expected_value, - GenmcScalar new_value, - GenmcScalar old_val, - MemOrdering success_ordering, - MemOrdering fail_load_ordering, - bool can_fail_spuriously -) -> CompareExchangeResult { - // NOTE: Both the store and load events should get the same `ordering`, it should not be split - // into a load and a store component. This means we can have for example `AcqRel` loads and - // stores, but this is intended for CAS operations. - - // FIXME(GenMC): properly handle failure memory ordering. - - auto expectedVal = GenmcScalarExt::to_sval(expected_value); - auto new_val = GenmcScalarExt::to_sval(new_value); - - const auto load_ret = handle_load_reset_if_none( - thread_id, - GenmcScalarExt::try_to_sval(old_val), - success_ordering, - SAddr(address), - ASize(size), - AType::Unsigned, // The type is only used for printing. - expectedVal, - new_val - ); - if (const auto* err = std::get_if(&load_ret)) - return CompareExchangeResultExt::from_error(format_error(*err)); - const auto* ret_val = std::get_if(&load_ret); - // FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values. - ERROR_ON(nullptr == ret_val, "Unimplemented: load returned unexpected result."); - const auto read_old_val = *ret_val; - if (read_old_val != expectedVal) - return CompareExchangeResultExt::failure(read_old_val); - - // FIXME(GenMC): Add support for modelling spurious failures. - - const auto storePos = inc_pos(thread_id); - const auto store_ret = GenMCDriver::handleStore( - nullptr, - storePos, - GenmcScalarExt::try_to_sval(old_val), - success_ordering, - SAddr(address), - ASize(size), - AType::Unsigned, // The type is only used for printing. - new_val - ); - if (const auto* err = std::get_if(&store_ret)) - return CompareExchangeResultExt::from_error(format_error(*err)); - const bool* is_coherence_order_maximal_write = std::get_if(&store_ret); - // FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values. - ERROR_ON( - nullptr == is_coherence_order_maximal_write, - "Unimplemented: compare-exchange store returned unexpected result." - ); - return CompareExchangeResultExt::success(read_old_val, *is_coherence_order_maximal_write); -} - -/**** Memory (de)allocation ****/ - -auto MiriGenmcShim::handle_malloc(ThreadId thread_id, uint64_t size, uint64_t alignment) - -> uint64_t { - const auto pos = inc_pos(thread_id); - - // These are only used for printing and features Miri-GenMC doesn't support (yet). - const auto storage_duration = StorageDuration::SD_Heap; - // Volatile, as opposed to "persistent" (i.e., non-volatile memory that persists over reboots) - const auto storage_type = StorageType::ST_Volatile; - const auto address_space = AddressSpace::AS_User; - - const SVal ret_val = GenMCDriver::handleMalloc( - nullptr, - pos, - size, - alignment, - storage_duration, - storage_type, - address_space, - EventDeps() - ); - return ret_val.get(); -} - -auto MiriGenmcShim::handle_free(ThreadId thread_id, uint64_t address) -> bool { - const auto pos = inc_pos(thread_id); - GenMCDriver::handleFree(nullptr, pos, SAddr(address), EventDeps()); - // FIXME(genmc): use returned error from `handleFree` once implemented in GenMC. - return getResult().status.has_value(); -} diff --git a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp index 7722c4bfab69..a052ef491dc3 100644 --- a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp +++ b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp @@ -1,4 +1,5 @@ -/** This file contains functionality related to exploration, such as scheduling. */ +/** This file contains functionality related to exploration events + * such as loads, stores and memory (de)allocation. */ #include "MiriInterface.hpp" @@ -6,13 +7,32 @@ #include "genmc-sys/src/lib.rs.h" // GenMC headers: +#include "ADT/value_ptr.hpp" +#include "ExecutionGraph/EventLabel.hpp" +#include "ExecutionGraph/LoadAnnotation.hpp" +#include "Runtime/InterpreterEnumAPI.hpp" +#include "Static/ModuleID.hpp" +#include "Support/ASize.hpp" #include "Support/Error.hpp" +#include "Support/Logger.hpp" +#include "Support/MemAccess.hpp" +#include "Support/RMWOps.hpp" +#include "Support/SAddr.hpp" +#include "Support/SVal.hpp" +#include "Support/ThreadInfo.hpp" #include "Support/Verbosity.hpp" +#include "Verification/GenMCDriver.hpp" +#include "Verification/MemoryModel.hpp" // C++ headers: #include +#include #include #include +#include +#include + +/** Scheduling */ auto MiriGenmcShim::schedule_next( const int curr_thread_id, @@ -41,8 +61,6 @@ auto MiriGenmcShim::schedule_next( ); } -/**** Execution start/end handling ****/ - void MiriGenmcShim::handle_execution_start() { threads_action_.clear(); threads_action_.push_back(Action(ActionKind::Load, Event::getInit())); @@ -55,6 +73,240 @@ auto MiriGenmcShim::handle_execution_end() -> std::unique_ptr { return {}; } +/**** Blocking instructions ****/ + +void MiriGenmcShim::handle_assume_block(ThreadId thread_id, AssumeType assume_type) { + BUG_ON(getExec().getGraph().isThreadBlocked(thread_id)); + GenMCDriver::handleAssume(nullptr, inc_pos(thread_id), assume_type); +} + +/**** Memory access handling ****/ + +[[nodiscard]] auto MiriGenmcShim::handle_load( + ThreadId thread_id, + uint64_t address, + uint64_t size, + MemOrdering ord, + GenmcScalar old_val +) -> LoadResult { + // `type` is only used for printing. + const auto type = AType::Unsigned; + const auto ret = handle_load_reset_if_none( + thread_id, + GenmcScalarExt::try_to_sval(old_val), + ord, + SAddr(address), + ASize(size), + type + ); + + if (const auto* err = std::get_if(&ret)) + return LoadResultExt::from_error(format_error(*err)); + const auto* ret_val = std::get_if(&ret); + // FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values. + if (ret_val == nullptr) + ERROR("Unimplemented: load returned unexpected result."); + return LoadResultExt::from_value(*ret_val); +} + +[[nodiscard]] auto MiriGenmcShim::handle_store( + ThreadId thread_id, + uint64_t address, + uint64_t size, + GenmcScalar value, + GenmcScalar old_val, + MemOrdering ord +) -> StoreResult { + const auto pos = inc_pos(thread_id); + const auto ret = GenMCDriver::handleStore( + nullptr, + pos, + GenmcScalarExt::try_to_sval(old_val), + ord, + SAddr(address), + ASize(size), + /* type */ AType::Unsigned, // `type` is only used for printing. + GenmcScalarExt::to_sval(value), + EventDeps() + ); + + if (const auto* err = std::get_if(&ret)) + return StoreResultExt::from_error(format_error(*err)); + + const bool* is_coherence_order_maximal_write = std::get_if(&ret); + // FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values. + ERROR_ON( + nullptr == is_coherence_order_maximal_write, + "Unimplemented: Store returned unexpected result." + ); + return StoreResultExt::ok(*is_coherence_order_maximal_write); +} + +void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) { + const auto pos = inc_pos(thread_id); + GenMCDriver::handleFence(nullptr, pos, ord, EventDeps()); +} + +[[nodiscard]] auto MiriGenmcShim::handle_read_modify_write( + ThreadId thread_id, + uint64_t address, + uint64_t size, + RMWBinOp rmw_op, + MemOrdering ordering, + GenmcScalar rhs_value, + GenmcScalar old_val +) -> ReadModifyWriteResult { + // NOTE: Both the store and load events should get the same `ordering`, it should not be split + // into a load and a store component. This means we can have for example `AcqRel` loads and + // stores, but this is intended for RMW operations. + + // Somewhat confusingly, the GenMC term for RMW read/write labels is + // `FaiRead` and `FaiWrite`. + const auto load_ret = handle_load_reset_if_none( + thread_id, + GenmcScalarExt::try_to_sval(old_val), + ordering, + SAddr(address), + ASize(size), + AType::Unsigned, // The type is only used for printing. + rmw_op, + GenmcScalarExt::to_sval(rhs_value), + EventDeps() + ); + if (const auto* err = std::get_if(&load_ret)) + return ReadModifyWriteResultExt::from_error(format_error(*err)); + + const auto* ret_val = std::get_if(&load_ret); + // FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values. + if (nullptr == ret_val) { + ERROR("Unimplemented: read-modify-write returned unexpected result."); + } + const auto read_old_val = *ret_val; + const auto new_value = + executeRMWBinOp(read_old_val, GenmcScalarExt::to_sval(rhs_value), size, rmw_op); + + const auto storePos = inc_pos(thread_id); + const auto store_ret = GenMCDriver::handleStore( + nullptr, + storePos, + GenmcScalarExt::try_to_sval(old_val), + ordering, + SAddr(address), + ASize(size), + AType::Unsigned, // The type is only used for printing. + new_value + ); + if (const auto* err = std::get_if(&store_ret)) + return ReadModifyWriteResultExt::from_error(format_error(*err)); + + const bool* is_coherence_order_maximal_write = std::get_if(&store_ret); + // FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values. + ERROR_ON( + nullptr == is_coherence_order_maximal_write, + "Unimplemented: RMW store returned unexpected result." + ); + return ReadModifyWriteResultExt::ok( + /* old_value: */ read_old_val, + new_value, + *is_coherence_order_maximal_write + ); +} + +[[nodiscard]] auto MiriGenmcShim::handle_compare_exchange( + ThreadId thread_id, + uint64_t address, + uint64_t size, + GenmcScalar expected_value, + GenmcScalar new_value, + GenmcScalar old_val, + MemOrdering success_ordering, + MemOrdering fail_load_ordering, + bool can_fail_spuriously +) -> CompareExchangeResult { + // NOTE: Both the store and load events should get the same `ordering`, it should not be split + // into a load and a store component. This means we can have for example `AcqRel` loads and + // stores, but this is intended for CAS operations. + + // FIXME(GenMC): properly handle failure memory ordering. + + auto expectedVal = GenmcScalarExt::to_sval(expected_value); + auto new_val = GenmcScalarExt::to_sval(new_value); + + const auto load_ret = handle_load_reset_if_none( + thread_id, + GenmcScalarExt::try_to_sval(old_val), + success_ordering, + SAddr(address), + ASize(size), + AType::Unsigned, // The type is only used for printing. + expectedVal, + new_val + ); + if (const auto* err = std::get_if(&load_ret)) + return CompareExchangeResultExt::from_error(format_error(*err)); + const auto* ret_val = std::get_if(&load_ret); + // FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values. + ERROR_ON(nullptr == ret_val, "Unimplemented: load returned unexpected result."); + const auto read_old_val = *ret_val; + if (read_old_val != expectedVal) + return CompareExchangeResultExt::failure(read_old_val); + + // FIXME(GenMC): Add support for modelling spurious failures. + + const auto storePos = inc_pos(thread_id); + const auto store_ret = GenMCDriver::handleStore( + nullptr, + storePos, + GenmcScalarExt::try_to_sval(old_val), + success_ordering, + SAddr(address), + ASize(size), + AType::Unsigned, // The type is only used for printing. + new_val + ); + if (const auto* err = std::get_if(&store_ret)) + return CompareExchangeResultExt::from_error(format_error(*err)); + const bool* is_coherence_order_maximal_write = std::get_if(&store_ret); + // FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values. + ERROR_ON( + nullptr == is_coherence_order_maximal_write, + "Unimplemented: compare-exchange store returned unexpected result." + ); + return CompareExchangeResultExt::success(read_old_val, *is_coherence_order_maximal_write); +} + +/**** Memory (de)allocation ****/ + +auto MiriGenmcShim::handle_malloc(ThreadId thread_id, uint64_t size, uint64_t alignment) + -> uint64_t { + const auto pos = inc_pos(thread_id); + + // These are only used for printing and features Miri-GenMC doesn't support (yet). + const auto storage_duration = StorageDuration::SD_Heap; + // Volatile, as opposed to "persistent" (i.e., non-volatile memory that persists over reboots) + const auto storage_type = StorageType::ST_Volatile; + const auto address_space = AddressSpace::AS_User; + + const SVal ret_val = GenMCDriver::handleMalloc( + nullptr, + pos, + size, + alignment, + storage_duration, + storage_type, + address_space, + EventDeps() + ); + return ret_val.get(); +} + +auto MiriGenmcShim::handle_free(ThreadId thread_id, uint64_t address) -> bool { + const auto pos = inc_pos(thread_id); + GenMCDriver::handleFree(nullptr, pos, SAddr(address), EventDeps()); + // FIXME(genmc): use returned error from `handleFree` once implemented in GenMC. + return getResult().status.has_value(); +} + /**** Estimation mode result ****/ auto MiriGenmcShim::get_estimation_results() const -> EstimationResult { @@ -66,3 +318,203 @@ auto MiriGenmcShim::get_estimation_results() const -> EstimationResult { .blocked_execs = static_cast(res.exploredBlocked), }; } + +/** Mutexes */ + +#define MUTEX_UNLOCKED SVal(0) +#define MUTEX_LOCKED SVal(1) + +auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint64_t size) + -> MutexLockResult { + // 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::create( + // `RegisterExpr` marks the value of the current expression, i.e., the loaded value. + // The `id` is ignored by GenMC; it is only used by the LLI frontend to substitute + // other variables from previous expressions that may be used here. + RegisterExpr::create(size_bits, /* id */ 0), + ConcreteExpr::create(size_bits, MUTEX_LOCKED) + ) + .release() + ) + )); + + // As usual, we need to tell GenMC which value was stored at this location before this atomic + // access, if there previously was a non-atomic initializing access. We set the initial state of + // a mutex to be "unlocked". + const auto old_val = MUTEX_UNLOCKED; + const auto load_ret = handle_load_reset_if_none( + thread_id, + old_val, + address, + size, + annot, + EventDeps() + ); + if (const auto* err = std::get_if(&load_ret)) + return MutexLockResultExt::from_error(format_error(*err)); + // If we get a `Reset`, GenMC decided that this lock operation should not yet run, since it + // would not acquire the mutex. Like the handling of the case further down where we read a `1` + // ("Mutex already locked"), Miri should call the handle function again once the current thread + // is scheduled by GenMC the next time. + if (std::holds_alternative(load_ret)) + return MutexLockResultExt::reset(); + + const auto* ret_val = std::get_if(&load_ret); + ERROR_ON(!ret_val, "Unimplemented: mutex lock returned unexpected result."); + ERROR_ON( + *ret_val != MUTEX_UNLOCKED && *ret_val != MUTEX_LOCKED, + "Mutex read value was neither 0 nor 1" + ); + const bool is_lock_acquired = *ret_val == MUTEX_UNLOCKED; + if (is_lock_acquired) { + const auto store_ret = GenMCDriver::handleStore( + nullptr, + inc_pos(thread_id), + old_val, + address, + size, + EventDeps() + ); + if (const auto* err = std::get_if(&store_ret)) + return MutexLockResultExt::from_error(format_error(*err)); + // We don't update Miri's memory for this operation so we don't need to know if the store + // was the co-maximal store, but we still check that we at least get a boolean as the result + // of the store. + const bool* is_coherence_order_maximal_write = std::get_if(&store_ret); + ERROR_ON( + nullptr == is_coherence_order_maximal_write, + "Unimplemented: store part of mutex try_lock returned unexpected result." + ); + } else { + // We did not acquire the mutex, so we tell GenMC to block the thread until we can acquire + // it. GenMC determines this based on the annotation we pass with the load further up in + // this function, namely when that load will read a value other than `MUTEX_LOCKED`. + this->handle_assume_block(thread_id, AssumeType::Spinloop); + } + return MutexLockResultExt::ok(is_lock_acquired); +} + +auto MiriGenmcShim::handle_mutex_try_lock(ThreadId thread_id, uint64_t address, uint64_t size) + -> MutexLockResult { + auto& currPos = threads_action_[thread_id].event; + // As usual, we need to tell GenMC which value was stored at this location before this atomic + // access, if there previously was a non-atomic initializing access. We set the initial state of + // a mutex to be "unlocked". + const auto old_val = MUTEX_UNLOCKED; + const auto load_ret = GenMCDriver::handleLoad( + nullptr, + ++currPos, + old_val, + SAddr(address), + ASize(size) + ); + if (const auto* err = std::get_if(&load_ret)) + return MutexLockResultExt::from_error(format_error(*err)); + const auto* ret_val = std::get_if(&load_ret); + if (nullptr == ret_val) { + ERROR("Unimplemented: mutex trylock load returned unexpected result."); + } + + ERROR_ON( + *ret_val != MUTEX_UNLOCKED && *ret_val != MUTEX_LOCKED, + "Mutex read value was neither 0 nor 1" + ); + const bool is_lock_acquired = *ret_val == MUTEX_UNLOCKED; + if (!is_lock_acquired) { + return MutexLockResultExt::ok(false); /* Lock already held. */ + } + + const auto store_ret = GenMCDriver::handleStore( + nullptr, + ++currPos, + old_val, + SAddr(address), + ASize(size) + ); + if (const auto* err = std::get_if(&store_ret)) + return MutexLockResultExt::from_error(format_error(*err)); + // We don't update Miri's memory for this operation so we don't need to know if the store was + // co-maximal, but we still check that we get a boolean result. + const bool* is_coherence_order_maximal_write = std::get_if(&store_ret); + ERROR_ON( + nullptr == is_coherence_order_maximal_write, + "Unimplemented: store part of mutex try_lock returned unexpected result." + ); + return MutexLockResultExt::ok(true); +} + +auto MiriGenmcShim::handle_mutex_unlock(ThreadId thread_id, uint64_t address, uint64_t size) + -> StoreResult { + const auto pos = inc_pos(thread_id); + const auto ret = GenMCDriver::handleStore( + nullptr, + pos, + // As usual, we need to tell GenMC which value was stored at this location before this + // atomic access, if there previously was a non-atomic initializing access. We set the + // initial state of a mutex to be "unlocked". + /* old_val */ MUTEX_UNLOCKED, + MemOrdering::Release, + SAddr(address), + ASize(size), + AType::Signed, + /* store_value */ MUTEX_UNLOCKED, + EventDeps() + ); + if (const auto* err = std::get_if(&ret)) + return StoreResultExt::from_error(format_error(*err)); + const bool* is_coherence_order_maximal_write = std::get_if(&ret); + ERROR_ON( + nullptr == is_coherence_order_maximal_write, + "Unimplemented: store part of mutex unlock returned unexpected result." + ); + return StoreResultExt::ok(*is_coherence_order_maximal_write); +} + +/** Thread creation/joining */ + +void MiriGenmcShim::handle_thread_create(ThreadId thread_id, ThreadId parent_id) { + // NOTE: The threadCreate event happens in the parent: + const auto pos = inc_pos(parent_id); + // FIXME(genmc): for supporting symmetry reduction, these will need to be properly set: + const unsigned fun_id = 0; + const SVal arg = SVal(0); + const ThreadInfo child_info = + ThreadInfo { thread_id, parent_id, fun_id, arg, "unknown thread" }; + + // NOTE: Default memory ordering (`Release`) used here. + const auto child_tid = GenMCDriver::handleThreadCreate(nullptr, pos, child_info, EventDeps()); + // Sanity check the thread id, which is the index in the `threads_action_` array. + BUG_ON(child_tid != thread_id || child_tid <= 0 || child_tid != threads_action_.size()); + threads_action_.push_back(Action(ActionKind::Load, Event(child_tid, 0))); +} + +void MiriGenmcShim::handle_thread_join(ThreadId thread_id, ThreadId child_id) { + // The thread join event happens in the parent. + const auto pos = inc_pos(thread_id); + + // NOTE: Default memory ordering (`Acquire`) used here. + const auto ret = GenMCDriver::handleThreadJoin(nullptr, pos, child_id, EventDeps()); + // If the join failed, decrease the event index again: + if (!std::holds_alternative(ret)) { + dec_pos(thread_id); + } + // FIXME(genmc): handle `HandleResult::{Invalid, Reset, VerificationError}` return values. + + // NOTE: Thread return value is ignored, since Miri doesn't need it. +} + +void MiriGenmcShim::handle_thread_finish(ThreadId thread_id, uint64_t ret_val) { + const auto pos = inc_pos(thread_id); + // NOTE: Default memory ordering (`Release`) used here. + GenMCDriver::handleThreadFinish(nullptr, pos, SVal(ret_val)); +} + +void MiriGenmcShim::handle_thread_kill(ThreadId thread_id) { + const auto pos = inc_pos(thread_id); + GenMCDriver::handleThreadKill(nullptr, pos); +} diff --git a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Mutex.cpp b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Mutex.cpp deleted file mode 100644 index af7e30186cbe..000000000000 --- a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Mutex.cpp +++ /dev/null @@ -1,163 +0,0 @@ -/** This file contains functionality related to handling mutexes. */ - -#include "MiriInterface.hpp" - -// GenMC headers: -#include "Static/ModuleID.hpp" - -// CXX.rs generated headers: -#include "genmc-sys/src/lib.rs.h" - -#define MUTEX_UNLOCKED SVal(0) -#define MUTEX_LOCKED SVal(1) - -auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint64_t size) - -> MutexLockResult { - // 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::create( - // `RegisterExpr` marks the value of the current expression, i.e., the loaded value. - // The `id` is ignored by GenMC; it is only used by the LLI frontend to substitute - // other variables from previous expressions that may be used here. - RegisterExpr::create(size_bits, /* id */ 0), - ConcreteExpr::create(size_bits, MUTEX_LOCKED) - ) - .release() - ) - )); - - // As usual, we need to tell GenMC which value was stored at this location before this atomic - // access, if there previously was a non-atomic initializing access. We set the initial state of - // a mutex to be "unlocked". - const auto old_val = MUTEX_UNLOCKED; - const auto load_ret = handle_load_reset_if_none( - thread_id, - old_val, - address, - size, - annot, - EventDeps() - ); - if (const auto* err = std::get_if(&load_ret)) - return MutexLockResultExt::from_error(format_error(*err)); - // If we get a `Reset`, GenMC decided that this lock operation should not yet run, since it - // would not acquire the mutex. Like the handling of the case further down where we read a `1` - // ("Mutex already locked"), Miri should call the handle function again once the current thread - // is scheduled by GenMC the next time. - if (std::holds_alternative(load_ret)) - return MutexLockResultExt::reset(); - - const auto* ret_val = std::get_if(&load_ret); - ERROR_ON(!ret_val, "Unimplemented: mutex lock returned unexpected result."); - ERROR_ON( - *ret_val != MUTEX_UNLOCKED && *ret_val != MUTEX_LOCKED, - "Mutex read value was neither 0 nor 1" - ); - const bool is_lock_acquired = *ret_val == MUTEX_UNLOCKED; - if (is_lock_acquired) { - const auto store_ret = GenMCDriver::handleStore( - nullptr, - inc_pos(thread_id), - old_val, - address, - size, - EventDeps() - ); - if (const auto* err = std::get_if(&store_ret)) - return MutexLockResultExt::from_error(format_error(*err)); - // We don't update Miri's memory for this operation so we don't need to know if the store - // was the co-maximal store, but we still check that we at least get a boolean as the result - // of the store. - const bool* is_coherence_order_maximal_write = std::get_if(&store_ret); - ERROR_ON( - nullptr == is_coherence_order_maximal_write, - "Unimplemented: store part of mutex try_lock returned unexpected result." - ); - } else { - // We did not acquire the mutex, so we tell GenMC to block the thread until we can acquire - // it. GenMC determines this based on the annotation we pass with the load further up in - // this function, namely when that load will read a value other than `MUTEX_LOCKED`. - this->handle_assume_block(thread_id, AssumeType::Spinloop); - } - return MutexLockResultExt::ok(is_lock_acquired); -} - -auto MiriGenmcShim::handle_mutex_try_lock(ThreadId thread_id, uint64_t address, uint64_t size) - -> MutexLockResult { - auto& currPos = threads_action_[thread_id].event; - // As usual, we need to tell GenMC which value was stored at this location before this atomic - // access, if there previously was a non-atomic initializing access. We set the initial state of - // a mutex to be "unlocked". - const auto old_val = MUTEX_UNLOCKED; - const auto load_ret = GenMCDriver::handleLoad( - nullptr, - ++currPos, - old_val, - SAddr(address), - ASize(size) - ); - if (const auto* err = std::get_if(&load_ret)) - return MutexLockResultExt::from_error(format_error(*err)); - const auto* ret_val = std::get_if(&load_ret); - if (nullptr == ret_val) { - ERROR("Unimplemented: mutex trylock load returned unexpected result."); - } - - ERROR_ON( - *ret_val != MUTEX_UNLOCKED && *ret_val != MUTEX_LOCKED, - "Mutex read value was neither 0 nor 1" - ); - const bool is_lock_acquired = *ret_val == MUTEX_UNLOCKED; - if (!is_lock_acquired) { - return MutexLockResultExt::ok(false); /* Lock already held. */ - } - - const auto store_ret = GenMCDriver::handleStore( - nullptr, - ++currPos, - old_val, - SAddr(address), - ASize(size) - ); - if (const auto* err = std::get_if(&store_ret)) - return MutexLockResultExt::from_error(format_error(*err)); - // We don't update Miri's memory for this operation so we don't need to know if the store was - // co-maximal, but we still check that we get a boolean result. - const bool* is_coherence_order_maximal_write = std::get_if(&store_ret); - ERROR_ON( - nullptr == is_coherence_order_maximal_write, - "Unimplemented: store part of mutex try_lock returned unexpected result." - ); - return MutexLockResultExt::ok(true); -} - -auto MiriGenmcShim::handle_mutex_unlock(ThreadId thread_id, uint64_t address, uint64_t size) - -> StoreResult { - const auto pos = inc_pos(thread_id); - const auto ret = GenMCDriver::handleStore( - nullptr, - pos, - // As usual, we need to tell GenMC which value was stored at this location before this - // atomic access, if there previously was a non-atomic initializing access. We set the - // initial state of a mutex to be "unlocked". - /* old_val */ MUTEX_UNLOCKED, - MemOrdering::Release, - SAddr(address), - ASize(size), - AType::Signed, - /* store_value */ MUTEX_UNLOCKED, - EventDeps() - ); - if (const auto* err = std::get_if(&ret)) - return StoreResultExt::from_error(format_error(*err)); - const bool* is_coherence_order_maximal_write = std::get_if(&ret); - ERROR_ON( - nullptr == is_coherence_order_maximal_write, - "Unimplemented: store part of mutex unlock returned unexpected result." - ); - return StoreResultExt::ok(*is_coherence_order_maximal_write); -} diff --git a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/ThreadManagement.cpp b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/ThreadManagement.cpp deleted file mode 100644 index 85fc7d92f78f..000000000000 --- a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/ThreadManagement.cpp +++ /dev/null @@ -1,56 +0,0 @@ - -/** This file contains functionality related thread management (creation, finishing, join, etc.) */ - -#include "MiriInterface.hpp" - -// CXX.rs generated headers: -#include "genmc-sys/src/lib.rs.h" - -// GenMC headers: -#include "Support/Error.hpp" -#include "Support/Verbosity.hpp" - -// C++ headers: -#include - -void MiriGenmcShim::handle_thread_create(ThreadId thread_id, ThreadId parent_id) { - // NOTE: The threadCreate event happens in the parent: - const auto pos = inc_pos(parent_id); - // FIXME(genmc): for supporting symmetry reduction, these will need to be properly set: - const unsigned fun_id = 0; - const SVal arg = SVal(0); - const ThreadInfo child_info = - ThreadInfo { thread_id, parent_id, fun_id, arg, "unknown thread" }; - - // NOTE: Default memory ordering (`Release`) used here. - const auto child_tid = GenMCDriver::handleThreadCreate(nullptr, pos, child_info, EventDeps()); - // Sanity check the thread id, which is the index in the `threads_action_` array. - BUG_ON(child_tid != thread_id || child_tid <= 0 || child_tid != threads_action_.size()); - threads_action_.push_back(Action(ActionKind::Load, Event(child_tid, 0))); -} - -void MiriGenmcShim::handle_thread_join(ThreadId thread_id, ThreadId child_id) { - // The thread join event happens in the parent. - const auto pos = inc_pos(thread_id); - - // NOTE: Default memory ordering (`Acquire`) used here. - const auto ret = GenMCDriver::handleThreadJoin(nullptr, pos, child_id, EventDeps()); - // If the join failed, decrease the event index again: - if (!std::holds_alternative(ret)) { - dec_pos(thread_id); - } - // FIXME(genmc): handle `HandleResult::{Invalid, Reset, VerificationError}` return values. - - // NOTE: Thread return value is ignored, since Miri doesn't need it. -} - -void MiriGenmcShim::handle_thread_finish(ThreadId thread_id, uint64_t ret_val) { - const auto pos = inc_pos(thread_id); - // NOTE: Default memory ordering (`Release`) used here. - GenMCDriver::handleThreadFinish(nullptr, pos, SVal(ret_val)); -} - -void MiriGenmcShim::handle_thread_kill(ThreadId thread_id) { - const auto pos = inc_pos(thread_id); - GenMCDriver::handleThreadKill(nullptr, pos); -} From e2c62e49c1c3fdca2cd1c9bf2b71985e09389c42 Mon Sep 17 00:00:00 2001 From: Michalis Kokologiannakis Date: Thu, 27 Nov 2025 20:19:10 +0100 Subject: [PATCH 02/10] genmc/api: Use ERROR_ON instead of if (cond) ERROR() This commit makes the code a bit more compact by using ERROR_ON() whenever possible. It also renames a particularly verbose variable used in ERROR's condition. --- .../cpp/src/MiriInterface/Exploration.cpp | 64 ++++++------------- 1 file changed, 20 insertions(+), 44 deletions(-) diff --git a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp index a052ef491dc3..809ec77b94f0 100644 --- a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp +++ b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp @@ -104,8 +104,7 @@ void MiriGenmcShim::handle_assume_block(ThreadId thread_id, AssumeType assume_ty return LoadResultExt::from_error(format_error(*err)); const auto* ret_val = std::get_if(&ret); // FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values. - if (ret_val == nullptr) - ERROR("Unimplemented: load returned unexpected result."); + ERROR_ON(!ret_val, "Unimplemented: load returned unexpected result."); return LoadResultExt::from_value(*ret_val); } @@ -133,13 +132,10 @@ void MiriGenmcShim::handle_assume_block(ThreadId thread_id, AssumeType assume_ty if (const auto* err = std::get_if(&ret)) return StoreResultExt::from_error(format_error(*err)); - const bool* is_coherence_order_maximal_write = std::get_if(&ret); + const auto* is_co_max = std::get_if(&ret); // FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values. - ERROR_ON( - nullptr == is_coherence_order_maximal_write, - "Unimplemented: Store returned unexpected result." - ); - return StoreResultExt::ok(*is_coherence_order_maximal_write); + ERROR_ON(!is_co_max, "Unimplemented: Store returned unexpected result."); + return StoreResultExt::ok(*is_co_max); } void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) { @@ -178,9 +174,7 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) { const auto* ret_val = std::get_if(&load_ret); // FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values. - if (nullptr == ret_val) { - ERROR("Unimplemented: read-modify-write returned unexpected result."); - } + ERROR_ON(!ret_val, "Unimplemented: read-modify-write returned unexpected result."); const auto read_old_val = *ret_val; const auto new_value = executeRMWBinOp(read_old_val, GenmcScalarExt::to_sval(rhs_value), size, rmw_op); @@ -199,16 +193,13 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) { if (const auto* err = std::get_if(&store_ret)) return ReadModifyWriteResultExt::from_error(format_error(*err)); - const bool* is_coherence_order_maximal_write = std::get_if(&store_ret); + const auto* is_co_max = std::get_if(&store_ret); // FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values. - ERROR_ON( - nullptr == is_coherence_order_maximal_write, - "Unimplemented: RMW store returned unexpected result." - ); + ERROR_ON(!is_co_max, "Unimplemented: RMW store returned unexpected result."); return ReadModifyWriteResultExt::ok( /* old_value: */ read_old_val, new_value, - *is_coherence_order_maximal_write + *is_co_max ); } @@ -266,13 +257,10 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) { ); if (const auto* err = std::get_if(&store_ret)) return CompareExchangeResultExt::from_error(format_error(*err)); - const bool* is_coherence_order_maximal_write = std::get_if(&store_ret); + const auto* is_co_max = std::get_if(&store_ret); // FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values. - ERROR_ON( - nullptr == is_coherence_order_maximal_write, - "Unimplemented: compare-exchange store returned unexpected result." - ); - return CompareExchangeResultExt::success(read_old_val, *is_coherence_order_maximal_write); + ERROR_ON(!is_co_max, "Unimplemented: compare-exchange store returned unexpected result."); + return CompareExchangeResultExt::success(read_old_val, *is_co_max); } /**** Memory (de)allocation ****/ @@ -385,11 +373,8 @@ auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint // We don't update Miri's memory for this operation so we don't need to know if the store // was the co-maximal store, but we still check that we at least get a boolean as the result // of the store. - const bool* is_coherence_order_maximal_write = std::get_if(&store_ret); - ERROR_ON( - nullptr == is_coherence_order_maximal_write, - "Unimplemented: store part of mutex try_lock returned unexpected result." - ); + const auto* is_co_max = std::get_if(&store_ret); + ERROR_ON(!is_co_max, "Unimplemented: mutex_try_lock store returned unexpected result."); } else { // We did not acquire the mutex, so we tell GenMC to block the thread until we can acquire // it. GenMC determines this based on the annotation we pass with the load further up in @@ -416,18 +401,15 @@ auto MiriGenmcShim::handle_mutex_try_lock(ThreadId thread_id, uint64_t address, if (const auto* err = std::get_if(&load_ret)) return MutexLockResultExt::from_error(format_error(*err)); const auto* ret_val = std::get_if(&load_ret); - if (nullptr == ret_val) { - ERROR("Unimplemented: mutex trylock load returned unexpected result."); - } + ERROR_ON(!ret_val, "Unimplemented: mutex trylock load returned unexpected result."); ERROR_ON( *ret_val != MUTEX_UNLOCKED && *ret_val != MUTEX_LOCKED, "Mutex read value was neither 0 nor 1" ); const bool is_lock_acquired = *ret_val == MUTEX_UNLOCKED; - if (!is_lock_acquired) { + if (!is_lock_acquired) return MutexLockResultExt::ok(false); /* Lock already held. */ - } const auto store_ret = GenMCDriver::handleStore( nullptr, @@ -440,11 +422,8 @@ auto MiriGenmcShim::handle_mutex_try_lock(ThreadId thread_id, uint64_t address, return MutexLockResultExt::from_error(format_error(*err)); // We don't update Miri's memory for this operation so we don't need to know if the store was // co-maximal, but we still check that we get a boolean result. - const bool* is_coherence_order_maximal_write = std::get_if(&store_ret); - ERROR_ON( - nullptr == is_coherence_order_maximal_write, - "Unimplemented: store part of mutex try_lock returned unexpected result." - ); + const auto* is_co_max = std::get_if(&store_ret); + ERROR_ON(!is_co_max, "Unimplemented: store part of mutex try_lock returned unexpected result."); return MutexLockResultExt::ok(true); } @@ -467,12 +446,9 @@ auto MiriGenmcShim::handle_mutex_unlock(ThreadId thread_id, uint64_t address, ui ); if (const auto* err = std::get_if(&ret)) return StoreResultExt::from_error(format_error(*err)); - const bool* is_coherence_order_maximal_write = std::get_if(&ret); - ERROR_ON( - nullptr == is_coherence_order_maximal_write, - "Unimplemented: store part of mutex unlock returned unexpected result." - ); - return StoreResultExt::ok(*is_coherence_order_maximal_write); + const auto* is_co_max = std::get_if(&ret); + ERROR_ON(!is_co_max, "Unimplemented: store part of mutex unlock returned unexpected result."); + return StoreResultExt::ok(*is_co_max); } /** Thread creation/joining */ From 286fac035a998958bdcd80b93fa8793f562d1216 Mon Sep 17 00:00:00 2001 From: Michalis Kokologiannakis Date: Thu, 27 Nov 2025 20:24:34 +0100 Subject: [PATCH 03/10] genmc/api: Prefer early exits to joining if/else clauses --- .../cpp/src/MiriInterface/Exploration.cpp | 39 ++++++++++--------- 1 file changed, 20 insertions(+), 19 deletions(-) diff --git a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp index 809ec77b94f0..3220e03cef9b 100644 --- a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp +++ b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp @@ -358,30 +358,31 @@ auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint *ret_val != MUTEX_UNLOCKED && *ret_val != MUTEX_LOCKED, "Mutex read value was neither 0 nor 1" ); - const bool is_lock_acquired = *ret_val == MUTEX_UNLOCKED; - if (is_lock_acquired) { - const auto store_ret = GenMCDriver::handleStore( - nullptr, - inc_pos(thread_id), - old_val, - address, - size, - EventDeps() - ); - if (const auto* err = std::get_if(&store_ret)) - return MutexLockResultExt::from_error(format_error(*err)); - // We don't update Miri's memory for this operation so we don't need to know if the store - // was the co-maximal store, but we still check that we at least get a boolean as the result - // of the store. - const auto* is_co_max = std::get_if(&store_ret); - ERROR_ON(!is_co_max, "Unimplemented: mutex_try_lock store returned unexpected result."); - } else { + auto is_lock_acquired = *ret_val == MUTEX_UNLOCKED; + if (!is_lock_acquired) { // We did not acquire the mutex, so we tell GenMC to block the thread until we can acquire // it. GenMC determines this based on the annotation we pass with the load further up in // this function, namely when that load will read a value other than `MUTEX_LOCKED`. this->handle_assume_block(thread_id, AssumeType::Spinloop); + return MutexLockResultExt::ok(false); } - return MutexLockResultExt::ok(is_lock_acquired); + + const auto store_ret = GenMCDriver::handleStore( + nullptr, + inc_pos(thread_id), + old_val, + address, + size, + EventDeps() + ); + if (const auto* err = std::get_if(&store_ret)) + return MutexLockResultExt::from_error(format_error(*err)); + // We don't update Miri's memory for this operation so we don't need to know if the store + // was the co-maximal store, but we still check that we at least get a boolean as the result + // of the store. + const auto* is_co_max = std::get_if(&store_ret); + ERROR_ON(!is_co_max, "Unimplemented: mutex_try_lock store returned unexpected result."); + return MutexLockResultExt::ok(true); } auto MiriGenmcShim::handle_mutex_try_lock(ThreadId thread_id, uint64_t address, uint64_t size) From d2176c36a1745d64ba948b68247cef2ae16f2efc Mon Sep 17 00:00:00 2001 From: Michalis Kokologiannakis Date: Fri, 28 Nov 2025 17:22:32 +0100 Subject: [PATCH 04/10] genmc/api: Don't use macros for mutex state Use scoped constexprs instead. --- .../cpp/src/MiriInterface/Exploration.cpp | 38 +++++++++---------- 1 file changed, 18 insertions(+), 20 deletions(-) diff --git a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp index 3220e03cef9b..91eaf9be8e9b 100644 --- a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp +++ b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp @@ -309,8 +309,14 @@ auto MiriGenmcShim::get_estimation_results() const -> EstimationResult { /** Mutexes */ -#define MUTEX_UNLOCKED SVal(0) -#define MUTEX_LOCKED SVal(1) +struct MutexState { + static constexpr SVal UNLOCKED { 0 }; + static constexpr SVal LOCKED { 1 }; + + static constexpr bool isValid(SVal v) { + return v == UNLOCKED || v == LOCKED; + } +}; auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint64_t size) -> MutexLockResult { @@ -325,7 +331,7 @@ auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint // The `id` is ignored by GenMC; it is only used by the LLI frontend to substitute // other variables from previous expressions that may be used here. RegisterExpr::create(size_bits, /* id */ 0), - ConcreteExpr::create(size_bits, MUTEX_LOCKED) + ConcreteExpr::create(size_bits, MutexState::LOCKED) ) .release() ) @@ -334,7 +340,7 @@ auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint // As usual, we need to tell GenMC which value was stored at this location before this atomic // access, if there previously was a non-atomic initializing access. We set the initial state of // a mutex to be "unlocked". - const auto old_val = MUTEX_UNLOCKED; + const auto old_val = MutexState::UNLOCKED; const auto load_ret = handle_load_reset_if_none( thread_id, old_val, @@ -354,15 +360,11 @@ auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint const auto* ret_val = std::get_if(&load_ret); ERROR_ON(!ret_val, "Unimplemented: mutex lock returned unexpected result."); - ERROR_ON( - *ret_val != MUTEX_UNLOCKED && *ret_val != MUTEX_LOCKED, - "Mutex read value was neither 0 nor 1" - ); - auto is_lock_acquired = *ret_val == MUTEX_UNLOCKED; - if (!is_lock_acquired) { + ERROR_ON(!MutexState::isValid(*ret_val), "Mutex read value was neither 0 nor 1"); + if (*ret_val == MutexState::LOCKED) { // We did not acquire the mutex, so we tell GenMC to block the thread until we can acquire // it. GenMC determines this based on the annotation we pass with the load further up in - // this function, namely when that load will read a value other than `MUTEX_LOCKED`. + // this function, namely when that load will read a value other than `MutexState::LOCKED`. this->handle_assume_block(thread_id, AssumeType::Spinloop); return MutexLockResultExt::ok(false); } @@ -391,7 +393,7 @@ auto MiriGenmcShim::handle_mutex_try_lock(ThreadId thread_id, uint64_t address, // As usual, we need to tell GenMC which value was stored at this location before this atomic // access, if there previously was a non-atomic initializing access. We set the initial state of // a mutex to be "unlocked". - const auto old_val = MUTEX_UNLOCKED; + const auto old_val = MutexState::UNLOCKED; const auto load_ret = GenMCDriver::handleLoad( nullptr, ++currPos, @@ -404,12 +406,8 @@ auto MiriGenmcShim::handle_mutex_try_lock(ThreadId thread_id, uint64_t address, const auto* ret_val = std::get_if(&load_ret); ERROR_ON(!ret_val, "Unimplemented: mutex trylock load returned unexpected result."); - ERROR_ON( - *ret_val != MUTEX_UNLOCKED && *ret_val != MUTEX_LOCKED, - "Mutex read value was neither 0 nor 1" - ); - const bool is_lock_acquired = *ret_val == MUTEX_UNLOCKED; - if (!is_lock_acquired) + ERROR_ON(!MutexState::isValid(*ret_val), "Mutex read value was neither 0 nor 1"); + if (*ret_val == MutexState::LOCKED) return MutexLockResultExt::ok(false); /* Lock already held. */ const auto store_ret = GenMCDriver::handleStore( @@ -437,12 +435,12 @@ auto MiriGenmcShim::handle_mutex_unlock(ThreadId thread_id, uint64_t address, ui // As usual, we need to tell GenMC which value was stored at this location before this // atomic access, if there previously was a non-atomic initializing access. We set the // initial state of a mutex to be "unlocked". - /* old_val */ MUTEX_UNLOCKED, + /* old_val */ MutexState::UNLOCKED, MemOrdering::Release, SAddr(address), ASize(size), AType::Signed, - /* store_value */ MUTEX_UNLOCKED, + /* store_value */ MutexState::UNLOCKED, EventDeps() ); if (const auto* err = std::get_if(&ret)) From fafd6de3cee9cdccac794c5449ceaf324262214b Mon Sep 17 00:00:00 2001 From: Michalis Kokologiannakis Date: Thu, 27 Nov 2025 20:27:21 +0100 Subject: [PATCH 05/10] genmc/api: Remove unnecessary comments These comments explain the default values used internally in (some) calls of the GenMC library, which is unnecessary. --- src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp index 91eaf9be8e9b..00b73100b4fc 100644 --- a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp +++ b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp @@ -461,7 +461,6 @@ void MiriGenmcShim::handle_thread_create(ThreadId thread_id, ThreadId parent_id) const ThreadInfo child_info = ThreadInfo { thread_id, parent_id, fun_id, arg, "unknown thread" }; - // NOTE: Default memory ordering (`Release`) used here. const auto child_tid = GenMCDriver::handleThreadCreate(nullptr, pos, child_info, EventDeps()); // Sanity check the thread id, which is the index in the `threads_action_` array. BUG_ON(child_tid != thread_id || child_tid <= 0 || child_tid != threads_action_.size()); @@ -472,7 +471,6 @@ void MiriGenmcShim::handle_thread_join(ThreadId thread_id, ThreadId child_id) { // The thread join event happens in the parent. const auto pos = inc_pos(thread_id); - // NOTE: Default memory ordering (`Acquire`) used here. const auto ret = GenMCDriver::handleThreadJoin(nullptr, pos, child_id, EventDeps()); // If the join failed, decrease the event index again: if (!std::holds_alternative(ret)) { @@ -485,7 +483,6 @@ void MiriGenmcShim::handle_thread_join(ThreadId thread_id, ThreadId child_id) { void MiriGenmcShim::handle_thread_finish(ThreadId thread_id, uint64_t ret_val) { const auto pos = inc_pos(thread_id); - // NOTE: Default memory ordering (`Release`) used here. GenMCDriver::handleThreadFinish(nullptr, pos, SVal(ret_val)); } From 5e6d9fa6a53d6fc0e2b99c08b7b2137eb2d859f1 Mon Sep 17 00:00:00 2001 From: Michalis Kokologiannakis Date: Thu, 27 Nov 2025 20:32:16 +0100 Subject: [PATCH 06/10] genmc/api: Use returned value from handleFree() GenMC's handleFree() does return an optional, so we may as well use that value. --- src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp | 5 ++++- .../genmc-sys/cpp/src/MiriInterface/Exploration.cpp | 10 +++++----- src/tools/miri/genmc-sys/src/lib.rs | 6 +++++- src/tools/miri/src/concurrency/genmc/mod.rs | 9 ++++----- 4 files changed, 18 insertions(+), 12 deletions(-) diff --git a/src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp b/src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp index 4929c0cfa150..b6b7b06509a5 100644 --- a/src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp +++ b/src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp @@ -125,8 +125,11 @@ struct MiriGenmcShim : private GenMCDriver { 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_free(ThreadId thread_id, uint64_t address) -> bool; + + /** Returns null on success, or an error string if an error occurs. */ + auto handle_free(ThreadId thread_id, uint64_t address) -> std::unique_ptr; /**** Thread management ****/ void handle_thread_create(ThreadId thread_id, ThreadId parent_id); diff --git a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp index 00b73100b4fc..a725ab12f5ec 100644 --- a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp +++ b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp @@ -288,11 +288,11 @@ auto MiriGenmcShim::handle_malloc(ThreadId thread_id, uint64_t size, uint64_t al return ret_val.get(); } -auto MiriGenmcShim::handle_free(ThreadId thread_id, uint64_t address) -> bool { - const auto pos = inc_pos(thread_id); - GenMCDriver::handleFree(nullptr, pos, SAddr(address), EventDeps()); - // FIXME(genmc): use returned error from `handleFree` once implemented in GenMC. - return getResult().status.has_value(); +auto MiriGenmcShim::handle_free(ThreadId thread_id, uint64_t address) + -> std::unique_ptr { + auto pos = inc_pos(thread_id); + auto ret = GenMCDriver::handleFree(nullptr, pos, SAddr(address), EventDeps()); + return ret.has_value() ? format_error(*ret) : nullptr; } /**** Estimation mode result ****/ diff --git a/src/tools/miri/genmc-sys/src/lib.rs b/src/tools/miri/genmc-sys/src/lib.rs index 69aeca3ebc72..b3a9880211de 100644 --- a/src/tools/miri/genmc-sys/src/lib.rs +++ b/src/tools/miri/genmc-sys/src/lib.rs @@ -438,7 +438,11 @@ mod ffi { alignment: u64, ) -> u64; /// Returns true if an error was found. - fn handle_free(self: Pin<&mut MiriGenmcShim>, thread_id: i32, address: u64) -> bool; + fn handle_free( + self: Pin<&mut MiriGenmcShim>, + thread_id: i32, + address: u64, + ) -> UniquePtr; /**** Thread management ****/ fn handle_thread_create(self: Pin<&mut MiriGenmcShim>, thread_id: i32, parent_id: i32); diff --git a/src/tools/miri/src/concurrency/genmc/mod.rs b/src/tools/miri/src/concurrency/genmc/mod.rs index 6628e096a25d..f47064b0d167 100644 --- a/src/tools/miri/src/concurrency/genmc/mod.rs +++ b/src/tools/miri/src/concurrency/genmc/mod.rs @@ -622,15 +622,14 @@ impl GenmcCtx { !self.get_alloc_data_races(), "memory deallocation with data race checking disabled." ); - if self + let free_result = self .handle .borrow_mut() .pin_mut() - .handle_free(self.active_thread_genmc_tid(machine), address.bytes()) - { + .handle_free(self.active_thread_genmc_tid(machine), address.bytes()); + if let Some(error) = free_result.as_ref() { // FIXME(genmc): improve error handling. - // An error was detected, so we get the error string from GenMC. - throw_ub_format!("{}", self.try_get_error().unwrap()); + throw_ub_format!("{}", error.to_string_lossy()); } interp_ok(()) From 0bcadabb23e6913cda406244373c3d7a913bc734 Mon Sep 17 00:00:00 2001 From: Michalis Kokologiannakis Date: Fri, 28 Nov 2025 16:51:08 +0100 Subject: [PATCH 07/10] genmc/api: Use returned value for handleExecutionEnd() --- .../miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp index a725ab12f5ec..d5a3833e2e83 100644 --- a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp +++ b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp @@ -68,9 +68,8 @@ void MiriGenmcShim::handle_execution_start() { } auto MiriGenmcShim::handle_execution_end() -> std::unique_ptr { - // FIXME(genmc): add error handling once GenMC returns an error here. - GenMCDriver::handleExecutionEnd(); - return {}; + auto ret = GenMCDriver::handleExecutionEnd(); + return ret.has_value() ? format_error(*ret) : nullptr; } /**** Blocking instructions ****/ From 1302f6c5018f7500ab85a3924354d1e35e361ce9 Mon Sep 17 00:00:00 2001 From: Michalis Kokologiannakis Date: Sat, 29 Nov 2025 11:57:11 +0100 Subject: [PATCH 08/10] genmc,tests: Throw when GenMC runs out of memory GenMC can currently allocate up to 4GB per thread. If it cannot allocated any more memory, it will return nullptr. This commit adds a test in Miri that ensures we gracefully throw if this ever happens. --- src/tools/miri/src/concurrency/genmc/mod.rs | 6 +++-- .../fail/simple/alloc_large.multiple.stderr | 25 +++++++++++++++++++ .../tests/genmc/fail/simple/alloc_large.rs | 24 ++++++++++++++++++ .../fail/simple/alloc_large.single.stderr | 25 +++++++++++++++++++ 4 files changed, 78 insertions(+), 2 deletions(-) create mode 100644 src/tools/miri/tests/genmc/fail/simple/alloc_large.multiple.stderr create mode 100644 src/tools/miri/tests/genmc/fail/simple/alloc_large.rs create mode 100644 src/tools/miri/tests/genmc/fail/simple/alloc_large.single.stderr diff --git a/src/tools/miri/src/concurrency/genmc/mod.rs b/src/tools/miri/src/concurrency/genmc/mod.rs index f47064b0d167..73da0e11daaf 100644 --- a/src/tools/miri/src/concurrency/genmc/mod.rs +++ b/src/tools/miri/src/concurrency/genmc/mod.rs @@ -592,9 +592,11 @@ impl GenmcCtx { genmc_size, alignment.bytes(), ); + if chosen_address == 0 { + throw_exhaust!(AddressSpaceFull); + } - // Non-global addresses should not be in the global address space or null. - assert_ne!(0, chosen_address, "GenMC malloc returned nullptr."); + // Non-global addresses should not be in the global address space. assert_eq!(0, chosen_address & GENMC_GLOBAL_ADDRESSES_MASK); // Sanity check the address alignment: assert!( diff --git a/src/tools/miri/tests/genmc/fail/simple/alloc_large.multiple.stderr b/src/tools/miri/tests/genmc/fail/simple/alloc_large.multiple.stderr new file mode 100644 index 000000000000..8c52193d4e68 --- /dev/null +++ b/src/tools/miri/tests/genmc/fail/simple/alloc_large.multiple.stderr @@ -0,0 +1,25 @@ +Running GenMC Verification... +error: resource exhaustion: there are no more free addresses in the address space + --> RUSTLIB/alloc/src/raw_vec/mod.rs:LL:CC + | +LL | AllocInit::Uninitialized => alloc.allocate(layout), + | ^^^^^^^^^^^^^^^^^^^^^^ resource exhaustion occurred here + | + = note: BACKTRACE: + = note: inside `alloc::raw_vec::RawVecInner::try_allocate_in` at RUSTLIB/alloc/src/raw_vec/mod.rs:LL:CC + = note: inside `alloc::raw_vec::RawVecInner::with_capacity_in` at RUSTLIB/alloc/src/raw_vec/mod.rs:LL:CC + = note: inside `alloc::raw_vec::RawVec::::with_capacity_in` at RUSTLIB/alloc/src/raw_vec/mod.rs:LL:CC + = note: inside `std::vec::Vec::::with_capacity_in` at RUSTLIB/alloc/src/vec/mod.rs:LL:CC + = note: inside `std::vec::Vec::::with_capacity` at RUSTLIB/alloc/src/vec/mod.rs:LL:CC +note: inside `miri_start` + --> tests/genmc/fail/simple/alloc_large.rs:LL:CC + | +LL | let _v = Vec::::with_capacity(1024 * 1024 * 1024); + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace + +note: add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report + +error: aborting due to 1 previous error + diff --git a/src/tools/miri/tests/genmc/fail/simple/alloc_large.rs b/src/tools/miri/tests/genmc/fail/simple/alloc_large.rs new file mode 100644 index 000000000000..27d92bf66d42 --- /dev/null +++ b/src/tools/miri/tests/genmc/fail/simple/alloc_large.rs @@ -0,0 +1,24 @@ +//@revisions: single multiple +//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows +//@error-in-other-file: resource exhaustion + +// Ensure that we emit a proper error if GenMC fails to fulfill an allocation. +// Two variants: one for a single large allocation, one for multiple ones +// that are individually below the limit, but together are too big. + +#![no_main] + +#[path = "../../../utils/genmc.rs"] +mod genmc; + +#[unsafe(no_mangle)] +fn miri_start(_argc: isize, _argv: *const *const u8) -> isize { + if cfg!(multiple) { + for _i in 1..8 { + let _v = Vec::::with_capacity(1024 * 1024 * 1024); + } + } else { + let _v = Vec::::with_capacity(8 * 1024 * 1024 * 1024); + } + 0 +} diff --git a/src/tools/miri/tests/genmc/fail/simple/alloc_large.single.stderr b/src/tools/miri/tests/genmc/fail/simple/alloc_large.single.stderr new file mode 100644 index 000000000000..7460689bbb61 --- /dev/null +++ b/src/tools/miri/tests/genmc/fail/simple/alloc_large.single.stderr @@ -0,0 +1,25 @@ +Running GenMC Verification... +error: resource exhaustion: there are no more free addresses in the address space + --> RUSTLIB/alloc/src/raw_vec/mod.rs:LL:CC + | +LL | AllocInit::Uninitialized => alloc.allocate(layout), + | ^^^^^^^^^^^^^^^^^^^^^^ resource exhaustion occurred here + | + = note: BACKTRACE: + = note: inside `alloc::raw_vec::RawVecInner::try_allocate_in` at RUSTLIB/alloc/src/raw_vec/mod.rs:LL:CC + = note: inside `alloc::raw_vec::RawVecInner::with_capacity_in` at RUSTLIB/alloc/src/raw_vec/mod.rs:LL:CC + = note: inside `alloc::raw_vec::RawVec::::with_capacity_in` at RUSTLIB/alloc/src/raw_vec/mod.rs:LL:CC + = note: inside `std::vec::Vec::::with_capacity_in` at RUSTLIB/alloc/src/vec/mod.rs:LL:CC + = note: inside `std::vec::Vec::::with_capacity` at RUSTLIB/alloc/src/vec/mod.rs:LL:CC +note: inside `miri_start` + --> tests/genmc/fail/simple/alloc_large.rs:LL:CC + | +LL | let _v = Vec::::with_capacity(8 * 1024 * 1024 * 1024); + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace + +note: add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report + +error: aborting due to 1 previous error + From c9f27c42bf2ca9a86844463739a8249eaefb3b0f Mon Sep 17 00:00:00 2001 From: Michalis Kokologiannakis Date: Sat, 29 Nov 2025 12:59:52 +0100 Subject: [PATCH 09/10] diagnostics: Explain why programs might run OOM in GenMC mode GenMC's allocator can currently only allocate up to 4GB per thread. Authored-by: Ralf Jung --- src/tools/miri/src/diagnostics.rs | 4 ++++ .../miri/tests/genmc/fail/simple/alloc_large.multiple.stderr | 1 + .../miri/tests/genmc/fail/simple/alloc_large.single.stderr | 1 + 3 files changed, 6 insertions(+) diff --git a/src/tools/miri/src/diagnostics.rs b/src/tools/miri/src/diagnostics.rs index bb8ba196983c..8e252d306b29 100644 --- a/src/tools/miri/src/diagnostics.rs +++ b/src/tools/miri/src/diagnostics.rs @@ -362,6 +362,10 @@ pub fn report_result<'tcx>( vec![ note!("this is likely not a bug in the program; it indicates that the program performed an operation that Miri does not support"), ], + ResourceExhaustion(ResourceExhaustionInfo::AddressSpaceFull) if ecx.machine.data_race.as_genmc_ref().is_some() => + vec![ + note!("in GenMC mode, the address space is limited to 4GB per thread, and addresses cannot be reused") + ], UndefinedBehavior(AlignmentCheckFailed { .. }) if ecx.machine.check_alignment == AlignmentCheck::Symbolic => diff --git a/src/tools/miri/tests/genmc/fail/simple/alloc_large.multiple.stderr b/src/tools/miri/tests/genmc/fail/simple/alloc_large.multiple.stderr index 8c52193d4e68..1d56614c7f03 100644 --- a/src/tools/miri/tests/genmc/fail/simple/alloc_large.multiple.stderr +++ b/src/tools/miri/tests/genmc/fail/simple/alloc_large.multiple.stderr @@ -5,6 +5,7 @@ error: resource exhaustion: there are no more free addresses in the address spac LL | AllocInit::Uninitialized => alloc.allocate(layout), | ^^^^^^^^^^^^^^^^^^^^^^ resource exhaustion occurred here | + = help: in GenMC mode, the address space is limited to 4GB per thread, and addresses cannot be reused = note: BACKTRACE: = note: inside `alloc::raw_vec::RawVecInner::try_allocate_in` at RUSTLIB/alloc/src/raw_vec/mod.rs:LL:CC = note: inside `alloc::raw_vec::RawVecInner::with_capacity_in` at RUSTLIB/alloc/src/raw_vec/mod.rs:LL:CC diff --git a/src/tools/miri/tests/genmc/fail/simple/alloc_large.single.stderr b/src/tools/miri/tests/genmc/fail/simple/alloc_large.single.stderr index 7460689bbb61..8595612811fd 100644 --- a/src/tools/miri/tests/genmc/fail/simple/alloc_large.single.stderr +++ b/src/tools/miri/tests/genmc/fail/simple/alloc_large.single.stderr @@ -5,6 +5,7 @@ error: resource exhaustion: there are no more free addresses in the address spac LL | AllocInit::Uninitialized => alloc.allocate(layout), | ^^^^^^^^^^^^^^^^^^^^^^ resource exhaustion occurred here | + = help: in GenMC mode, the address space is limited to 4GB per thread, and addresses cannot be reused = note: BACKTRACE: = note: inside `alloc::raw_vec::RawVecInner::try_allocate_in` at RUSTLIB/alloc/src/raw_vec/mod.rs:LL:CC = note: inside `alloc::raw_vec::RawVecInner::with_capacity_in` at RUSTLIB/alloc/src/raw_vec/mod.rs:LL:CC From 68a81c42fafa6016168062b740bac4a589d6f36c Mon Sep 17 00:00:00 2001 From: Michalis Kokologiannakis Date: Fri, 28 Nov 2025 12:25:42 +0100 Subject: [PATCH 10/10] genmc/build,tests: Update GenMC version to 0.16.1 This version fixes some issues with atomic_{umix,umax} operation and memory allocation. --- src/tools/miri/genmc-sys/build.rs | 2 +- src/tools/miri/tests/genmc/pass/atomics/rmw_ops.rs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/tools/miri/genmc-sys/build.rs b/src/tools/miri/genmc-sys/build.rs index 1c06387ac928..a22e3341d67a 100644 --- a/src/tools/miri/genmc-sys/build.rs +++ b/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 = "aa10ed65117c3291524efc19253b5d443a4602ac"; + pub(crate) const GENMC_COMMIT: &str = "22d3d0b44dedb4e8e1aae3330e546465e4664529"; /// 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. diff --git a/src/tools/miri/tests/genmc/pass/atomics/rmw_ops.rs b/src/tools/miri/tests/genmc/pass/atomics/rmw_ops.rs index 7e6e33c8a7b1..411207b79b7e 100644 --- a/src/tools/miri/tests/genmc/pass/atomics/rmw_ops.rs +++ b/src/tools/miri/tests/genmc/pass/atomics/rmw_ops.rs @@ -67,7 +67,7 @@ macro_rules! test_rmw_edge_cases { x.store(10, ORD); assert_eq(10, x.fetch_add(<$int>::MAX, ORD)); // definitely overflows, so new value of x is smaller than 10 assert_eq(<$int>::MAX.wrapping_add(10), x.fetch_max(10, ORD)); // new value of x should be 10 - // assert_eq(10, x.load(ORD)); // FIXME(genmc,#4572): enable this check once GenMC correctly handles min/max truncation. + assert_eq(10, x.load(ORD)); }}; }