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 ---------------------- 1 file changed, 50 deletions(-) delete mode 100644 src/tools/miri/genmc-sys/src_cpp/MiriInterface.cpp (limited to 'src/tools/miri/genmc-sys/src_cpp/MiriInterface.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; -} -- cgit 1.4.1-3-g733a5