From 286fac035a998958bdcd80b93fa8793f562d1216 Mon Sep 17 00:00:00 2001 From: Michalis Kokologiannakis Date: Thu, 27 Nov 2025 20:24:34 +0100 Subject: [PATCH] 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)