diff --git a/genmc-sys/build.rs b/genmc-sys/build.rs index 4a5cc58513..bde9ce7fea 100644 --- a/genmc-sys/build.rs +++ b/genmc-sys/build.rs @@ -178,7 +178,7 @@ fn compile_cpp_dependencies(genmc_path: &Path) { // 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/Exploration.cpp", "MiriInterface/Setup.cpp"] + let cpp_files = ["Exploration.cpp", "Setup.cpp"] .map(|file| std::path::absolute(cpp_files_base_path.join(file)).unwrap()); let mut bridge = cxx_build::bridge("src/lib.rs"); diff --git a/genmc-sys/cpp/include/MiriInterface.hpp b/genmc-sys/cpp/include/MiriInterface.hpp index 7c89c630c3..efe874cd7f 100644 --- a/genmc-sys/cpp/include/MiriInterface.hpp +++ b/genmc-sys/cpp/include/MiriInterface.hpp @@ -32,11 +32,13 @@ struct GenmcScalar; struct SchedulingResult; struct EstimationResult; struct LoadResult; +struct NonAtomicResult; struct StoreResult; struct ReadModifyWriteResult; struct CompareExchangeResult; struct MutexLockResult; struct MallocResult; +struct FreeResult; // GenMC uses `int` for its thread IDs. using ThreadId = int; @@ -52,26 +54,26 @@ using ThreadId = int; /// Never calling this function is safe, GenMC will fall back to its default log level. /* unsafe */ void set_log_level_raw(LogLevel log_level); -struct MiriGenmcShim : private GenMCDriver { +struct MiriGenMCInterface : private GenMCDriver { public: - MiriGenmcShim(std::shared_ptr conf, Mode mode /* = VerificationMode{} */) + MiriGenMCInterface(std::shared_ptr conf, Mode mode /* = VerificationMode{} */) : GenMCDriver(std::move(conf), nullptr, mode) {} - /// Create a new `MiriGenmcShim`, which wraps a `GenMCDriver`. + /// Create a new `MiriGenMCInterface`, which wraps a `GenMCDriver`. /// /// # Safety /// /// This function is marked as unsafe since the `logLevel` global variable is non-atomic. /// This function should not be called in an unsynchronized way with `set_log_level_raw`, - /// since this function and any methods on the returned `MiriGenmcShim` may read the + /// since this function and any methods on the returned `MiriGenMCInterface` may read the /// `logLevel`, causing a data race. The safest way to use these functions is to call /// `set_log_level_raw` once, and only then start creating handles. There should not be any - /// other (safe) way to create a `MiriGenmcShim`. + /// other (safe) way to create a `MiriGenMCInterface`. /* unsafe */ static auto create_handle(const GenmcParams& params, bool estimation_mode) - -> std::unique_ptr; + -> std::unique_ptr; - virtual ~MiriGenmcShim() {} + virtual ~MiriGenMCInterface() {} /**** Execution start/end handling ****/ @@ -94,7 +96,7 @@ struct MiriGenmcShim : private GenMCDriver { MemOrdering ord, GenmcScalar old_val ); - [[nodiscard]] LoadResult + [[nodiscard]] NonAtomicResult handle_non_atomic_load(ThreadId thread_id, uint64_t address, uint64_t size); [[nodiscard]] ReadModifyWriteResult handle_read_modify_write( ThreadId thread_id, @@ -124,7 +126,7 @@ struct MiriGenmcShim : private GenMCDriver { GenmcScalar old_val, MemOrdering ord ); - [[nodiscard]] StoreResult + [[nodiscard]] NonAtomicResult handle_non_atomic_store(ThreadId thread_id, uint64_t address, uint64_t size); void handle_fence(ThreadId thread_id, MemOrdering ord); @@ -134,7 +136,7 @@ struct MiriGenmcShim : private GenMCDriver { auto handle_malloc(ThreadId thread_id, uint64_t size, uint64_t alignment) -> MallocResult; /** Returns null on success, or an error string if an error occurs. */ - auto handle_free(ThreadId thread_id, uint64_t address) -> std::unique_ptr; + auto handle_free(ThreadId thread_id, uint64_t address) -> FreeResult; /**** Thread management ****/ void handle_thread_create(ThreadId thread_id, ThreadId parent_id); @@ -240,8 +242,8 @@ constexpr auto get_global_alloc_static_mask() -> uint64_t { } // CXX.rs generated headers: -// NOTE: this must be included *after* `MiriGenmcShim` and all the other types we use are defined, -// otherwise there will be compilation errors due to missing definitions. +// NOTE: this must be included *after* `MiriGenMCInterface` and all the other types we use are +// defined, otherwise there will be compilation errors due to missing definitions. #include "genmc-sys/src/lib.rs.h" /**** Result handling ****/ @@ -277,154 +279,169 @@ inline std::optional try_to_sval(GenmcScalar scalar) { } } // namespace GenmcScalarExt -namespace LoadResultExt { -inline LoadResult no_value() { - return LoadResult { - .invalid = false, - .error = std::unique_ptr(nullptr), - .read_value = GenmcScalarExt::uninit(), - }; +namespace MakeLoadResult { +inline LoadResult value(SVal read_value) { + return LoadResult { .status = OperationStatus::Ok, + .error = nullptr, + .read_value = GenmcScalarExt::from_sval(read_value) }; } -inline LoadResult from_value(SVal read_value) { - return LoadResult { .invalid = false, - .error = std::unique_ptr(nullptr), - .read_value = GenmcScalarExt::from_sval(read_value) }; +inline LoadResult error(std::unique_ptr err) { + return LoadResult { .status = OperationStatus::Error, + .error = std::move(err), + .read_value = GenmcScalarExt::uninit() }; } -inline LoadResult from_error(std::unique_ptr error) { - return LoadResult { .invalid = false, - .error = std::move(error), +inline LoadResult invalid() { + return LoadResult { .status = OperationStatus::Invalid, + .error = nullptr, .read_value = GenmcScalarExt::uninit() }; } +} // namespace MakeLoadResult + +namespace MakeNonAtomicResult { +inline NonAtomicResult ok() { + return NonAtomicResult { .status = OperationStatus::Ok, .error = nullptr }; +} -inline LoadResult from_invalid() { - return LoadResult { .invalid = true, .error = nullptr, .read_value = GenmcScalarExt::uninit() }; +inline NonAtomicResult error(std::unique_ptr err) { + return NonAtomicResult { .status = OperationStatus::Error, .error = std::move(err) }; } -} // namespace LoadResultExt +inline NonAtomicResult invalid() { + return NonAtomicResult { .status = OperationStatus::Invalid, .error = nullptr }; +} +} // namespace MakeNonAtomicResult -namespace StoreResultExt { +namespace MakeStoreResult { inline StoreResult ok(bool is_coherence_order_maximal_write) { - return StoreResult { .invalid = false, - .error = std::unique_ptr(nullptr), + return StoreResult { .status = OperationStatus::Ok, + .error = nullptr, .is_coherence_order_maximal_write = is_coherence_order_maximal_write }; } -inline StoreResult from_error(std::unique_ptr error) { - return StoreResult { .invalid = false, - .error = std::move(error), +inline StoreResult error(std::unique_ptr err) { + return StoreResult { .status = OperationStatus::Error, + .error = std::move(err), .is_coherence_order_maximal_write = false }; } -inline StoreResult from_invalid() { - return StoreResult { .invalid = true, +inline StoreResult invalid() { + return StoreResult { .status = OperationStatus::Invalid, .error = nullptr, .is_coherence_order_maximal_write = false }; } -} // namespace StoreResultExt +} // namespace MakeStoreResult -namespace ReadModifyWriteResultExt { +namespace MakeReadModifyWriteResult { inline ReadModifyWriteResult ok(SVal old_value, SVal new_value, bool is_coherence_order_maximal_write) { - return ReadModifyWriteResult { .invalid = false, - .error = std::unique_ptr(nullptr), + return ReadModifyWriteResult { .status = OperationStatus::Ok, + .error = nullptr, .old_value = GenmcScalarExt::from_sval(old_value), .new_value = GenmcScalarExt::from_sval(new_value), .is_coherence_order_maximal_write = is_coherence_order_maximal_write }; } -inline ReadModifyWriteResult from_error(std::unique_ptr error) { - return ReadModifyWriteResult { .invalid = false, - .error = std::move(error), +inline ReadModifyWriteResult error(std::unique_ptr err) { + return ReadModifyWriteResult { .status = OperationStatus::Error, + .error = std::move(err), .old_value = GenmcScalarExt::uninit(), .new_value = GenmcScalarExt::uninit(), .is_coherence_order_maximal_write = false }; } -inline ReadModifyWriteResult from_invalid() { - return ReadModifyWriteResult { .invalid = true, +inline ReadModifyWriteResult invalid() { + return ReadModifyWriteResult { .status = OperationStatus::Invalid, .error = nullptr, .old_value = GenmcScalarExt::uninit(), .new_value = GenmcScalarExt::uninit(), .is_coherence_order_maximal_write = false }; } -} // namespace ReadModifyWriteResultExt +} // namespace MakeReadModifyWriteResult -namespace CompareExchangeResultExt { -inline CompareExchangeResult success(SVal old_value, bool is_coherence_order_maximal_write) { - return CompareExchangeResult { .invalid = false, +namespace MakeCasResult { +inline CompareExchangeResult succeeded(SVal old_value, bool is_coherence_order_maximal_write) { + return CompareExchangeResult { .status = CasStatus::Succeeded, .error = nullptr, .old_value = GenmcScalarExt::from_sval(old_value), - .is_success = true, .is_coherence_order_maximal_write = is_coherence_order_maximal_write }; } -inline CompareExchangeResult failure(SVal old_value) { - return CompareExchangeResult { .invalid = false, +inline CompareExchangeResult failed(SVal old_value) { + return CompareExchangeResult { .status = CasStatus::Failed, .error = nullptr, .old_value = GenmcScalarExt::from_sval(old_value), - .is_success = false, .is_coherence_order_maximal_write = false }; } -inline CompareExchangeResult from_error(std::unique_ptr error) { - return CompareExchangeResult { .invalid = false, - .error = std::move(error), +inline CompareExchangeResult error(std::unique_ptr err) { + return CompareExchangeResult { .status = CasStatus::Error, + .error = std::move(err), .old_value = GenmcScalarExt::uninit(), - .is_success = false, .is_coherence_order_maximal_write = false }; } -inline CompareExchangeResult from_invalid() { - return CompareExchangeResult { .invalid = true, +inline CompareExchangeResult invalid() { + return CompareExchangeResult { .status = CasStatus::Invalid, .error = nullptr, .old_value = GenmcScalarExt::uninit(), - .is_success = false, .is_coherence_order_maximal_write = false }; } -} // namespace CompareExchangeResultExt +} // namespace MakeCasResult -namespace MutexLockResultExt { -inline MutexLockResult ok(bool is_lock_acquired) { - return MutexLockResult { .invalid = false, - .error = nullptr, - .is_reset = false, - .is_lock_acquired = is_lock_acquired }; +namespace MakeMutexLockResult { +inline MutexLockResult acquired() { + return MutexLockResult { .status = MutexLockStatus::Acquired, .error = nullptr }; +} + +inline MutexLockResult not_acquired() { + return MutexLockResult { .status = MutexLockStatus::NotAcquired, .error = nullptr }; } inline MutexLockResult reset() { - return MutexLockResult { .invalid = false, - .error = nullptr, - .is_reset = true, - .is_lock_acquired = false }; + return MutexLockResult { .status = MutexLockStatus::Reset, .error = nullptr }; } -inline MutexLockResult from_error(std::unique_ptr error) { - return MutexLockResult { .invalid = false, - .error = std::move(error), - .is_reset = false, - .is_lock_acquired = false }; +inline MutexLockResult error(std::unique_ptr err) { + return MutexLockResult { .status = MutexLockStatus::Error, .error = std::move(err) }; } -inline MutexLockResult from_invalid() { - return MutexLockResult { .invalid = true, - .error = nullptr, - .is_reset = false, - .is_lock_acquired = false }; +inline MutexLockResult invalid() { + return MutexLockResult { .status = MutexLockStatus::Invalid, .error = nullptr }; } -} // namespace MutexLockResultExt +} // namespace MakeMutexLockResult -namespace MallocResultExt { +namespace MakeMallocResult { inline MallocResult ok(SVal addr) { - return MallocResult { .error = nullptr, .address = addr.get() }; + return MallocResult { .status = OperationStatus::Ok, .error = nullptr, .address = addr.get() }; +} + +inline MallocResult error(std::unique_ptr err) { + return MallocResult { .status = OperationStatus::Error, + .error = std::move(err), + .address = 0UL }; +} + +inline MallocResult invalid() { + return MallocResult { .status = OperationStatus::Invalid, .error = nullptr, .address = 0UL }; +} +} // namespace MakeMallocResult + +namespace MakeFreeResult { +inline FreeResult ok() { + return FreeResult { .status = OperationStatus::Ok, .error = nullptr }; +} + +inline FreeResult error(std::unique_ptr err) { + return FreeResult { .status = OperationStatus::Error, .error = std::move(err) }; } -inline MallocResult from_error(std::unique_ptr error) { - return MallocResult { .error = std::move(error), .address = 0UL }; +inline FreeResult invalid() { + return FreeResult { .status = OperationStatus::Invalid, .error = nullptr }; } -} // namespace MallocResultExt +} // namespace MakeFreeResult #endif /* GENMC_MIRI_INTERFACE_HPP */ diff --git a/genmc-sys/cpp/include/ResultHandling.hpp b/genmc-sys/cpp/include/ResultHandling.hpp index 6df3a3af84..ca59866f39 100644 --- a/genmc-sys/cpp/include/ResultHandling.hpp +++ b/genmc-sys/cpp/include/ResultHandling.hpp @@ -20,4 +20,10 @@ static auto format_error(VerificationError err) -> std::unique_ptr return std::make_unique(s.str()); } +/** Standard overloaded-lambda helper for std::visit. + * See https://en.cppreference.com/w/cpp/utility/variant/visit2.html for usage. */ +template struct overloaded : Ts... { + using Ts::operator()...; +}; + #endif /* GENMC_RESULT_HANDLING_HPP */ diff --git a/genmc-sys/cpp/src/MiriInterface/Exploration.cpp b/genmc-sys/cpp/src/Exploration.cpp similarity index 68% rename from genmc-sys/cpp/src/MiriInterface/Exploration.cpp rename to genmc-sys/cpp/src/Exploration.cpp index 1c5186bfff..75a66bc553 100644 --- a/genmc-sys/cpp/src/MiriInterface/Exploration.cpp +++ b/genmc-sys/cpp/src/Exploration.cpp @@ -34,7 +34,7 @@ /** Scheduling */ -auto MiriGenmcShim::schedule_next( +auto MiriGenMCInterface::schedule_next( const int curr_thread_id, const ActionKind curr_thread_next_instr_kind ) -> SchedulingResult { @@ -61,27 +61,27 @@ auto MiriGenmcShim::schedule_next( ); } -void MiriGenmcShim::handle_execution_start() { +void MiriGenMCInterface::handle_execution_start() { threads_action_.clear(); threads_action_.push_back(Action(ActionKind::Load, Event::getInit())); GenMCDriver::handleExecutionStart(); } -auto MiriGenmcShim::handle_execution_end() -> std::unique_ptr { +auto MiriGenMCInterface::handle_execution_end() -> std::unique_ptr { auto ret = GenMCDriver::handleExecutionEnd(); return ret.has_value() ? format_error(*ret) : nullptr; } /**** Blocking instructions ****/ -void MiriGenmcShim::handle_assume_block(ThreadId thread_id, AssumeType assume_type) { +void MiriGenMCInterface::handle_assume_block(ThreadId thread_id, AssumeType assume_type) { auto ret = GenMCDriver::handleAssume(nullptr, curr_pos(thread_id), assume_type); inc_pos(thread_id, ret.count); } /**** Memory access handling ****/ -[[nodiscard]] auto MiriGenmcShim::handle_atomic_load( +[[nodiscard]] auto MiriGenMCInterface::handle_atomic_load( ThreadId thread_id, uint64_t address, uint64_t size, @@ -100,19 +100,24 @@ void MiriGenmcShim::handle_assume_block(ThreadId thread_id, AssumeType assume_ty EventDeps() ); inc_pos(thread_id, ret.count); - if (const auto* err = std::get_if(&ret.result)) - return LoadResultExt::from_error(format_error(*err)); - if (std::holds_alternative(ret.result)) - return LoadResultExt::from_invalid(); - const auto* ret_val = std::get_if(&ret.result); // FIXME(genmc): handle `HandleResult::Reset` return value. - ERROR_ON(!ret_val, "Unimplemented: atomic load returned unexpected result."); - return LoadResultExt::from_value(*ret_val); + return std::visit( + overloaded { + [](const VerificationError& err) { return MakeLoadResult::error(format_error(err)); }, + [](const Invalid&) { return MakeLoadResult::invalid(); }, + [](const SVal& v) { return MakeLoadResult::value(v); }, + [](const auto&) { + UNREACHABLE(); + return MakeLoadResult::invalid(); + }, + }, + ret.result + ); } [[nodiscard]] auto -MiriGenmcShim::handle_non_atomic_load(ThreadId thread_id, uint64_t address, uint64_t size) - -> LoadResult { +MiriGenMCInterface::handle_non_atomic_load(ThreadId thread_id, uint64_t address, uint64_t size) + -> NonAtomicResult { const auto ret = GenMCDriver::handleNALoad( nullptr, curr_pos(thread_id), @@ -121,20 +126,24 @@ MiriGenmcShim::handle_non_atomic_load(ThreadId thread_id, uint64_t address, uint EventDeps() ); inc_pos(thread_id, ret.count); - - if (const auto* err = std::get_if(&ret.result)) - return LoadResultExt::from_error(format_error(*err)); - if (std::holds_alternative(ret.result)) - return LoadResultExt::from_invalid(); // FIXME(genmc): handle `HandleResult::Reset` return value. - ERROR_ON( - !std::holds_alternative(ret.result), - "Unimplemented: non-atomic load returned unexpected result." + return std::visit( + overloaded { + [](const VerificationError& err) { + return MakeNonAtomicResult::error(format_error(err)); + }, + [](const Invalid&) { return MakeNonAtomicResult::invalid(); }, + [](const std::monostate&) { return MakeNonAtomicResult::ok(); }, + [](const auto&) { + UNREACHABLE(); + return MakeNonAtomicResult::invalid(); + }, + }, + ret.result ); - return LoadResultExt::no_value(); } -[[nodiscard]] auto MiriGenmcShim::handle_atomic_store( +[[nodiscard]] auto MiriGenMCInterface::handle_atomic_store( ThreadId thread_id, uint64_t address, uint64_t size, @@ -155,20 +164,24 @@ MiriGenmcShim::handle_non_atomic_load(ThreadId thread_id, uint64_t address, uint ); inc_pos(thread_id, ret.count); - if (const auto* err = std::get_if(&ret.result)) - return StoreResultExt::from_error(format_error(*err)); - if (std::holds_alternative(ret.result)) - return StoreResultExt::from_invalid(); - - const auto* is_co_max = std::get_if(&ret.result); // FIXME(genmc): handle `HandleResult::Reset` return value. - ERROR_ON(!is_co_max, "Unimplemented: atomic store returned unexpected result."); - return StoreResultExt::ok(*is_co_max); + return std::visit( + overloaded { + [](const VerificationError& err) { return MakeStoreResult::error(format_error(err)); }, + [](const Invalid&) { return MakeStoreResult::invalid(); }, + [](bool is_co_max) { return MakeStoreResult::ok(is_co_max); }, + [](const auto&) { + UNREACHABLE(); + return MakeStoreResult::invalid(); + }, + }, + ret.result + ); } [[nodiscard]] auto -MiriGenmcShim::handle_non_atomic_store(ThreadId thread_id, uint64_t address, uint64_t size) - -> StoreResult { +MiriGenMCInterface::handle_non_atomic_store(ThreadId thread_id, uint64_t address, uint64_t size) + -> NonAtomicResult { const auto ret = GenMCDriver::handleNAStore( nullptr, curr_pos(thread_id), @@ -177,25 +190,29 @@ MiriGenmcShim::handle_non_atomic_store(ThreadId thread_id, uint64_t address, uin EventDeps() ); inc_pos(thread_id, ret.count); - - if (const auto* err = std::get_if(&ret.result)) - return StoreResultExt::from_error(format_error(*err)); - if (std::holds_alternative(ret.result)) - return StoreResultExt::from_invalid(); // FIXME(genmc): handle `HandleResult::Reset` return value. - ERROR_ON( - !std::holds_alternative(ret.result), - "Unimplemented: non-atomic store returned unexpected result." + return std::visit( + overloaded { + [](const VerificationError& err) -> NonAtomicResult { + return MakeNonAtomicResult::error(format_error(err)); + }, + [](const Invalid&) { return MakeNonAtomicResult::invalid(); }, + [](const std::monostate&) { return MakeNonAtomicResult::ok(); }, + [](const auto&) { + UNREACHABLE(); + return MakeNonAtomicResult::invalid(); + }, + }, + ret.result ); - return StoreResultExt::ok(true); } -void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) { +void MiriGenMCInterface::handle_fence(ThreadId thread_id, MemOrdering ord) { auto ret = GenMCDriver::handleFence(nullptr, curr_pos(thread_id), ord, EventDeps()); inc_pos(thread_id, ret.count); } -[[nodiscard]] auto MiriGenmcShim::handle_read_modify_write( +[[nodiscard]] auto MiriGenMCInterface::handle_read_modify_write( ThreadId thread_id, uint64_t address, uint64_t size, @@ -224,9 +241,9 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) { ); inc_pos(thread_id, load_ret.count); if (const auto* err = std::get_if(&load_ret.result)) - return ReadModifyWriteResultExt::from_error(format_error(*err)); + return MakeReadModifyWriteResult::error(format_error(*err)); if (std::holds_alternative(load_ret.result)) - return ReadModifyWriteResultExt::from_invalid(); + return MakeReadModifyWriteResult::invalid(); const auto* ret_val = std::get_if(&load_ret.result); // FIXME(genmc): handle `HandleResult::Reset` return values. @@ -247,22 +264,26 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) { EventDeps() ); inc_pos(thread_id, store_ret.count); - if (const auto* err = std::get_if(&store_ret.result)) - return ReadModifyWriteResultExt::from_error(format_error(*err)); - if (std::holds_alternative(store_ret.result)) - return ReadModifyWriteResultExt::from_invalid(); - - const auto* is_co_max = std::get_if(&store_ret.result); // FIXME(genmc): handle `HandleResult::Reset` return values. - ERROR_ON(!is_co_max, "Unimplemented: RMW store returned unexpected result."); - return ReadModifyWriteResultExt::ok( - /* old_value: */ read_old_val, - new_value, - *is_co_max + return std::visit( + overloaded { + [](const VerificationError& err) { + return MakeReadModifyWriteResult::error(format_error(err)); + }, + [](const GenMCDriver::Invalid&) { return MakeReadModifyWriteResult::invalid(); }, + [&read_old_val, &new_value](bool is_co_max) { + return MakeReadModifyWriteResult::ok(read_old_val, new_value, is_co_max); + }, + [](const auto&) { + UNREACHABLE(); + return MakeReadModifyWriteResult::invalid(); + }, + }, + store_ret.result ); } -[[nodiscard]] auto MiriGenmcShim::handle_compare_exchange( +[[nodiscard]] auto MiriGenMCInterface::handle_compare_exchange( ThreadId thread_id, uint64_t address, uint64_t size, @@ -298,16 +319,16 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) { ); inc_pos(thread_id, load_ret.count); if (const auto* err = std::get_if(&load_ret.result)) - return CompareExchangeResultExt::from_error(format_error(*err)); + return MakeCasResult::error(format_error(*err)); if (std::holds_alternative(load_ret.result)) - return CompareExchangeResultExt::from_invalid(); + return MakeCasResult::invalid(); const auto* ret_val = std::get_if(&load_ret.result); // FIXME(genmc): handle `HandleResult::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); + return MakeCasResult::failed(read_old_val); // FIXME(GenMC): Add support for modelling spurious failures. @@ -323,20 +344,26 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) { EventDeps() ); inc_pos(thread_id, store_ret.count); - if (const auto* err = std::get_if(&store_ret.result)) - return CompareExchangeResultExt::from_error(format_error(*err)); - if (std::holds_alternative(store_ret.result)) - return CompareExchangeResultExt::from_invalid(); - - const auto* is_co_max = std::get_if(&store_ret.result); // FIXME(genmc): handle `HandleResult::Reset` return values. - ERROR_ON(!is_co_max, "Unimplemented: compare-exchange store returned unexpected result."); - return CompareExchangeResultExt::success(read_old_val, *is_co_max); + return std::visit( + overloaded { + [](const VerificationError& err) { return MakeCasResult::error(format_error(err)); }, + [](const GenMCDriver::Invalid&) { return MakeCasResult::invalid(); }, + [&read_old_val](bool is_co_max) { + return MakeCasResult::succeeded(read_old_val, is_co_max); + }, + [](const auto&) { + UNREACHABLE(); + return MakeCasResult::invalid(); + }, + }, + store_ret.result + ); } /**** Memory (de)allocation ****/ -auto MiriGenmcShim::handle_malloc(ThreadId thread_id, uint64_t size, uint64_t alignment) +auto MiriGenMCInterface::handle_malloc(ThreadId thread_id, uint64_t size, uint64_t alignment) -> MallocResult { // These are only used for printing and features Miri-GenMC doesn't support (yet). const auto storage_duration = StorageDuration::SD_Heap; @@ -357,30 +384,38 @@ auto MiriGenmcShim::handle_malloc(ThreadId thread_id, uint64_t size, uint64_t al EventDeps() ); inc_pos(thread_id, ret.count); - if (const auto* err = std::get_if(&ret.result)) - return MallocResultExt::from_error(format_error(*err)); - const auto* addr = std::get_if(&ret.result); - ERROR_ON(!addr, "Unimplemented: malloc returned unexpected result."); - return MallocResultExt::ok(*addr); + return std::visit( + overloaded { + [](const VerificationError& err) { return MakeMallocResult::error(format_error(err)); }, + [](const SVal& addr) { return MakeMallocResult::ok(addr); }, + [](const auto&) { + UNREACHABLE(); + return MakeMallocResult::invalid(); + }, + }, + ret.result + ); } -auto MiriGenmcShim::handle_free(ThreadId thread_id, uint64_t address) - -> std::unique_ptr { +auto MiriGenMCInterface::handle_free(ThreadId thread_id, uint64_t address) -> FreeResult { auto ret = GenMCDriver::handleFree(nullptr, curr_pos(thread_id), SAddr(address), EventDeps()); inc_pos(thread_id, ret.count); - if (const auto* err = std::get_if(&ret.result)) - return format_error(*err); - - ERROR_ON( - !std::holds_alternative(ret.result), - "Unimplemented: free returned unexpected result." + return std::visit( + overloaded { + [](const VerificationError& err) { return MakeFreeResult::error(format_error(err)); }, + [](const std::monostate&) { return MakeFreeResult::ok(); }, + [](const auto&) { + UNREACHABLE(); + return MakeFreeResult::invalid(); + }, + }, + ret.result ); - return nullptr; } /**** Estimation mode result ****/ -auto MiriGenmcShim::get_estimation_results() const -> EstimationResult { +auto MiriGenMCInterface::get_estimation_results() const -> EstimationResult { const auto& res = getResult(); return EstimationResult { .mean = static_cast(res.estimationMean), @@ -401,7 +436,7 @@ struct MutexState { } }; -auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint64_t size) +auto MiriGenMCInterface::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`. @@ -435,15 +470,15 @@ auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint ); inc_pos(thread_id, load_ret.count); if (const auto* err = std::get_if(&load_ret.result)) - return MutexLockResultExt::from_error(format_error(*err)); + return MakeMutexLockResult::error(format_error(*err)); if (std::holds_alternative(load_ret.result)) - return MutexLockResultExt::from_invalid(); + return MakeMutexLockResult::invalid(); // 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.result)) - return MutexLockResultExt::reset(); + return MakeMutexLockResult::reset(); const auto* ret_val = std::get_if(&load_ret.result); ERROR_ON(!ret_val, "Unimplemented: mutex lock returned unexpected result."); @@ -457,25 +492,31 @@ auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint // 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 `MutexState::LOCKED`. this->handle_assume_block(thread_id, AssumeType::Spinloop); - return MutexLockResultExt::ok(false); + return MakeMutexLockResult::not_acquired(); } const auto store_ret = GenMCDriver::handleLockCasWrite(nullptr, curr_pos(thread_id), address, size, EventDeps()); inc_pos(thread_id, store_ret.count); - if (const auto* err = std::get_if(&store_ret.result)) - return MutexLockResultExt::from_error(format_error(*err)); - if (std::holds_alternative(store_ret.result)) - return MutexLockResultExt::from_invalid(); // 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.result); - ERROR_ON(!is_co_max, "Unimplemented: mutex_try_lock store returned unexpected result."); - return MutexLockResultExt::ok(true); + // was the co-maximal store. + return std::visit( + overloaded { + [](const VerificationError& err) { + return MakeMutexLockResult::error(format_error(err)); + }, + [](const GenMCDriver::Invalid&) { return MakeMutexLockResult::invalid(); }, + [](bool) { return MakeMutexLockResult::acquired(); }, + [](const auto&) { + UNREACHABLE(); + return MakeMutexLockResult::invalid(); + }, + }, + store_ret.result + ); } -auto MiriGenmcShim::handle_mutex_try_lock(ThreadId thread_id, uint64_t address, uint64_t size) +auto MiriGenMCInterface::handle_mutex_try_lock(ThreadId thread_id, uint64_t address, uint64_t size) -> MutexLockResult { // 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 @@ -492,15 +533,15 @@ auto MiriGenmcShim::handle_mutex_try_lock(ThreadId thread_id, uint64_t address, ); inc_pos(thread_id, load_ret.count); if (const auto* err = std::get_if(&load_ret.result)) - return MutexLockResultExt::from_error(format_error(*err)); + return MakeMutexLockResult::error(format_error(*err)); if (std::holds_alternative(load_ret.result)) - return MutexLockResultExt::from_invalid(); + return MakeMutexLockResult::invalid(); const auto* ret_val = std::get_if(&load_ret.result); ERROR_ON(!ret_val, "Unimplemented: mutex trylock load returned unexpected result."); 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. */ + return MakeMutexLockResult::not_acquired(); /* Lock already held. */ const auto store_ret = GenMCDriver::handleTrylockCasWrite( nullptr, @@ -510,18 +551,25 @@ auto MiriGenmcShim::handle_mutex_try_lock(ThreadId thread_id, uint64_t address, EventDeps() ); inc_pos(thread_id, store_ret.count); - if (const auto* err = std::get_if(&store_ret.result)) - return MutexLockResultExt::from_error(format_error(*err)); - if (std::holds_alternative(store_ret.result)) - return MutexLockResultExt::from_invalid(); // 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 auto* is_co_max = std::get_if(&store_ret.result); - ERROR_ON(!is_co_max, "Unimplemented: store part of mutex try_lock returned unexpected result."); - return MutexLockResultExt::ok(true); + // co-maximal. + return std::visit( + overloaded { + [](const VerificationError& err) { + return MakeMutexLockResult::error(format_error(err)); + }, + [](const GenMCDriver::Invalid&) { return MakeMutexLockResult::invalid(); }, + [](bool) { return MakeMutexLockResult::acquired(); }, + [](const auto&) { + UNREACHABLE(); + return MakeMutexLockResult::invalid(); + }, + }, + store_ret.result + ); } -auto MiriGenmcShim::handle_mutex_unlock(ThreadId thread_id, uint64_t address, uint64_t size) +auto MiriGenMCInterface::handle_mutex_unlock(ThreadId thread_id, uint64_t address, uint64_t size) -> StoreResult { const auto ret = GenMCDriver::handleUnlockWrite( nullptr, @@ -538,18 +586,23 @@ auto MiriGenmcShim::handle_mutex_unlock(ThreadId thread_id, uint64_t address, ui EventDeps() ); inc_pos(thread_id, ret.count); - if (const auto* err = std::get_if(&ret.result)) - return StoreResultExt::from_error(format_error(*err)); - if (std::holds_alternative(ret.result)) - return StoreResultExt::from_invalid(); - const auto* is_co_max = std::get_if(&ret.result); - ERROR_ON(!is_co_max, "Unimplemented: store part of mutex unlock returned unexpected result."); - return StoreResultExt::ok(*is_co_max); + return std::visit( + overloaded { + [](const VerificationError& err) { return MakeStoreResult::error(format_error(err)); }, + [](const GenMCDriver::Invalid&) { return MakeStoreResult::invalid(); }, + [](bool is_co_max) { return MakeStoreResult::ok(is_co_max); }, + [](const auto&) { + UNREACHABLE(); + return MakeStoreResult::invalid(); + }, + }, + ret.result + ); } /** Thread creation/joining */ -void MiriGenmcShim::handle_thread_create(ThreadId thread_id, ThreadId parent_id) { +void MiriGenMCInterface::handle_thread_create(ThreadId thread_id, ThreadId 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); @@ -571,7 +624,7 @@ void MiriGenmcShim::handle_thread_create(ThreadId thread_id, ThreadId parent_id) threads_action_.push_back(Action(ActionKind::Load, Event(child_tid, 0))); } -void MiriGenmcShim::handle_thread_join(ThreadId thread_id, ThreadId child_id) { +void MiriGenMCInterface::handle_thread_join(ThreadId thread_id, ThreadId child_id) { // The thread join event happens in the parent. const auto ret = GenMCDriver::handleThreadJoin(nullptr, curr_pos(thread_id), child_id, EventDeps()); @@ -592,7 +645,7 @@ void MiriGenmcShim::handle_thread_join(ThreadId thread_id, ThreadId child_id) { // NOTE: Thread return value is ignored, since Miri doesn't need it. } -void MiriGenmcShim::handle_thread_finish(ThreadId thread_id, uint64_t ret_val) { +void MiriGenMCInterface::handle_thread_finish(ThreadId thread_id, uint64_t ret_val) { auto ret = GenMCDriver::handleThreadFinish(nullptr, curr_pos(thread_id), SVal(ret_val)); inc_pos(thread_id, ret.count); ERROR_ON( @@ -601,7 +654,7 @@ void MiriGenmcShim::handle_thread_finish(ThreadId thread_id, uint64_t ret_val) { ); } -void MiriGenmcShim::handle_thread_kill(ThreadId thread_id) { +void MiriGenMCInterface::handle_thread_kill(ThreadId thread_id) { auto ret = GenMCDriver::handleThreadKill(nullptr, curr_pos(thread_id)); inc_pos(thread_id, ret.count); ERROR_ON( diff --git a/genmc-sys/cpp/src/MiriInterface/Setup.cpp b/genmc-sys/cpp/src/Setup.cpp similarity index 94% rename from genmc-sys/cpp/src/MiriInterface/Setup.cpp rename to genmc-sys/cpp/src/Setup.cpp index a0c7ca6cd9..ed95bafbac 100644 --- a/genmc-sys/cpp/src/MiriInterface/Setup.cpp +++ b/genmc-sys/cpp/src/Setup.cpp @@ -52,13 +52,13 @@ static auto to_genmc_verbosity_level(const LogLevel log_level) -> VerbosityLevel /* unsafe */ void set_log_level_raw(LogLevel log_level) { // The `logLevel` is a static, non-atomic variable. - // It should never be changed if `MiriGenmcShim` still exists, since any of its methods may read - // the `logLevel`, otherwise it may cause data races. + // It should never be changed if `MiriGenMCInterface` still exists, since any of its methods may + // read the `logLevel`, otherwise it may cause data races. logLevel = to_genmc_verbosity_level(log_level); } -/* unsafe */ auto MiriGenmcShim::create_handle(const GenmcParams& params, bool estimation_mode) - -> std::unique_ptr { +/* unsafe */ auto MiriGenMCInterface::create_handle(const GenmcParams& params, bool estimation_mode) + -> std::unique_ptr { auto conf = std::make_shared(); // Set whether GenMC should print execution graphs after every explored/blocked execution. @@ -164,7 +164,7 @@ static auto to_genmc_verbosity_level(const LogLevel log_level) -> VerbosityLevel exit(EUSER); } - // Create the actual driver and Miri-GenMC communication shim. - auto driver = std::make_unique(std::move(conf), mode); + // Create the actual driver and Miri-GenMC communication interface. + auto driver = std::make_unique(std::move(conf), mode); return driver; } diff --git a/genmc-sys/src/lib.rs b/genmc-sys/src/lib.rs index 84250007ed..7251a1eafb 100644 --- a/genmc-sys/src/lib.rs +++ b/genmc-sys/src/lib.rs @@ -5,6 +5,28 @@ pub use cxx::UniquePtr; pub use self::ffi::*; +/// The result of a GenMC handle operation, after converting the raw C++ result struct into an +/// idiomatic Rust type. +/// +/// The payload type `T` is operation-specific: +/// - [`LoadResult`]: `T = GenmcScalar` (the value read) +/// - [`NonAtomicResult`]: `T = ()` (no payload) +/// - [`StoreResult`]: `T = bool` (is the write co-max) +/// - [`ReadModifyWriteResult`]:`T = (GenmcScalar, GenmcScalar, bool)` (old, new, is_co_max) +/// +/// For operations with more than one success mode ([`CompareExchangeResult`], +/// [`MutexLockResult`]) the status enums carry sufficient information and should be +/// matched directly. +#[must_use] +pub enum GenmcHandleResult { + /// This execution should be dropped. + Invalid, + /// A verification error occurred; the message is formatted as a string. + Error(String), + /// The operation completed successfully. + Ok(T), +} + /// Defined in "genmc/src/Support/SAddr.hpp". /// The first bit of all global addresses must be set to `1`. /// This means the mask, interpreted as an address, is the lower bound of where the global address space starts. @@ -19,7 +41,7 @@ pub const GENMC_GLOBAL_ADDRESSES_MASK: u64 = 1 << 63; pub const GENMC_MAIN_THREAD_ID: i32 = 0; /// Changing GenMC's log level is not thread safe, so we limit it to only be set once to prevent any data races. -/// This value will be initialized when the first `MiriGenmcShim` is created. +/// This value will be initialized when the first `MiriGenMCInterface` is created. static GENMC_LOG_LEVEL: OnceLock = OnceLock::new(); // Create a new handle to the GenMC model checker. @@ -28,11 +50,11 @@ pub fn create_genmc_driver_handle( params: &GenmcParams, genmc_log_level: LogLevel, do_estimation: bool, -) -> UniquePtr { +) -> UniquePtr { // SAFETY: Only setting the GenMC log level once is guaranteed by the `OnceLock`. // No other place calls `set_log_level_raw`, so the `logLevel` value in GenMC will not change once we initialize it once. - // All functions that use GenMC's `logLevel` can only be accessed in safe Rust through a `MiriGenmcShim`. - // There is no way to get `MiriGenmcShim` other than through `create_handle`, and we only call it *after* setting the log level, preventing any possible data races. + // All functions that use GenMC's `logLevel` can only be accessed in safe Rust through a `MiriGenMCInterface`. + // There is no way to get `MiriGenMCInterface` other than through `create_handle`, and we only call it *after* setting the log level, preventing any possible data races. assert_eq!( &genmc_log_level, GENMC_LOG_LEVEL.get_or_init(|| { @@ -41,7 +63,82 @@ pub fn create_genmc_driver_handle( }), "Attempt to change the GenMC log level after it was already set" ); - unsafe { MiriGenmcShim::create_handle(params, do_estimation) } + unsafe { MiriGenMCInterface::create_handle(params, do_estimation) } +} + +fn cxx_string_to_owned(s: &cxx::UniquePtr) -> String { + s.as_ref().unwrap().to_string_lossy().into_owned() +} + +impl LoadResult { + pub fn into_genmc_result(self) -> GenmcHandleResult { + match self.status { + OperationStatus::Ok => GenmcHandleResult::Ok(self.read_value), + OperationStatus::Error => GenmcHandleResult::Error(cxx_string_to_owned(&self.error)), + OperationStatus::Invalid => GenmcHandleResult::Invalid, + _ => unreachable!("unexpected OperationStatus"), + } + } +} + +impl NonAtomicResult { + pub fn into_genmc_result(self) -> GenmcHandleResult<()> { + match self.status { + OperationStatus::Ok => GenmcHandleResult::Ok(()), + OperationStatus::Error => GenmcHandleResult::Error(cxx_string_to_owned(&self.error)), + OperationStatus::Invalid => GenmcHandleResult::Invalid, + _ => unreachable!("unexpected OperationStatus"), + } + } +} + +impl StoreResult { + pub fn into_genmc_result(self) -> GenmcHandleResult { + match self.status { + OperationStatus::Ok => GenmcHandleResult::Ok(self.is_coherence_order_maximal_write), + OperationStatus::Error => GenmcHandleResult::Error(cxx_string_to_owned(&self.error)), + OperationStatus::Invalid => GenmcHandleResult::Invalid, + _ => unreachable!("unexpected OperationStatus"), + } + } +} + +impl ReadModifyWriteResult { + pub fn into_genmc_result(self) -> GenmcHandleResult<(GenmcScalar, GenmcScalar, bool)> { + match self.status { + OperationStatus::Ok => + GenmcHandleResult::Ok(( + self.old_value, + self.new_value, + self.is_coherence_order_maximal_write, + )), + OperationStatus::Error => GenmcHandleResult::Error(cxx_string_to_owned(&self.error)), + OperationStatus::Invalid => GenmcHandleResult::Invalid, + _ => unreachable!("unexpected OperationStatus"), + } + } +} + +impl MallocResult { + pub fn into_genmc_result(self) -> GenmcHandleResult { + match self.status { + OperationStatus::Ok => GenmcHandleResult::Ok(self.address), + OperationStatus::Error => GenmcHandleResult::Error(cxx_string_to_owned(&self.error)), + OperationStatus::Invalid => GenmcHandleResult::Invalid, + _ => unreachable!("unexpected OperationStatus"), + } + } +} + +impl FreeResult { + pub fn into_genmc_result(self) -> GenmcHandleResult<()> { + match self.status { + OperationStatus::Ok => GenmcHandleResult::Ok(()), + OperationStatus::Error => GenmcHandleResult::Error(cxx_string_to_owned(&self.error)), + OperationStatus::Invalid => GenmcHandleResult::Invalid, + _ => unreachable!("unexpected OperationStatus"), + } + } } impl GenmcScalar { @@ -209,80 +306,131 @@ mod ffi { blocked_execs: u64, } + #[derive(Debug, Clone, Copy)] + /// Status tag shared by operations with a single success mode + /// (atomic loads/stores, non-atomic loads/stores, and FAIs. + /// For operations with multiple success modes, see [`CasStatus`] and [`MutexLockStatus`]. + enum OperationStatus { + /// This execution should be dropped. + Invalid, + /// A verification error occurred; the `error` field is valid. + Error, + /// The operation completed; check the result struct's payload fields. + Ok, + } + + #[derive(Debug, Clone, Copy)] + /// Status tag for [`CompareExchangeResult`]: CAS has two distinct success modes. + enum CasStatus { + /// This execution should be dropped. + Invalid, + /// A verification error occurred; the `error` field is valid. + Error, + /// CAS failed: `old_value` was read but did not equal expected; no write should occur. + Failed, + /// CAS succeeded: `old_value` equals expected; the write should occur, + /// `is_coherence_order_maximal_write` is valid. + Succeeded, + } + + #[derive(Debug, Clone, Copy)] + /// Status tag for [`MutexLockResult`]: mutex lock has three distinct success modes. + enum MutexLockStatus { + /// This execution should be dropped. + Invalid, + /// A verification error occurred; the `error` field is valid. + Error, + /// GenMC wants Miri to retry the lock once this thread is rescheduled. + Reset, + /// The lock was successfully acquired by this thread. + Acquired, + /// The lock is already held; this thread has been blocked on the GenMC side. + NotAcquired, + } + #[must_use] #[derive(Debug)] + /// Result from an atomic load. When `status == Ok`, `read_value` is valid. struct LoadResult { - /// If `true`, exploration should be dropped, **and all other fields are invalid**. - invalid: bool, - /// If not null, contains the error encountered during the handling of the load. + status: OperationStatus, + /// Valid when `status == Error`. error: UniquePtr, - /// The value that was read. Should not be used if `has_value` is `false`. + /// Valid when `status == Ok`. read_value: GenmcScalar, } + #[must_use] + #[derive(Debug)] + /// Result from a non-atomic load or store. GenMC uses these only for data-race detection; + /// no value is communicated back to Miri. When `status == Ok` there is no payload. + struct NonAtomicResult { + status: OperationStatus, + /// Valid when `status == Error`. + error: UniquePtr, + } + #[must_use] #[derive(Debug)] struct StoreResult { - /// If `true`, exploration should be dropped, **and all other fields are invalid**. - invalid: bool, - /// If not null, contains the error encountered during the handling of the store. + status: OperationStatus, + /// Valid when `status == Error`. error: UniquePtr, - /// `true` if the write should also be reflected in Miri's memory representation. + /// Valid when `status == Ok`. `true` if the write should be reflected in Miri's memory. is_coherence_order_maximal_write: bool, } #[must_use] #[derive(Debug)] struct ReadModifyWriteResult { - /// If `true`, exploration should be dropped, **and all other fields are invalid**. - invalid: bool, - /// If there was an error, it will be stored in `error`, otherwise it is `None`. + status: OperationStatus, + /// Valid when `status == Error`. error: UniquePtr, - /// The value that was read by the RMW operation as the left operand. + /// Valid when `status == Ok`. The value read by the RMW. old_value: GenmcScalar, - /// The value that was produced by the RMW operation. + /// Valid when `status == Ok`. The value written by the RMW. new_value: GenmcScalar, - /// `true` if the write should also be reflected in Miri's memory representation. + /// Valid when `status == Ok`. `true` if the write should be reflected in Miri's memory. is_coherence_order_maximal_write: bool, } #[must_use] #[derive(Debug)] struct CompareExchangeResult { - /// If `true`, exploration should be dropped, **and all other fields are invalid**. - invalid: bool, - /// If there was an error, it will be stored in `error`, otherwise it is `None`. + status: CasStatus, + /// Valid when `status == Error`. error: UniquePtr, - /// The value that was read by the compare-exchange. + /// Valid when `status == Failed` or `status == Succeeded`. old_value: GenmcScalar, - /// `true` if compare_exchange op was successful. - is_success: bool, - /// `true` if the write should also be reflected in Miri's memory representation. + /// Valid when `status == Succeeded`. `true` if the write should be reflected in Miri's memory. is_coherence_order_maximal_write: bool, } #[must_use] #[derive(Debug)] struct MutexLockResult { - /// If `true`, exploration should be dropped, **and all other fields are invalid**. - invalid: bool, - /// If there was an error, it will be stored in `error`, otherwise it is `None`. + status: MutexLockStatus, + /// Valid when `status == Error`. error: UniquePtr, - /// If true, GenMC determined that we should retry the mutex lock operation once the thread attempting to lock is scheduled again. - is_reset: bool, - /// Indicate whether the lock was acquired by this thread. - is_lock_acquired: bool, } #[must_use] #[derive(Debug)] struct MallocResult { - /// If not null, contains the error encountered during the handling of malloc. + status: OperationStatus, + /// Valid when `status == Error`. error: UniquePtr, - /// The allocated address. + /// Valid when `status == Ok`. The allocated address. address: u64, } + #[must_use] + #[derive(Debug)] + struct FreeResult { + status: OperationStatus, + /// Valid when `status == Error`. + error: UniquePtr, + } + /**** These are GenMC types that we have to copy-paste here since cxx does not support "importing" externally defined C++ types. ****/ @@ -346,14 +494,14 @@ mod ffi { // This block is unsafe to allow defining safe methods inside. // // `get_global_alloc_static_mask` is safe since it just returns a constant. - // All methods on `MiriGenmcShim` are safe by the correct usage of the two unsafe functions - // `set_log_level_raw` and `MiriGenmcShim::create_handle`. + // All methods on `MiriGenMCInterface` are safe by the correct usage of the two unsafe functions + // `set_log_level_raw` and `MiriGenMCInterface::create_handle`. // See the doc comment on those two functions for their safety requirements. unsafe extern "C++" { include!("MiriInterface.hpp"); /**** Types shared between Miri/Rust and Miri/C++: ****/ - type MiriGenmcShim; + type MiriGenMCInterface; /**** Types shared between Miri/Rust and GenMC/C++: (This tells cxx that the enums defined above are already defined on the C++ side; @@ -374,36 +522,36 @@ mod ffi { /// Never calling this function is safe, GenMC will fall back to its default log level. unsafe fn set_log_level_raw(log_level: LogLevel); - /// Create a new `MiriGenmcShim`, which wraps a `GenMCDriver`. + /// Create a new `MiriGenMCInterface`, which wraps a `GenMCDriver`. /// /// # Safety /// /// This function is marked as unsafe since the `logLevel` global variable is non-atomic. /// This function should not be called in an unsynchronized way with `set_log_level_raw`, since - /// this function and any methods on the returned `MiriGenmcShim` may read the `logLevel`, + /// this function and any methods on the returned `MiriGenMCInterface` may read the `logLevel`, /// causing a data race. /// The safest way to use these functions is to call `set_log_level_raw` once, and only then /// start creating handles. - /// There should not be any other (safe) way to create a `MiriGenmcShim`. - #[Self = "MiriGenmcShim"] + /// There should not be any other (safe) way to create a `MiriGenMCInterface`. + #[Self = "MiriGenMCInterface"] unsafe fn create_handle( params: &GenmcParams, estimation_mode: bool, - ) -> UniquePtr; + ) -> UniquePtr; /// Get the bit mask that GenMC expects for global memory allocations. fn get_global_alloc_static_mask() -> u64; /// This function must be called at the start of any execution, before any events are reported to GenMC. - fn handle_execution_start(self: Pin<&mut MiriGenmcShim>); + fn handle_execution_start(self: Pin<&mut MiriGenMCInterface>); /// This function must be called at the end of any execution, even if an error was found during the execution. /// Returns `null`, or a string containing an error message if an error occurred. - fn handle_execution_end(self: Pin<&mut MiriGenmcShim>) -> UniquePtr; + fn handle_execution_end(self: Pin<&mut MiriGenMCInterface>) -> UniquePtr; /***** Functions for handling events encountered during program execution. *****/ /**** Memory access handling ****/ fn handle_atomic_load( - self: Pin<&mut MiriGenmcShim>, + self: Pin<&mut MiriGenMCInterface>, thread_id: i32, address: u64, size: u64, @@ -411,13 +559,13 @@ mod ffi { old_value: GenmcScalar, ) -> LoadResult; fn handle_non_atomic_load( - self: Pin<&mut MiriGenmcShim>, + self: Pin<&mut MiriGenMCInterface>, thread_id: i32, address: u64, size: u64, - ) -> LoadResult; + ) -> NonAtomicResult; fn handle_read_modify_write( - self: Pin<&mut MiriGenmcShim>, + self: Pin<&mut MiriGenMCInterface>, thread_id: i32, address: u64, size: u64, @@ -427,7 +575,7 @@ mod ffi { old_value: GenmcScalar, ) -> ReadModifyWriteResult; fn handle_compare_exchange( - self: Pin<&mut MiriGenmcShim>, + self: Pin<&mut MiriGenMCInterface>, thread_id: i32, address: u64, size: u64, @@ -439,7 +587,7 @@ mod ffi { can_fail_spuriously: bool, ) -> CompareExchangeResult; fn handle_atomic_store( - self: Pin<&mut MiriGenmcShim>, + self: Pin<&mut MiriGenMCInterface>, thread_id: i32, address: u64, size: u64, @@ -448,62 +596,62 @@ mod ffi { memory_ordering: MemOrdering, ) -> StoreResult; fn handle_non_atomic_store( - self: Pin<&mut MiriGenmcShim>, + self: Pin<&mut MiriGenMCInterface>, thread_id: i32, address: u64, size: u64, - ) -> StoreResult; + ) -> NonAtomicResult; fn handle_fence( - self: Pin<&mut MiriGenmcShim>, + self: Pin<&mut MiriGenMCInterface>, thread_id: i32, memory_ordering: MemOrdering, ); /**** Memory (de)allocation ****/ fn handle_malloc( - self: Pin<&mut MiriGenmcShim>, + self: Pin<&mut MiriGenMCInterface>, thread_id: i32, size: u64, alignment: u64, ) -> MallocResult; /// Returns true if an error was found. fn handle_free( - self: Pin<&mut MiriGenmcShim>, + self: Pin<&mut MiriGenMCInterface>, thread_id: i32, address: u64, - ) -> UniquePtr; + ) -> FreeResult; /**** Thread management ****/ - fn handle_thread_create(self: Pin<&mut MiriGenmcShim>, thread_id: i32, parent_id: i32); - fn handle_thread_join(self: Pin<&mut MiriGenmcShim>, thread_id: i32, child_id: i32); - fn handle_thread_finish(self: Pin<&mut MiriGenmcShim>, thread_id: i32, ret_val: u64); - fn handle_thread_kill(self: Pin<&mut MiriGenmcShim>, thread_id: i32); + fn handle_thread_create(self: Pin<&mut MiriGenMCInterface>, thread_id: i32, parent_id: i32); + fn handle_thread_join(self: Pin<&mut MiriGenMCInterface>, thread_id: i32, child_id: i32); + fn handle_thread_finish(self: Pin<&mut MiriGenMCInterface>, thread_id: i32, ret_val: u64); + fn handle_thread_kill(self: Pin<&mut MiriGenMCInterface>, thread_id: i32); /**** Blocking instructions ****/ /// Inform GenMC that the thread should be blocked. /// Note: this function is currently hardcoded for `AssumeType::User`, corresponding to user supplied assume statements. /// This can become a parameter once more types of assumes are added. fn handle_assume_block( - self: Pin<&mut MiriGenmcShim>, + self: Pin<&mut MiriGenMCInterface>, thread_id: i32, assume_type: AssumeType, ); /**** Mutex handling ****/ fn handle_mutex_lock( - self: Pin<&mut MiriGenmcShim>, + self: Pin<&mut MiriGenMCInterface>, thread_id: i32, address: u64, size: u64, ) -> MutexLockResult; fn handle_mutex_try_lock( - self: Pin<&mut MiriGenmcShim>, + self: Pin<&mut MiriGenMCInterface>, thread_id: i32, address: u64, size: u64, ) -> MutexLockResult; fn handle_mutex_unlock( - self: Pin<&mut MiriGenmcShim>, + self: Pin<&mut MiriGenMCInterface>, thread_id: i32, address: u64, size: u64, @@ -515,14 +663,14 @@ mod ffi { /// return whether the execution is finished, blocked, or can continue. /// Updates the next instruction kind for the given thread id. fn schedule_next( - self: Pin<&mut MiriGenmcShim>, + self: Pin<&mut MiriGenMCInterface>, curr_thread_id: i32, curr_thread_next_instr_kind: ActionKind, ) -> SchedulingResult; /// Check whether there are more executions to explore. /// If there are more executions, this method prepares for the next execution and returns `true`. - fn is_exploration_done(self: Pin<&mut MiriGenmcShim>) -> bool; + fn is_exploration_done(self: Pin<&mut MiriGenMCInterface>) -> bool; /**** Result querying functionality. ****/ @@ -530,24 +678,24 @@ mod ffi { // is very large, uses features that CXX.rs doesn't support and may change as GenMC changes. // Instead, we only use the result on the C++ side, and only expose these getter function to // the Rust side. - // Each `GenMCDriver` contains one `VerificationResult`, and each `MiriGenmcShim` contains on `GenMCDriver`. + // Each `GenMCDriver` contains one `VerificationResult`, and each `MiriGenMCInterface` contains on `GenMCDriver`. // GenMC builds up the content of the `struct VerificationResult` over the course of an exploration, - // but it's safe to look at it at any point, since it is only accessible through exactly one `MiriGenmcShim`. + // but it's safe to look at it at any point, since it is only accessible through exactly one `MiriGenMCInterface`. // All these functions for querying the result can be safely called repeatedly and at any time, // though the results may be incomplete if called before `handle_execution_end`. /// Get the number of blocked executions encountered by GenMC (cast into a fixed with integer) - fn get_blocked_execution_count(self: &MiriGenmcShim) -> u64; + fn get_blocked_execution_count(self: &MiriGenMCInterface) -> u64; /// Get the number of executions explored by GenMC (cast into a fixed with integer) - fn get_explored_execution_count(self: &MiriGenmcShim) -> u64; + fn get_explored_execution_count(self: &MiriGenMCInterface) -> u64; /// Get all messages that GenMC produced (errors, warnings), combined into one string. - fn get_result_message(self: &MiriGenmcShim) -> UniquePtr; + fn get_result_message(self: &MiriGenMCInterface) -> UniquePtr; /// If an error occurred, return a string describing the error, otherwise, return `nullptr`. - fn get_error_string(self: &MiriGenmcShim) -> UniquePtr; + fn get_error_string(self: &MiriGenMCInterface) -> UniquePtr; /**** Printing functionality. ****/ /// Get the results of a run in estimation mode. - fn get_estimation_results(self: &MiriGenmcShim) -> EstimationResult; + fn get_estimation_results(self: &MiriGenMCInterface) -> EstimationResult; } } diff --git a/src/concurrency/genmc/mod.rs b/src/concurrency/genmc/mod.rs index b2a4b2dd85..db57ee8529 100644 --- a/src/concurrency/genmc/mod.rs +++ b/src/concurrency/genmc/mod.rs @@ -2,8 +2,8 @@ use std::cell::{Cell, RefCell}; use std::sync::Arc; use genmc_sys::{ - EstimationResult, GENMC_GLOBAL_ADDRESSES_MASK, GenmcScalar, MemOrdering, MiriGenmcShim, - RMWBinOp, UniquePtr, create_genmc_driver_handle, + CasStatus, EstimationResult, GENMC_GLOBAL_ADDRESSES_MASK, GenmcHandleResult, GenmcScalar, + MemOrdering, MiriGenMCInterface, RMWBinOp, UniquePtr, create_genmc_driver_handle, }; use rustc_abi::{Align, Size}; use rustc_const_eval::interpret::{AllocId, InterpCx, InterpResult, interp_ok}; @@ -103,7 +103,7 @@ impl GlobalState { } /// The main interface with GenMC. -/// Each `GenmcCtx` owns one `MiriGenmcShim`, which owns one `GenMCDriver` (the GenMC model checker). +/// Each `GenmcCtx` owns one `MiriGenMCInterface`, which owns one `GenMCDriver` (the GenMC model checker). /// For each GenMC run (estimation or verification), one or more `GenmcCtx` can be created (one per Miri thread). /// However, for now, we only ever have one `GenmcCtx` per run. /// @@ -116,7 +116,7 @@ impl GlobalState { /// Some state is reset between each execution in the same run. pub struct GenmcCtx { /// Handle to the GenMC model checker. - handle: RefCell>, + handle: RefCell>, /// State that is reset at the start of every execution. exec_state: PerExecutionState, @@ -451,24 +451,26 @@ impl GenmcCtx { can_fail_spuriously, ); - if cas_result.invalid { - throw_machine_stop!(TerminationInfo::GenmcSkip); - } - if let Some(error) = cas_result.error.as_ref() { + match cas_result.status { + CasStatus::Invalid => throw_machine_stop!(TerminationInfo::GenmcSkip), + CasStatus::Error => // FIXME(genmc): error handling - throw_ub_format!("{}", error.to_string_lossy()); + throw_ub_format!("{}", cas_result.error.as_ref().unwrap().to_string_lossy()), + CasStatus::Failed | CasStatus::Succeeded => {} + status => unreachable!("unexpected CasStatus: {status:?}"), } let return_scalar = genmc_scalar_to_scalar(ecx, self, cas_result.old_value, size)?; + let is_success = matches!(cas_result.status, CasStatus::Succeeded); debug!( "GenMC: atomic_compare_exchange: result: {cas_result:?}, returning scalar: {return_scalar:?}" ); // The write can only be a co-maximal write if the CAS succeeded. - assert!(cas_result.is_success || !cas_result.is_coherence_order_maximal_write); + assert!(is_success || !cas_result.is_coherence_order_maximal_write); interp_ok(( return_scalar, cas_result.is_coherence_order_maximal_write.then_some(new_value), - cas_result.is_success, + is_success, )) } @@ -553,10 +555,12 @@ impl GenmcCtx { genmc_size, alignment.bytes(), ); - if let Some(_error) = malloc_result.error.as_ref() { - throw_exhaust!(AddressSpaceFull); - } - let chosen_address = malloc_result.address; + // FIXME(genmc): error handling + let chosen_address = match malloc_result.into_genmc_result() { + GenmcHandleResult::Invalid => throw_machine_stop!(TerminationInfo::GenmcSkip), + GenmcHandleResult::Error(_e) => throw_exhaust!(AddressSpaceFull), + GenmcHandleResult::Ok(a) => a, + }; // Non-global addresses should not be in the global address space. assert_eq!(0, chosen_address & GENMC_GLOBAL_ADDRESSES_MASK); @@ -591,11 +595,13 @@ impl GenmcCtx { .borrow_mut() .pin_mut() .handle_free(self.active_thread_genmc_tid(machine), address.bytes()); - if let Some(error) = free_result.as_ref() { - // FIXME(genmc): improve error handling. - throw_ub_format!("{}", error.to_string_lossy()); - } + // FIXME(genmc): error handling + match free_result.into_genmc_result() { + GenmcHandleResult::Invalid => throw_machine_stop!(TerminationInfo::GenmcSkip), + GenmcHandleResult::Error(e) => throw_ub_format!("{e}"), + GenmcHandleResult::Ok(()) => {} + } interp_ok(()) } @@ -716,16 +722,14 @@ impl GenmcCtx { genmc_old_value, ); - if load_result.invalid { - throw_machine_stop!(TerminationInfo::GenmcSkip); - } - if let Some(error) = load_result.error.as_ref() { - // FIXME(genmc): error handling - throw_ub_format!("{}", error.to_string_lossy()); - } - - debug!("GenMC: load returned value: {:?}", load_result.read_value); - interp_ok(load_result.read_value) + // FIXME(genmc): error handling + let read_value = match load_result.into_genmc_result() { + GenmcHandleResult::Invalid => throw_machine_stop!(TerminationInfo::GenmcSkip), + GenmcHandleResult::Error(e) => throw_ub_format!("{e}"), + GenmcHandleResult::Ok(v) => v, + }; + debug!("GenMC: load returned value: {:?}", read_value); + interp_ok(read_value) } /// Inform GenMC about a non-atomic load. @@ -746,12 +750,11 @@ impl GenmcCtx { size.bytes(), ); - if load_result.invalid { - throw_machine_stop!(TerminationInfo::GenmcSkip); - } - if let Some(error) = load_result.error.as_ref() { - // FIXME(genmc): error handling - throw_ub_format!("{}", error.to_string_lossy()); + // FIXME(genmc): error handling + match load_result.into_genmc_result() { + GenmcHandleResult::Invalid => throw_machine_stop!(TerminationInfo::GenmcSkip), + GenmcHandleResult::Error(e) => throw_ub_format!("{e}"), + GenmcHandleResult::Ok(()) => {} } // `load_result.read_value` is just a dummy for non-atomic loads. And anyway Miri doesn't // give us a chance to change the value here, it'll always use the one from its memory. @@ -791,15 +794,13 @@ impl GenmcCtx { memory_ordering, ); - if store_result.invalid { - throw_machine_stop!(TerminationInfo::GenmcSkip); - } - if let Some(error) = store_result.error.as_ref() { - // FIXME(genmc): error handling - throw_ub_format!("{}", error.to_string_lossy()); - } - - interp_ok(store_result.is_coherence_order_maximal_write) + // FIXME(genmc): error handling + let is_co_max = match store_result.into_genmc_result() { + GenmcHandleResult::Invalid => throw_machine_stop!(TerminationInfo::GenmcSkip), + GenmcHandleResult::Error(e) => throw_ub_format!("{e}"), + GenmcHandleResult::Ok(v) => v, + }; + interp_ok(is_co_max) } /// Inform GenMC about a non-atomic store. @@ -820,15 +821,12 @@ impl GenmcCtx { size.bytes(), ); - if store_result.invalid { - throw_machine_stop!(TerminationInfo::GenmcSkip); - } - if let Some(error) = store_result.error.as_ref() { - // FIXME(genmc): error handling - throw_ub_format!("{}", error.to_string_lossy()); + // FIXME(genmc): error handling + match store_result.into_genmc_result() { + GenmcHandleResult::Invalid => throw_machine_stop!(TerminationInfo::GenmcSkip), + GenmcHandleResult::Error(e) => throw_ub_format!("{e}"), + GenmcHandleResult::Ok(()) => {} } - // Miri will always write non-atomic stores to memory. Make sure GenMC agrees with that. - assert!(store_result.is_coherence_order_maximal_write); interp_ok(()) } @@ -870,18 +868,15 @@ impl GenmcCtx { genmc_old_value, ); - if rmw_result.invalid { - throw_machine_stop!(TerminationInfo::GenmcSkip); - } - if let Some(error) = rmw_result.error.as_ref() { - // FIXME(genmc): error handling - throw_ub_format!("{}", error.to_string_lossy()); - } - - let old_value_scalar = genmc_scalar_to_scalar(ecx, self, rmw_result.old_value, size)?; - - let new_value_scalar = if rmw_result.is_coherence_order_maximal_write { - Some(genmc_scalar_to_scalar(ecx, self, rmw_result.new_value, size)?) + // FIXME(genmc): error handling + let (old_value, new_value, is_co_max) = match rmw_result.into_genmc_result() { + GenmcHandleResult::Invalid => throw_machine_stop!(TerminationInfo::GenmcSkip), + GenmcHandleResult::Error(e) => throw_ub_format!("{e}"), + GenmcHandleResult::Ok(v) => v, + }; + let old_value_scalar = genmc_scalar_to_scalar(ecx, self, old_value, size)?; + let new_value_scalar = if is_co_max { + Some(genmc_scalar_to_scalar(ecx, self, new_value, size)?) } else { None }; diff --git a/src/concurrency/genmc/shims.rs b/src/concurrency/genmc/shims.rs index ff9d43e70a..2718366614 100644 --- a/src/concurrency/genmc/shims.rs +++ b/src/concurrency/genmc/shims.rs @@ -1,4 +1,4 @@ -use genmc_sys::AssumeType; +use genmc_sys::{AssumeType, GenmcHandleResult, MutexLockStatus}; use rustc_middle::ty; use tracing::debug; @@ -85,46 +85,53 @@ trait EvalContextExtPriv<'tcx>: crate::MiriInterpCxExt<'tcx> { mutex.ptr().addr().bytes(), size, ); - if let Some(error) = result.error.as_ref() { + match result.status { + MutexLockStatus::Invalid => throw_machine_stop!(TerminationInfo::GenmcSkip), + MutexLockStatus::Error => // FIXME(genmc): improve error handling. - throw_ub_format!("{}", error.to_string_lossy()); - } - if result.is_reset { - debug!("GenMC: Mutex::lock: Reset"); - // GenMC informed us to reset and try the lock again later. - // We block the current thread until GenMC schedules it again. - this.block_thread( - crate::BlockReason::Genmc, - None, - crate::callback!( - @capture<'tcx> { - mutex: MPlaceTy<'tcx>, - } - |this, unblock: crate::UnblockKind| { - debug!("GenMC: Mutex::lock: unblocking callback called, attempting to lock the Mutex again."); - assert_eq!(unblock, crate::UnblockKind::Ready); - this.intercept_mutex_lock(mutex)?; - interp_ok(()) - } - ), - ); - } else if result.is_lock_acquired { - debug!("GenMC: Mutex::lock successfully acquired the Mutex."); - } else { - debug!("GenMC: Mutex::lock failed to acquire the Mutex, permanently blocking thread."); - // NOTE: `handle_mutex_lock` already blocked the current thread on the GenMC side. - this.block_thread( - crate::BlockReason::Genmc, - None, - crate::callback!( - @capture<'tcx> { - mutex: MPlaceTy<'tcx>, - } - |_this, _unblock: crate::UnblockKind| { - unreachable!("A thread blocked on `Mutex::lock` should not be unblocked again."); - } - ), - ); + throw_ub_format!("{}", result.error.as_ref().unwrap().to_string_lossy()), + MutexLockStatus::Reset => { + debug!("GenMC: Mutex::lock: Reset"); + // GenMC informed us to reset and try the lock again later. + // We block the current thread until GenMC schedules it again. + this.block_thread( + crate::BlockReason::Genmc, + None, + crate::callback!( + @capture<'tcx> { + mutex: MPlaceTy<'tcx>, + } + |this, unblock: crate::UnblockKind| { + debug!("GenMC: Mutex::lock: unblocking callback called, attempting to lock the Mutex again."); + assert_eq!(unblock, crate::UnblockKind::Ready); + this.intercept_mutex_lock(mutex)?; + interp_ok(()) + } + ), + ); + } + MutexLockStatus::Acquired => { + debug!("GenMC: Mutex::lock successfully acquired the Mutex."); + } + MutexLockStatus::NotAcquired => { + debug!( + "GenMC: Mutex::lock failed to acquire the Mutex, permanently blocking thread." + ); + // NOTE: `handle_mutex_lock` already blocked the current thread on the GenMC side. + this.block_thread( + crate::BlockReason::Genmc, + None, + crate::callback!( + @capture<'tcx> { + mutex: MPlaceTy<'tcx>, + } + |_this, _unblock: crate::UnblockKind| { + unreachable!("A thread blocked on `Mutex::lock` should not be unblocked again."); + } + ), + ); + } + status => unreachable!("unexpected MutexLockStatus: {status:?}"), } // NOTE: We don't write anything back to Miri's memory where the Mutex is located, that state is handled only by GenMC. interp_ok(()) @@ -148,17 +155,19 @@ trait EvalContextExtPriv<'tcx>: crate::MiriInterpCxExt<'tcx> { mutex.ptr().addr().bytes(), size, ); - if let Some(error) = result.error.as_ref() { + match result.status { + MutexLockStatus::Invalid => throw_machine_stop!(TerminationInfo::GenmcSkip), + MutexLockStatus::Error => // FIXME(genmc): improve error handling. - throw_ub_format!("{}", error.to_string_lossy()); + throw_ub_format!("{}", result.error.as_ref().unwrap().to_string_lossy()), + MutexLockStatus::Reset => panic!("GenMC returned 'reset' for a mutex try_lock."), + MutexLockStatus::Acquired | MutexLockStatus::NotAcquired => {} + status => unreachable!("unexpected MutexLockStatus: {status:?}"), } - debug!( - "GenMC: Mutex::try_lock(): is_reset: {}, is_lock_acquired: {}", - result.is_reset, result.is_lock_acquired - ); - assert!(!result.is_reset, "GenMC returned 'reset' for a mutex try_lock."); + debug!("GenMC: Mutex::try_lock(): status: {:?}", result.status); + let is_acquired = matches!(result.status, MutexLockStatus::Acquired); // Write the return value of try_lock, i.e., whether we acquired the mutex. - this.write_scalar(Scalar::from_bool(result.is_lock_acquired), dest)?; + this.write_scalar(Scalar::from_bool(is_acquired), dest)?; // NOTE: We don't write anything back to Miri's memory where the Mutex is located, that state is handled only by GenMC. interp_ok(()) } @@ -172,11 +181,13 @@ trait EvalContextExtPriv<'tcx>: crate::MiriInterpCxExt<'tcx> { mutex.ptr().addr().bytes(), mutex.layout.size.bytes(), ); - if let Some(error) = result.error.as_ref() { - // FIXME(genmc): improve error handling. - throw_ub_format!("{}", error.to_string_lossy()); + // FIXME(genmc): improve error handling. + match result.into_genmc_result() { + GenmcHandleResult::Invalid => throw_machine_stop!(TerminationInfo::GenmcSkip), + GenmcHandleResult::Error(e) => throw_ub_format!("{e}"), + GenmcHandleResult::Ok(_) => {} } - // NOTE: We don't write anything back to Miri's memory where the Mutex is located, that state is handled only by GenMC.} + // NOTE: We don't write anything back to Miri's memory where the Mutex is located, that state is handled only by GenMC. interp_ok(()) } }