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); -}