From 545f39ea457ff0749a1758a44ab6893ec37126ae Mon Sep 17 00:00:00 2001 From: Michalis Kokologiannakis Date: Fri, 14 Nov 2025 19:47:33 +0100 Subject: [PATCH 1/5] genmc/build: Drop LLVM dependency from build GenMC (v0.14.1) no longer depends on LLVM when built as a library. This commit adjust genmc building and shim accordingly. --- genmc-sys/build.rs | 58 +----------------------- genmc-sys/cpp/include/ResultHandling.hpp | 8 ++-- 2 files changed, 6 insertions(+), 60 deletions(-) diff --git a/genmc-sys/build.rs b/genmc-sys/build.rs index 1b4e064d1b..d3f81fa1d7 100644 --- a/genmc-sys/build.rs +++ b/genmc-sys/build.rs @@ -140,51 +140,6 @@ mod downloading { } } -// FIXME(genmc,llvm): Remove once the LLVM dependency of the GenMC model checker is removed. -/// The linked LLVM version is in the generated `config.h`` file, which we parse and use to link to LLVM. -/// Returns c++ compiler definitions required for building with/including LLVM, and the include path for LLVM headers. -fn link_to_llvm(config_file: &Path) -> (String, String) { - /// Search a string for a line matching `//@VARIABLE_NAME: VARIABLE CONTENT` - fn extract_value<'a>(input: &'a str, name: &str) -> Option<&'a str> { - input - .lines() - .find_map(|line| line.strip_prefix("//@")?.strip_prefix(name)?.strip_prefix(": ")) - } - - let file_content = std::fs::read_to_string(&config_file).unwrap_or_else(|err| { - panic!("GenMC config file ({}) should exist, but got errror {err:?}", config_file.display()) - }); - - let llvm_definitions = extract_value(&file_content, "LLVM_DEFINITIONS") - .expect("Config file should contain LLVM_DEFINITIONS"); - let llvm_include_dirs = extract_value(&file_content, "LLVM_INCLUDE_DIRS") - .expect("Config file should contain LLVM_INCLUDE_DIRS"); - let llvm_library_dir = extract_value(&file_content, "LLVM_LIBRARY_DIR") - .expect("Config file should contain LLVM_LIBRARY_DIR"); - let llvm_config_path = extract_value(&file_content, "LLVM_CONFIG_PATH") - .expect("Config file should contain LLVM_CONFIG_PATH"); - - // Add linker search path. - let lib_dir = PathBuf::from_str(llvm_library_dir).unwrap(); - println!("cargo::rustc-link-search=native={}", lib_dir.display()); - - // Add libraries to link. - let output = std::process::Command::new(llvm_config_path) - .arg("--libs") // Print the libraries to link to (space-separated list) - .output() - .expect("failed to execute llvm-config"); - let llvm_link_libs = - String::try_from(output.stdout).expect("llvm-config output should be a valid string"); - - for link_lib in llvm_link_libs.trim().split(" ") { - let link_lib = - link_lib.strip_prefix("-l").expect("Linker parameter should start with \"-l\""); - println!("cargo::rustc-link-lib=dylib={link_lib}"); - } - - (llvm_definitions.to_string(), llvm_include_dirs.to_string()) -} - /// Build the GenMC model checker library and the Rust-C++ interop library with cxx.rs fn compile_cpp_dependencies(genmc_path: &Path, always_configure: bool) { // Give each step a separate build directory to prevent interference. @@ -204,6 +159,7 @@ fn compile_cpp_dependencies(genmc_path: &Path, always_configure: bool) { .always_configure(always_configure) // We force running the configure step when the GenMC commit changed. .out_dir(genmc_build_dir) .profile(GENMC_CMAKE_PROFILE) + .define("BUILD_LLI", "OFF") .define("GENMC_DEBUG", if enable_genmc_debug { "ON" } else { "OFF" }); // The actual compilation happens here: @@ -214,19 +170,11 @@ fn compile_cpp_dependencies(genmc_path: &Path, always_configure: bool) { println!("cargo::rustc-link-search=native={}", cmake_lib_dir.display()); println!("cargo::rustc-link-lib=static={GENMC_MODEL_CHECKER}"); - // FIXME(genmc,llvm): Remove once the LLVM dependency of the GenMC model checker is removed. - let config_file = genmc_install_dir.join("include").join("genmc").join("config.h"); - let (llvm_definitions, llvm_include_dirs) = link_to_llvm(&config_file); - // Part 2: // Compile the cxx_bridge (the link between the Rust and C++ code). let genmc_include_dir = genmc_install_dir.join("include").join("genmc"); - // FIXME(genmc,llvm): remove once LLVM dependency is removed. - // These definitions are parsed into a cmake list and then printed to the config.h file, so they are ';' separated. - let definitions = llvm_definitions.split(";"); - // These are all the C++ files we need to compile, which needs to be updated if more C++ files are added to Miri. // We use absolute paths since relative paths can confuse IDEs when attempting to go-to-source on a path in a compiler error. let cpp_files_base_path = Path::new("cpp/src/"); @@ -244,16 +192,12 @@ fn compile_cpp_dependencies(genmc_path: &Path, always_configure: bool) { if enable_genmc_debug { bridge.define("ENABLE_GENMC_DEBUG", None); } - for definition in definitions { - bridge.flag(definition); - } bridge .opt_level(2) .debug(true) // Same settings that GenMC uses (default for cmake `RelWithDebInfo`) .warnings(false) // NOTE: enabling this produces a lot of warnings. .std("c++23") .include(genmc_include_dir) - .include(llvm_include_dirs) .include("./cpp/include") .files(&cpp_files) .out_dir(interface_build_dir) diff --git a/genmc-sys/cpp/include/ResultHandling.hpp b/genmc-sys/cpp/include/ResultHandling.hpp index 189f32e6f5..cb5f49c179 100644 --- a/genmc-sys/cpp/include/ResultHandling.hpp +++ b/genmc-sys/cpp/include/ResultHandling.hpp @@ -7,14 +7,16 @@ // GenMC headers: #include "Verification/VerificationError.hpp" +#include +#include +#include #include /** Information about an error, formatted as a string to avoid having to share an error enum and * printing functionality with the Rust side. */ static auto format_error(VerificationError err) -> std::unique_ptr { - auto buf = std::string(); - auto s = llvm::raw_string_ostream(buf); - s << err; + std::stringstream s; + s << std::format("{}", err); return std::make_unique(s.str()); } From 4bb682cf59ad91fa7ba3de967c4e63dc42d51a36 Mon Sep 17 00:00:00 2001 From: Michalis Kokologiannakis Date: Fri, 14 Nov 2025 20:15:10 +0100 Subject: [PATCH 2/5] genmc/setup: Check GenMC config validity GenMC v0.14.1 does not throw an error internally if the config is invalid, but rather returns an appropriate error value. This commit has setup code in Miri check the returned value, and exit if there are any errors. --- genmc-sys/cpp/src/MiriInterface/Setup.cpp | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/genmc-sys/cpp/src/MiriInterface/Setup.cpp b/genmc-sys/cpp/src/MiriInterface/Setup.cpp index 5455b1a8de..20c827221a 100644 --- a/genmc-sys/cpp/src/MiriInterface/Setup.cpp +++ b/genmc-sys/cpp/src/MiriInterface/Setup.cpp @@ -147,9 +147,16 @@ static auto to_genmc_verbosity_level(const LogLevel log_level) -> VerbosityLevel // that is allowed to leak and memory that is not. conf->warnUnfreedMemory = false; - // FIXME(genmc,error handling): This function currently exits on error, but will return an - // error value in the future. The return value should be checked once this change is made. - checkConfig(*conf); + // Validate the config and exit if there are any errors + std::vector warnings; + auto config_valid = conf->validate(warnings); + for (const auto& w : warnings) + WARN("{}", w); + if (auto* errors = std::get_if(&config_valid); errors) { + for (const auto& e : *errors) + LOG(VerbosityLevel::Error, "{}", e); + exit(EUSER); + } // Create the actual driver and Miri-GenMC communication shim. auto driver = std::make_unique(std::move(conf), mode); From 149df8a257f87ecd17991775171c7375f0a69f82 Mon Sep 17 00:00:00 2001 From: Michalis Kokologiannakis Date: Sat, 15 Nov 2025 17:09:14 +0100 Subject: [PATCH 3/5] genmc/api: Handle new GenMC error API The new error-reporting mechanism of GenMC changed its public API. This commit adjusts the Miri interface accordingly (all driver calls need an extra argument that represents possible debugging information). --- genmc-sys/cpp/include/MiriInterface.hpp | 3 ++- genmc-sys/cpp/src/MiriInterface/EventHandling.cpp | 10 +++++++--- genmc-sys/cpp/src/MiriInterface/Mutex.cpp | 4 ++++ genmc-sys/cpp/src/MiriInterface/ThreadManagement.cpp | 11 ++++++----- 4 files changed, 19 insertions(+), 9 deletions(-) diff --git a/genmc-sys/cpp/include/MiriInterface.hpp b/genmc-sys/cpp/include/MiriInterface.hpp index 3a04edc013..4929c0cfa1 100644 --- a/genmc-sys/cpp/include/MiriInterface.hpp +++ b/genmc-sys/cpp/include/MiriInterface.hpp @@ -220,7 +220,8 @@ struct MiriGenmcShim : private GenMCDriver { auto handle_load_reset_if_none(ThreadId tid, std::optional old_val, Ts&&... params) -> HandleResult { const auto pos = inc_pos(tid); - const auto ret = GenMCDriver::handleLoad(pos, old_val, std::forward(params)...); + const auto ret = + GenMCDriver::handleLoad(nullptr, pos, old_val, std::forward(params)...); // If we didn't get a value, we have to reset the index of the current thread. if (!std::holds_alternative(ret)) { dec_pos(tid); diff --git a/genmc-sys/cpp/src/MiriInterface/EventHandling.cpp b/genmc-sys/cpp/src/MiriInterface/EventHandling.cpp index 2b6e5749d4..96fb803bcc 100644 --- a/genmc-sys/cpp/src/MiriInterface/EventHandling.cpp +++ b/genmc-sys/cpp/src/MiriInterface/EventHandling.cpp @@ -34,7 +34,7 @@ void MiriGenmcShim::handle_assume_block(ThreadId thread_id, AssumeType assume_type) { BUG_ON(getExec().getGraph().isThreadBlocked(thread_id)); - GenMCDriver::handleAssume(inc_pos(thread_id), assume_type); + GenMCDriver::handleAssume(nullptr, inc_pos(thread_id), assume_type); } /**** Memory access handling ****/ @@ -76,6 +76,7 @@ void MiriGenmcShim::handle_assume_block(ThreadId thread_id, AssumeType assume_ty ) -> StoreResult { const auto pos = inc_pos(thread_id); const auto ret = GenMCDriver::handleStore( + nullptr, pos, GenmcScalarExt::try_to_sval(old_val), ord, @@ -100,7 +101,7 @@ void MiriGenmcShim::handle_assume_block(ThreadId thread_id, AssumeType assume_ty void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) { const auto pos = inc_pos(thread_id); - GenMCDriver::handleFence(pos, ord, EventDeps()); + GenMCDriver::handleFence(nullptr, pos, ord, EventDeps()); } [[nodiscard]] auto MiriGenmcShim::handle_read_modify_write( @@ -143,6 +144,7 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) { const auto storePos = inc_pos(thread_id); const auto store_ret = GenMCDriver::handleStore( + nullptr, storePos, GenmcScalarExt::try_to_sval(old_val), ordering, @@ -210,6 +212,7 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) { const auto storePos = inc_pos(thread_id); const auto store_ret = GenMCDriver::handleStore( + nullptr, storePos, GenmcScalarExt::try_to_sval(old_val), success_ordering, @@ -242,6 +245,7 @@ auto MiriGenmcShim::handle_malloc(ThreadId thread_id, uint64_t size, uint64_t al const auto address_space = AddressSpace::AS_User; const SVal ret_val = GenMCDriver::handleMalloc( + nullptr, pos, size, alignment, @@ -255,7 +259,7 @@ auto MiriGenmcShim::handle_malloc(ThreadId thread_id, uint64_t size, uint64_t al auto MiriGenmcShim::handle_free(ThreadId thread_id, uint64_t address) -> bool { const auto pos = inc_pos(thread_id); - GenMCDriver::handleFree(pos, SAddr(address), EventDeps()); + GenMCDriver::handleFree(nullptr, pos, SAddr(address), EventDeps()); // FIXME(genmc): use returned error from `handleFree` once implemented in GenMC. return getResult().status.has_value(); } diff --git a/genmc-sys/cpp/src/MiriInterface/Mutex.cpp b/genmc-sys/cpp/src/MiriInterface/Mutex.cpp index fc3f5e6e09..af7e30186c 100644 --- a/genmc-sys/cpp/src/MiriInterface/Mutex.cpp +++ b/genmc-sys/cpp/src/MiriInterface/Mutex.cpp @@ -60,6 +60,7 @@ auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint const bool is_lock_acquired = *ret_val == MUTEX_UNLOCKED; if (is_lock_acquired) { const auto store_ret = GenMCDriver::handleStore( + nullptr, inc_pos(thread_id), old_val, address, @@ -93,6 +94,7 @@ auto MiriGenmcShim::handle_mutex_try_lock(ThreadId thread_id, uint64_t address, // a mutex to be "unlocked". const auto old_val = MUTEX_UNLOCKED; const auto load_ret = GenMCDriver::handleLoad( + nullptr, ++currPos, old_val, SAddr(address), @@ -115,6 +117,7 @@ auto MiriGenmcShim::handle_mutex_try_lock(ThreadId thread_id, uint64_t address, } const auto store_ret = GenMCDriver::handleStore( + nullptr, ++currPos, old_val, SAddr(address), @@ -136,6 +139,7 @@ auto MiriGenmcShim::handle_mutex_unlock(ThreadId thread_id, uint64_t address, ui -> StoreResult { const auto pos = inc_pos(thread_id); const auto ret = GenMCDriver::handleStore( + nullptr, pos, // As usual, we need to tell GenMC which value was stored at this location before this // atomic access, if there previously was a non-atomic initializing access. We set the diff --git a/genmc-sys/cpp/src/MiriInterface/ThreadManagement.cpp b/genmc-sys/cpp/src/MiriInterface/ThreadManagement.cpp index d2061fcb40..85fc7d92f7 100644 --- a/genmc-sys/cpp/src/MiriInterface/ThreadManagement.cpp +++ b/genmc-sys/cpp/src/MiriInterface/ThreadManagement.cpp @@ -19,10 +19,11 @@ void MiriGenmcShim::handle_thread_create(ThreadId thread_id, ThreadId parent_id) // FIXME(genmc): for supporting symmetry reduction, these will need to be properly set: const unsigned fun_id = 0; const SVal arg = SVal(0); - const ThreadInfo child_info = ThreadInfo { thread_id, parent_id, fun_id, arg }; + const ThreadInfo child_info = + ThreadInfo { thread_id, parent_id, fun_id, arg, "unknown thread" }; // NOTE: Default memory ordering (`Release`) used here. - const auto child_tid = GenMCDriver::handleThreadCreate(pos, child_info, EventDeps()); + const auto child_tid = GenMCDriver::handleThreadCreate(nullptr, pos, child_info, EventDeps()); // Sanity check the thread id, which is the index in the `threads_action_` array. BUG_ON(child_tid != thread_id || child_tid <= 0 || child_tid != threads_action_.size()); threads_action_.push_back(Action(ActionKind::Load, Event(child_tid, 0))); @@ -33,7 +34,7 @@ void MiriGenmcShim::handle_thread_join(ThreadId thread_id, ThreadId child_id) { const auto pos = inc_pos(thread_id); // NOTE: Default memory ordering (`Acquire`) used here. - const auto ret = GenMCDriver::handleThreadJoin(pos, child_id, EventDeps()); + const auto ret = GenMCDriver::handleThreadJoin(nullptr, pos, child_id, EventDeps()); // If the join failed, decrease the event index again: if (!std::holds_alternative(ret)) { dec_pos(thread_id); @@ -46,10 +47,10 @@ void MiriGenmcShim::handle_thread_join(ThreadId thread_id, ThreadId child_id) { void MiriGenmcShim::handle_thread_finish(ThreadId thread_id, uint64_t ret_val) { const auto pos = inc_pos(thread_id); // NOTE: Default memory ordering (`Release`) used here. - GenMCDriver::handleThreadFinish(pos, SVal(ret_val)); + GenMCDriver::handleThreadFinish(nullptr, pos, SVal(ret_val)); } void MiriGenmcShim::handle_thread_kill(ThreadId thread_id) { const auto pos = inc_pos(thread_id); - GenMCDriver::handleThreadKill(pos); + GenMCDriver::handleThreadKill(nullptr, pos); } From 3822fd2558485854052b6afd8fbe35dfdc95df4b Mon Sep 17 00:00:00 2001 From: Michalis Kokologiannakis Date: Sat, 15 Nov 2025 17:10:11 +0100 Subject: [PATCH 4/5] genmc/schedule: Handle new GenMC scheduling API When GenMC says that an execution should not be explored further, Miri needs to know why (e.g., so that it returns an appropriate exit value). Until now, some (erroneous) heuristics were used for that. This commit changes the Miri/GenMC API to check the scheduling result of GenMC (that now reflects the "stop type"). --- .../cpp/src/MiriInterface/Exploration.cpp | 24 +++++++++++++------ 1 file changed, 17 insertions(+), 7 deletions(-) diff --git a/genmc-sys/cpp/src/MiriInterface/Exploration.cpp b/genmc-sys/cpp/src/MiriInterface/Exploration.cpp index 0f64083ddd..7722c4bfab 100644 --- a/genmc-sys/cpp/src/MiriInterface/Exploration.cpp +++ b/genmc-sys/cpp/src/MiriInterface/Exploration.cpp @@ -22,13 +22,23 @@ auto MiriGenmcShim::schedule_next( // a scheduling decision. threads_action_[curr_thread_id].kind = curr_thread_next_instr_kind; - if (const auto result = GenMCDriver::scheduleNext(threads_action_)) - return SchedulingResult { ExecutionState::Ok, static_cast(result.value()) }; - if (getExec().getGraph().isBlocked()) - return SchedulingResult { ExecutionState::Blocked, 0 }; - if (getResult().status.has_value()) // the "value" here is a `VerificationError` - return SchedulingResult { ExecutionState::Error, 0 }; - return SchedulingResult { ExecutionState::Finished, 0 }; + auto result = GenMCDriver::scheduleNext(threads_action_); + return std::visit( + [](auto&& arg) { + using T = std::decay_t; + if constexpr (std::is_same_v) + return SchedulingResult { ExecutionState::Ok, static_cast(arg) }; + else if constexpr (std::is_same_v) + return SchedulingResult { ExecutionState::Blocked, 0 }; + else if constexpr (std::is_same_v) + return SchedulingResult { ExecutionState::Error, 0 }; + else if constexpr (std::is_same_v) + return SchedulingResult { ExecutionState::Finished, 0 }; + else + static_assert(false, "non-exhaustive visitor!"); + }, + result + ); } /**** Execution start/end handling ****/ From 89a97b9f96cabe462e86b37ae18cd75884930505 Mon Sep 17 00:00:00 2001 From: Michalis Kokologiannakis Date: Sun, 16 Nov 2025 18:29:30 +0100 Subject: [PATCH 5/5] genmc/build: Update GenMC version (v0.15.1) Now GenMC can be built as a standalone library, without LLVM dependencies. --- genmc-sys/build.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/genmc-sys/build.rs b/genmc-sys/build.rs index d3f81fa1d7..9e956449a1 100644 --- a/genmc-sys/build.rs +++ b/genmc-sys/build.rs @@ -28,7 +28,7 @@ mod downloading { /// The GenMC repository the we get our commit from. pub(crate) const GENMC_GITHUB_URL: &str = "https://github.com/MPI-SWS/genmc.git"; /// The GenMC commit we depend on. It must be available on the specified GenMC repository. - pub(crate) const GENMC_COMMIT: &str = "d9527280bb99f1cef64326b1803ffd952e3880df"; + pub(crate) const GENMC_COMMIT: &str = "aa10ed65117c3291524efc19253b5d443a4602ac"; /// Ensure that a local GenMC repo is present and set to the correct commit. /// Return the path of the GenMC repo and whether the checked out commit was changed.