diff options
| author | bors <bors@rust-lang.org> | 2025-09-19 15:22:22 +0000 |
|---|---|---|
| committer | bors <bors@rust-lang.org> | 2025-09-19 15:22:22 +0000 |
| commit | 59043567a5cf12800e1457c36ad6a6b0fa02c6b6 (patch) | |
| tree | ceb1ed6622a93c560420980158f61c44d2aebffa /src/tools/miri/genmc-sys/src_cpp | |
| parent | e10aa8891182378de002bd71bf4d04181fb8231d (diff) | |
| parent | 5d404e05bc57a4ce117f8ec0275fe81655120b02 (diff) | |
Auto merge of #146765 - Zalathar:rollup-ewh4s9o, r=Zalathar
Rollup of 10 pull requests Successful merges: - rust-lang/rust#146229 (Automatically switch to lto-fat when flag RUSTFLAGS="- Zautodiff=Enable" is set) - rust-lang/rust#146484 (rustdoc-search: JavaScript optimization based on Firefox Profiler output) - rust-lang/rust#146541 (std: simplify host lookup) - rust-lang/rust#146615 (rustc_codegen_llvm: Feature Conversion Tidying) - rust-lang/rust#146638 (`rustc_next_trait_solver`: canonical out of `EvalCtxt`) - rust-lang/rust#146663 (Allow windows resource compiler to be overridden) - rust-lang/rust#146691 (std: Fix WASI implementation of `remove_dir_all`) - rust-lang/rust#146709 (stdarch subtree update) - rust-lang/rust#146738 (Fix tidy spellchecking on Windows) - rust-lang/rust#146740 (miri subtree update) r? `@ghost` `@rustbot` modify labels: rollup
Diffstat (limited to 'src/tools/miri/genmc-sys/src_cpp')
| -rw-r--r-- | src/tools/miri/genmc-sys/src_cpp/MiriInterface.cpp | 50 | ||||
| -rw-r--r-- | src/tools/miri/genmc-sys/src_cpp/MiriInterface.hpp | 44 |
2 files changed, 0 insertions, 94 deletions
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<MiriGenMCShim> -{ - auto conf = std::make_shared<Config>(); - - // 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<MiriGenMCShim>(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 <iostream> - -/**** 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<const Config> 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<MiriGenMCShim> 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<MiriGenMCShim> -{ - return MiriGenMCShim::createHandle(config); -} - -#endif /* GENMC_MIRI_INTERFACE_HPP */ |
