diff options
Diffstat (limited to 'src/tools/miri/genmc-sys/cpp')
6 files changed, 924 insertions, 0 deletions
diff --git a/src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp b/src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp new file mode 100644 index 00000000000..444c9375319 --- /dev/null +++ b/src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp @@ -0,0 +1,345 @@ +#ifndef GENMC_MIRI_INTERFACE_HPP +#define GENMC_MIRI_INTERFACE_HPP + +// CXX.rs generated headers: +#include "rust/cxx.h" + +// GenMC generated headers: +#include "config.h" + +// Miri `genmc-sys/src_cpp` headers: +#include "ResultHandling.hpp" + +// GenMC headers: +#include "ExecutionGraph/EventLabel.hpp" +#include "Static/ModuleID.hpp" +#include "Support/MemOrdering.hpp" +#include "Support/RMWOps.hpp" +#include "Verification/Config.hpp" +#include "Verification/GenMCDriver.hpp" + +// C++ headers: +#include <cstdint> +#include <format> +#include <iomanip> +#include <memory> + +/**** Types available to both Rust and C++ ****/ + +struct GenmcParams; +enum class LogLevel : std::uint8_t; + +struct GenmcScalar; +struct SchedulingResult; +struct EstimationResult; +struct LoadResult; +struct StoreResult; +struct ReadModifyWriteResult; +struct CompareExchangeResult; + +// GenMC uses `int` for its thread IDs. +using ThreadId = int; + +/// Set the log level for GenMC. +/// +/// # Safety +/// +/// This function is not thread safe, since it writes to the global, mutable, non-atomic `logLevel` +/// variable. Any GenMC function may read from `logLevel` unsynchronized. +/// The safest way to use this function is to set the log level exactly once before first calling +/// `create_handle`. +/// 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 { + + public: + MiriGenmcShim(std::shared_ptr<const Config> conf, Mode mode /* = VerificationMode{} */) + : GenMCDriver(std::move(conf), nullptr, mode) {} + + /// Create a new `MiriGenmcShim`, 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`, 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`. + /* unsafe */ static auto create_handle(const GenmcParams& params, bool estimation_mode) + -> std::unique_ptr<MiriGenmcShim>; + + virtual ~MiriGenmcShim() {} + + /**** Execution start/end handling ****/ + + // This function must be called at the start of any execution, before any events are + // reported to GenMC. + void handle_execution_start(); + // 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 occured. + std::unique_ptr<std::string> handle_execution_end(); + + /***** Functions for handling events encountered during program execution. *****/ + + /**** Memory access handling ****/ + + [[nodiscard]] LoadResult handle_load( + ThreadId thread_id, + uint64_t address, + uint64_t size, + MemOrdering ord, + GenmcScalar old_val + ); + [[nodiscard]] ReadModifyWriteResult handle_read_modify_write( + ThreadId thread_id, + uint64_t address, + uint64_t size, + RMWBinOp rmw_op, + MemOrdering ordering, + GenmcScalar rhs_value, + GenmcScalar old_val + ); + [[nodiscard]] CompareExchangeResult 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 + ); + [[nodiscard]] StoreResult handle_store( + ThreadId thread_id, + uint64_t address, + uint64_t size, + GenmcScalar value, + GenmcScalar old_val, + MemOrdering ord + ); + + 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; + void handle_free(ThreadId thread_id, uint64_t address); + + /**** Thread management ****/ + void handle_thread_create(ThreadId thread_id, ThreadId parent_id); + void handle_thread_join(ThreadId thread_id, ThreadId child_id); + void handle_thread_finish(ThreadId thread_id, uint64_t ret_val); + void handle_thread_kill(ThreadId thread_id); + + /***** Exploration related functionality *****/ + + /** Ask the GenMC scheduler for a new thread to schedule and return whether the execution is + * finished, blocked, or can continue. + * Updates the next instruction kind for the given thread id. */ + auto schedule_next(const int curr_thread_id, const ActionKind curr_thread_next_instr_kind) + -> SchedulingResult; + + /** + * Check whether there are more executions to explore. + * If there are more executions, this method prepares for the next execution and returns + * `true`. Returns true if there are no more executions to explore. */ + auto is_exploration_done() -> bool { + return GenMCDriver::done(); + } + + /**** Result querying functionality. ****/ + + // NOTE: We don't want to share the `VerificationResult` type with the Rust side, since it + // 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. + + // Note that CXX.rs doesn't support returning a C++ string to Rust by value, + // it must be behind an indirection like a `unique_ptr` (tested with CXX 1.0.170). + + /// Get the number of blocked executions encountered by GenMC (cast into a fixed with + /// integer) + auto get_blocked_execution_count() const -> uint64_t { + return static_cast<uint64_t>(getResult().exploredBlocked); + } + + /// Get the number of executions explored by GenMC (cast into a fixed with integer) + auto get_explored_execution_count() const -> uint64_t { + return static_cast<uint64_t>(getResult().explored); + } + + /// Get all messages that GenMC produced (errors, warnings), combined into one string. + auto get_result_message() const -> std::unique_ptr<std::string> { + return std::make_unique<std::string>(getResult().message); + } + + /// If an error occurred, return a string describing the error, otherwise, return `nullptr`. + auto get_error_string() const -> std::unique_ptr<std::string> { + const auto& result = GenMCDriver::getResult(); + if (result.status.has_value()) + return format_error(result.status.value()); + return nullptr; + } + + /**** Printing and estimation mode functionality. ****/ + + /// Get the results of a run in estimation mode. + auto get_estimation_results() const -> EstimationResult; + + private: + /** Increment the event index in the given thread by 1 and return the new event. */ + [[nodiscard]] inline auto inc_pos(ThreadId tid) -> Event { + ERROR_ON(tid >= threads_action_.size(), "ThreadId out of bounds"); + return ++threads_action_[tid].event; + } + /** Decrement the event index in the given thread by 1 and return the new event. */ + inline auto dec_pos(ThreadId tid) -> Event { + ERROR_ON(tid >= threads_action_.size(), "ThreadId out of bounds"); + return --threads_action_[tid].event; + } + + /** + * Helper function for loads that need to reset the event counter when no value is returned. + * Same syntax as `GenMCDriver::handleLoad`, but this takes a thread id instead of an Event. + * Automatically calls `inc_pos` and `dec_pos` where needed for the given thread. + */ + template <EventLabel::EventLabelKind k, typename... Ts> + auto handle_load_reset_if_none(ThreadId tid, Ts&&... params) -> HandleResult<SVal> { + const auto pos = inc_pos(tid); + const auto ret = GenMCDriver::handleLoad<k>(pos, std::forward<Ts>(params)...); + // If we didn't get a value, we have to reset the index of the current thread. + if (!std::holds_alternative<SVal>(ret)) { + dec_pos(tid); + } + return ret; + } + + /** + * GenMC uses the term `Action` to refer to a struct of: + * - `ActionKind`, storing whether the next instruction in a thread may be a load + * - `Event`, storing the most recent event index added for a thread + * + * Here we store the "action" for each thread. In particular we use this to assign event + * indices, since GenMC expects us to do that. + */ + std::vector<Action> threads_action_; +}; + +/// Get the bit mask that GenMC expects for global memory allocations. +/// FIXME(genmc): currently we use `get_global_alloc_static_mask()` to ensure the +/// `SAddr::staticMask` constant is consistent between Miri and GenMC, but if +/// https://github.com/dtolnay/cxx/issues/1051 is fixed we could share the constant +/// directly. +constexpr auto get_global_alloc_static_mask() -> uint64_t { + return SAddr::staticMask; +} + +// 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. +#include "genmc-sys/src/lib.rs.h" + +/**** Result handling ****/ +// NOTE: these must come after the cxx_bridge generated code, since that contains the actual +// definitions of these types. + +namespace GenmcScalarExt { +inline GenmcScalar uninit() { + return GenmcScalar { + .value = 0, + .is_init = false, + }; +} + +inline GenmcScalar from_sval(SVal sval) { + return GenmcScalar { + .value = sval.get(), + .is_init = true, + }; +} + +inline SVal to_sval(GenmcScalar scalar) { + ERROR_ON(!scalar.is_init, "Cannot convert an uninitialized `GenmcScalar` into an `SVal`\n"); + return SVal(scalar.value); +} +} // namespace GenmcScalarExt + +namespace LoadResultExt { +inline LoadResult no_value() { + return LoadResult { + .error = std::unique_ptr<std::string>(nullptr), + .has_value = false, + .read_value = GenmcScalarExt::uninit(), + }; +} + +inline LoadResult from_value(SVal read_value) { + return LoadResult { .error = std::unique_ptr<std::string>(nullptr), + .has_value = true, + .read_value = GenmcScalarExt::from_sval(read_value) }; +} + +inline LoadResult from_error(std::unique_ptr<std::string> error) { + return LoadResult { .error = std::move(error), + .has_value = false, + .read_value = GenmcScalarExt::uninit() }; +} +} // namespace LoadResultExt + +namespace StoreResultExt { +inline StoreResult ok(bool is_coherence_order_maximal_write) { + return StoreResult { /* error: */ std::unique_ptr<std::string>(nullptr), + is_coherence_order_maximal_write }; +} + +inline StoreResult from_error(std::unique_ptr<std::string> error) { + return StoreResult { .error = std::move(error), .is_coherence_order_maximal_write = false }; +} +} // namespace StoreResultExt + +namespace ReadModifyWriteResultExt { +inline ReadModifyWriteResult +ok(SVal old_value, SVal new_value, bool is_coherence_order_maximal_write) { + return ReadModifyWriteResult { .error = std::unique_ptr<std::string>(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<std::string> error) { + return ReadModifyWriteResult { .error = std::move(error), + .old_value = GenmcScalarExt::uninit(), + .new_value = GenmcScalarExt::uninit(), + .is_coherence_order_maximal_write = false }; +} +} // namespace ReadModifyWriteResultExt + +namespace CompareExchangeResultExt { +inline CompareExchangeResult success(SVal old_value, bool is_coherence_order_maximal_write) { + return CompareExchangeResult { .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 { .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<std::string> error) { + return CompareExchangeResult { .error = std::move(error), + .old_value = GenmcScalarExt::uninit(), + .is_success = false, + .is_coherence_order_maximal_write = false }; +} +} // namespace CompareExchangeResultExt + +#endif /* GENMC_MIRI_INTERFACE_HPP */ diff --git a/src/tools/miri/genmc-sys/cpp/include/ResultHandling.hpp b/src/tools/miri/genmc-sys/cpp/include/ResultHandling.hpp new file mode 100644 index 00000000000..189f32e6f51 --- /dev/null +++ b/src/tools/miri/genmc-sys/cpp/include/ResultHandling.hpp @@ -0,0 +1,21 @@ +#ifndef GENMC_RESULT_HANDLING_HPP +#define GENMC_RESULT_HANDLING_HPP + +// CXX.rs generated headers: +#include "rust/cxx.h" + +// GenMC headers: +#include "Verification/VerificationError.hpp" + +#include <string> + +/** Information about an error, formatted as a string to avoid having to share an error enum and + * printing functionality with the Rust side. */ +static auto format_error(VerificationError err) -> std::unique_ptr<std::string> { + auto buf = std::string(); + auto s = llvm::raw_string_ostream(buf); + s << err; + return std::make_unique<std::string>(s.str()); +} + +#endif /* GENMC_RESULT_HANDLING_HPP */ diff --git a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/EventHandling.cpp b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/EventHandling.cpp new file mode 100644 index 00000000000..05c82641df9 --- /dev/null +++ b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/EventHandling.cpp @@ -0,0 +1,251 @@ +/** 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 <cstddef> +#include <cstdint> +#include <memory> +#include <utility> + +/**** 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<EventLabel::EventLabelKind::Read>( + thread_id, + ord, + SAddr(address), + ASize(size), + type + ); + + if (const auto* err = std::get_if<VerificationError>(&ret)) + return LoadResultExt::from_error(format_error(*err)); + const auto* ret_val = std::get_if<SVal>(&ret); + 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<EventLabel::EventLabelKind::Write>( + pos, + 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<VerificationError>(&ret)) + return StoreResultExt::from_error(format_error(*err)); + if (!std::holds_alternative<std::monostate>(ret)) + ERROR("store returned unexpected result"); + + // FIXME(genmc,mixed-accesses): Use the value that GenMC returns from handleStore (once + // available). + const auto& g = getExec().getGraph(); + return StoreResultExt::ok( + /* is_coherence_order_maximal_write */ g.co_max(SAddr(address))->getPos() == pos + ); +} + +void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) { + const auto pos = inc_pos(thread_id); + GenMCDriver::handleFence(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<EventLabel::EventLabelKind::FaiRead>( + thread_id, + 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<VerificationError>(&load_ret)) + return ReadModifyWriteResultExt::from_error(format_error(*err)); + + const auto* ret_val = std::get_if<SVal>(&load_ret); + 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<EventLabel::EventLabelKind::FaiWrite>( + storePos, + ordering, + SAddr(address), + ASize(size), + AType::Unsigned, // The type is only used for printing. + new_value + ); + if (const auto* err = std::get_if<VerificationError>(&store_ret)) + return ReadModifyWriteResultExt::from_error(format_error(*err)); + + const auto* store_ret_val = std::get_if<std::monostate>(&store_ret); + ERROR_ON(nullptr == store_ret_val, "Unimplemented: RMW store returned unexpected result."); + + // FIXME(genmc,mixed-accesses): Use the value that GenMC returns from handleStore (once + // available). + const auto& g = getExec().getGraph(); + return ReadModifyWriteResultExt::ok( + /* old_value: */ read_old_val, + new_value, + /* is_coherence_order_maximal_write */ g.co_max(SAddr(address))->getPos() == storePos + ); +} + +[[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<EventLabel::EventLabelKind::CasRead>( + thread_id, + 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<VerificationError>(&load_ret)) + return CompareExchangeResultExt::from_error(format_error(*err)); + const auto* ret_val = std::get_if<SVal>(&load_ret); + 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<EventLabel::EventLabelKind::CasWrite>( + storePos, + success_ordering, + SAddr(address), + ASize(size), + AType::Unsigned, // The type is only used for printing. + new_val + ); + if (const auto* err = std::get_if<VerificationError>(&store_ret)) + return CompareExchangeResultExt::from_error(format_error(*err)); + const auto* store_ret_val = std::get_if<std::monostate>(&store_ret); + ERROR_ON( + nullptr == store_ret_val, + "Unimplemented: compare-exchange store returned unexpected result." + ); + + // FIXME(genmc,mixed-accesses): Use the value that GenMC returns from handleStore (once + // available). + const auto& g = getExec().getGraph(); + return CompareExchangeResultExt::success( + read_old_val, + /* is_coherence_order_maximal_write */ g.co_max(SAddr(address))->getPos() == storePos + ); +} + +/**** 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( + pos, + size, + alignment, + storage_duration, + storage_type, + address_space, + EventDeps() + ); + return ret_val.get(); +} + +void MiriGenmcShim::handle_free(ThreadId thread_id, uint64_t address) { + const auto pos = inc_pos(thread_id); + GenMCDriver::handleFree(pos, SAddr(address), EventDeps()); + // FIXME(genmc): add error handling once GenMC returns errors from `handleFree` +} diff --git a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp new file mode 100644 index 00000000000..5e7188f17e0 --- /dev/null +++ b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp @@ -0,0 +1,56 @@ +/** This file contains functionality related to exploration, such as scheduling. */ + +#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 <cmath> +#include <cstdint> +#include <limits> + +auto MiriGenmcShim::schedule_next( + const int curr_thread_id, + const ActionKind curr_thread_next_instr_kind +) -> SchedulingResult { + // The current thread is the only one where the `kind` could have changed since we last made + // a scheduling decision. + threads_action_[curr_thread_id].kind = curr_thread_next_instr_kind; + + if (const auto result = GenMCDriver::scheduleNext(threads_action_)) + return SchedulingResult { ExecutionState::Ok, static_cast<int32_t>(result.value()) }; + if (GenMCDriver::isExecutionBlocked()) + return SchedulingResult { ExecutionState::Blocked, 0 }; + return SchedulingResult { ExecutionState::Finished, 0 }; +} + +/**** Execution start/end handling ****/ + +void MiriGenmcShim::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<std::string> { + // FIXME(genmc): add error handling once GenMC returns an error here. + GenMCDriver::handleExecutionEnd(); + return {}; +} + +/**** Estimation mode result ****/ + +auto MiriGenmcShim::get_estimation_results() const -> EstimationResult { + const auto& res = getResult(); + return EstimationResult { + .mean = static_cast<double>(res.estimationMean), + .sd = static_cast<double>(std::sqrt(res.estimationVariance)), + .explored_execs = static_cast<uint64_t>(res.explored), + .blocked_execs = static_cast<uint64_t>(res.exploredBlocked), + }; +} diff --git a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Setup.cpp b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Setup.cpp new file mode 100644 index 00000000000..af13f0d0774 --- /dev/null +++ b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Setup.cpp @@ -0,0 +1,197 @@ +/** This file contains functionality related to creation of the GenMCDriver, + * including translating settings set by Miri. */ + +#include "MiriInterface.hpp" + +// CXX.rs generated headers: +#include "genmc-sys/src/lib.rs.h" + +// GenMC headers: +#include "Support/Error.hpp" +#include "Support/Verbosity.hpp" +#include "Verification/InterpreterCallbacks.hpp" + +// C++ headers: +#include <cstdint> + +/** + * Translate the Miri-GenMC `LogLevel` to the GenMC `VerbosityLevel`. + * Downgrade any debug options to `Tip` if `ENABLE_GENMC_DEBUG` is not enabled. + */ +static auto to_genmc_verbosity_level(const LogLevel log_level) -> VerbosityLevel { + switch (log_level) { + case LogLevel::Quiet: + return VerbosityLevel::Quiet; + case LogLevel::Error: + return VerbosityLevel::Error; + case LogLevel::Warning: + return VerbosityLevel::Warning; + case LogLevel::Tip: + return VerbosityLevel::Tip; +#ifdef ENABLE_GENMC_DEBUG + case LogLevel::Debug1Revisits: + return VerbosityLevel::Debug1; + case LogLevel::Debug2MemoryAccesses: + return VerbosityLevel::Debug2; + case LogLevel::Debug3ReadsFrom: + return VerbosityLevel::Debug3; +#else + // Downgrade to `Tip` if the debug levels are not available. + case LogLevel::Debug1Revisits: + case LogLevel::Debug2MemoryAccesses: + case LogLevel::Debug3ReadsFrom: + return VerbosityLevel::Tip; +#endif + default: + WARN_ONCE( + "unknown-log-level", + "Unknown `LogLevel`, defaulting to `VerbosityLevel::Tip`." + ); + return VerbosityLevel::Tip; + } +} + +/* 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. + logLevel = to_genmc_verbosity_level(log_level); +} + +/* unsafe */ auto MiriGenmcShim::create_handle(const GenmcParams& params, bool estimation_mode) + -> std::unique_ptr<MiriGenmcShim> { + auto conf = std::make_shared<Config>(); + + // Set whether GenMC should print execution graphs after every explored/blocked execution. + conf->printExecGraphs = + (params.print_execution_graphs == ExecutiongraphPrinting::Explored || + params.print_execution_graphs == ExecutiongraphPrinting::ExploredAndBlocked); + conf->printBlockedExecs = + (params.print_execution_graphs == ExecutiongraphPrinting::Blocked || + params.print_execution_graphs == ExecutiongraphPrinting::ExploredAndBlocked); + + // `1024` is the default value that GenMC uses. + // If any thread has at least this many events, a warning/tip will be printed. + // + // Miri produces a lot more events than GenMC, so the graph size warning triggers on almost + // all programs. The current value is large enough so the warning is not be triggered by any + // reasonable programs. + // FIXME(genmc): The emitted warning mentions features not supported by Miri ('--unroll' + // parameter). + // FIXME(genmc): A more appropriate limit should be chosen once the warning is useful for + // Miri. + conf->warnOnGraphSize = 1024 * 1024; + + // We only support the `RC11` memory model for Rust, and `SC` when weak memory emulation is + // disabled. + conf->model = params.disable_weak_memory_emulation ? ModelType::SC : ModelType::RC11; + + // This prints the seed that GenMC picks for randomized scheduling during estimation mode. + conf->printRandomScheduleSeed = params.print_random_schedule_seed; + + // FIXME(genmc): supporting IPR requires annotations for `assume` and `spinloops`. + conf->ipr = false; + // FIXME(genmc): supporting BAM requires `Barrier` support + detecting whether return value + // of barriers are used. + conf->disableBAM = true; + + // Instruction caching could help speed up verification by filling the graph from cache, if + // the list of values read by all load events in a thread have been seen before. Combined + // with not replaying completed threads, this can also reducing the amount of Mir + // interpretation required by Miri. With the current setup, this would be incorrect, since + // Miri doesn't give GenMC the actual values read by non-atomic reads. + conf->instructionCaching = false; + // Many of Miri's checks work under the assumption that threads are only executed in an + // order that could actually happen during a normal execution. Formally, this means that + // replaying an execution needs to respect the po-rf-relation of the executiongraph (po == + // program-order, rf == reads-from). This means, any event in the graph, when replayed, must + // happen after any events that happen before it in the same graph according to the program + // code, and all (non-atomic) reads must happen after the write event they read from. + // + // Not replaying completed threads means any read event from that thread never happens in + // Miri's memory, so this would only work if there are never any non-atomic reads from any + // value written by the skipped thread. + conf->replayCompletedThreads = true; + + // FIXME(genmc): implement symmetry reduction. + ERROR_ON( + params.do_symmetry_reduction, + "Symmetry reduction is currently unsupported in GenMC mode." + ); + conf->symmetryReduction = params.do_symmetry_reduction; + + // Set the scheduling policy. GenMC uses `WFR` for estimation mode. + // For normal verification, `WF` has the best performance and is the GenMC default. + // Other scheduling policies are used by GenMC for testing and for modes currently + // unsupported with Miri such as bounding, which uses LTR. + conf->schedulePolicy = estimation_mode ? SchedulePolicy::WFR : SchedulePolicy::WF; + + // Set the min and max number of executions tested in estimation mode. + conf->estimationMin = 10; // default taken from GenMC + conf->estimationMax = params.estimation_max; + // Deviation threshold % under which estimation is deemed good enough. + conf->sdThreshold = 10; // default taken from GenMC + // Set the mode used for this driver, either estimation or verification. + const auto mode = estimation_mode ? GenMCDriver::Mode(GenMCDriver::EstimationMode {}) + : GenMCDriver::Mode(GenMCDriver::VerificationMode {}); + + // Running Miri-GenMC without race detection is not supported. + // Disabling this option also changes the behavior of the replay scheduler to only schedule + // at atomic operations, which is required with Miri. This happens because Miri can generate + // multiple GenMC events for a single MIR terminator. Without this option, the scheduler + // might incorrectly schedule an atomic MIR terminator because the first event it creates is + // a non-atomic (e.g., `StorageLive`). + conf->disableRaceDetection = false; + + // Miri can already check for unfreed memory. Also, GenMC cannot distinguish between memory + // that is allowed to leak and memory that is not. + conf->warnUnfreedMemory = false; + + // FIXME(genmc,error handling): This function currently exits on error, but will return an + // error value in the future. The return value should be checked once this change is made. + checkConfig(*conf); + + // Create the actual driver and Miri-GenMC communication shim. + auto driver = std::make_unique<MiriGenmcShim>(std::move(conf), mode); + + // FIXME(genmc,HACK): Until a proper solution is implemented in GenMC, these callbacks will + // allow Miri to return information about global allocations and override uninitialized memory + // checks for non-atomic loads (Miri handles those without GenMC, so the error would be wrong). + auto interpreter_callbacks = InterpreterCallbacks { + // Miri already ensures that memory accesses are valid, so this check doesn't matter. + // We check that the address is static, but skip checking if it is part of an actual + // allocation. + .isStaticallyAllocated = [](SAddr addr) { return addr.isStatic(); }, + // FIXME(genmc,error reporting): Once a proper a proper API for passing such information is + // implemented in GenMC, Miri should use it to improve the produced error messages. + .getStaticName = [](SAddr addr) { return "[UNKNOWN STATIC]"; }, + // This function is called to get the initial value stored at the given address. + // + // From a Miri perspective, this API doesn't work very well: most memory starts out + // "uninitialized"; + // only statics have an initial value. And their initial value is just a sequence of bytes, + // but GenMC + // expect this to be already split into separate atomic variables. So we return a dummy + // value. + // This value should never be visible to the interpreted program. + // GenMC does not understand uninitialized memory the same way Miri does, which may cause + // this function to be called. The returned value can be visible to Miri or the user: + // - Printing the execution graph may contain this value in place of uninitialized values. + // FIXME(genmc): NOTE: printing the execution graph is not yet implemented. + // - Non-atomic loads may return this value, but Miri ignores values of non-atomic loads. + // - Atomic loads will *not* see this value once mixed atomic-non-atomic support is added. + // Currently, atomic loads can see this value, unless initialized by an *atomic* store. + // FIXME(genmc): update this comment once mixed atomic-non-atomic support is added. + // + // FIXME(genmc): implement proper support for uninitialized memory in GenMC. Ideally, the + // initial value getter would return an `optional<SVal>`, since the memory location may be + // uninitialized. + .initValGetter = [](const AAccess& a) { return SVal(0xDEAD); }, + // Miri serves non-atomic loads from its own memory and these GenMC checks are wrong in + // that case. This should no longer be required with proper mixed-size access support. + .skipUninitLoadChecks = [](MemOrdering ord) { return ord == MemOrdering::NotAtomic; }, + }; + driver->setInterpCallbacks(std::move(interpreter_callbacks)); + + return driver; +} diff --git a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/ThreadManagement.cpp b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/ThreadManagement.cpp new file mode 100644 index 00000000000..352d27adc3e --- /dev/null +++ b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/ThreadManagement.cpp @@ -0,0 +1,54 @@ + +/** 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 <cstdint> + +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 }; + + // NOTE: Default memory ordering (`Release`) used here. + const auto child_tid = GenMCDriver::handleThreadCreate(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(pos, child_id, EventDeps()); + // If the join failed, decrease the event index again: + if (!std::holds_alternative<SVal>(ret)) { + dec_pos(thread_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) { + const auto pos = inc_pos(thread_id); + // NOTE: Default memory ordering (`Release`) used here. + GenMCDriver::handleThreadFinish(pos, SVal(ret_val)); +} + +void MiriGenmcShim::handle_thread_kill(ThreadId thread_id) { + const auto pos = inc_pos(thread_id); + GenMCDriver::handleThreadKill(pos); +} |