Merge pull request #4498 from RalfJung/genmc-build

Add support for building and linking against genmc

23 files changed, 1130 insertions, 42 deletions

diff --git a/src/tools/miri/.gitignore b/src/tools/miri/.gitignore
index ed2d0ba7ba0..4a238dc0313 100644
--- a/src/tools/miri/.gitignore
+++ b/src/tools/miri/.gitignore
@@ -1,5 +1,4 @@
 target
-/doc
 tex/*/out
 *.dot
 *.out
diff --git a/src/tools/miri/Cargo.lock b/src/tools/miri/Cargo.lock
index 0af4181dc15..ece51f2ba74 100644
--- a/src/tools/miri/Cargo.lock
+++ b/src/tools/miri/Cargo.lock
@@ -170,6 +170,8 @@ version = "1.2.30"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "deec109607ca693028562ed836a5f1c4b8bd77755c4e132fc5ce11b0b6211ae7"
 dependencies = [
+ "jobserver",
+ "libc",
  "shlex",
 ]
 
@@ -215,6 +217,52 @@ dependencies = [
 ]
 
 [[package]]
+name = "clap"
+version = "4.5.41"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "be92d32e80243a54711e5d7ce823c35c41c9d929dc4ab58e1276f625841aadf9"
+dependencies = [
+ "clap_builder",
+]
+
+[[package]]
+name = "clap_builder"
+version = "4.5.41"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "707eab41e9622f9139419d573eca0900137718000c517d47da73045f54331c3d"
+dependencies = [
+ "anstyle",
+ "clap_lex",
+ "strsim",
+]
+
+[[package]]
+name = "clap_lex"
+version = "0.7.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b94f61472cee1439c0b966b47e3aca9ae07e45d070759512cd390ea2bebc6675"
+
+[[package]]
+name = "cmake"
+version = "0.1.54"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e7caa3f9de89ddbe2c607f4101924c5abec803763ae9534e4f4d7d8f84aa81f0"
+dependencies = [
+ "cc",
+]
+
+[[package]]
+name = "codespan-reporting"
+version = "0.12.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "fe6d2e5af09e8c8ad56c969f2157a3d4238cebc7c55f0a517728c38f7b200f81"
+dependencies = [
+ "serde",
+ "termcolor",
+ "unicode-width 0.2.1",
+]
+
+[[package]]
 name = "color-eyre"
 version = "0.6.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
@@ -314,6 +362,68 @@ dependencies = [
 ]
 
 [[package]]
+name = "cxx"
+version = "1.0.161"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a3523cc02ad831111491dd64b27ad999f1ae189986728e477604e61b81f828df"
+dependencies = [
+ "cc",
+ "cxxbridge-cmd",
+ "cxxbridge-flags",
+ "cxxbridge-macro",
+ "foldhash",
+ "link-cplusplus",
+]
+
+[[package]]
+name = "cxx-build"
+version = "1.0.161"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "212b754247a6f07b10fa626628c157593f0abf640a3dd04cce2760eca970f909"
+dependencies = [
+ "cc",
+ "codespan-reporting",
+ "indexmap",
+ "proc-macro2",
+ "quote",
+ "scratch",
+ "syn",
+]
+
+[[package]]
+name = "cxxbridge-cmd"
+version = "1.0.161"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f426a20413ec2e742520ba6837c9324b55ffac24ead47491a6e29f933c5b135a"
+dependencies = [
+ "clap",
+ "codespan-reporting",
+ "indexmap",
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
+[[package]]
+name = "cxxbridge-flags"
+version = "1.0.161"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a258b6069020b4e5da6415df94a50ee4f586a6c38b037a180e940a43d06a070d"
+
+[[package]]
+name = "cxxbridge-macro"
+version = "1.0.161"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e8dec184b52be5008d6eaf7e62fc1802caf1ad1227d11b3b7df2c409c7ffc3f4"
+dependencies = [
+ "indexmap",
+ "proc-macro2",
+ "quote",
+ "rustversion",
+ "syn",
+]
+
+[[package]]
 name = "directories"
 version = "6.0.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
@@ -335,12 +445,29 @@ dependencies = [
 ]
 
 [[package]]
+name = "displaydoc"
+version = "0.2.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "97369cbbc041bc366949bc74d34658d6cda5621039731c6310521892a3a20ae0"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
+[[package]]
 name = "encode_unicode"
 version = "1.0.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "34aa73646ffb006b8f5147f3dc182bd4bcb190227ce861fc4a4844bf8e3cb2c0"
 
 [[package]]
+name = "equivalent"
+version = "1.0.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "877a4ace8713b0bcf2a4e7eec82529c029f1d0619886d18145fea96c3ffe5c0f"
+
+[[package]]
 name = "errno"
 version = "0.3.13"
 source = "registry+https://github.com/rust-lang/crates.io-index"
@@ -373,6 +500,21 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "3f9eec918d3f24069decb9af1554cad7c880e2da24a9afd88aca000531ab82c1"
 
 [[package]]
+name = "foldhash"
+version = "0.1.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d9c4f5dac5e15c24eb999c26181a6ca40b39fe946cbe4c263c7209467bc83af2"
+
+[[package]]
+name = "form_urlencoded"
+version = "1.2.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e13624c2627564efccf4934284bdd98cbaa14e79b0b5a141218e507b3a823456"
+dependencies = [
+ "percent-encoding",
+]
+
+[[package]]
 name = "generic-array"
 version = "0.14.7"
 source = "registry+https://github.com/rust-lang/crates.io-index"
@@ -383,6 +525,17 @@ dependencies = [
 ]
 
 [[package]]
+name = "genmc-sys"
+version = "0.1.0"
+dependencies = [
+ "cc",
+ "cmake",
+ "cxx",
+ "cxx-build",
+ "git2",
+]
+
+[[package]]
 name = "getrandom"
 version = "0.2.16"
 source = "registry+https://github.com/rust-lang/crates.io-index"
@@ -412,12 +565,150 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "07e28edb80900c19c28f1072f2e8aeca7fa06b23cd4169cefe1af5aa3260783f"
 
 [[package]]
+name = "git2"
+version = "0.20.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "2deb07a133b1520dc1a5690e9bd08950108873d7ed5de38dcc74d3b5ebffa110"
+dependencies = [
+ "bitflags",
+ "libc",
+ "libgit2-sys",
+ "log",
+ "openssl-probe",
+ "openssl-sys",
+ "url",
+]
+
+[[package]]
+name = "hashbrown"
+version = "0.15.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5971ac85611da7067dbfcabef3c70ebb5606018acd9e2a3903a0da507521e0d5"
+
+[[package]]
+name = "icu_collections"
+version = "2.0.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "200072f5d0e3614556f94a9930d5dc3e0662a652823904c3a75dc3b0af7fee47"
+dependencies = [
+ "displaydoc",
+ "potential_utf",
+ "yoke",
+ "zerofrom",
+ "zerovec",
+]
+
+[[package]]
+name = "icu_locale_core"
+version = "2.0.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0cde2700ccaed3872079a65fb1a78f6c0a36c91570f28755dda67bc8f7d9f00a"
+dependencies = [
+ "displaydoc",
+ "litemap",
+ "tinystr",
+ "writeable",
+ "zerovec",
+]
+
+[[package]]
+name = "icu_normalizer"
+version = "2.0.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "436880e8e18df4d7bbc06d58432329d6458cc84531f7ac5f024e93deadb37979"
+dependencies = [
+ "displaydoc",
+ "icu_collections",
+ "icu_normalizer_data",
+ "icu_properties",
+ "icu_provider",
+ "smallvec",
+ "zerovec",
+]
+
+[[package]]
+name = "icu_normalizer_data"
+version = "2.0.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "00210d6893afc98edb752b664b8890f0ef174c8adbb8d0be9710fa66fbbf72d3"
+
+[[package]]
+name = "icu_properties"
+version = "2.0.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "016c619c1eeb94efb86809b015c58f479963de65bdb6253345c1a1276f22e32b"
+dependencies = [
+ "displaydoc",
+ "icu_collections",
+ "icu_locale_core",
+ "icu_properties_data",
+ "icu_provider",
+ "potential_utf",
+ "zerotrie",
+ "zerovec",
+]
+
+[[package]]
+name = "icu_properties_data"
+version = "2.0.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "298459143998310acd25ffe6810ed544932242d3f07083eee1084d83a71bd632"
+
+[[package]]
+name = "icu_provider"
+version = "2.0.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "03c80da27b5f4187909049ee2d72f276f0d9f99a42c306bd0131ecfe04d8e5af"
+dependencies = [
+ "displaydoc",
+ "icu_locale_core",
+ "stable_deref_trait",
+ "tinystr",
+ "writeable",
+ "yoke",
+ "zerofrom",
+ "zerotrie",
+ "zerovec",
+]
+
+[[package]]
+name = "idna"
+version = "1.0.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "686f825264d630750a544639377bae737628043f20d38bbc029e8f29ea968a7e"
+dependencies = [
+ "idna_adapter",
+ "smallvec",
+ "utf8_iter",
+]
+
+[[package]]
+name = "idna_adapter"
+version = "1.2.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3acae9609540aa318d1bc588455225fb2085b9ed0c4f6bd0d9d5bcd86f1a0344"
+dependencies = [
+ "icu_normalizer",
+ "icu_properties",
+]
+
+[[package]]
 name = "indenter"
 version = "0.3.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "ce23b50ad8242c51a442f3ff322d56b02f08852c77e4c0b4d3fd684abc89c683"
 
 [[package]]
+name = "indexmap"
+version = "2.10.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "fe4cd85333e22411419a0bcae1297d25e58c9443848b11dc6a86fefe8c78a661"
+dependencies = [
+ "equivalent",
+ "hashbrown",
+]
+
+[[package]]
 name = "indicatif"
 version = "0.17.11"
 source = "registry+https://github.com/rust-lang/crates.io-index"
@@ -464,6 +755,16 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "4a5f13b858c8d314ee3e8f639011f7ccefe71f97f96e50151fb991f267928e2c"
 
 [[package]]
+name = "jobserver"
+version = "0.1.33"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "38f262f097c174adebe41eb73d66ae9c06b2844fb0da69969647bbddd9b0538a"
+dependencies = [
+ "getrandom 0.3.3",
+ "libc",
+]
+
+[[package]]
 name = "js-sys"
 version = "0.3.77"
 source = "registry+https://github.com/rust-lang/crates.io-index"
@@ -511,6 +812,19 @@ dependencies = [
 ]
 
 [[package]]
+name = "libgit2-sys"
+version = "0.18.2+1.9.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1c42fe03df2bd3c53a3a9c7317ad91d80c81cd1fb0caec8d7cc4cd2bfa10c222"
+dependencies = [
+ "cc",
+ "libc",
+ "libz-sys",
+ "openssl-sys",
+ "pkg-config",
+]
+
+[[package]]
 name = "libloading"
 version = "0.8.8"
 source = "registry+https://github.com/rust-lang/crates.io-index"
@@ -531,12 +845,39 @@ dependencies = [
 ]
 
 [[package]]
+name = "libz-sys"
+version = "1.1.22"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8b70e7a7df205e92a1a4cd9aaae7898dac0aa555503cc0a649494d0d60e7651d"
+dependencies = [
+ "cc",
+ "libc",
+ "pkg-config",
+ "vcpkg",
+]
+
+[[package]]
+name = "link-cplusplus"
+version = "1.0.10"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "4a6f6da007f968f9def0d65a05b187e2960183de70c160204ecfccf0ee330212"
+dependencies = [
+ "cc",
+]
+
+[[package]]
 name = "linux-raw-sys"
 version = "0.9.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "cd945864f07fe9f5371a27ad7b52a172b4b499999f1d97574c9fa68373937e12"
 
 [[package]]
+name = "litemap"
+version = "0.8.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "241eaef5fd12c88705a01fc1066c48c4b36e0dd4377dcdc7ec3942cea7a69956"
+
+[[package]]
 name = "lock_api"
 version = "0.4.13"
 source = "registry+https://github.com/rust-lang/crates.io-index"
@@ -612,6 +953,7 @@ dependencies = [
  "chrono-tz",
  "colored 3.0.0",
  "directories",
+ "genmc-sys",
  "getrandom 0.3.3",
  "ipc-channel",
  "libc",
@@ -673,6 +1015,24 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "42f5e15c9953c5e4ccceeb2e7382a716482c34515315f7b03532b8b4e8393d2d"
 
 [[package]]
+name = "openssl-probe"
+version = "0.1.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d05e27ee213611ffe7d6348b942e8f942b37114c00cc03cec254295a4a17852e"
+
+[[package]]
+name = "openssl-sys"
+version = "0.9.109"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "90096e2e47630d78b7d1c20952dc621f957103f8bc2c8359ec81290d75238571"
+dependencies = [
+ "cc",
+ "libc",
+ "pkg-config",
+ "vcpkg",
+]
+
+[[package]]
 name = "option-ext"
 version = "0.2.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
@@ -723,6 +1083,12 @@ dependencies = [
 ]
 
 [[package]]
+name = "percent-encoding"
+version = "2.3.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e3148f5046208a5d56bcfc03053e3ca6334e51da8dfb19b6cdc8b306fae3283e"
+
+[[package]]
 name = "perf-event-open-sys"
 version = "3.0.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
@@ -756,12 +1122,27 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "3b3cff922bd51709b605d9ead9aa71031d81447142d828eb4a6eba76fe619f9b"
 
 [[package]]
+name = "pkg-config"
+version = "0.3.32"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "7edddbd0b52d732b21ad9a5fab5c704c14cd949e5e9a1ec5929a24fded1b904c"
+
+[[package]]
 name = "portable-atomic"
 version = "1.11.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "f84267b20a16ea918e43c6a88433c2d54fa145c92a811b5b047ccbe153674483"
 
 [[package]]
+name = "potential_utf"
+version = "0.1.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e5a7c30837279ca13e7c867e9e40053bc68740f988cb07f7ca6df43cc734b585"
+dependencies = [
+ "zerovec",
+]
+
+[[package]]
 name = "ppv-lite86"
 version = "0.2.21"
 source = "registry+https://github.com/rust-lang/crates.io-index"
@@ -947,6 +1328,12 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49"
 
 [[package]]
+name = "scratch"
+version = "1.0.8"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9f6280af86e5f559536da57a45ebc84948833b3bee313a7dd25232e09c878a52"
+
+[[package]]
 name = "semver"
 version = "1.0.26"
 source = "registry+https://github.com/rust-lang/crates.io-index"
@@ -1026,6 +1413,18 @@ dependencies = [
 ]
 
 [[package]]
+name = "stable_deref_trait"
+version = "1.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a8f112729512f8e442d81f95a8a7ddf2b7c6b8a1a6f509a95864142b30cab2d3"
+
+[[package]]
+name = "strsim"
+version = "0.11.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "7da8b5736845d9f2fcb837ea5d9e2628564b3b043a70948a3f0b778838c5fb4f"
+
+[[package]]
 name = "syn"
 version = "2.0.104"
 source = "registry+https://github.com/rust-lang/crates.io-index"
@@ -1037,6 +1436,17 @@ dependencies = [
 ]
 
 [[package]]
+name = "synstructure"
+version = "0.13.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "728a70f3dbaf5bab7f0c4b1ac8d7ae5ea60a4b5549c8a5914361c99147a709d2"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
+[[package]]
 name = "tempfile"
 version = "3.20.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
@@ -1050,6 +1460,15 @@ dependencies = [
 ]
 
 [[package]]
+name = "termcolor"
+version = "1.4.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "06794f8f6c5c898b3275aebefa6b8a1cb24cd2c6c79397ab15774837a0bc5755"
+dependencies = [
+ "winapi-util",
+]
+
+[[package]]
 name = "thiserror"
 version = "1.0.69"
 source = "registry+https://github.com/rust-lang/crates.io-index"
@@ -1109,6 +1528,16 @@ dependencies = [
 ]
 
 [[package]]
+name = "tinystr"
+version = "0.8.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5d4f6d1145dcb577acf783d4e601bc1d76a13337bb54e6233add580b07344c8b"
+dependencies = [
+ "displaydoc",
+ "zerovec",
+]
+
+[[package]]
 name = "tracing"
 version = "0.1.41"
 source = "registry+https://github.com/rust-lang/crates.io-index"
@@ -1200,6 +1629,23 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "4a1a07cc7db3810833284e8d372ccdc6da29741639ecc70c9ec107df0fa6154c"
 
 [[package]]
+name = "url"
+version = "2.5.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "32f8b686cadd1473f4bd0117a5d28d36b1ade384ea9b5069a1c40aefed7fda60"
+dependencies = [
+ "form_urlencoded",
+ "idna",
+ "percent-encoding",
+]
+
+[[package]]
+name = "utf8_iter"
+version = "1.0.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b6c140620e7ffbb22c2dee59cafe6084a59b5ffc27a8859a5f0d494b5d52b6be"
+
+[[package]]
 name = "uuid"
 version = "1.17.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
@@ -1217,6 +1663,12 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "ba73ea9cf16a25df0c8caa16c51acb937d5712a8429db78a3ee29d5dcacd3a65"
 
 [[package]]
+name = "vcpkg"
+version = "0.2.15"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "accd4ea62f7bb7a82fe23066fb0957d48ef677f6eeb8215f372f52e48bb32426"
+
+[[package]]
 name = "version_check"
 version = "0.9.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
@@ -1306,6 +1758,15 @@ dependencies = [
 ]
 
 [[package]]
+name = "winapi-util"
+version = "0.1.9"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "cf221c93e13a30d793f7645a0e7762c55d169dbb0a49671918a2319d289b10bb"
+dependencies = [
+ "windows-sys 0.59.0",
+]
+
+[[package]]
 name = "windows"
 version = "0.58.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
@@ -1525,6 +1986,36 @@ dependencies = [
 ]
 
 [[package]]
+name = "writeable"
+version = "0.6.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ea2f10b9bb0928dfb1b42b65e1f9e36f7f54dbdf08457afefb38afcdec4fa2bb"
+
+[[package]]
+name = "yoke"
+version = "0.8.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5f41bb01b8226ef4bfd589436a297c53d118f65921786300e427be8d487695cc"
+dependencies = [
+ "serde",
+ "stable_deref_trait",
+ "yoke-derive",
+ "zerofrom",
+]
+
+[[package]]
+name = "yoke-derive"
+version = "0.8.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "38da3c9736e16c5d3c8c597a9aaa5d1fa565d0532ae05e27c24aa62fb32c0ab6"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+ "synstructure",
+]
+
+[[package]]
 name = "zerocopy"
 version = "0.8.26"
 source = "registry+https://github.com/rust-lang/crates.io-index"
@@ -1543,3 +2034,57 @@ dependencies = [
  "quote",
  "syn",
 ]
+
+[[package]]
+name = "zerofrom"
+version = "0.1.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "50cc42e0333e05660c3587f3bf9d0478688e15d870fab3346451ce7f8c9fbea5"
+dependencies = [
+ "zerofrom-derive",
+]
+
+[[package]]
+name = "zerofrom-derive"
+version = "0.1.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d71e5d6e06ab090c67b5e44993ec16b72dcbaabc526db883a360057678b48502"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+ "synstructure",
+]
+
+[[package]]
+name = "zerotrie"
+version = "0.2.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "36f0bbd478583f79edad978b407914f61b2972f5af6fa089686016be8f9af595"
+dependencies = [
+ "displaydoc",
+ "yoke",
+ "zerofrom",
+]
+
+[[package]]
+name = "zerovec"
+version = "0.11.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "4a05eb080e015ba39cc9e23bbe5e7fb04d5fb040350f99f34e338d5fdd294428"
+dependencies = [
+ "yoke",
+ "zerofrom",
+ "zerovec-derive",
+]
+
+[[package]]
+name = "zerovec-derive"
+version = "0.11.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5b96237efa0c878c64bd89c436f661be4e46b2f3eff1ebb976f7ef2321d2f58f"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+]
diff --git a/src/tools/miri/Cargo.toml b/src/tools/miri/Cargo.toml
index d293af5cea2..91dadf78a2f 100644
--- a/src/tools/miri/Cargo.toml
+++ b/src/tools/miri/Cargo.toml
@@ -48,6 +48,10 @@ nix = { version = "0.30.1", features = ["mman", "ptrace", "signal"], optional =
 ipc-channel = { version = "0.20.0", optional = true }
 capstone = { version = "0.13", optional = true }
 
+# FIXME(genmc,macos): Add `target_os = "macos"` once https://github.com/dtolnay/cxx/issues/1535 is fixed.
+[target.'cfg(all(target_os = "linux", target_pointer_width = "64", target_endian = "little"))'.dependencies]
+genmc-sys = { path = "./genmc-sys/", version = "0.1.0", optional = true }
+
 [dev-dependencies]
 ui_test = "0.30.2"
 colored = "3"
@@ -66,7 +70,7 @@ harness = false
 
 [features]
 default = ["stack-cache", "native-lib"]
-genmc = []
+genmc = ["dep:genmc-sys"] # this enables a GPL dependency!
 stack-cache = []
 stack-cache-consistency-check = ["stack-cache"]
 tracing = ["serde_json"]
diff --git a/src/tools/miri/doc/genmc.md b/src/tools/miri/doc/genmc.md
new file mode 100644
index 00000000000..5aabe90b5da
--- /dev/null
+++ b/src/tools/miri/doc/genmc.md
@@ -0,0 +1,62 @@
+# **(WIP)** Documentation for Miri-GenMC
+
+[GenMC](https://github.com/MPI-SWS/genmc) is a stateless model checker for exploring concurrent executions of a program.
+Miri-GenMC integrates that model checker into Miri.
+
+**NOTE: Currently, no actual GenMC functionality is part of Miri, this is still WIP.**
+
+<!-- FIXME(genmc): add explanation. -->
+
+## Usage
+
+**IMPORTANT: The license of GenMC and thus the `genmc-sys` crate in the Miri repo is currently "GPL-3.0-or-later", so a binary produced with the `genmc` feature is subject to the requirements of the GPL. As long as that remains the case, the `genmc` feature of Miri is OFF-BY-DEFAULT and must be OFF for all Miri releases.**
+
+For testing/developing Miri-GenMC (while keeping in mind the licensing issues):
+- clone the Miri repo.
+- build Miri-GenMC with `./miri build --features=genmc`.
+- OR: install Miri-GenMC in the current system with `./miri install --features=genmc`
+
+Basic usage:
+```shell
+MIRIFLAGS="-Zmiri-genmc" cargo miri run
+```
+
+<!-- FIXME(genmc): explain options. -->
+
+<!-- FIXME(genmc): explain Miri-GenMC specific functions. -->
+
+## Tips
+
+<!-- FIXME(genmc): add tips for using Miri-GenMC more efficiently. -->
+
+## Limitations
+
+Some or all of these limitations might get removed in the future:
+
+- Borrow tracking is currently incompatible (stacked/tree borrows).
+- Only Linux is supported for now.
+- No support for 32-bit or big-endian targets.
+- No cross-target interpretation.
+
+<!-- FIXME(genmc): document remaining limitations -->
+
+## Development
+
+GenMC is written in C++, which complicates development a bit.
+The prerequisites for building Miri-GenMC are:
+- A compiler with C++23 support.
+- LLVM developments headers and clang.
+  <!-- FIXME(genmc,llvm): remove once LLVM dependency is no longer required. -->
+
+The actual code for GenMC is not contained in the Miri repo itself, but in a [separate GenMC repo](https://github.com/MPI-SWS/genmc) (with its own maintainers).
+These sources need to be available to build Miri-GenMC.
+The process for obtaining them is as follows:
+- By default, a fixed commit of GenMC is downloaded to `genmc-sys/genmc-src` and built automatically.
+  (The commit is determined by `GENMC_COMMIT` in `genmc-sys/build.rs`.)
+- If you want to overwrite that, set the `GENMC_SRC_PATH` environment variable to a path that contains the GenMC sources.
+  If you place this directory inside the Miri folder, it is recommended to call it `genmc-src` as that tells `./miri fmt` to avoid
+  formatting the Rust files inside that folder.
+
+<!-- FIXME(genmc): explain how submitting code to GenMC should be handled. -->
+
+<!-- FIXME(genmc): explain development. -->
diff --git a/src/tools/miri/etc/rust_analyzer_helix.toml b/src/tools/miri/etc/rust_analyzer_helix.toml
index 91e4070478c..c46b246049f 100644
--- a/src/tools/miri/etc/rust_analyzer_helix.toml
+++ b/src/tools/miri/etc/rust_analyzer_helix.toml
@@ -5,6 +5,7 @@ source = "discover"
 linkedProjects = [
     "Cargo.toml",
     "cargo-miri/Cargo.toml",
+    "genmc-sys/Cargo.toml",
     "miri-script/Cargo.toml",
 ]
 
diff --git a/src/tools/miri/etc/rust_analyzer_vscode.json b/src/tools/miri/etc/rust_analyzer_vscode.json
index 6917c6a1fd8..8e647f5331f 100644
--- a/src/tools/miri/etc/rust_analyzer_vscode.json
+++ b/src/tools/miri/etc/rust_analyzer_vscode.json
@@ -3,6 +3,7 @@
     "rust-analyzer.linkedProjects": [
         "Cargo.toml",
         "cargo-miri/Cargo.toml",
+        "genmc-sys/Cargo.toml",
         "miri-script/Cargo.toml",
     ],
     "rust-analyzer.check.invocationStrategy": "once",
diff --git a/src/tools/miri/genmc-sys/.gitignore b/src/tools/miri/genmc-sys/.gitignore
new file mode 100644
index 00000000000..276a053cd05
--- /dev/null
+++ b/src/tools/miri/genmc-sys/.gitignore
@@ -0,0 +1 @@
+genmc-src*/
diff --git a/src/tools/miri/genmc-sys/Cargo.toml b/src/tools/miri/genmc-sys/Cargo.toml
new file mode 100644
index 00000000000..95aef75afc4
--- /dev/null
+++ b/src/tools/miri/genmc-sys/Cargo.toml
@@ -0,0 +1,17 @@
+[package]
+authors = ["Miri Team"]
+# The parts in this repo are MIT OR Apache-2.0, but we are linking in
+# code from https://github.com/MPI-SWS/genmc which is GPL-3.0-or-later.
+license = "(MIT OR Apache-2.0) AND GPL-3.0-or-later"
+name = "genmc-sys"
+version = "0.1.0"
+edition = "2024"
+
+[dependencies]
+cxx = { version = "1.0.160", features = ["c++20"] }
+
+[build-dependencies]
+cc = "1.2.30"
+cmake = "0.1.54"
+git2 = { version = "0.20.2", default-features = false, features = ["https"] }
+cxx-build = { version = "1.0.160", features = ["parallel"] }
diff --git a/src/tools/miri/genmc-sys/build.rs b/src/tools/miri/genmc-sys/build.rs
new file mode 100644
index 00000000000..f20e0e8d525
--- /dev/null
+++ b/src/tools/miri/genmc-sys/build.rs
@@ -0,0 +1,267 @@
+use std::path::{Path, PathBuf};
+use std::str::FromStr;
+
+// Build script for running Miri with GenMC.
+// Check out doc/genmc.md for more info.
+
+/// Path where the downloaded GenMC repository will be stored (relative to the `genmc-sys` directory).
+/// Note that this directory is *not* cleaned up automatically by `cargo clean`.
+const GENMC_DOWNLOAD_PATH: &str = "./genmc-src/";
+
+/// Name of the library of the GenMC model checker.
+const GENMC_MODEL_CHECKER: &str = "genmc_lib";
+
+/// Path where the `cxx_bridge!` macro is used to define the Rust-C++ interface.
+const RUST_CXX_BRIDGE_FILE_PATH: &str = "src/lib.rs";
+
+/// The profile with which to build GenMC.
+const GENMC_CMAKE_PROFILE: &str = "RelWithDebInfo";
+
+mod downloading {
+    use std::path::PathBuf;
+    use std::str::FromStr;
+
+    use git2::{Commit, Oid, Remote, Repository, StatusOptions};
+
+    use super::GENMC_DOWNLOAD_PATH;
+
+    /// The GenMC repository the we get our commit from.
+    pub(crate) const GENMC_GITHUB_URL: &str = "https://github.com/MPI-SWS/genmc.git";
+    /// The GenMC commit we depend on. It must be available on the specified GenMC repository.
+    pub(crate) const GENMC_COMMIT: &str = "3438dd2c1202cd4a47ed7881d099abf23e4167ab";
+
+    pub(crate) fn download_genmc() -> PathBuf {
+        let Ok(genmc_download_path) = PathBuf::from_str(GENMC_DOWNLOAD_PATH);
+        let commit_oid = Oid::from_str(GENMC_COMMIT).expect("Commit should be valid.");
+
+        match Repository::open(&genmc_download_path) {
+            Ok(repo) => {
+                assert_repo_unmodified(&repo);
+                let commit = update_local_repo(&repo, commit_oid);
+                checkout_commit(&repo, &commit);
+            }
+            Err(_) => {
+                let repo = clone_remote_repo(&genmc_download_path);
+                let Ok(commit) = repo.find_commit(commit_oid) else {
+                    panic!(
+                        "Cloned GenMC repository does not contain required commit '{GENMC_COMMIT}'"
+                    );
+                };
+                checkout_commit(&repo, &commit);
+            }
+        };
+
+        genmc_download_path
+    }
+
+    fn get_remote(repo: &Repository) -> Remote<'_> {
+        let remote = repo.find_remote("origin").unwrap_or_else(|e| {
+                panic!(
+                    "Could not load commit ({GENMC_COMMIT}) from remote repository '{GENMC_GITHUB_URL}'. Error: {e}"
+                );
+            });
+
+        // Ensure that the correct remote URL is set.
+        let remote_url = remote.url();
+        if let Some(remote_url) = remote_url
+            && remote_url == GENMC_GITHUB_URL
+        {
+            return remote;
+        }
+
+        // Update remote URL.
+        println!(
+            "cargo::warning=GenMC repository remote URL has changed from '{remote_url:?}' to '{GENMC_GITHUB_URL}'"
+        );
+        repo.remote_set_url("origin", GENMC_GITHUB_URL)
+            .expect("cannot rename url of remote 'origin'");
+
+        // Reacquire the `Remote`, since `remote_set_url` doesn't update Remote objects already in memory.
+        repo.find_remote("origin").unwrap()
+    }
+
+    // Check if the required commit exists already, otherwise try fetching it.
+    fn update_local_repo(repo: &Repository, commit_oid: Oid) -> Commit<'_> {
+        repo.find_commit(commit_oid).unwrap_or_else(|_find_error| {
+            println!("GenMC repository at path '{GENMC_DOWNLOAD_PATH}' does not contain commit '{GENMC_COMMIT}'.");
+            // The commit is not in the checkout. Try `git fetch` and hope that we find the commit then.
+            let mut remote = get_remote(repo);
+            remote.fetch(&[GENMC_COMMIT], None, None).expect("Failed to fetch from remote.");
+
+            repo.find_commit(commit_oid)
+                .expect("Remote repository should contain expected commit")
+        })
+    }
+
+    fn clone_remote_repo(genmc_download_path: &PathBuf) -> Repository {
+        Repository::clone(GENMC_GITHUB_URL, &genmc_download_path).unwrap_or_else(|e| {
+            panic!("Cannot clone GenMC repo from '{GENMC_GITHUB_URL}': {e:?}");
+        })
+    }
+
+    /// Set the state of the repo to a specific commit
+    fn checkout_commit(repo: &Repository, commit: &Commit<'_>) {
+        repo.checkout_tree(commit.as_object(), None).expect("Failed to checkout");
+        repo.set_head_detached(commit.id()).expect("Failed to set HEAD");
+        println!("Successfully set checked out commit {commit:?}");
+    }
+
+    /// Check that the downloaded repository is unmodified.
+    /// If it is modified, explain that it shouldn't be, and hint at how to do local development with GenMC.
+    /// We don't overwrite any changes made to the directory, to prevent data loss.
+    fn assert_repo_unmodified(repo: &Repository) {
+        let statuses = repo
+            .statuses(Some(
+                StatusOptions::new()
+                    .include_untracked(true)
+                    .include_ignored(false)
+                    .include_unmodified(false),
+            ))
+            .expect("should be able to get repository status");
+        if statuses.is_empty() {
+            return;
+        }
+
+        panic!(
+            "Downloaded GenMC repository at path '{GENMC_DOWNLOAD_PATH}' has been modified. Please undo any changes made, or delete the '{GENMC_DOWNLOAD_PATH}' directory to have it downloaded again.\n\
+            HINT: For local development, set the environment variable 'GENMC_SRC_PATH' to the path of a GenMC repository."
+        );
+    }
+}
+
+// FIXME(genmc,llvm): Remove once the LLVM dependency of the GenMC model checker is removed.
+/// The linked LLVM version is in the generated `config.h`` file, which we parse and use to link to LLVM.
+/// Returns c++ compiler definitions required for building with/including LLVM, and the include path for LLVM headers.
+fn link_to_llvm(config_file: &Path) -> (String, String) {
+    /// Search a string for a line matching `//@VARIABLE_NAME: VARIABLE CONTENT`
+    fn extract_value<'a>(input: &'a str, name: &str) -> Option<&'a str> {
+        input
+            .lines()
+            .find_map(|line| line.strip_prefix("//@")?.strip_prefix(name)?.strip_prefix(": "))
+    }
+
+    let file_content = std::fs::read_to_string(&config_file).unwrap_or_else(|err| {
+        panic!("GenMC config file ({}) should exist, but got errror {err:?}", config_file.display())
+    });
+
+    let llvm_definitions = extract_value(&file_content, "LLVM_DEFINITIONS")
+        .expect("Config file should contain LLVM_DEFINITIONS");
+    let llvm_include_dirs = extract_value(&file_content, "LLVM_INCLUDE_DIRS")
+        .expect("Config file should contain LLVM_INCLUDE_DIRS");
+    let llvm_library_dir = extract_value(&file_content, "LLVM_LIBRARY_DIR")
+        .expect("Config file should contain LLVM_LIBRARY_DIR");
+    let llvm_config_path = extract_value(&file_content, "LLVM_CONFIG_PATH")
+        .expect("Config file should contain LLVM_CONFIG_PATH");
+
+    // Add linker search path.
+    let lib_dir = PathBuf::from_str(llvm_library_dir).unwrap();
+    println!("cargo::rustc-link-search=native={}", lib_dir.display());
+
+    // Add libraries to link.
+    let output = std::process::Command::new(llvm_config_path)
+        .arg("--libs") // Print the libraries to link to (space-separated list)
+        .output()
+        .expect("failed to execute llvm-config");
+    let llvm_link_libs =
+        String::try_from(output.stdout).expect("llvm-config output should be a valid string");
+
+    for link_lib in llvm_link_libs.trim().split(" ") {
+        let link_lib =
+            link_lib.strip_prefix("-l").expect("Linker parameter should start with \"-l\"");
+        println!("cargo::rustc-link-lib=dylib={link_lib}");
+    }
+
+    (llvm_definitions.to_string(), llvm_include_dirs.to_string())
+}
+
+/// Build the GenMC model checker library and the Rust-C++ interop library with cxx.rs
+fn compile_cpp_dependencies(genmc_path: &Path) {
+    // Part 1:
+    // Compile the GenMC library using cmake.
+
+    let cmakelists_path = genmc_path.join("CMakeLists.txt");
+
+    // FIXME(genmc,cargo): Switch to using `CARGO_CFG_DEBUG_ASSERTIONS` once https://github.com/rust-lang/cargo/issues/15760 is completed.
+    // Enable/disable additional debug checks, prints and options for GenMC, based on the Rust profile (debug/release)
+    let enable_genmc_debug = matches!(std::env::var("PROFILE").as_deref().unwrap(), "debug");
+
+    let mut config = cmake::Config::new(cmakelists_path);
+    config.profile(GENMC_CMAKE_PROFILE);
+    config.define("GENMC_DEBUG", if enable_genmc_debug { "ON" } else { "OFF" });
+
+    // The actual compilation happens here:
+    let genmc_install_dir = config.build();
+
+    // Add the model checker library to be linked and tell rustc where to find it:
+    let cmake_lib_dir = genmc_install_dir.join("lib").join("genmc");
+    println!("cargo::rustc-link-search=native={}", cmake_lib_dir.display());
+    println!("cargo::rustc-link-lib=static={GENMC_MODEL_CHECKER}");
+
+    // FIXME(genmc,llvm): Remove once the LLVM dependency of the GenMC model checker is removed.
+    let config_file = genmc_install_dir.join("include").join("genmc").join("config.h");
+    let (llvm_definitions, llvm_include_dirs) = link_to_llvm(&config_file);
+
+    // Part 2:
+    // Compile the cxx_bridge (the link between the Rust and C++ code).
+
+    let genmc_include_dir = genmc_install_dir.join("include").join("genmc");
+
+    // FIXME(genmc,llvm): remove once LLVM dependency is removed.
+    // These definitions are parsed into a cmake list and then printed to the config.h file, so they are ';' separated.
+    let definitions = llvm_definitions.split(";");
+
+    let mut bridge = cxx_build::bridge("src/lib.rs");
+    // FIXME(genmc,cmake): Remove once the GenMC debug setting is available in the config.h file.
+    if enable_genmc_debug {
+        bridge.define("ENABLE_GENMC_DEBUG", None);
+    }
+    bridge
+        .flags(definitions)
+        .opt_level(2)
+        .debug(true) // Same settings that GenMC uses (default for cmake `RelWithDebInfo`)
+        .warnings(false) // NOTE: enabling this produces a lot of warnings.
+        .std("c++23")
+        .include(genmc_include_dir)
+        .include(llvm_include_dirs)
+        .include("./src_cpp")
+        .file("./src_cpp/MiriInterface.hpp")
+        .file("./src_cpp/MiriInterface.cpp")
+        .compile("genmc_interop");
+
+    // Link the Rust-C++ interface library generated by cxx_build:
+    println!("cargo::rustc-link-lib=static=genmc_interop");
+}
+
+fn main() {
+    // Make sure we don't accidentally distribute a binary with GPL code.
+    if option_env!("RUSTC_STAGE").is_some() {
+        panic!(
+            "genmc should not be enabled in the rustc workspace since it includes a GPL dependency"
+        );
+    }
+
+    // Select which path to use for the GenMC repo:
+    let genmc_path = if let Ok(genmc_src_path) = std::env::var("GENMC_SRC_PATH") {
+        let genmc_src_path =
+            PathBuf::from_str(&genmc_src_path).expect("GENMC_SRC_PATH should contain a valid path");
+        assert!(
+            genmc_src_path.exists(),
+            "GENMC_SRC_PATH={} does not exist!",
+            genmc_src_path.display()
+        );
+        genmc_src_path
+    } else {
+        downloading::download_genmc()
+    };
+
+    // Build all required components:
+    compile_cpp_dependencies(&genmc_path);
+
+    // Only rebuild if anything changes:
+    // Note that we don't add the downloaded GenMC repo, since that should never be modified
+    // manually. Adding that path here would also trigger an unnecessary rebuild after the repo is
+    // cloned (since cargo detects that as a file modification).
+    println!("cargo::rerun-if-changed={RUST_CXX_BRIDGE_FILE_PATH}");
+    println!("cargo::rerun-if-changed=./src");
+    println!("cargo::rerun-if-changed=./src_cpp");
+}
diff --git a/src/tools/miri/genmc-sys/src/lib.rs b/src/tools/miri/genmc-sys/src/lib.rs
new file mode 100644
index 00000000000..ab46d729ea1
--- /dev/null
+++ b/src/tools/miri/genmc-sys/src/lib.rs
@@ -0,0 +1,30 @@
+pub use self::ffi::*;
+
+impl Default for GenmcParams {
+    fn default() -> Self {
+        Self {
+            print_random_schedule_seed: false,
+            do_symmetry_reduction: false,
+            // FIXME(GenMC): Add defaults for remaining parameters
+        }
+    }
+}
+
+#[cxx::bridge]
+mod ffi {
+    /// Parameters that will be given to GenMC for setting up the model checker.
+    /// (The fields of this struct are visible to both Rust and C++)
+    #[derive(Clone, Debug)]
+    struct GenmcParams {
+        pub print_random_schedule_seed: bool,
+        pub do_symmetry_reduction: bool,
+        // FIXME(GenMC): Add remaining parameters.
+    }
+    unsafe extern "C++" {
+        include!("MiriInterface.hpp");
+
+        type MiriGenMCShim;
+
+        fn createGenmcHandle(config: &GenmcParams) -> UniquePtr<MiriGenMCShim>;
+    }
+}
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;
+}
diff --git a/src/tools/miri/genmc-sys/src_cpp/MiriInterface.hpp b/src/tools/miri/genmc-sys/src_cpp/MiriInterface.hpp
new file mode 100644
index 00000000000..e55522ef418
--- /dev/null
+++ b/src/tools/miri/genmc-sys/src_cpp/MiriInterface.hpp
@@ -0,0 +1,44 @@
+#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 */
diff --git a/src/tools/miri/miri-script/src/commands.rs b/src/tools/miri/miri-script/src/commands.rs
index 017e461cd80..ee09b9b4b73 100644
--- a/src/tools/miri/miri-script/src/commands.rs
+++ b/src/tools/miri/miri-script/src/commands.rs
@@ -534,8 +534,8 @@ impl Command {
                 if ty.is_file() {
                     name.ends_with(".rs")
                 } else {
-                    // dir or symlink. skip `target` and `.git`.
-                    &name != "target" && &name != ".git"
+                    // dir or symlink. skip `target`, `.git` and `genmc-src*`
+                    &name != "target" && &name != ".git" && !name.starts_with("genmc-src")
                 }
             })
             .filter_ok(|item| item.file_type().is_file())
diff --git a/src/tools/miri/src/bin/miri.rs b/src/tools/miri/src/bin/miri.rs
index 89fa980ff64..ae1b25f8857 100644
--- a/src/tools/miri/src/bin/miri.rs
+++ b/src/tools/miri/src/bin/miri.rs
@@ -67,8 +67,6 @@ use crate::log::setup::{deinit_loggers, init_early_loggers, init_late_loggers};
 struct MiriCompilerCalls {
     miri_config: Option<MiriConfig>,
     many_seeds: Option<ManySeedsConfig>,
-    /// Settings for using GenMC with Miri.
-    genmc_config: Option<GenmcConfig>,
 }
 
 struct ManySeedsConfig {
@@ -77,12 +75,8 @@ struct ManySeedsConfig {
 }
 
 impl MiriCompilerCalls {
-    fn new(
-        miri_config: MiriConfig,
-        many_seeds: Option<ManySeedsConfig>,
-        genmc_config: Option<GenmcConfig>,
-    ) -> Self {
-        Self { miri_config: Some(miri_config), many_seeds, genmc_config }
+    fn new(miri_config: MiriConfig, many_seeds: Option<ManySeedsConfig>) -> Self {
+        Self { miri_config: Some(miri_config), many_seeds }
     }
 }
 
@@ -192,8 +186,8 @@ impl rustc_driver::Callbacks for MiriCompilerCalls {
                     optimizations is usually marginal at best.");
         }
 
-        if let Some(genmc_config) = &self.genmc_config {
-            let _genmc_ctx = Rc::new(GenmcCtx::new(&config, genmc_config));
+        if let Some(_genmc_config) = &config.genmc_config {
+            let _genmc_ctx = Rc::new(GenmcCtx::new(&config));
 
             todo!("GenMC mode not yet implemented");
         };
@@ -487,7 +481,6 @@ fn main() {
     let mut many_seeds_keep_going = false;
     let mut miri_config = MiriConfig::default();
     miri_config.env = env_snapshot;
-    let mut genmc_config = None;
 
     let mut rustc_args = vec![];
     let mut after_dashdash = false;
@@ -603,9 +596,9 @@ fn main() {
         } else if arg == "-Zmiri-many-seeds-keep-going" {
             many_seeds_keep_going = true;
         } else if let Some(trimmed_arg) = arg.strip_prefix("-Zmiri-genmc") {
-            // FIXME(GenMC): Currently, GenMC mode is incompatible with aliasing model checking.
-            miri_config.borrow_tracker = None;
-            GenmcConfig::parse_arg(&mut genmc_config, trimmed_arg);
+            if let Err(msg) = GenmcConfig::parse_arg(&mut miri_config.genmc_config, trimmed_arg) {
+                fatal_error!("{msg}");
+            }
         } else if let Some(param) = arg.strip_prefix("-Zmiri-env-forward=") {
             miri_config.forwarded_env_vars.push(param.to_owned());
         } else if let Some(param) = arg.strip_prefix("-Zmiri-env-set=") {
@@ -740,13 +733,18 @@ fn main() {
         many_seeds.map(|seeds| ManySeedsConfig { seeds, keep_going: many_seeds_keep_going });
 
     // Validate settings for data race detection and GenMC mode.
-    assert_eq!(genmc_config.is_some(), miri_config.genmc_mode);
-    if genmc_config.is_some() {
+    if miri_config.genmc_config.is_some() {
         if !miri_config.data_race_detector {
             fatal_error!("Cannot disable data race detection in GenMC mode (currently)");
         } else if !miri_config.weak_memory_emulation {
             fatal_error!("Cannot disable weak memory emulation in GenMC mode");
         }
+        if miri_config.borrow_tracker.is_some() {
+            eprintln!(
+                "warning: borrow tracking has been disabled, it is not (yet) supported in GenMC mode."
+            );
+            miri_config.borrow_tracker = None;
+        }
     } else if miri_config.weak_memory_emulation && !miri_config.data_race_detector {
         fatal_error!(
             "Weak memory emulation cannot be enabled when the data race detector is disabled"
@@ -765,8 +763,5 @@ fn main() {
             );
         }
     }
-    run_compiler_and_exit(
-        &rustc_args,
-        &mut MiriCompilerCalls::new(miri_config, many_seeds, genmc_config),
-    )
+    run_compiler_and_exit(&rustc_args, &mut MiriCompilerCalls::new(miri_config, many_seeds))
 }
diff --git a/src/tools/miri/src/concurrency/genmc/config.rs b/src/tools/miri/src/concurrency/genmc/config.rs
index f91211a670f..c56adab90fe 100644
--- a/src/tools/miri/src/concurrency/genmc/config.rs
+++ b/src/tools/miri/src/concurrency/genmc/config.rs
@@ -1,19 +1,35 @@
-use crate::MiriConfig;
+use super::GenmcParams;
 
+/// Configuration for GenMC mode.
+/// The `params` field is shared with the C++ side.
+/// The remaining options are kept on the Rust side.
 #[derive(Debug, Default, Clone)]
 pub struct GenmcConfig {
-    // TODO: add fields
+    pub(super) params: GenmcParams,
+    do_estimation: bool,
+    // FIXME(GenMC): add remaining options.
 }
 
 impl GenmcConfig {
     /// Function for parsing command line options for GenMC mode.
+    ///
     /// All GenMC arguments start with the string "-Zmiri-genmc".
+    /// Passing any GenMC argument will enable GenMC mode.
     ///
-    /// `trimmed_arg` should be the argument to be parsed, with the suffix "-Zmiri-genmc" removed
-    pub fn parse_arg(genmc_config: &mut Option<GenmcConfig>, trimmed_arg: &str) {
+    /// `trimmed_arg` should be the argument to be parsed, with the suffix "-Zmiri-genmc" removed.
+    pub fn parse_arg(
+        genmc_config: &mut Option<GenmcConfig>,
+        trimmed_arg: &str,
+    ) -> Result<(), String> {
+        // FIXME(genmc): Ensure host == target somewhere.
+
         if genmc_config.is_none() {
             *genmc_config = Some(Default::default());
         }
-        todo!("implement parsing of GenMC options")
+        if trimmed_arg.is_empty() {
+            return Ok(()); // this corresponds to "-Zmiri-genmc"
+        }
+        // FIXME(GenMC): implement remaining parameters.
+        todo!();
     }
 }
diff --git a/src/tools/miri/src/concurrency/genmc/dummy.rs b/src/tools/miri/src/concurrency/genmc/dummy.rs
index 3d0558fb685..79d27c4be15 100644
--- a/src/tools/miri/src/concurrency/genmc/dummy.rs
+++ b/src/tools/miri/src/concurrency/genmc/dummy.rs
@@ -16,7 +16,7 @@ pub struct GenmcCtx {}
 pub struct GenmcConfig {}
 
 impl GenmcCtx {
-    pub fn new(_miri_config: &MiriConfig, _genmc_config: &GenmcConfig) -> Self {
+    pub fn new(_miri_config: &MiriConfig) -> Self {
         unreachable!()
     }
 
@@ -227,10 +227,15 @@ impl VisitProvenance for GenmcCtx {
 }
 
 impl GenmcConfig {
-    pub fn parse_arg(_genmc_config: &mut Option<GenmcConfig>, trimmed_arg: &str) {
-        unimplemented!(
-            "GenMC feature im Miri is disabled, cannot handle argument: \"-Zmiri-genmc{trimmed_arg}\""
-        );
+    pub fn parse_arg(
+        _genmc_config: &mut Option<GenmcConfig>,
+        trimmed_arg: &str,
+    ) -> Result<(), String> {
+        if cfg!(feature = "genmc") {
+            Err(format!("GenMC is disabled in this build of Miri"))
+        } else {
+            Err(format!("GenMC is not supported on this target"))
+        }
     }
 
     pub fn should_print_graph(&self, _rep: usize) -> bool {
diff --git a/src/tools/miri/src/concurrency/genmc/mod.rs b/src/tools/miri/src/concurrency/genmc/mod.rs
index 0dfd4b9b80f..3617775e27e 100644
--- a/src/tools/miri/src/concurrency/genmc/mod.rs
+++ b/src/tools/miri/src/concurrency/genmc/mod.rs
@@ -2,6 +2,7 @@
 
 use std::cell::Cell;
 
+use genmc_sys::{GenmcParams, createGenmcHandle};
 use rustc_abi::{Align, Size};
 use rustc_const_eval::interpret::{InterpCx, InterpResult, interp_ok};
 use rustc_middle::mir;
@@ -24,9 +25,19 @@ pub struct GenmcCtx {
 
 impl GenmcCtx {
     /// Create a new `GenmcCtx` from a given config.
-    pub fn new(miri_config: &MiriConfig, genmc_config: &GenmcConfig) -> Self {
-        assert!(miri_config.genmc_mode);
-        todo!()
+    pub fn new(miri_config: &MiriConfig) -> Self {
+        let genmc_config = miri_config.genmc_config.as_ref().unwrap();
+
+        let handle = createGenmcHandle(&genmc_config.params);
+        assert!(!handle.is_null());
+
+        eprintln!("Miri: GenMC handle creation successful!");
+
+        drop(handle);
+        eprintln!("Miri: Dropping GenMC handle successful!");
+
+        // FIXME(GenMC): implement
+        std::process::exit(0);
     }
 
     pub fn get_stuck_execution_count(&self) -> usize {
diff --git a/src/tools/miri/src/concurrency/mod.rs b/src/tools/miri/src/concurrency/mod.rs
index c2ea8a00dec..435615efd9f 100644
--- a/src/tools/miri/src/concurrency/mod.rs
+++ b/src/tools/miri/src/concurrency/mod.rs
@@ -8,7 +8,17 @@ mod vector_clock;
 pub mod weak_memory;
 
 // Import either the real genmc adapter or a dummy module.
-#[cfg_attr(not(feature = "genmc"), path = "genmc/dummy.rs")]
+// On unsupported platforms, we always include the dummy module, even if the `genmc` feature is enabled.
+// FIXME(genmc,macos): Add `target_os = "macos"` once `https://github.com/dtolnay/cxx/issues/1535` is fixed.
+#[cfg_attr(
+    not(all(
+        feature = "genmc",
+        target_os = "linux",
+        target_pointer_width = "64",
+        target_endian = "little"
+    )),
+    path = "genmc/dummy.rs"
+)]
 mod genmc;
 
 pub use self::data_race_handler::{AllocDataRaceHandler, GlobalDataRaceHandler};
diff --git a/src/tools/miri/src/eval.rs b/src/tools/miri/src/eval.rs
index f78908aba8e..4c531a8d1f5 100644
--- a/src/tools/miri/src/eval.rs
+++ b/src/tools/miri/src/eval.rs
@@ -125,8 +125,8 @@ pub struct MiriConfig {
     pub data_race_detector: bool,
     /// Determine if weak memory emulation should be enabled. Requires data race detection to be enabled.
     pub weak_memory_emulation: bool,
-    /// Determine if we are running in GenMC mode. In this mode, Miri will explore multiple concurrent executions of the given program.
-    pub genmc_mode: bool,
+    /// Determine if we are running in GenMC mode and with which settings. In GenMC mode, Miri will explore multiple concurrent executions of the given program.
+    pub genmc_config: Option<GenmcConfig>,
     /// Track when an outdated (weak memory) load happens.
     pub track_outdated_loads: bool,
     /// Rate of spurious failures for compare_exchange_weak atomic operations,
@@ -192,7 +192,7 @@ impl Default for MiriConfig {
             track_alloc_accesses: false,
             data_race_detector: true,
             weak_memory_emulation: true,
-            genmc_mode: false,
+            genmc_config: None,
             track_outdated_loads: false,
             cmpxchg_weak_failure_rate: 0.8, // 80%
             measureme_out: None,
diff --git a/src/tools/miri/src/machine.rs b/src/tools/miri/src/machine.rs
index 142c6ddf933..8f0814a070c 100644
--- a/src/tools/miri/src/machine.rs
+++ b/src/tools/miri/src/machine.rs
@@ -602,6 +602,9 @@ pub struct MiriMachine<'tcx> {
 }
 
 impl<'tcx> MiriMachine<'tcx> {
+    /// Create a new MiriMachine.
+    ///
+    /// Invariant: `genmc_ctx.is_some() == config.genmc_config.is_some()`
     pub(crate) fn new(
         config: &MiriConfig,
         layout_cx: LayoutCx<'tcx>,
@@ -625,7 +628,7 @@ impl<'tcx> MiriMachine<'tcx> {
         });
         let rng = StdRng::seed_from_u64(config.seed.unwrap_or(0));
         let borrow_tracker = config.borrow_tracker.map(|bt| bt.instantiate_global_state(config));
-        let data_race = if config.genmc_mode {
+        let data_race = if config.genmc_config.is_some() {
             // `genmc_ctx` persists across executions, so we don't create a new one here.
             GlobalDataRaceHandler::Genmc(genmc_ctx.unwrap())
         } else if config.data_race_detector {
diff --git a/src/tools/miri/tests/genmc/pass/test_cxx_build.rs b/src/tools/miri/tests/genmc/pass/test_cxx_build.rs
new file mode 100644
index 00000000000..f621bd9114f
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/test_cxx_build.rs
@@ -0,0 +1,8 @@
+//@compile-flags: -Zmiri-genmc
+
+#![no_main]
+
+#[unsafe(no_mangle)]
+fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
+    0
+}
diff --git a/src/tools/miri/tests/genmc/pass/test_cxx_build.stderr b/src/tools/miri/tests/genmc/pass/test_cxx_build.stderr
new file mode 100644
index 00000000000..4b7aa824bd1
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/test_cxx_build.stderr
@@ -0,0 +1,5 @@
+warning: borrow tracking has been disabled, it is not (yet) supported in GenMC mode.
+C++: GenMC handle created!
+Miri: GenMC handle creation successful!
+C++: GenMC handle destroyed!
+Miri: Dropping GenMC handle successful!
diff --git a/src/tools/miri/tests/ui.rs b/src/tools/miri/tests/ui.rs
index cb915b11b67..73fbe2cc020 100644
--- a/src/tools/miri/tests/ui.rs
+++ b/src/tools/miri/tests/ui.rs
@@ -338,6 +338,20 @@ fn main() -> Result<()> {
         ui(Mode::Fail, "tests/native-lib/fail", &target, WithoutDependencies, tmpdir.path())?;
     }
 
+    // We only enable GenMC tests when the `genmc` feature is enabled, but also only on platforms we support:
+    // FIXME(genmc,macos): Add `target_os = "macos"` once `https://github.com/dtolnay/cxx/issues/1535` is fixed.
+    // FIXME(genmc,cross-platform): remove `host == target` check once cross-platform support with GenMC is possible.
+    if cfg!(all(
+        feature = "genmc",
+        target_os = "linux",
+        target_pointer_width = "64",
+        target_endian = "little"
+    )) && host == target
+    {
+        ui(Mode::Pass, "tests/genmc/pass", &target, WithDependencies, tmpdir.path())?;
+        ui(Mode::Fail, "tests/genmc/fail", &target, WithDependencies, tmpdir.path())?;
+    }
+
     Ok(())
 }