about summary refs log tree commit diff
path: root/src/tools/miri/genmc-sys/src_cpp
diff options
context:
space:
mode:
authorPatrick-6 <pamu99@gmx.ch>2025-04-14 08:53:50 +0200
committerPatrick-6 <pamu99@gmx.ch>2025-09-03 12:41:32 +0200
commitc1be740564dd4a3aaafca93539ca428223226278 (patch)
tree2cd553b043db22a06fd5db3224a1387caedf2ddc /src/tools/miri/genmc-sys/src_cpp
parentd366f26421125e11bfcec5e4a9f202813cbd3229 (diff)
downloadrust-c1be740564dd4a3aaafca93539ca428223226278.tar.gz
rust-c1be740564dd4a3aaafca93539ca428223226278.zip
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 <post@ralfj.de>
Diffstat (limited to 'src/tools/miri/genmc-sys/src_cpp')
-rw-r--r--src/tools/miri/genmc-sys/src_cpp/MiriInterface.cpp50
-rw-r--r--src/tools/miri/genmc-sys/src_cpp/MiriInterface.hpp44
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 */