diff --git a/src/tools/miri/genmc-sys/build.rs b/src/tools/miri/genmc-sys/build.rs index 9e956449a13d..a22e3341d67a 100644 --- a/src/tools/miri/genmc-sys/build.rs +++ b/src/tools/miri/genmc-sys/build.rs @@ -28,7 +28,7 @@ mod downloading { /// The GenMC repository the we get our commit from. pub(crate) const GENMC_GITHUB_URL: &str = "https://github.com/MPI-SWS/genmc.git"; /// The GenMC commit we depend on. It must be available on the specified GenMC repository. - pub(crate) const GENMC_COMMIT: &str = "aa10ed65117c3291524efc19253b5d443a4602ac"; + pub(crate) const GENMC_COMMIT: &str = "22d3d0b44dedb4e8e1aae3330e546465e4664529"; /// Ensure that a local GenMC repo is present and set to the correct commit. /// Return the path of the GenMC repo and whether the checked out commit was changed. @@ -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/include/MiriInterface.hpp b/src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp index 4929c0cfa150..b6b7b06509a5 100644 --- a/src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp +++ b/src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp @@ -125,8 +125,11 @@ struct MiriGenmcShim : private GenMCDriver { void handle_fence(ThreadId thread_id, MemOrdering ord); /**** Memory (de)allocation ****/ + auto handle_malloc(ThreadId thread_id, uint64_t size, uint64_t alignment) -> uint64_t; - auto handle_free(ThreadId thread_id, uint64_t address) -> bool; + + /** Returns null on success, or an error string if an error occurs. */ + auto handle_free(ThreadId thread_id, uint64_t address) -> std::unique_ptr; /**** Thread management ****/ void handle_thread_create(ThreadId thread_id, ThreadId parent_id); diff --git a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/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..d5a3833e2e83 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())); @@ -50,9 +68,230 @@ void MiriGenmcShim::handle_execution_start() { } auto MiriGenmcShim::handle_execution_end() -> std::unique_ptr { - // FIXME(genmc): add error handling once GenMC returns an error here. - GenMCDriver::handleExecutionEnd(); - return {}; + auto ret = GenMCDriver::handleExecutionEnd(); + return ret.has_value() ? format_error(*ret) : nullptr; +} + +/**** Blocking instructions ****/ + +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. + ERROR_ON(!ret_val, "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 auto* is_co_max = std::get_if(&ret); + // FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values. + ERROR_ON(!is_co_max, "Unimplemented: Store returned unexpected result."); + return StoreResultExt::ok(*is_co_max); +} + +void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) { + 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. + ERROR_ON(!ret_val, "Unimplemented: read-modify-write returned unexpected result."); + const auto read_old_val = *ret_val; + const auto new_value = + executeRMWBinOp(read_old_val, GenmcScalarExt::to_sval(rhs_value), size, rmw_op); + + 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 auto* is_co_max = std::get_if(&store_ret); + // FIXME(genmc): handle `HandleResult::{Invalid, 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 + ); +} + +[[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 auto* is_co_max = std::get_if(&store_ret); + // FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values. + ERROR_ON(!is_co_max, "Unimplemented: compare-exchange store returned unexpected result."); + return CompareExchangeResultExt::success(read_old_val, *is_co_max); +} + +/**** 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) + -> std::unique_ptr { + auto pos = inc_pos(thread_id); + auto ret = GenMCDriver::handleFree(nullptr, pos, SAddr(address), EventDeps()); + return ret.has_value() ? format_error(*ret) : nullptr; } /**** Estimation mode result ****/ @@ -66,3 +305,187 @@ auto MiriGenmcShim::get_estimation_results() const -> EstimationResult { .blocked_execs = static_cast(res.exploredBlocked), }; } + +/** Mutexes */ + +struct MutexState { + static constexpr SVal UNLOCKED { 0 }; + static constexpr SVal LOCKED { 1 }; + + static constexpr bool isValid(SVal v) { + return v == UNLOCKED || v == LOCKED; + } +}; + +auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint64_t size) + -> MutexLockResult { + // 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, MutexState::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 = MutexState::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(!MutexState::isValid(*ret_val), "Mutex read value was neither 0 nor 1"); + if (*ret_val == MutexState::LOCKED) { + // We did not acquire the mutex, so we tell GenMC to block the thread until we can acquire + // it. GenMC determines this based on the annotation we pass with the load further up in + // this function, namely when that load will read a value other than `MutexState::LOCKED`. + this->handle_assume_block(thread_id, AssumeType::Spinloop); + return MutexLockResultExt::ok(false); + } + + const auto store_ret = GenMCDriver::handleStore( + nullptr, + inc_pos(thread_id), + old_val, + address, + size, + EventDeps() + ); + if (const auto* err = std::get_if(&store_ret)) + return MutexLockResultExt::from_error(format_error(*err)); + // We don't update Miri's memory for this operation so we don't need to know if the store + // was the co-maximal store, but we still check that we at least get a boolean as the result + // of the store. + const auto* is_co_max = std::get_if(&store_ret); + ERROR_ON(!is_co_max, "Unimplemented: mutex_try_lock store returned unexpected result."); + return MutexLockResultExt::ok(true); +} + +auto MiriGenmcShim::handle_mutex_try_lock(ThreadId thread_id, uint64_t address, uint64_t size) + -> 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 = MutexState::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); + 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. */ + + 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 auto* is_co_max = std::get_if(&store_ret); + ERROR_ON(!is_co_max, "Unimplemented: store part of mutex try_lock returned unexpected result."); + return MutexLockResultExt::ok(true); +} + +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 */ MutexState::UNLOCKED, + MemOrdering::Release, + SAddr(address), + ASize(size), + AType::Signed, + /* store_value */ MutexState::UNLOCKED, + EventDeps() + ); + if (const auto* err = std::get_if(&ret)) + return StoreResultExt::from_error(format_error(*err)); + const auto* is_co_max = std::get_if(&ret); + ERROR_ON(!is_co_max, "Unimplemented: store part of mutex unlock returned unexpected result."); + return StoreResultExt::ok(*is_co_max); +} + +/** Thread creation/joining */ + +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" }; + + 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); + + 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); + 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); -} diff --git a/src/tools/miri/genmc-sys/src/lib.rs b/src/tools/miri/genmc-sys/src/lib.rs index 69aeca3ebc72..b3a9880211de 100644 --- a/src/tools/miri/genmc-sys/src/lib.rs +++ b/src/tools/miri/genmc-sys/src/lib.rs @@ -438,7 +438,11 @@ mod ffi { alignment: u64, ) -> u64; /// Returns true if an error was found. - fn handle_free(self: Pin<&mut MiriGenmcShim>, thread_id: i32, address: u64) -> bool; + fn handle_free( + self: Pin<&mut MiriGenmcShim>, + thread_id: i32, + address: u64, + ) -> UniquePtr; /**** Thread management ****/ fn handle_thread_create(self: Pin<&mut MiriGenmcShim>, thread_id: i32, parent_id: i32); diff --git a/src/tools/miri/src/concurrency/genmc/mod.rs b/src/tools/miri/src/concurrency/genmc/mod.rs index 6628e096a25d..73da0e11daaf 100644 --- a/src/tools/miri/src/concurrency/genmc/mod.rs +++ b/src/tools/miri/src/concurrency/genmc/mod.rs @@ -592,9 +592,11 @@ impl GenmcCtx { genmc_size, alignment.bytes(), ); + if chosen_address == 0 { + throw_exhaust!(AddressSpaceFull); + } - // Non-global addresses should not be in the global address space or null. - assert_ne!(0, chosen_address, "GenMC malloc returned nullptr."); + // Non-global addresses should not be in the global address space. assert_eq!(0, chosen_address & GENMC_GLOBAL_ADDRESSES_MASK); // Sanity check the address alignment: assert!( @@ -622,15 +624,14 @@ impl GenmcCtx { !self.get_alloc_data_races(), "memory deallocation with data race checking disabled." ); - if self + let free_result = self .handle .borrow_mut() .pin_mut() - .handle_free(self.active_thread_genmc_tid(machine), address.bytes()) - { + .handle_free(self.active_thread_genmc_tid(machine), address.bytes()); + if let Some(error) = free_result.as_ref() { // FIXME(genmc): improve error handling. - // An error was detected, so we get the error string from GenMC. - throw_ub_format!("{}", self.try_get_error().unwrap()); + throw_ub_format!("{}", error.to_string_lossy()); } interp_ok(()) diff --git a/src/tools/miri/src/diagnostics.rs b/src/tools/miri/src/diagnostics.rs index bb8ba196983c..8e252d306b29 100644 --- a/src/tools/miri/src/diagnostics.rs +++ b/src/tools/miri/src/diagnostics.rs @@ -362,6 +362,10 @@ pub fn report_result<'tcx>( vec![ note!("this is likely not a bug in the program; it indicates that the program performed an operation that Miri does not support"), ], + ResourceExhaustion(ResourceExhaustionInfo::AddressSpaceFull) if ecx.machine.data_race.as_genmc_ref().is_some() => + vec![ + note!("in GenMC mode, the address space is limited to 4GB per thread, and addresses cannot be reused") + ], UndefinedBehavior(AlignmentCheckFailed { .. }) if ecx.machine.check_alignment == AlignmentCheck::Symbolic => diff --git a/src/tools/miri/tests/genmc/fail/simple/alloc_large.multiple.stderr b/src/tools/miri/tests/genmc/fail/simple/alloc_large.multiple.stderr new file mode 100644 index 000000000000..1d56614c7f03 --- /dev/null +++ b/src/tools/miri/tests/genmc/fail/simple/alloc_large.multiple.stderr @@ -0,0 +1,26 @@ +Running GenMC Verification... +error: resource exhaustion: there are no more free addresses in the address space + --> RUSTLIB/alloc/src/raw_vec/mod.rs:LL:CC + | +LL | AllocInit::Uninitialized => alloc.allocate(layout), + | ^^^^^^^^^^^^^^^^^^^^^^ resource exhaustion occurred here + | + = help: in GenMC mode, the address space is limited to 4GB per thread, and addresses cannot be reused + = note: BACKTRACE: + = note: inside `alloc::raw_vec::RawVecInner::try_allocate_in` at RUSTLIB/alloc/src/raw_vec/mod.rs:LL:CC + = note: inside `alloc::raw_vec::RawVecInner::with_capacity_in` at RUSTLIB/alloc/src/raw_vec/mod.rs:LL:CC + = note: inside `alloc::raw_vec::RawVec::::with_capacity_in` at RUSTLIB/alloc/src/raw_vec/mod.rs:LL:CC + = note: inside `std::vec::Vec::::with_capacity_in` at RUSTLIB/alloc/src/vec/mod.rs:LL:CC + = note: inside `std::vec::Vec::::with_capacity` at RUSTLIB/alloc/src/vec/mod.rs:LL:CC +note: inside `miri_start` + --> tests/genmc/fail/simple/alloc_large.rs:LL:CC + | +LL | let _v = Vec::::with_capacity(1024 * 1024 * 1024); + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace + +note: add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report + +error: aborting due to 1 previous error + diff --git a/src/tools/miri/tests/genmc/fail/simple/alloc_large.rs b/src/tools/miri/tests/genmc/fail/simple/alloc_large.rs new file mode 100644 index 000000000000..27d92bf66d42 --- /dev/null +++ b/src/tools/miri/tests/genmc/fail/simple/alloc_large.rs @@ -0,0 +1,24 @@ +//@revisions: single multiple +//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows +//@error-in-other-file: resource exhaustion + +// Ensure that we emit a proper error if GenMC fails to fulfill an allocation. +// Two variants: one for a single large allocation, one for multiple ones +// that are individually below the limit, but together are too big. + +#![no_main] + +#[path = "../../../utils/genmc.rs"] +mod genmc; + +#[unsafe(no_mangle)] +fn miri_start(_argc: isize, _argv: *const *const u8) -> isize { + if cfg!(multiple) { + for _i in 1..8 { + let _v = Vec::::with_capacity(1024 * 1024 * 1024); + } + } else { + let _v = Vec::::with_capacity(8 * 1024 * 1024 * 1024); + } + 0 +} diff --git a/src/tools/miri/tests/genmc/fail/simple/alloc_large.single.stderr b/src/tools/miri/tests/genmc/fail/simple/alloc_large.single.stderr new file mode 100644 index 000000000000..8595612811fd --- /dev/null +++ b/src/tools/miri/tests/genmc/fail/simple/alloc_large.single.stderr @@ -0,0 +1,26 @@ +Running GenMC Verification... +error: resource exhaustion: there are no more free addresses in the address space + --> RUSTLIB/alloc/src/raw_vec/mod.rs:LL:CC + | +LL | AllocInit::Uninitialized => alloc.allocate(layout), + | ^^^^^^^^^^^^^^^^^^^^^^ resource exhaustion occurred here + | + = help: in GenMC mode, the address space is limited to 4GB per thread, and addresses cannot be reused + = note: BACKTRACE: + = note: inside `alloc::raw_vec::RawVecInner::try_allocate_in` at RUSTLIB/alloc/src/raw_vec/mod.rs:LL:CC + = note: inside `alloc::raw_vec::RawVecInner::with_capacity_in` at RUSTLIB/alloc/src/raw_vec/mod.rs:LL:CC + = note: inside `alloc::raw_vec::RawVec::::with_capacity_in` at RUSTLIB/alloc/src/raw_vec/mod.rs:LL:CC + = note: inside `std::vec::Vec::::with_capacity_in` at RUSTLIB/alloc/src/vec/mod.rs:LL:CC + = note: inside `std::vec::Vec::::with_capacity` at RUSTLIB/alloc/src/vec/mod.rs:LL:CC +note: inside `miri_start` + --> tests/genmc/fail/simple/alloc_large.rs:LL:CC + | +LL | let _v = Vec::::with_capacity(8 * 1024 * 1024 * 1024); + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace + +note: add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report + +error: aborting due to 1 previous error + diff --git a/src/tools/miri/tests/genmc/pass/atomics/rmw_ops.rs b/src/tools/miri/tests/genmc/pass/atomics/rmw_ops.rs index 7e6e33c8a7b1..411207b79b7e 100644 --- a/src/tools/miri/tests/genmc/pass/atomics/rmw_ops.rs +++ b/src/tools/miri/tests/genmc/pass/atomics/rmw_ops.rs @@ -67,7 +67,7 @@ macro_rules! test_rmw_edge_cases { x.store(10, ORD); assert_eq(10, x.fetch_add(<$int>::MAX, ORD)); // definitely overflows, so new value of x is smaller than 10 assert_eq(<$int>::MAX.wrapping_add(10), x.fetch_max(10, ORD)); // new value of x should be 10 - // assert_eq(10, x.load(ORD)); // FIXME(genmc,#4572): enable this check once GenMC correctly handles min/max truncation. + assert_eq(10, x.load(ORD)); }}; }