Implement building GenMC C++ code #4453

Patrick-6 · 2025-07-07T10:04:16Z

This PR is in preparation for adding GenMC support to Miri.
It adds the genmc-sys crate, which can automatically load GenMC from a git repo (temporarily pointing to a private repo, but will point to the GenMC Github repo after everything is implemented)

This PR doesn't add any functionality for GenMC mode, only a test for calling C++ functions from Rust code through the cxx crate.

Cargo.toml

genmc-sys/build.rs

genmc-sys/src_cpp/MiriInterface.hpp

RalfJung · 2025-07-09T12:27:44Z

@rustbot author
Please mark it as ready when CI is green.

rustbot · 2025-07-09T12:27:49Z

Reminder, once the PR becomes ready for a review, use @rustbot ready.

Patrick-6 · 2025-07-09T15:55:15Z

@rustbot ready

genmc-sys/build.rs

Cargo.toml

genmc-sys/Cargo.toml

genmc-sys/build.rs

src/bin/miri.rs

src/concurrency/genmc/dummy.rs

src/concurrency/mod.rs

Cargo.toml

tests/ui.rs

RalfJung · 2025-07-11T14:25:11Z

Here's my first round of comments. :)

@rustbot author

Patrick-6 · 2025-07-12T13:29:18Z

Should the build script not download anything if cargo is invoked with --offline or --frozen (which causes cargo to not access the network)? I can't really find anything about how a build script should behave in such a case, or if it can even detect it. There is the CARGO_NET_OFFLINE env. var, but that appears to be only for changing cargo's behavior, it's not one of the env. vars set for build scripts..

genmc-sys/build.rs

Patrick-6 · 2025-07-13T21:33:12Z

genmc-sys/build.rs

+    // 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");
+    println!("cargo::rerun-if-changed={GENMC_LOCAL_PATH}");


For some reason, adding this path to the rerun-if-changed if the path doesn't exist yet causes full rebuilds on every build. I think the non-existing directory is seen as a change by cargo.

Here is the output from running CARGO_LOG=cargo::core::compiler::fingerprint=info ./miri build --features=genmc after a complete build without any file modifications (as described here):

cargo::core::compiler::fingerprint: stale: missing "/path/to/miri/genmc-sys/./genmc/" cargo::core::compiler::fingerprint: fingerprint dirty for miri v0.1.0 (/path/to/miri)

Is this intended behavior for cargo?

Can you just add GENMC_LOCAL_PATH only if you actually use the local path, not the download?

Yes, but I think then we wouldn't trigger an automatic rebuild if a user adds the ./genmc directory. That's probably still better than constantly rebuilding, since this case should be rare.

Oh, you are using the existence of the directory as the signal for using it... yeah that doesn't work with cargo's model, it seems. I'll ask the cargo devs about it, but for now, let's use an env var to signal explicitly that you want a local build instead of a download, and then add that env var to rerun-if-changed.

Also see rust-lang/cargo#6003

genmc-sys/build.rs

RalfJung · 2025-07-14T10:21:40Z

Should the build script not download anything if cargo is invoked with --offline or --frozen (which causes cargo to not access the network)? I can't really find anything about how a build script should behave in such a case, or if it can even detect it. There is the CARGO_NET_OFFLINE env. var, but that appears to be only for changing cargo's behavior, it's not one of the env. vars set for build scripts..

Yeah I don't think we have a way to check for that.

Please ask on some RUst forum (URLO on Zulip) what the typical approach here is, I don't know.

genmc-sys/build.rs

RalfJung · 2025-07-14T10:29:57Z

genmc-sys/build.rs

+    // 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");
+    println!("cargo::rerun-if-changed={GENMC_LOCAL_PATH}");


Can you just add GENMC_LOCAL_PATH only if you actually use the local path, not the download?

RalfJung · 2025-07-14T18:42:39Z

which one, adding the warning?

Ah, sorry, stopped reading too early... Add the flag to disable SB to the tests.

genmc-sys/build.rs

doc/GenMC.md

genmc-sys/build.rs

RalfJung · 2025-07-23T09:56:14Z

genmc-sys/build.rs

+    } else 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


Suggested change

} else 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

The point of the env var was to control whether we download or not, wasn't it?

I thought we would keep this so you can use the normal ./miri commands for development, without having to set the env var, by having your development copy of GenMC in genmc-sys/genmc/.

Normal ./miri doesn't turn on the feature. ./miri build --feature genmc should use the downloaded version -- that's the right default for most contributors.

So for Miri-GenMC contributors the way to do it is GENMC_SRC_PATH="/some/path/" ./miri build --features=genmc ? (or export GENMC_SRC_PATH=...)

For the extremely rare contributor that needs a custom genmc, yeah.

It'd be nicer if you just had to create a folder, but that doesn't seem to be possible with cargo currently.

The current implementation uses:

path in GENMC_SRC_PATH if set

genmc-sys/genmc if present

