From c1be740564dd4a3aaafca93539ca428223226278 Mon Sep 17 00:00:00 2001 From: Patrick-6 Date: Mon, 14 Apr 2025 08:53:50 +0200 Subject: Implement basic support for running Miri with GenMC. - Implement memory allocation compatible with GenMC. - Extract address generator struct from Miri's allocator. - Support thread creation and joining. - Support atomic load and store. - Support scheduling through GenMC. - Add tests for GenMC mode. - Add clang-format file for C++ code in Miri. - Update genmc-sys crate license to MIT/Apache to match GenMC dependency. - Add documentation for GenMC mode. Note: this commit depends on changes to GenMC not yet upstreamed to its official repository. Co-authored-by: Ralf Jung --- src/tools/miri/genmc-sys/src_cpp/MiriInterface.cpp | 50 ---------------------- src/tools/miri/genmc-sys/src_cpp/MiriInterface.hpp | 44 ------------------- 2 files changed, 94 deletions(-) delete mode 100644 src/tools/miri/genmc-sys/src_cpp/MiriInterface.cpp delete mode 100644 src/tools/miri/genmc-sys/src_cpp/MiriInterface.hpp (limited to 'src/tools/miri/genmc-sys/src_cpp') diff --git a/src/tools/miri/genmc-sys/src_cpp/MiriInterface.cpp b/src/tools/miri/genmc-sys/src_cpp/MiriInterface.cpp deleted file mode 100644 index 0827bb3d407..00000000000 --- a/src/tools/miri/genmc-sys/src_cpp/MiriInterface.cpp +++ /dev/null @@ -1,50 +0,0 @@ -#include "MiriInterface.hpp" - -#include "genmc-sys/src/lib.rs.h" - -auto MiriGenMCShim::createHandle(const GenmcParams &config) - -> std::unique_ptr -{ - auto conf = std::make_shared(); - - // Miri needs all threads to be replayed, even fully completed ones. - conf->replayCompletedThreads = true; - - // We only support the RC11 memory model for Rust. - conf->model = ModelType::RC11; - - conf->printRandomScheduleSeed = config.print_random_schedule_seed; - - // FIXME(genmc): disable any options we don't support currently: - conf->ipr = false; - conf->disableBAM = true; - conf->instructionCaching = false; - - ERROR_ON(config.do_symmetry_reduction, "Symmetry reduction is currently unsupported in GenMC mode."); - conf->symmetryReduction = config.do_symmetry_reduction; - - // FIXME(genmc): Should there be a way to change this option from Miri? - conf->schedulePolicy = SchedulePolicy::WF; - - // FIXME(genmc): implement estimation mode: - conf->estimate = false; - conf->estimationMax = 1000; - const auto mode = conf->estimate ? 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): check config: - // checkConfigOptions(*conf); - - auto driver = std::make_unique(std::move(conf), mode); - return driver; -} diff --git a/src/tools/miri/genmc-sys/src_cpp/MiriInterface.hpp b/src/tools/miri/genmc-sys/src_cpp/MiriInterface.hpp deleted file mode 100644 index e55522ef418..00000000000 --- a/src/tools/miri/genmc-sys/src_cpp/MiriInterface.hpp +++ /dev/null @@ -1,44 +0,0 @@ -#ifndef GENMC_MIRI_INTERFACE_HPP -#define GENMC_MIRI_INTERFACE_HPP - -#include "rust/cxx.h" - -#include "config.h" - -#include "Config/Config.hpp" -#include "Verification/GenMCDriver.hpp" - -#include - -/**** Types available to Miri ****/ - -// Config struct defined on the Rust side and translated to C++ by cxx.rs: -struct GenmcParams; - -struct MiriGenMCShim : private GenMCDriver -{ - -public: - MiriGenMCShim(std::shared_ptr conf, Mode mode /* = VerificationMode{} */) - : GenMCDriver(std::move(conf), nullptr, mode) - { - std::cerr << "C++: GenMC handle created!" << std::endl; - } - - virtual ~MiriGenMCShim() - { - std::cerr << "C++: GenMC handle destroyed!" << std::endl; - } - - static std::unique_ptr createHandle(const GenmcParams &config); -}; - -/**** Functions available to Miri ****/ - -// NOTE: CXX doesn't support exposing static methods to Rust currently, so we expose this function instead. -static inline auto createGenmcHandle(const GenmcParams &config) -> std::unique_ptr -{ - return MiriGenMCShim::createHandle(config); -} - -#endif /* GENMC_MIRI_INTERFACE_HPP */ -- cgit 1.4.1-3-g733a5