Rust and LLVM issues

Hi, thanks for the publications and the GenMC tool. I'm working on a medium/large Rust project and want to use GenMC to check parts of it. Specifically, I want to isolate where we get clever with atomics into modules that are well-tested, or at least have some reference examples demonstrating correct patterns. It's these modules that I'd like to check with GenMC, since checking the overall project would be impractical.

I tried to set up and use GenMC but encountered a lot of difficulty. As you'll see I was more persistent than the typical user. I hacked through some of it, but so far I have failed to check a basic example in Rust. I want to share what I learned in case it helps others and in case that's useful to the maintainer(s). It seems like GenMC might be close to practical for Rust but really needs some love.

BTW, I think my best alternative for Rust is [Loom](https://github.com/tokio-rs/loom), which is based on [CDSchecker](https://dl.acm.org/doi/10.1145/2544173.2509514)'s approach. It's relatively easy to run as part of a Rust unit test suite (for thread-based examples). However, it currently has [significant limitations](https://github.com/tokio-rs/loom#unsupported-features) in its modeling.

## Building LLVM 22

The first issue I encountered was needing a newer version of LLVM. We use Rust's latest stable release (1.95), which uses LLVM 22.

Alternatives:

- I should have used an older version of Rust, which would have been a smarter way to get started. Our project uses features introduced in 1.95, however.
- Maybe I could have gotten away with LLVM 21 from Debian's trixie-backports repo, but I built LLVM from source instead.

I figured I might as well use the same LLVM release as Rust, so I got the source from:

```sh
git clone --branch 'rustc/22.1-2026-03-22' --depth 1 \
    https://github.com/rust-lang/llvm-project.git llvm
```

And ultimately built it like this:

```sh
cmake \
    -B build \
    -DCMAKE_INSTALL_PREFIX=~/opt/llvm \
    -DCMAKE_BUILD_TYPE=Release \
    -DLLVM_BUILD_LLVM_DYLIB=On \
    -DLLVM_ENABLE_PROJECTS='clang' \
    -DLLVM_ENABLE_RTTI=On \
    -DLLVM_USE_LINKER=lld \
    -DLLVM_TARGETS_TO_BUILD='AArch64;X86' \
    -G Ninja \
    -S llvm
cmake --build build --target install
```

Notes:

- I enabled `lld` and restricted the target architectures just to speed up the build a little.
- I think I needed to enable the `clang` subproject.
- `DLLVM_BUILD_LLVM_DYLIB=On` is needed to emit a `libLLVM.so`, which GenMC needs.
- The [RTTI](https://en.wikipedia.org/wiki/Run-time_type_information) setting fixed a bunch of linker errors like:

  ```
  undefined reference to `typeinfo for llvm::CallbackVH'
  ```

  Thanks for this [15-year old StackOverflow comment](https://stackoverflow.com/questions/307352/g-undefined-reference-to-typeinfo/4184877#4184877) for this one. I think GenMC needs RTTI for a `dynamic_cast`.


## Updating GenMC for LLVM 22

I hacked this up to work for LLVM 22, but I assume you need `#ifdef`s to keep compatibility accross LLVM releases. I'm not familiar with LLVM, so I may have done the wrong things here.

The `PassPlugin.h` header file moved (5 occurrences):

```diff
-#include <llvm/Passes/PassPlugin.h>
+#include <llvm/Plugins/PassPlugin.h>
```

I'm not sure what changed here, but I gave it an empty array ref instead of a null one:

```diff
diff --git a/lli/Runtime/Interpreter.cpp b/lli/Runtime/Interpreter.cpp
index 3cabc7ad7c..3da16ce18e 100644
--- a/lli/Runtime/Interpreter.cpp
+++ b/lli/Runtime/Interpreter.cpp
@@ -480,11 +480,7 @@
                // Setup the ctor/dtor SF and quit
                if (Function *F = dyn_cast<Function>(FP))
                        setupFunctionCall(F,
-#if LLVM_VERSION_MAJOR >= 16
-                                         std::nullopt
-#else
-                                         None
-#endif
+                                         ArrayRef<GenericValue>()
                        );

                // FIXME: It is marginally lame that we just do nothing here if we see an
```

I think the debug instructions were removed:

```diff
diff --git a/passes/passes/Transforms/EliminateCastsPass.cpp b/passes/passes/Transforms/EliminateCastsPass.cpp
index 5e33aaaa4b..3ff07df1f5 100644
--- a/passes/passes/Transforms/EliminateCastsPass.cpp
+++ b/passes/passes/Transforms/EliminateCastsPass.cpp
@@ -401,7 +401,7 @@
                        li->mutateType(ai->getAllocatedType());
                        auto opc = CastInst::getCastOpcode(li, false, prevType, false);
                        auto *res = CastInst::Create(opc, li, prevType, "",
-                                                    li->getNextNonDebugInstruction());
+                                                    li->getNextNode());
                        replaceUsesWithIf(li, res, [&](Use &u) {
                                auto *us = dyn_cast<Instruction>(u.getUser());
                                return us && us != res;
```

The `GlobalValue::getGlobalIdentifier()` method without arguments was made private. Under the hood, it does what I've done here:

```diff
diff --git a/passes/passes/Transforms/RustPrepPass.cpp b/passes/passes/Transforms/RustPrepPass.cpp
index 35bfd960cc..41fe43d242 100644
--- a/passes/passes/Transforms/RustPrepPass.cpp
+++ b/passes/passes/Transforms/RustPrepPass.cpp
@@ -177,7 +177,11 @@
                if (!calledF) // Skip indirect function calls
                        continue;

-               std::string fName = calledF->getGlobalIdentifier();
+               std::string fName = GlobalValue::getGlobalIdentifier(
+                       calledF->getName(),
+                       calledF->getLinkage(),
+                       calledF->getParent()->getSourceFileName()
+               );
                if ("__rust_alloc" == fName) {
                        CI->setCalledFunction(genmc__rust_alloc);
                        modified = true;
```

## Building GenMC itself

There are already instructions for building GenMC, but here's what I did:

```sh
cmake \
    -B RelWithDebInfo \
    -DCMAKE_BUILD_TYPE=RelWithDebInfo \
    -DCMAKE_EXPORT_COMPILE_COMMANDS=ON \
    -DCMAKE_INSTALL_PREFIX=~/opt/genmc \
    -DCMAKE_PREFIX_PATH='~/opt/llvm/lib/cmake;~/path/to/.local/rustup/toolchains/1.95-x86_64-unknown-linux-gnu/bin' \
    -DENABLE_RUST=ON \
    -DLLVM_TOOLS_BINARY_DIR='~/opt/llvm/bin' \
    -G Ninja \
    -S .
cmake --build RelWithDebInfo
ln -fs ~/w/genmc/RelWithDebInfo/bin/genmc ~/bin/
```

Notes:
- Probably the build directory name could be simpler like `build`.
- I used `-DCMAKE_EXPORT_COMPILE_COMMANDS=ON` to generate a `compile_commands.json` in the build directory. Then I pointed clangd with it in VS Code with:

  ```json
  "clangd.arguments": [
      "--compile-commands-dir=RelWithDebInfo"
  ]
  ```

  This enabled some more features in VS Code with the `llvm-vs-code-extensions.vscode-clangd` extension.
- I used Ninja to get parallelism in the build.
- The install target didn't end up working out because of the library search path, but a symlink into the build directory did seem to work.

## Runing a C example

I ran the `mp.c` example, which passed. I introduced a bug and reran it, and I got nice output. I want this for Rust!

## Running a `main.rs` hello world

Here's a very simple Rust program:

```rust
fn main() {
    println!("hello world");
}
```

I got:

```console
$ genmc ./main.rs
terminate called after throwing an instance of 'std::filesystem::__cxx11::filesystem_error'
  what():  filesystem error: cannot set current path: No such file or directory
```

```console
$ strace -f --detach-on=execve --string-limit=10000 -e quiet=attach,exit genmc ./main.rs
[...snip...]
getcwd("/home/diego/w/genmc-test/src", 4096) = 29
chdir("/home/diego/w/genmc/lli/runtime-include/rust/genmc-std") = -1 ENOENT (No such file or directory)
futex(0x7f7bf8391230, FUTEX_WAKE_PRIVATE, 2147483647) = 0
write(2, "terminate called after throwing an instance of '", 48terminate called after throwing an instance of ') = 48
write(2, "std::filesystem::__cxx11::filesystem_error", 42std::filesystem::__cxx11::filesystem_error) = 42
[...snip...]
```

There's an `rust` directory within the `rust` directory now (why?), so that path needs to change:

```diff
diff --git a/lli/main.cpp b/lli/main.cpp
index d7e0e00884..c07ae27b1e 100644
--- a/lli/main.cpp
+++ b/lli/main.cpp
@@ -606,14 +606,14 @@
        auto rustcPath = std::string(RUSTC_PATH);
        auto cargoPath = std::string(CARGO_PATH);

-       std::filesystem::path pathGenmcStd(std::string(RUST_DIR) + "/genmc-std");
+       std::filesystem::path pathGenmcStd(std::string(RUST_DIR) + "/rust/genmc-std");
        std::filesystem::path pathDebug = pathGenmcStd / "target" / "debug";
        std::filesystem::path pathRlib = pathDebug / "libgenmc_std.rlib";

        /* Build genmc-std, skip if a build exists that we're allowed to use */
        bool skipBuild = lliConfig.skipGenmcStdBuild && std::filesystem::exists(pathRlib);
        bool buildSuccessful =
-               buildCargoProject(cargoPath, RUST_DIR + std::string("/genmc-std"), skipBuild);
+               buildCargoProject(cargoPath, pathGenmcStd, skipBuild);
        if (!buildSuccessful)
                return false;
```

This almost works now, except for my poor choice of example program:

```console
$ genmc ./main.rs
[...snip...]
GenMC v0.17.0 (LLVM 22.1.4)
Copyright (C) 2024 MPI-SWS. All rights reserved.

*** Compilation complete.
WARNING: Cannot promote non-constant-length mem intrinsic! Skipping...

*** Transformation complete.
Tip: Estimating state-space size before verification. For better performance, you can use --disable-estimation.
ERROR: Tried to execute an unknown external function: _RNvNtNtCsjrHSEGnQ3l9_3std2io5stdio6__print
Command exited with status 17
```

I changed the print statement to an `assert!(true);`, and it succeeds.

## Running an assertion in `main.rs`

Let's try something more complicated:

```rust
use std::sync::atomic::{AtomicU64, Ordering};

fn main() {
    let v = AtomicU64::new(0);
    v.fetch_add(1, Ordering::Relaxed);
    v.fetch_add(1, Ordering::Relaxed);
    let r = v.load(Ordering::Relaxed);
    assert_eq!(2, r);
}
```

This works!

If I change the `assert_eq!` to the wrong value (like `3`), it fails, just more spectacularly than it should:

```
ERROR: Tried to execute an unknown external function: _RINvNtCsgEmfK2I1SDS_4core9panicking13assert_failedyyEB4_
```

Normal `panic!`s and `std::panic::panic_any` have similar issues.

## Spawning a thread in `main.rs`

This is as simple as multi-threaded programs get:

```rust
use std::thread;

fn main() {
    let t = thread::spawn(|| {
        // do nothing
    });
    t.join().unwrap();
}
```

And it didn't work:

```
$ genmc ./main.rs
[...snip...]
ERROR: Tried to execute an unknown external function: _RNvCsfLfy6EI15iL_7___rustc35___rust_no_alloc_shim_is_unstable_v2
```

## Running a Cargo project

Most Rust projects use Cargo and have dependencies. That's what I actually want to use, and maybe it'll help the situation by being more explicit about the `genmc-std` location.

I created this `Cargo.toml` file:

```toml
[package]
name = "genmc-test"
edition = "2024"
version = "0.0.1"

[dependencies]
std = { path = '/home/diego/w/genmc/lli/runtime-include/rust/rust/genmc-std', package = 'genmc-std'}
```

And this `src/main.rs` file:

```rust
fn main() {
    assert!(true);
}
```

And `cargo run` works.

`genmc` fails with the path given as `Cargo.toml`:

```console
$ genmc Cargo.toml
terminate called after throwing an instance of 'std::filesystem::__cxx11::filesystem_error'
  what():  filesystem error: cannot set current path: No such file or directory
```

```console
$ strace -f --detach-on=execve --string-limit=10000 -e quiet=attach,exit genmc Cargo.toml
[...snip...]
getcwd("/home/diego/w/genmc-test", 4096) = 25
getcwd("/home/diego/w/genmc-test", 4096) = 25
chdir("")                               = -1 ENOENT (No such file or directory)
futex(0x7ff2cfa13230, FUTEX_WAKE_PRIVATE, 2147483647) = 0
write(2, "terminate called after throwing an instance of '", 48terminate called after throwing an instance of ') = 48
[...snip...]
```

`genmc` accepts the path given as `./Cargo.toml` and succeeds.

## Spawning a thread in a Cargo project

I changed the `main.rs` file to the above `spawn-join` example. Now nothing works.

`cargo run` fails:

```console
$ RUST_BACKTRACE=1 cargo run
[...snip...]

thread 'main' (4052492) panicked at /path/to/.local/rustup/toolchains/stable-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/unique.rs:89:36:
unsafe precondition(s) violated: NonNull::new_unchecked requires that the pointer is non-null

This indicates a bug in the program. This Undefined Behavior check is optional, and cannot be relied on for safety.
stack backtrace:
[...snip...]
   3: core::ptr::non_null::NonNull<T>::new_unchecked::precondition_check
             at /path/to/.local/rustup/toolchains/stable-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ub_checks.rs:73:21
   4: new_unchecked<()>
             at /path/to/.local/rustup/toolchains/stable-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ub_checks.rs:78:17
   5: new_unchecked<()>
             at /path/to/.local/rustup/toolchains/stable-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/unique.rs:89:36
   6: from_raw_in<(), alloc::alloc::Global>
             at /path/to/.local/rustup/toolchains/stable-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/boxed.rs:1527:22
   7: from_raw<()>
             at /path/to/.local/rustup/toolchains/stable-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/boxed.rs:1300:18
   8: genmc_std::thread::JoinInner<T>::join_keep
             at /home/diego/w/genmc/lli/runtime-include/rust/rust/genmc-std/src/thread/mod.rs:46:19
   9: genmc_std::thread::JoinInner<T>::join
             at /home/diego/w/genmc/lli/runtime-include/rust/rust/genmc-std/src/thread/mod.rs:35:23
  10: genmc_std::thread::JoinHandle<T>::join
             at /home/diego/w/genmc/lli/runtime-include/rust/rust/genmc-std/src/thread/mod.rs:56:16
  11: main
[...snip...]
```

`genmc` fails:

```console
$ genmc ./Cargo.toml
[...snip...]
ERROR: Tried to execute an unknown external function: _RNvCsfLfy6EI15iL_7___rustc35___rust_no_alloc_shim_is_unstable_v2
```

## An older Rust

I've surely gotten ahead of the Rust version that GenMC currently supports, so let me try an older one. I picked Rust 1.71 as it's the MSRV for [Tokio](https://github.com/tokio-rs/tokio#supported-rust-versions), which has synchronization primitives we'll need to involve in our tests. It's also not much newer than the [1.69.0 version in the GenMC `README.md` example](https://github.com/MPI-SWS/genmc#enabling-rust-support-experimental).

I reduced the `edition` to 2021 in `Cargo.toml` and put this in `rust-toolchain.toml`:

```toml
[toolchain]
channel = "1.71"
```

Note: Rust 1.71.1 uses LLVM 16.0.5, but I'll stick with my LLVM 22 for the moment. I don't think this matters yet.

The thread spawn-join example works with `cargo run` but not with `genmc`:

```console
$ genmc ./Cargo.toml
[...snip...]
error: the `-Z unstable-options` flag must also be passed to enable the flag `check-cfg`

error: could not compile `genmc-test` (bin "genmc-test")

Caused by:
  process didn't exit successfully: `rustc --crate-name genmc_test --edition=2021 src/main.rs --error-format=json --json=diagnostic-rendered-ansi,artifacts,future-incompat --diagnostic-width=203 --crate-type bin --emit=dep-info,link -C embed-bitcode=no -C debuginfo=line-tables-only --check-cfg 'cfg(docsrs,test)' --check-cfg 'cfg(feature, values())' -C metadata=1842548526d09be9 -C extra-filename=-ca3cda01f63f0505 --out-dir /home/diego/w/genmc-test/target/debug/deps -C incremental=/home/diego/w/genmc-test/target/debug/incremental -L dependency=/home/diego/w/genmc-test/target/debug/deps --extern std=/home/diego/w/genmc-test/target/debug/deps/libgenmc_std-2c0f2ba260ed04ee.rlib --emit=llvm-bc` (exit status: 1)
[...snip...]
```

I got the same issue with Rust 1.69 and Rust 1.75. I think [1.79 stabilized rustc's `--check-cfg`](https://releases.rs/docs/1.79.0/).

The behavior is indeed different with Rust 1.79. `cargo run` fails with the `NonNull` check we saw earlier, and GenMC fails to build for new reasons:

```console
$ cargo clean; genmc ./Cargo.toml
[...snip...]
   Compiling genmc-test v0.0.1 (/home/diego/w/genmc-test)
error[E0514]: found crate `std` compiled by an incompatible version of rustc
  |
  = note: the following crate versions were found:
          crate `std` compiled by <unknown rustc version>: /home/diego/w/genmc-test/target/debug/deps/libgenmc_std-0f0eba7641a7b118.rlib
  = help: please recompile that crate using this compiler (rustc 1.79.0 (129f3b996 2024-06-10)) (consider running `cargo clean` first)

error[E0514]: found crate `std` compiled by an incompatible version of rustc
 --> src/main.rs:2:5
  |
2 | use std::thread;
  |     ^^^
  |
  = note: the following crate versions were found:
          crate `std` compiled by <unknown rustc version>: /home/diego/w/genmc-test/target/debug/deps/libgenmc_std-0f0eba7641a7b118.rlib
  = help: please recompile that crate using this compiler (rustc 1.79.0 (129f3b996 2024-06-10)) (consider running `cargo clean` first)

error: `#[panic_handler]` function required, but not found

error: unwinding panics are not supported without std
  |
  = help: using nightly cargo, use -Zbuild-std with panic="abort" to avoid unwinding
  = note: since the core library is usually precompiled with panic="unwind", rebuilding your crate with panic="abort" may not be enough to fix the problem

error: requires `sized` lang_item
[...snip...]
```

Running `genmc` with `main.rs` (without Cargo) gives the earlier error:

```
ERROR: Tried to execute an unknown external function: _RNvCsfLfy6EI15iL_7___rustc35___rust_no_alloc_shim_is_unstable_v2
```

I can't be sure, but it doesn't seem like these issues would be a result of using LLVM 22.

## Rust project integration

To truly integrate this into our project workflow, including CI, I'd like to be able to run GenMC on a subset of (potentially custom-purpose) unit tests. There are a few challenges to this. Currently, GenMC runs only the `main` function AFAICT. It'd be nice if it could run a different function from compiling a unit test target, and then even better if it could integrate with a test running harness.

Like many medium/large Rust projects, ours has many packages within a Cargo workspace. Currently, `GenMC` assumes that the `Cargo.toml` file is a top-level one, and that the `target` directory will appear next to it. GenMC would also need to support the Rust release used to build the entire workspace, which for us is currently Rust 1.95.

One place to look for inspiration is the [Miri](https://github.com/rust-lang/miri) project. It's a cargo plugin (which is mostly a naming convention) that allows running tests, including with [cargo-nextest](https://nexte.st/) (which we use).

## Misc

- These are missing from `.gitignore`:
  - `lli/runtime-include/rust/rust/genmc-std/Cargo.lock`
  - `lli/runtime-include/rust/rust/genmc-std/target/`

- These 7 warnings are annoying:

  ```
  warning: `#[inline]` is ignored on externally exported functions
     --> src/genmc.rs:160:1
      |
  160 | #[inline(always)]
      | ^^^^^^^^^^^^^^^^^
      |
      = help: externally exported functions are functions with `#[no_mangle]`, `#[export_name]`, or `#[linkage]`
  ```

- The default edition when compiling with `rustc` is 2015, which is quite out of date now. It'd be better to set `--edition=2021` or `--edition=2024` when compiling loose `.rs` files. I ran into this papercut when copying an example that used format arguments inside a panic macro, which were [added in the 2021 edition](https://doc.rust-lang.org/edition-guide/rust-2021/panic-macro-consistency.html). Later editions require more recent Rust versions:
  - Rust 1.56 (Oct. 2021) is required for the 2021 edition.
  - Rust 1.85 (Feb. 2025) is required for the 2024 edition.

## Closing remarks

I'll admit, this has been disappointing and is a showstopper for me for now. However, I think these are all integration issues that aren't fundamental to the design of the tool (at least if we accept that we need a rustc-compatible LLVM). What I mean is, I think these issues are probably pretty resolvable without major changes, so I retain some hope. I'll try to give GenMC another try once these are patched up, and I still hope to be able to integrate it into our project someday soon.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Rust and LLVM issues #71

Building LLVM 22

Updating GenMC for LLVM 22

Building GenMC itself

Runing a C example

Running a `main.rs` hello world

Running an assertion in `main.rs`

Spawning a thread in `main.rs`

Running a Cargo project

Spawning a thread in a Cargo project

An older Rust

Rust project integration

Misc

Closing remarks

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Rust and LLVM issues #71

Description

Building LLVM 22

Updating GenMC for LLVM 22

Building GenMC itself

Runing a C example

Running a main.rs hello world

Running an assertion in main.rs

Spawning a thread in main.rs

Running a Cargo project

Spawning a thread in a Cargo project

An older Rust

Rust project integration

Misc

Closing remarks

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions

Running a `main.rs` hello world

Running an assertion in `main.rs`

Spawning a thread in `main.rs`