genmc-sys/downloaded/genmc if present

do the download into downloaded/genmc

But that is what we have if I don't remove that if

But it doesn't work: if you first build without the folder existing, and then you create the folder, it won't rebuild and will keep using the downloaded genmc.

Nothing a little touch genmc-sys/build.rs doesn't fix ;)

But ok, we can remove it.

Nothing a little touch genmc-sys/build.rs doesn't fix ;)

If you prefer that, we can also do that, and carefully document it.

But we don't want that and the env var. Let's have one way and one way only for local builds.

I've switched to only the env var + download ways, it is still reasonably usable by doing export GENMC_SRC_PATH=... in the current shell, then the path doesn't need to be passed every time.

…ure)

…ugh GENMC_SRC_PATH env var.

…ailable in the configuration file.

genmc-sys/build.rs

Patrick-6 · 2025-07-24T13:40:48Z

etc/rust_analyzer_helix.toml

 linkedProjects = [
    "Cargo.toml",
    "cargo-miri/Cargo.toml",
+    "genmc-sys/Cargo.toml",
    "miri-script/Cargo.toml",
 ]


Apparently using the linkedProjects setting means that rust-analyzer auto-discovery is turned off, so you get no RA help at all in directories no listed here. Adding the genmc-sys lines fixes it for VSCode, but I can't test it for helix (no reason to believe it wouldn't work though).

There still another issue (maybe not for this PR): I still don't get any RA help in any Rust files in the miri/tests/ directory, but maybe that could be added too somehow? I'm unsure how this would work though, since the settings file here also overrides the check command to use ./miri clippy/check instead of cargo clippy/check, which may not work with the tests directory.

Also, this setting expects paths to either Cargo.toml, rust-project.json, or loose .rs files, and we definitely don't want to add all tests here.

Yeah RA doesn't have support for ui test suites like we're using them, unfortunately.

miri-script/src/commands.rs

genmc-sys/build.rs

…matting exception for downloaded GenMC.

Patrick-6 · 2025-07-24T22:58:19Z

As mentioned on Zulip, the license changes are still missing, so this probably shouldn't be merged yet, but otherwise:

From a technical point of view, everything should be in order now.
The documentation might need to be improved/cleaned up/expanded.
We don't yet have any formatting & linting rules (and automatic checks) for the C++ code that lives in the Miri repo (but that's a low priority for now).

@rustbot ready

RalfJung · 2025-07-25T10:09:29Z

genmc-sys/Cargo.toml

+[package]
+name = "genmc-sys"
+version = "0.1.0"
+edition = "2024"


This need a license declaration, and it should probably be the genmc GPL license to ensure this is reflected somewhere on the Rust side.

Suggested change

edition = "2024"

edition = "2024"

license = "GPL-3.0-or-later"

I've added the license already locally before I saw your comment

genmc-sys/build.rs

Cargo.toml

Co-authored-by: Ralf Jung <post@ralfj.de>

…ng issues) Co-authored-by: Ralf Jung <post@ralfj.de>

Patrick-6 · 2025-07-25T11:10:02Z

genmc-sys/LICENSE

FWIU, this file is required too for the GPL license

genmc-sys/Cargo.toml

RalfJung reviewed Jul 7, 2025

View reviewed changes

Cargo.toml Outdated Show resolved Hide resolved

RalfJung reviewed Jul 7, 2025

View reviewed changes

genmc-sys/build.rs Outdated Show resolved Hide resolved

Patrick-6 commented Jul 7, 2025

View reviewed changes

genmc-sys/build.rs Outdated Show resolved Hide resolved

Patrick-6 commented Jul 7, 2025

View reviewed changes

genmc-sys/build.rs Outdated Show resolved Hide resolved

Patrick-6 commented Jul 7, 2025

View reviewed changes

genmc-sys/build.rs Outdated Show resolved Hide resolved

Patrick-6 commented Jul 8, 2025

View reviewed changes

genmc-sys/build.rs Outdated Show resolved Hide resolved

Patrick-6 commented Jul 8, 2025

View reviewed changes

genmc-sys/src_cpp/MiriInterface.hpp Outdated Show resolved Hide resolved

rustbot added the S-waiting-on-author Status: Waiting for the PR author to address review comments label Jul 9, 2025

rustbot added S-waiting-on-review Status: Waiting for a review to complete and removed S-waiting-on-author Status: Waiting for the PR author to address review comments labels Jul 9, 2025

Patrick-6 commented Jul 10, 2025

View reviewed changes

genmc-sys/build.rs Outdated Show resolved Hide resolved

RalfJung reviewed Jul 11, 2025

View reviewed changes

rustbot added S-waiting-on-author Status: Waiting for the PR author to address review comments and removed S-waiting-on-review Status: Waiting for a review to complete labels Jul 11, 2025

Patrick-6 commented Jul 13, 2025

View reviewed changes

