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.

- Add genmc-sys crate for building GenMC C++ code. - Implemented program features: - Handling of atomic loads, stores, allocations and deallocations. - Implement consistent address allocations for globals - Non-global addresses allocated by GenMC. - Limitation: No address randomization. - Limitation: No address reuse. - Handling of non-atomic memory accesses. - Limitation: need to split up NA reads and stores into max 8 byte chunks. - Limitation: no mixed size access support. - Limitation: Incomplete (unsound) handling of uninitialized memory. - Implement Pointer conversions to and from GenMC - Limitation: Aliasing model checking must be disabled. - Handling of Read-Modify-Write, Compare-Exchange and Atomic Exchange operations. - Limitation: Compare-Exchange currently ignores possibility of spurious failures. - Limitation: Compare-Exchange failure memory ordering is ignored. - Handling of thread creation and finishing. - Added Miri to GenMC thread id mapping. - Implement mutex lock, try_lock and unlock. - Make use of annotations to reduce number of blocked executions for programs with mutexes. - Add estimation mode for Miri-GenMC. - Limitation: Printing currently handled on C++ side (Should be moved once VerificationResult is available to Rust code) - Thread scheduling in Miri done through GenMC, add loop over eval_entry function. - Rebase GenMC to use new scheduler. - Added GenMC `__VERIFIER_assume` equivalent for Miri (`miri_genmc_verifier_assume`) - Add warnings for GenMC mode for unsupported features. - Add a lot of test, including translation of GenMC litmus tests. - Only run tests if 'genmc' feature enabled. - WIP: try implementing NonNullUniquePtr wrapper for CXX. - WIP: work on mixed atomic/non-atomics. - Partially working, some issues with globals - FIX: Make naming consistent with GenMC for blocked execution - Add git support to build, move C++ files into genmc-sys crate - Implement building GenMC-Miri after GenMC codebase split. - WIP: temporarily point GenMC repo to private branch.

…ild.

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

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

…itions.

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

Patrick-6 · 2025-07-13T21:24:31Z

genmc-sys/build.rs

+    // 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");
+
+    config.build_target(GENMC_MODEL_CHECKER);
+    let _dst = config.build();
+
+    let genmc_model_checker_build_directory = genmc_build_path.join(GENMC_MODEL_CHECKER);
+    println!("cargo::rustc-link-search=native={}", genmc_model_checker_build_directory.display());
+    println!("cargo::rustc-link-lib=static={GENMC_MODEL_CHECKER}");
+
+    genmc_build_path


I'm not quite happy with this code yet:

The Hack at the top seems to be required for building on older Ubuntu, which isn't relevant yet for Miri's CI, but might be if this should build in rustc's CI (or someone tries to compile Miri-GenMC on an older OS).

I suspect it's due to version differences with the older cmake that's installed there, possibly an edge case that's not handled by the cmake crate. We can either leave it as is or try to investigate further.

The "build" path extension seems to be undocumented by the cmake crate (it is added here), so it might not be a good idea to depend on that.

This might be unlikely to change, especially since the cmake crate lives in the rust-lang Github project too.

We may be able to use the return value (_dst) from config.build() instead (which should be the install directory), but I haven't yet figured out why the produced model_checker library is not in that directory. I'll have to investigate this further.

As discussed, I've switched to using a config.h file instead of compile definitions. This config file lives in the build directory (at {genmc_build_path}/config.h), which is then included in the cxx_bridge build step (That's why we return that path here).
With this config.h, no more manual settings syncing is required.

What is that -B flag and why is setting it a hack?

If the cmake crate currently provides no way of getting the build dir, then maybe open an issue to ask for such an API, and reference it here?

The -B flags sets the build directory, which I would expect to be taken care of automatically by the cmake crate. When I tested it on Ubuntu 22.04, the first of the two cmake command invocation used the wrong directory without this (first invocation is a configure step, the second invocation is the actual build).
The difference between the OSes makes me think this is not intended behavior, maybe I should make a bug report for that too.

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

Patrick-6 · 2025-07-13T21:47:10Z

genmc-sys/build.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";


Reminder to discuss this with Michalis before merging since the original comment is now marked as outdated.

What is the default used by GenMC itself?

Profile: RelWithDebInfo (with -O2 -g)
GENMC_DEBUG: OFF

We should do the same then for release builds. For debug builds it'd make sense to set GENMC_DEBUG to On.

I can't find any way for the build script to even detect if debug_assertions is enabled.
In the list of env vars set for a build script, there is only:

DEBUG, which I assume is whether or not debug info is included (assuming it matches the "debug" in Cargo.toml)

PROFILE, which I don't think will help us much for Miri since IIRC miri-script never uses --release anyway (?)

I can't really imagine that we are the first who would like to know if debug assertions are enabled from a build script, so I might be missing something here.

PROFILE, which I don't think will help us much for Miri since IIRC miri-script never uses --release anyway (?)

./miri install uses --release, as does the dist build.
So if debug_assertions cannot be checked (I didn't find a way either) I think PROFILE is exactly what you should check.

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?

…or checking supported targets.

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.

RalfJung · 2025-07-16T09:13:30Z

genmc-sys/build.rs

+
+    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/";


For all these paths it'd be good to know what they are relative to.^^

RalfJung · 2025-07-16T09:39:45Z

genmc-sys/build.rs

+
+    // Build all required components:
+    let genmc_install_dir = build_genmc_model_checker(&genmc_path);
+    build_cxx_bridge(&genmc_path, &genmc_install_dir);


This should only use genmc_install_dir since the headers should also be installed.

Patrick-6 added 5 commits July 7, 2025 09:52

Miri-GenMC build PR: Clear out tests directory

86ce52a

Miri-GenMC build PR: Reduce code changes to minimum needed to test bu…

0d45dbd

…ild.

Small cleanup, disable genmc feature by default

c058b1d

Update linked GenMC git commit

d53d4b9

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 added 3 commits July 7, 2025 13:55

Update linked GenMC git commit again

00671fa

Update linked GenMC git commit again 2

28b9640

Switch terms: 'vendoring' --> 'downloading'

04102b2

Patrick-6 commented Jul 7, 2025

View reviewed changes

genmc-sys/build.rs 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 added 2 commits July 8, 2025 10:18

Disable unsupported platforms.

9d425a3

WIP: Temporarily patch cxx crate to debug MacOS failure.

8c0109f

Patrick-6 commented Jul 8, 2025

View reviewed changes

genmc-sys/src_cpp/MiriInterface.hpp 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

Patrick-6 added 7 commits July 9, 2025 14:37

Undo patching cxx crate.

ca46c21

Throw an error when the downloaded GenMC repo is modified.

b5c532a

Update rebuild-if-changed paths

943c44e

Disable unused crate feature

d1328d9

Remove comment, run formatter

8baec72

Disable MacOS support.

232faa8

Run fmt

2839dc4

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

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 added 5 commits July 12, 2025 10:20

Disable cross-platform testing with GenMC.

c914943

Clean up GenMC config handling.

9472c19

Set genmc-sys version to 0.1.0

34d1e92

Improve build script output

5cfc8b4

Remove '_STR' from string constants.

27a81f4

Patrick-6 and others added 3 commits July 13, 2025 12:46

Rework GenMC git repo handling

a8bfb1a

Switch to using configuration file for GenMC instead of compile defin…

5c83f12

…itions.

Apply suggestions from code review

29a03c5

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

Patrick-6 commented Jul 13, 2025

View reviewed changes

RalfJung reviewed Jul 14, 2025

View reviewed changes

Patrick-6 added 4 commits July 14, 2025 14:50

Improve include directory handling with cmake

34f67f7

Remove 'doc/' from .gitignore

91146ce

Add little endian to supported platform conditions, add extra FIXME f…

a7b8597

…or checking supported targets.

Switch to using panic! for error handling in build script

fb33c77

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

Patrick-6 added 2 commits July 14, 2025 15:49

Only check local GenMC repo path for changes if it exists

570a069

Remove extra string in print.

e9f3c8a

Patrick-6 added 3 commits July 14, 2025 21:36

Add warning for enabled borrow tracking in GenMC mode

b4fb84f

WIP: Add documentation for GenMC mode usage and development.

e252faa

Run fmt.

4adb4bc

RalfJung reviewed Jul 16, 2025

View reviewed changes

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!

RalfJung commented Jul 11, 2025

Uh oh!

Patrick-6 commented Jul 12, 2025

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!

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!

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!

RalfJung Jul 14, 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!

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!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

RalfJung Jul 14, 2025 •

edited

Loading