diff --git a/.gitignore b/.gitignore index ed2d0ba7ba..4a238dc031 100644 --- a/.gitignore +++ b/.gitignore @@ -1,5 +1,4 @@ target -/doc tex/*/out *.dot *.out diff --git a/Cargo.lock b/Cargo.lock index aa6f059cec..17134ec582 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -170,6 +170,8 @@ version = "1.2.17" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "1fcb57c740ae1daf453ae85f16e37396f672b039e00d9d866e07ddb24e328e3a" dependencies = [ + "jobserver", + "libc", "shlex", ] @@ -225,6 +227,52 @@ dependencies = [ "inout", ] +[[package]] +name = "clap" +version = "4.5.40" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "40b6887a1d8685cebccf115538db5c0efe625ccac9696ad45c409d96566e910f" +dependencies = [ + "clap_builder", +] + +[[package]] +name = "clap_builder" +version = "4.5.40" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e0c66c08ce9f0c698cbce5c0279d0bb6ac936d8674174fe48f736533b964f59e" +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.0", +] + [[package]] name = "color-eyre" version = "0.6.3" @@ -315,6 +363,68 @@ dependencies = [ "typenum", ] +[[package]] +name = "cxx" +version = "1.0.160" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "be1149bab7a5580cb267215751389597c021bfad13c0bb00c54e19559333764c" +dependencies = [ + "cc", + "cxxbridge-cmd", + "cxxbridge-flags", + "cxxbridge-macro", + "foldhash", + "link-cplusplus", +] + +[[package]] +name = "cxx-build" +version = "1.0.160" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6aeeaf1aefae8e0f5141920a7ecbc64a22ab038d4b4ac59f2d19e0effafd5b53" +dependencies = [ + "cc", + "codespan-reporting", + "indexmap", + "proc-macro2", + "quote", + "scratch", + "syn", +] + +[[package]] +name = "cxxbridge-cmd" +version = "1.0.160" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c36ac1f9a72064b1f41fd7b49a4c1b3bf33b9ccb1274874dda6d264f57c55964" +dependencies = [ + "clap", + "codespan-reporting", + "indexmap", + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "cxxbridge-flags" +version = "1.0.160" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "170c6ff5d009663866857a91ebee55b98ea4d4b34e7d7aba6dc4a4c95cc7b748" + +[[package]] +name = "cxxbridge-macro" +version = "1.0.160" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4984a142211026786011a7e79fa22faa1eca1e9cbf0e60bffecfd57fd3db88f1" +dependencies = [ + "indexmap", + "proc-macro2", + "quote", + "rustversion", + "syn", +] + [[package]] name = "directories" version = "6.0.0" @@ -336,12 +446,29 @@ dependencies = [ "windows-sys 0.59.0", ] +[[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.11" @@ -374,6 +501,21 @@ version = "1.0.7" 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" @@ -384,6 +526,16 @@ dependencies = [ "version_check", ] +[[package]] +name = "genmc-sys" +version = "0.1.0" +dependencies = [ + "cmake", + "cxx", + "cxx-build", + "git2", +] + [[package]] name = "getrandom" version = "0.2.15" @@ -413,12 +565,150 @@ version = "0.28.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "4271d37baee1b8c7e4b708028c57d816cf9d2434acb33a549475f78c181f6253" +[[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" @@ -466,6 +756,16 @@ version = "1.0.15" 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.2", + "libc", +] + [[package]] name = "js-sys" version = "0.3.77" @@ -513,6 +813,19 @@ dependencies = [ "cc", ] +[[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.6" @@ -533,12 +846,39 @@ dependencies = [ "libc", ] +[[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.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "fe7db12097d22ec582439daf8618b8fdd1a7bef6270e9af3b1ebcd30893cf413" +[[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.12" @@ -616,6 +956,7 @@ dependencies = [ "chrono-tz", "colored", "directories", + "genmc-sys", "getrandom 0.3.2", "ipc-channel", "libc", @@ -676,6 +1017,24 @@ version = "1.21.3" 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" @@ -729,6 +1088,12 @@ dependencies = [ "regex", ] +[[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" @@ -782,12 +1147,27 @@ version = "0.2.16" 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.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "350e9b48cbc6b0e028b0473b114454c6316e57336ee184ceab6e53f72c178b3e" +[[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" @@ -986,6 +1366,12 @@ dependencies = [ "windows-sys 0.59.0", ] +[[package]] +name = "rustversion" +version = "1.0.21" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8a0d197bd2c9dc6e53b84da9556a69ba4cdfab8619eb41a8bd1cc2027a0f6b1d" + [[package]] name = "ryu" version = "1.0.20" @@ -998,6 +1384,12 @@ version = "1.2.0" 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" @@ -1076,6 +1468,18 @@ dependencies = [ "color-eyre", ] +[[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.100" @@ -1087,6 +1491,17 @@ dependencies = [ "unicode-ident", ] +[[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.19.1" @@ -1100,6 +1515,15 @@ dependencies = [ "windows-sys 0.59.0", ] +[[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" @@ -1160,6 +1584,16 @@ dependencies = [ "libc", ] +[[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" @@ -1251,6 +1685,23 @@ version = "0.2.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "1fc81956842c57dac11422a97c3b8195a1ff727f06e85c84ed2e8aa277c9a0fd" +[[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.16.0" @@ -1266,6 +1717,12 @@ version = "0.1.1" 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" @@ -1354,6 +1811,15 @@ dependencies = [ "wasm-bindgen", ] +[[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" @@ -1509,6 +1975,36 @@ dependencies = [ "bitflags", ] +[[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.24" @@ -1528,3 +2024,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/Cargo.toml b/Cargo.toml index 75476d7923..52257a17d8 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -47,6 +47,10 @@ ipc-channel = "0.19.0" serde = { version = "1.0.219", features = ["derive"] } capstone = "0.13" +# 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.29.1" colored = "2" @@ -65,7 +69,7 @@ harness = false [features] default = ["stack-cache"] -genmc = [] +genmc = ["dep:genmc-sys"] stack-cache = [] stack-cache-consistency-check = ["stack-cache"] tracing = ["serde_json"] diff --git a/doc/GenMC.md b/doc/GenMC.md new file mode 100644 index 0000000000..2ecaa01620 --- /dev/null +++ b/doc/GenMC.md @@ -0,0 +1,42 @@ +# **(WIP)** Documentation for Miri-GenMC +[GenMC](https://github.com/MPI-SWS/genmc) is a stateless model checker for exploring concurrent executions of a program. + +**NOTE: Currently, no actual GenMC functionality is part of Miri, this is still WIP.** + + + +## Usage +Basic usage: +```shell +MIRIFLAGS="-Zmiri-genmc" cargo miri run +``` + + + + + +## Tips + + + +## 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 32-bit platform support. +- No cross-platform interpretation. + + + +## Development + +GenMC is written in C++, which complicates development a bit. +For Rust-C++ interop, Miri uses [CXX.rs](https://cxx.rs/), and all handling of C++ code is contained in the `genmc-sys` crate (located in the Miri repository root directory: `miri/genmc-sys/`). + +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 different maintainers). +Note that this repo is just a mirror repo. + + + diff --git a/genmc-sys/.gitignore b/genmc-sys/.gitignore new file mode 100644 index 0000000000..f526fe37c0 --- /dev/null +++ b/genmc-sys/.gitignore @@ -0,0 +1,3 @@ +genmc/ +genmc-*/ +downloaded/ diff --git a/genmc-sys/Cargo.toml b/genmc-sys/Cargo.toml new file mode 100644 index 0000000000..5ebd733b77 --- /dev/null +++ b/genmc-sys/Cargo.toml @@ -0,0 +1,17 @@ +[package] +name = "genmc-sys" +version = "0.1.0" +edition = "2024" + +[features] +default = ["download_genmc"] +# If downloading is disabled, a local GenMC repo must be available in the "./genmc" path. +download_genmc = ["dep:git2"] + +[dependencies] +cxx = { version = "1.0.160", features = ["c++20"] } + +[build-dependencies] +cmake = "0.1.54" +git2 = { version = "0.20.2", optional = true, default-features = false, features = ["https"] } +cxx-build = { version = "1.0.160", features = ["parallel"] } diff --git a/genmc-sys/build.rs b/genmc-sys/build.rs new file mode 100644 index 0000000000..17c854673c --- /dev/null +++ b/genmc-sys/build.rs @@ -0,0 +1,201 @@ +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 used for development of Miri-GenMC. +/// A GenMC repository in this directory will take precedence over the downloaded GenMC repository. +/// If the `download` feature is disabled, this path must contain a GenMC repository. +const GENMC_LOCAL_PATH: &str = "./genmc/"; + +/// Name of the library of the GenMC model checker. +const GENMC_MODEL_CHECKER: &str = "model_checker"; + +/// Path where the `cxx_bridge!` macro is used to define the Rust-C++ interface. +const RUST_CXX_BRIDGE_FILE_PATH: &str = "src/lib.rs"; + +// FIXME(GenMC, build): decide whether to keep debug enabled or not (without this: calling BUG() ==> UB). +// FIXME(GenMC, build): decide on which profile to use. + +/// Enable/disable additional debug checks, prints and options for GenMC. +const ENABLE_GENMC_DEBUG: bool = true; +/// The profile with which to build GenMC. +const GENMC_CMAKE_PROFILE: &str = "RelWithDebInfo"; + +#[cfg(feature = "download_genmc")] +mod downloading { + use std::path::{Path, PathBuf}; + use std::str::FromStr; + + use git2::{Commit, Oid, Repository, StatusOptions}; + + use super::GENMC_LOCAL_PATH; + + pub(crate) const GENMC_GITHUB_URL: &str = "https://github.com/Patrick-6/genmc.git"; + pub(crate) const GENMC_COMMIT: &str = "2f503036ae14dc91746bfc292d142f332f31727e"; + pub(crate) const GENMC_DOWNLOAD_PATH: &str = "./downloaded/genmc/"; + + 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 + } + + // 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. + match repo.find_remote("origin") { + Ok(mut remote) => + remote.fetch(&[GENMC_COMMIT], None, None).expect("Failed to fetch from remote."), + Err(e) => { + panic!("Could not load commit ({GENMC_COMMIT}) from remote repository '{GENMC_GITHUB_URL}'. Error: {e}"); + } + } + 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; + } + + let local_path = Path::new(GENMC_LOCAL_PATH); + println!( + "HINT: For local development, place a GenMC repository in the path {:?}.", + std::path::absolute(local_path).unwrap_or_else(|_| local_path.into()) + ); + 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." + ); + } +} + +/// Build the Rust-C++ interop library with cxx.rs +fn build_cxx_bridge(genmc_path: &Path, genmc_install_dir: &Path) { + // Paths for include directories: + let model_checker_include_path = genmc_path.join(GENMC_MODEL_CHECKER).join("include"); + let genmc_common_include_path = genmc_path.join("common").join("include"); + + // FIXME(GenMC, build): can we use c++23? Does CXX support that? Does rustc CI support that? + cxx_build::bridge("src/lib.rs") + .opt_level(2) + .debug(true) // Same settings that GenMC uses ("-O2 -g") + .warnings(false) // NOTE: enabling this produces a lot of warnings. + .std("c++20") + .include(genmc_common_include_path) // Required for including GenMC helper files. + .include(model_checker_include_path) // Required for including GenMC model checker files. + .include(genmc_install_dir) // Required for including `config.h`. + .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"); +} + +/// Build the GenMC model checker library. +/// Returns the path where cmake installs the model checker library and the config.h file. +fn build_genmc_model_checker(genmc_path: &Path) -> PathBuf { + let cmakelists_path = genmc_path.join("CMakeLists.txt"); + + let mut config = cmake::Config::new(cmakelists_path); + config.profile(GENMC_CMAKE_PROFILE); + if ENABLE_GENMC_DEBUG { + config.define("GENMC_DEBUG", "ON"); + } + + // FIXME(GenMC,HACK): Required for unknown reasons on older cmake (version 3.22.1, works without this with version 3.31.6) + // Without this, the files are written into the source directory by the cmake configure step, and then + // the build step cannot find these files, because it correctly tries using the `target` directory. + let out_dir = std::env::var("OUT_DIR").unwrap(); + let genmc_build_path: PathBuf = [&out_dir, "build"].into_iter().collect(); + config.configure_arg(format!("-B {}", genmc_build_path.display())); + + // Enable only the components of GenMC that we need: + config.define("BUILD_LLI", "OFF"); + config.define("BUILD_INSTRUMENTATION", "OFF"); + config.define("BUILD_MODEL_CHECKER", "ON"); + + let cmake_install_dir = config.build(); + + // Add the model checker library to be linked and the install directory where it is located: + println!("cargo::rustc-link-search=native={}", cmake_install_dir.display()); + println!("cargo::rustc-link-lib=static={GENMC_MODEL_CHECKER}"); + + cmake_install_dir +} + +fn main() { + // Select between local GenMC repo, or downloading GenMC from a specific commit. + let Ok(genmc_local_path) = PathBuf::from_str(GENMC_LOCAL_PATH); + let genmc_path = if genmc_local_path.exists() { + // If the local repository exists, cargo should watch it for changes: + // FIXME(genmc,cargo): We could always watch this path even if it doesn't (yet) exist, depending on how `https://github.com/rust-lang/cargo/issues/6003` is resolved. + // Adding it here means we don't rebuild if a user creates `GENMC_LOCAL_PATH`, which isn't ideal. + // Cargo currently always rebuilds if a watched directory doesn't exist, so we can only add it if it exists. + println!("cargo::rerun-if-changed={GENMC_LOCAL_PATH}"); + genmc_local_path + } else if cfg!(feature = "download_genmc") { + downloading::download_genmc() + } else { + panic!("GenMC not found in path '{GENMC_LOCAL_PATH}', and downloading GenMC is disabled."); + }; + + // Build all required components: + let genmc_install_dir = build_genmc_model_checker(&genmc_path); + build_cxx_bridge(&genmc_path, &genmc_install_dir); + + // 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_cpp"); +} diff --git a/genmc-sys/src/lib.rs b/genmc-sys/src/lib.rs new file mode 100644 index 0000000000..ab46d729ea --- /dev/null +++ b/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; + } +} diff --git a/genmc-sys/src_cpp/MiriInterface.cpp b/genmc-sys/src_cpp/MiriInterface.cpp new file mode 100644 index 0000000000..e740d496c1 --- /dev/null +++ b/genmc-sys/src_cpp/MiriInterface.cpp @@ -0,0 +1,49 @@ +#include "MiriInterface.hpp" + +#include "genmc-sys/src/lib.rs.h" + +auto MiriGenMCShim::createHandle(const GenmcParams &config) + -> std::unique_ptr +{ + auto vConf = std::make_shared(); + + // Miri needs all threads to be replayed, even fully completed ones. + vConf->replayCompletedThreads = true; + + // We only support the RC11 memory model for Rust. + vConf->model = ModelType::RC11; + + vConf->printRandomScheduleSeed = config.print_random_schedule_seed; + + // FIXME(GenMC): disable any options we don't support currently: + vConf->ipr = false; + vConf->disableBAM = true; + vConf->instructionCaching = false; + + ERROR_ON(config.do_symmetry_reduction, "Symmetry reduction is currently unsupported in GenMC mode."); + vConf->symmetryReduction = config.do_symmetry_reduction; + + // FIXME(GenMC): Should there be a way to change this option from Miri? + vConf->schedulePolicy = SchedulePolicy::WF; + + // FIXME(GenMC): implement estimation mode: + vConf->estimate = false; + vConf->estimationMax = 1000; + const auto mode = vConf->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`). + vConf->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. + vConf->warnUnfreedMemory = false; + + checkVerificationConfigOptions(*vConf); + + auto driver = std::make_unique(std::move(vConf), mode); + return driver; +} diff --git a/genmc-sys/src_cpp/MiriInterface.hpp b/genmc-sys/src_cpp/MiriInterface.hpp new file mode 100644 index 0000000000..2591abb128 --- /dev/null +++ b/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 "Verification/GenMCDriver.hpp" +#include "Verification/VerificationConfig.hpp" + +#include + +/**** 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 vConf, Mode mode /* = VerificationMode{} */) + : GenMCDriver(std::move(vConf), nullptr, mode) + { + std::cerr << "C++: GenMC handle created!" << std::endl; + } + + virtual ~MiriGenMCShim() + { + std::cerr << "C++: GenMC handle destroyed!" << std::endl; + } + + static std::unique_ptr 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 +{ + return MiriGenMCShim::createHandle(config); +} + +#endif /* GENMC_MIRI_INTERFACE_HPP */ diff --git a/src/bin/miri.rs b/src/bin/miri.rs index e3b579a4ac..45c5a320fc 100644 --- a/src/bin/miri.rs +++ b/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, many_seeds: Option, - /// Settings for using GenMC with Miri. - genmc_config: Option, } struct ManySeedsConfig { @@ -77,12 +75,8 @@ struct ManySeedsConfig { } impl MiriCompilerCalls { - fn new( - miri_config: MiriConfig, - many_seeds: Option, - genmc_config: Option, - ) -> Self { - Self { miri_config: Some(miri_config), many_seeds, genmc_config } + fn new(miri_config: MiriConfig, many_seeds: Option) -> 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"); }; @@ -484,7 +478,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; @@ -598,9 +591,7 @@ 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); + GenmcConfig::parse_arg(&mut miri_config.genmc_config, trimmed_arg); } 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=") { @@ -735,13 +726,21 @@ 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() { + // FIXME(genmc): Add checks for currently supported platforms (64bit, target == host) 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"); } + // FIXME(genmc): Remove once GenMC mode is compatible with borrow tracking: + if miri_config.borrow_tracker.is_some() { + eprintln!( + "warning: Borrow tracking has been disabled, it is not (yet) supported in GenMC mode." + ); + eprintln!(); + 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" @@ -760,8 +759,5 @@ fn main() { // are async-signal-safe, as is accessing atomics //let _ = unsafe { miri::native_lib::init_sv() }; } - 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/concurrency/genmc/config.rs b/src/concurrency/genmc/config.rs index f91211a670..42591c9ac2 100644 --- a/src/concurrency/genmc/config.rs +++ b/src/concurrency/genmc/config.rs @@ -1,19 +1,41 @@ -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 + /// `trimmed_arg` should be the argument to be parsed, with the suffix "-Zmiri-genmc" removed. pub fn parse_arg(genmc_config: &mut Option, trimmed_arg: &str) { + // FIXME(genmc,macos): Add `target_os = "macos"` once `https://github.com/dtolnay/cxx/issues/1535` is fixed. + if !cfg!(all( + feature = "genmc", + any(target_os = "linux", target_os = "macos"), + target_pointer_width = "64", + target_endian = "little" + )) { + unimplemented!( + "GenMC mode is not supported on this platform, cannot handle argument: \"-Zmiri-genmc{trimmed_arg}\"" + ); + } if genmc_config.is_none() { *genmc_config = Some(Default::default()); } - todo!("implement parsing of GenMC options") + if trimmed_arg.is_empty() { + return; // this corresponds to "-Zmiri-genmc" + } + // FIXME(GenMC): implement remaining parameters. + todo!(); } } diff --git a/src/concurrency/genmc/dummy.rs b/src/concurrency/genmc/dummy.rs index 3d0558fb68..7570f8ba36 100644 --- a/src/concurrency/genmc/dummy.rs +++ b/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!() } @@ -228,9 +228,21 @@ impl VisitProvenance for GenmcCtx { impl GenmcConfig { pub fn parse_arg(_genmc_config: &mut Option, trimmed_arg: &str) { - unimplemented!( - "GenMC feature im Miri is disabled, cannot handle argument: \"-Zmiri-genmc{trimmed_arg}\"" - ); + // FIXME(genmc,macos): Add `target_os = "macos"` once `https://github.com/dtolnay/cxx/issues/1535` is fixed. + if cfg!(all( + feature = "genmc", + any(target_os = "linux", target_os = "macos"), + target_pointer_width = "64", + target_endian = "little" + )) { + unimplemented!( + "GenMC is disabled, cannot handle argument: \"-Zmiri-genmc{trimmed_arg}\"" + ); + } else { + unimplemented!( + "GenMC mode is not supported on this platform, cannot handle argument: \"-Zmiri-genmc{trimmed_arg}\"" + ); + } } pub fn should_print_graph(&self, _rep: usize) -> bool { diff --git a/src/concurrency/genmc/mod.rs b/src/concurrency/genmc/mod.rs index 0dfd4b9b80..3617775e27 100644 --- a/src/concurrency/genmc/mod.rs +++ b/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/concurrency/mod.rs b/src/concurrency/mod.rs index 49bcc0d30b..190dd3f3ed 100644 --- a/src/concurrency/mod.rs +++ b/src/concurrency/mod.rs @@ -9,7 +9,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/eval.rs b/src/eval.rs index 63578912c2..af6e5e369c 100644 --- a/src/eval.rs +++ b/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, /// Track when an outdated (weak memory) load happens. pub track_outdated_loads: bool, /// Rate of spurious failures for compare_exchange_weak atomic operations, @@ -190,7 +190,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/machine.rs b/src/machine.rs index 4f3dc48532..99d1617950 100644 --- a/src/machine.rs +++ b/src/machine.rs @@ -621,6 +621,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>, @@ -644,7 +647,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/tests/genmc/pass/test_cxx_build.rs b/tests/genmc/pass/test_cxx_build.rs new file mode 100644 index 0000000000..f621bd9114 --- /dev/null +++ b/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/tests/genmc/pass/test_cxx_build.stderr b/tests/genmc/pass/test_cxx_build.stderr new file mode 100644 index 0000000000..3773dbeff3 --- /dev/null +++ b/tests/genmc/pass/test_cxx_build.stderr @@ -0,0 +1,6 @@ +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/tests/ui.rs b/tests/ui.rs index 5239f8338e..9c43918fdb 100644 --- a/tests/ui.rs +++ b/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(()) }