genmc-sys/build.rs Outdated Show resolved Hide resolved

Patrick-6 commented Jul 13, 2025

View reviewed changes

genmc-sys/build.rs Outdated Show resolved Hide resolved

RalfJung reviewed Jul 14, 2025

View reviewed changes

RalfJung mentioned this pull request Jul 14, 2025

warn if rerun-if-changed=PATH is used but PATH points to none-existing file rust-lang/cargo#6003

Open

RalfJung reviewed Jul 16, 2025

View reviewed changes

genmc-sys/build.rs Outdated Show resolved Hide resolved

RalfJung reviewed Jul 16, 2025

View reviewed changes

genmc-sys/build.rs Outdated Show resolved Hide resolved

Patrick-6 commented Jul 16, 2025

View reviewed changes

doc/GenMC.md Outdated Show resolved Hide resolved

RalfJung reviewed Jul 17, 2025

View reviewed changes

doc/GenMC.md Outdated Show resolved Hide resolved

Switch cxx build step to C++23.

da61f52

RalfJung reviewed Jul 23, 2025

View reviewed changes

genmc-sys/build.rs Outdated Show resolved Hide resolved

RalfJung reviewed Jul 23, 2025

View reviewed changes

Patrick-6 added 4 commits July 23, 2025 14:40

Permanently enable downloading of GenMC (i.e, remove downloading feat…

245b31c

…ure)

Remove local GenMC path for development, only support local path thro…

3e5d3ab

…ugh GENMC_SRC_PATH env var.

Switch to passing cxx_build compiler parameters as struct.

2ee2e37

[temporary] Pass GenMC debug setting manually until GenMC makes it av…

a86b775

…ailable in the configuration file.

Patrick-6 commented Jul 24, 2025

View reviewed changes

genmc-sys/build.rs Outdated Show resolved Hide resolved

Patrick-6 added 2 commits July 24, 2025 15:26

Clean up C++ compilation steps and combine them into 1 function.

012781c

Add genmc-sys to rust-analyzer linkedProjects paths.

c16d420

Patrick-6 commented Jul 24, 2025

View reviewed changes

Patrick-6 added 3 commits July 24, 2025 19:39

Prevent Miri fmt from formatting downloaded GenMC Rust files.

0977206

Add handling for changing remote URL for downloaded GenMC repo.

e6a0ff3

Update GenMC repo to officially released version.

41d796e

Patrick-6 commented Jul 24, 2025

View reviewed changes

miri-script/src/commands.rs Outdated Show resolved Hide resolved

Patrick-6 commented Jul 24, 2025

View reviewed changes

genmc-sys/build.rs Show resolved Hide resolved

Give downloaded GenMC directory a better name. Improve docs about for…

9f14cd3

…matting exception for downloaded GenMC.

rustbot added S-waiting-on-review Status: Waiting for a review to complete and removed S-waiting-on-author Status: Waiting for the PR author to address review comments labels Jul 24, 2025

RalfJung reviewed Jul 25, 2025

View reviewed changes

genmc-sys/build.rs Show resolved Hide resolved

RalfJung reviewed Jul 25, 2025

View reviewed changes

Cargo.toml Outdated Show resolved Hide resolved

Patrick-6 and others added 4 commits July 25, 2025 12:41

Pin cc crate version to higher than what cxx_build requires.

a1239bd

Set genmc-sys license and update docs about licensing issues.

5177946

Add warning about genmc-sys license

2f401ba

Co-authored-by: Ralf Jung <post@ralfj.de>

Add error when compiling genmc-sys in rustc workspace (due to licensi…

c3ca2f2

…ng issues) Co-authored-by: Ralf Jung <post@ralfj.de>

Patrick-6 commented Jul 25, 2025

View reviewed changes

genmc-sys/LICENSE Outdated

Copy link

Contributor Author

Patrick-6 Jul 25, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

FWIU, this file is required too for the GPL license

run fmt

5cc2046

Patrick-6 commented Jul 25, 2025

View reviewed changes

genmc-sys/Cargo.toml Show resolved Hide resolved

	edition = "2024"
	edition = "2024"
	license = "GPL-3.0-or-later"

Implement building GenMC C++ code #4453

Are you sure you want to change the base?

Implement building GenMC C++ code #4453

Conversation

Patrick-6 commented Jul 7, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

RalfJung commented Jul 9, 2025

Uh oh!

rustbot commented Jul 9, 2025

Uh oh!

Patrick-6 commented Jul 9, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

RalfJung commented Jul 11, 2025

Uh oh!

Patrick-6 commented Jul 12, 2025

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

RalfJung commented Jul 14, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

RalfJung commented Jul 14, 2025 via email

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Patrick-6 Jul 23, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Patrick-6 Jul 23, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Patrick-6 Jul 23, 2025 •

edited

Loading

Patrick-6 Jul 23, 2025 •

edited

Loading

Patrick-6 Jul 24, 2025 •

edited

Loading