Auto merge of #144633 - Zalathar:rollup-h984m13, r=Zalathar

Rollup of 13 pull requests

Successful merges:

 - rust-lang/rust#144022 (Implementation: `#[feature(sync_nonpoison)]`, `#[feature(nonpoison_mutex)]`)
 - rust-lang/rust#144167 (Document why `Range*<&T> as RangeBounds<T>` impls are not `T: ?Sized`, and give an alternative.)
 - rust-lang/rust#144407 (fix(debuginfo): disable overflow check for recursive non-enum types)
 - rust-lang/rust#144451 (fix: Reject upvar scrutinees for `loop_match`)
 - rust-lang/rust#144482 (Add explicit download methods to download module in bootstrap)
 - rust-lang/rust#144500 (thread name in stack overflow message)
 - rust-lang/rust#144511 (tidy: increase performance of auto extra checks feature)
 - rust-lang/rust#144599 (bootstrap: enable tidy auto extra checks on tools profile)
 - rust-lang/rust#144600 (Ensure external paths passed via flags end up in rustdoc depinfo)
 - rust-lang/rust#144609 (feat: Right align line numbers)
 - rust-lang/rust#144623 (miri subtree update)
 - rust-lang/rust#144626 (cc dependencies: clarify comment)
 - rust-lang/rust#144627 (Add a test case for the issue rust-lang/rust#129882)

r? `@ghost`
`@rustbot` modify labels: rollup

1 files changed, 50 insertions, 0 deletions

diff --git a/src/tools/miri/genmc-sys/src_cpp/MiriInterface.cpp b/src/tools/miri/genmc-sys/src_cpp/MiriInterface.cpp
new file mode 100644
index 00000000000..0827bb3d407
--- /dev/null
+++ b/src/tools/miri/genmc-sys/src_cpp/MiriInterface.cpp
@@ -0,0 +1,50 @@
+#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;
+}