Skip to content

Implement building GenMC C++ code #4453

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 64 commits into from

Conversation

Patrick-6
Copy link
Contributor

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.

@RalfJung
Copy link
Member

RalfJung commented Jul 9, 2025

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

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

rustbot commented Jul 9, 2025

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

@Patrick-6
Copy link
Contributor Author

@rustbot ready

@rustbot 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
@RalfJung
Copy link
Member

Here's my first round of comments. :)

@rustbot author

@rustbot 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
Copy link
Contributor Author

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..

// 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}");
Copy link
Contributor Author

Choose a reason for hiding this comment

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

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?

Copy link
Member

Choose a reason for hiding this comment

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

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

Copy link
Contributor Author

Choose a reason for hiding this comment

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

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.

Copy link
Member

Choose a reason for hiding this comment

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

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.

Copy link
Member

Choose a reason for hiding this comment

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

@RalfJung
Copy link
Member

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.

// 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}");
Copy link
Member

Choose a reason for hiding this comment

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

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

@RalfJung
Copy link
Member

RalfJung commented Jul 14, 2025 via email

@Patrick-6
Copy link
Contributor Author

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

@rustbot 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
Copy link
Member

Thanks!

It's probably easiest for me to just do the remaining changes directly instead of you trying to read my mind. Usually I would just push that to your branch, but unfortunately you have disabled the setting that would let me do that. So I had to make a new PR instead: #4498. Please go through the 2nd commit there to see what I changed.

@RalfJung RalfJung closed this Jul 27, 2025
@rustbot rustbot removed the S-waiting-on-review Status: Waiting for a review to complete label Jul 27, 2025
Copy link
Member

Choose a reason for hiding this comment

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

I have drastically shortened these docs since they should explain the interface o how to build and work with Miri-GenMC, not all the implementation details.

@@ -677,8 +677,6 @@ trait EvalContextPrivExt<'tcx>: MiriInterpCxExt<'tcx> {
fn run_on_stack_empty(&mut self) -> InterpResult<'tcx, Poll<()>> {
let this = self.eval_context_mut();
// Inform GenMC that a thread has finished all user code. GenMC needs to know this for scheduling.
// FIXME(GenMC): Thread-local destructors *are* user code, so this is odd. Also now that we
// support pre-main constructors, it can get called there as well.
Copy link
Member

Choose a reason for hiding this comment

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

Why did you remove this comment? It is still correct, AFAIK.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants