Merge pull request #4697 from michaliskok/genmc-llvm-dep

genmc: Build without LLVM; adjust to API changes

Author: RalfJung

src/tools/miri/genmc-sys/build.rs

@@ -28,7 +28,7 @@ mod downloading {
 /// The GenMC repository the we get our commit from.
 pub(crate)constGENMC_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)constGENMC_COMMIT:&str = "d9527280bb99f1cef64326b1803ffd952e3880df";
+pub(crate)constGENMC_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.
@@ -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.
-fnlink_to_llvm(config_file:&Path) -> (String,String){
-/// Search a string for a line matching `//@VARIABLE_NAME: VARIABLE CONTENT`
-fnextract_value<'a>(input:&'astr,name:&str) -> Option<&'astr>{
- 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
 fncompile_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)

src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp

@@ -220,7 +220,8 @@ struct MiriGenmcShim : private GenMCDriver {
 autohandle_load_reset_if_none(ThreadId tid, std::optional<SVal> old_val, Ts&&... params)
  -> HandleResult<SVal> {
 constauto pos = inc_pos(tid);
-constauto ret = GenMCDriver::handleLoad<k>(pos, old_val, std::forward<Ts>(params)...);
+constauto ret =
+ GenMCDriver::handleLoad<k>(nullptr, pos, old_val, std::forward<Ts>(params)...);
 // If we didn't get a value, we have to reset the index of the current thread.
 if (!std::holds_alternative<SVal>(ret)) {
 dec_pos(tid);

src/tools/miri/genmc-sys/cpp/include/ResultHandling.hpp

@@ -7,14 +7,16 @@
 // GenMC headers:
 #include"Verification/VerificationError.hpp"
 
+#include<format>
+#include<memory>
+#include<sstream>
 #include<string>
 
 /** Information about an error, formatted as a string to avoid having to share an error enum and
  * printing functionality with the Rust side. */
 staticautoformat_error(VerificationError err) -> std::unique_ptr<std::string> {
-auto buf = std::string();
-auto s = llvm::raw_string_ostream(buf);
- s << err;
+ std::stringstream s;
+ s << std::format("{}", err);
 return std::make_unique<std::string>(s.str());
 }
 

src/tools/miri/genmc-sys/cpp/src/MiriInterface/EventHandling.cpp

@@ -34,7 +34,7 @@
 
 voidMiriGenmcShim::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 {
 constauto pos = inc_pos(thread_id);
 constauto ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::Write>(
+nullptr,
  pos,
 GenmcScalarExt::try_to_sval(old_val),
  ord,
@@ -100,7 +101,7 @@ void MiriGenmcShim::handle_assume_block(ThreadId thread_id, AssumeType assume_ty
 
 voidMiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
 constauto pos = inc_pos(thread_id);
-GenMCDriver::handleFence(pos, ord, EventDeps());
+GenMCDriver::handleFence(nullptr, pos, ord, EventDeps());
 }
 
 [[nodiscard]]autoMiriGenmcShim::handle_read_modify_write(
@@ -143,6 +144,7 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
 
 constauto storePos = inc_pos(thread_id);
 constauto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::FaiWrite>(
+nullptr,
  storePos,
 GenmcScalarExt::try_to_sval(old_val),
  ordering,
@@ -210,6 +212,7 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
 
 constauto storePos = inc_pos(thread_id);
 constauto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::CasWrite>(
+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
 constauto 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
 
 autoMiriGenmcShim::handle_free(ThreadId thread_id, uint64_t address) -> bool {
 constauto 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.
 returngetResult().status.has_value();
 }

src/tools/miri/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 (constauto result = GenMCDriver::scheduleNext(threads_action_))
-return SchedulingResult { ExecutionState::Ok, static_cast<int32_t>(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_);
+returnstd::visit(
+ [](auto&& arg) {
+using T = std::decay_t<decltype(arg)>;
+ifconstexpr (std::is_same_v<T, int>)
+return SchedulingResult { ExecutionState::Ok, static_cast<int32_t>(arg) };
+elseifconstexpr (std::is_same_v<T, Blocked>)
+return SchedulingResult { ExecutionState::Blocked, 0 };
+elseifconstexpr (std::is_same_v<T, Error>)
+return SchedulingResult { ExecutionState::Error, 0 };
+elseifconstexpr (std::is_same_v<T, Finished>)
+return SchedulingResult { ExecutionState::Finished, 0 };
+else
+static_assert(false, "non-exhaustive visitor!");
+ },
+ result
+ );
 }
 
 /**** Execution start/end handling ****/

src/tools/miri/genmc-sys/cpp/src/MiriInterface/Mutex.cpp

@@ -60,6 +60,7 @@ auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint
 constbool is_lock_acquired = *ret_val == MUTEX_UNLOCKED;
 if (is_lock_acquired) {
 constauto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::LockCasWrite>(
+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".
 constauto old_val = MUTEX_UNLOCKED;
 constauto load_ret = GenMCDriver::handleLoad<EventLabel::EventLabelKind::TrylockCasRead>(
+nullptr,
  ++currPos,
  old_val,
 SAddr(address),
@@ -115,6 +117,7 @@ auto MiriGenmcShim::handle_mutex_try_lock(ThreadId thread_id, uint64_t address,
  }
 
 constauto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::TrylockCasWrite>(
+nullptr,
  ++currPos,
  old_val,
 SAddr(address),
@@ -136,6 +139,7 @@ auto MiriGenmcShim::handle_mutex_unlock(ThreadId thread_id, uint64_t address, ui
  -> StoreResult {
 constauto pos = inc_pos(thread_id);
 constauto ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::UnlockWrite>(
+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

src/tools/miri/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<std::string> warnings;
+auto config_valid = conf->validate(warnings);
+for (constauto& w : warnings)
+WARN("{}", w);
+if (auto* errors = std::get_if<ConfigErrorList>(&config_valid); errors) {
+for (constauto& e : *errors)
+LOG(VerbosityLevel::Error, "{}", e);
+exit(EUSER);
+ }
 
 // Create the actual driver and Miri-GenMC communication shim.
 auto driver = std::make_unique<MiriGenmcShim>(std::move(conf), mode);

src/tools/miri/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:
 constunsigned 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.
-constauto child_tid = GenMCDriver::handleThreadCreate(pos, child_info, EventDeps());
+constauto 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) {
 constauto pos = inc_pos(thread_id);
 
 // NOTE: Default memory ordering (`Acquire`) used here.
-constauto ret = GenMCDriver::handleThreadJoin(pos, child_id, EventDeps());
+constauto ret = GenMCDriver::handleThreadJoin(nullptr, pos, child_id, EventDeps());
 // If the join failed, decrease the event index again:
 if (!std::holds_alternative<SVal>(ret)) {
 dec_pos(thread_id);
@@ -46,10 +47,10 @@ void MiriGenmcShim::handle_thread_join(ThreadId thread_id, ThreadId child_id) {
 voidMiriGenmcShim::handle_thread_finish(ThreadId thread_id, uint64_t ret_val) {
 constauto 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));
 }
 
 voidMiriGenmcShim::handle_thread_kill(ThreadId thread_id) {
 constauto pos = inc_pos(thread_id);
-GenMCDriver::handleThreadKill(pos);
+GenMCDriver::handleThreadKill(nullptr, pos);
 }

src/tools/miri/genmc-sys/build.rs

@@ -28,7 +28,7 @@ mod downloading {
 /// The GenMC repository the we get our commit from.
 pub(crate)constGENMC_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)constGENMC_COMMIT:&str = "d9527280bb99f1cef64326b1803ffd952e3880df";
+pub(crate)constGENMC_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.
@@ -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.
-fnlink_to_llvm(config_file:&Path) -> (String,String){
-/// Search a string for a line matching `//@VARIABLE_NAME: VARIABLE CONTENT`
-fnextract_value<'a>(input:&'astr,name:&str) -> Option<&'astr>{
- 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
 fncompile_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)

src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp

@@ -220,7 +220,8 @@ struct MiriGenmcShim : private GenMCDriver {
 autohandle_load_reset_if_none(ThreadId tid, std::optional<SVal> old_val, Ts&&... params)
  -> HandleResult<SVal> {
 constauto pos = inc_pos(tid);
-constauto ret = GenMCDriver::handleLoad<k>(pos, old_val, std::forward<Ts>(params)...);
+constauto ret =
+ GenMCDriver::handleLoad<k>(nullptr, pos, old_val, std::forward<Ts>(params)...);
 // If we didn't get a value, we have to reset the index of the current thread.
 if (!std::holds_alternative<SVal>(ret)) {
 dec_pos(tid);

src/tools/miri/genmc-sys/cpp/include/ResultHandling.hpp

@@ -7,14 +7,16 @@
 // GenMC headers:
 #include"Verification/VerificationError.hpp"
 
+#include<format>
+#include<memory>
+#include<sstream>
 #include<string>
 
 /** Information about an error, formatted as a string to avoid having to share an error enum and
  * printing functionality with the Rust side. */
 staticautoformat_error(VerificationError err) -> std::unique_ptr<std::string> {
-auto buf = std::string();
-auto s = llvm::raw_string_ostream(buf);
- s << err;
+ std::stringstream s;
+ s << std::format("{}", err);
 return std::make_unique<std::string>(s.str());
 }
 

src/tools/miri/genmc-sys/cpp/src/MiriInterface/EventHandling.cpp

@@ -34,7 +34,7 @@
 
 voidMiriGenmcShim::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 {
 constauto pos = inc_pos(thread_id);
 constauto ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::Write>(
+nullptr,
  pos,
 GenmcScalarExt::try_to_sval(old_val),
  ord,
@@ -100,7 +101,7 @@ void MiriGenmcShim::handle_assume_block(ThreadId thread_id, AssumeType assume_ty
 
 voidMiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
 constauto pos = inc_pos(thread_id);
-GenMCDriver::handleFence(pos, ord, EventDeps());
+GenMCDriver::handleFence(nullptr, pos, ord, EventDeps());
 }
 
 [[nodiscard]]autoMiriGenmcShim::handle_read_modify_write(
@@ -143,6 +144,7 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
 
 constauto storePos = inc_pos(thread_id);
 constauto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::FaiWrite>(
+nullptr,
  storePos,
 GenmcScalarExt::try_to_sval(old_val),
  ordering,
@@ -210,6 +212,7 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
 
 constauto storePos = inc_pos(thread_id);
 constauto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::CasWrite>(
+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
 constauto 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
 
 autoMiriGenmcShim::handle_free(ThreadId thread_id, uint64_t address) -> bool {
 constauto 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.
 returngetResult().status.has_value();
 }

src/tools/miri/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 (constauto result = GenMCDriver::scheduleNext(threads_action_))
-return SchedulingResult { ExecutionState::Ok, static_cast<int32_t>(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_);
+returnstd::visit(
+ [](auto&& arg) {
+using T = std::decay_t<decltype(arg)>;
+ifconstexpr (std::is_same_v<T, int>)
+return SchedulingResult { ExecutionState::Ok, static_cast<int32_t>(arg) };
+elseifconstexpr (std::is_same_v<T, Blocked>)
+return SchedulingResult { ExecutionState::Blocked, 0 };
+elseifconstexpr (std::is_same_v<T, Error>)
+return SchedulingResult { ExecutionState::Error, 0 };
+elseifconstexpr (std::is_same_v<T, Finished>)
+return SchedulingResult { ExecutionState::Finished, 0 };
+else
+static_assert(false, "non-exhaustive visitor!");
+ },
+ result
+ );
 }
 
 /**** Execution start/end handling ****/

src/tools/miri/genmc-sys/cpp/src/MiriInterface/Mutex.cpp

@@ -60,6 +60,7 @@ auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint
 constbool is_lock_acquired = *ret_val == MUTEX_UNLOCKED;
 if (is_lock_acquired) {
 constauto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::LockCasWrite>(
+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".
 constauto old_val = MUTEX_UNLOCKED;
 constauto load_ret = GenMCDriver::handleLoad<EventLabel::EventLabelKind::TrylockCasRead>(
+nullptr,
  ++currPos,
  old_val,
 SAddr(address),
@@ -115,6 +117,7 @@ auto MiriGenmcShim::handle_mutex_try_lock(ThreadId thread_id, uint64_t address,
  }
 
 constauto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::TrylockCasWrite>(
+nullptr,
  ++currPos,
  old_val,
 SAddr(address),
@@ -136,6 +139,7 @@ auto MiriGenmcShim::handle_mutex_unlock(ThreadId thread_id, uint64_t address, ui
  -> StoreResult {
 constauto pos = inc_pos(thread_id);
 constauto ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::UnlockWrite>(
+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

src/tools/miri/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<std::string> warnings;
+auto config_valid = conf->validate(warnings);
+for (constauto& w : warnings)
+WARN("{}", w);
+if (auto* errors = std::get_if<ConfigErrorList>(&config_valid); errors) {
+for (constauto& e : *errors)
+LOG(VerbosityLevel::Error, "{}", e);
+exit(EUSER);
+ }
 
 // Create the actual driver and Miri-GenMC communication shim.
 auto driver = std::make_unique<MiriGenmcShim>(std::move(conf), mode);

src/tools/miri/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:
 constunsigned 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.
-constauto child_tid = GenMCDriver::handleThreadCreate(pos, child_info, EventDeps());
+constauto 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) {
 constauto pos = inc_pos(thread_id);
 
 // NOTE: Default memory ordering (`Acquire`) used here.
-constauto ret = GenMCDriver::handleThreadJoin(pos, child_id, EventDeps());
+constauto ret = GenMCDriver::handleThreadJoin(nullptr, pos, child_id, EventDeps());
 // If the join failed, decrease the event index again:
 if (!std::holds_alternative<SVal>(ret)) {
 dec_pos(thread_id);
@@ -46,10 +47,10 @@ void MiriGenmcShim::handle_thread_join(ThreadId thread_id, ThreadId child_id) {
 voidMiriGenmcShim::handle_thread_finish(ThreadId thread_id, uint64_t ret_val) {
 constauto 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));
 }
 
 voidMiriGenmcShim::handle_thread_kill(ThreadId thread_id) {
 constauto pos = inc_pos(thread_id);
-GenMCDriver::handleThreadKill(pos);
+GenMCDriver::handleThreadKill(nullptr, pos);
 }

src/tools/miri/genmc-sys/build.rs

@@ -28,7 +28,7 @@ mod downloading {
 /// The GenMC repository the we get our commit from.
 pub(crate)constGENMC_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)constGENMC_COMMIT:&str = "d9527280bb99f1cef64326b1803ffd952e3880df";
+pub(crate)constGENMC_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.
@@ -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.
-fnlink_to_llvm(config_file:&Path) -> (String,String){
-/// Search a string for a line matching `//@VARIABLE_NAME: VARIABLE CONTENT`
-fnextract_value<'a>(input:&'astr,name:&str) -> Option<&'astr>{
- 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
 fncompile_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)

src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp

@@ -220,7 +220,8 @@ struct MiriGenmcShim : private GenMCDriver {
 autohandle_load_reset_if_none(ThreadId tid, std::optional<SVal> old_val, Ts&&... params)
  -> HandleResult<SVal> {
 constauto pos = inc_pos(tid);
-constauto ret = GenMCDriver::handleLoad<k>(pos, old_val, std::forward<Ts>(params)...);
+constauto ret =
+ GenMCDriver::handleLoad<k>(nullptr, pos, old_val, std::forward<Ts>(params)...);
 // If we didn't get a value, we have to reset the index of the current thread.
 if (!std::holds_alternative<SVal>(ret)) {
 dec_pos(tid);

src/tools/miri/genmc-sys/cpp/include/ResultHandling.hpp

@@ -7,14 +7,16 @@
 // GenMC headers:
 #include"Verification/VerificationError.hpp"
 
+#include<format>
+#include<memory>
+#include<sstream>
 #include<string>
 
 /** Information about an error, formatted as a string to avoid having to share an error enum and
  * printing functionality with the Rust side. */
 staticautoformat_error(VerificationError err) -> std::unique_ptr<std::string> {
-auto buf = std::string();
-auto s = llvm::raw_string_ostream(buf);
- s << err;
+ std::stringstream s;
+ s << std::format("{}", err);
 return std::make_unique<std::string>(s.str());
 }
 

src/tools/miri/genmc-sys/cpp/src/MiriInterface/EventHandling.cpp

@@ -34,7 +34,7 @@
 
 voidMiriGenmcShim::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 {
 constauto pos = inc_pos(thread_id);
 constauto ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::Write>(
+nullptr,
  pos,
 GenmcScalarExt::try_to_sval(old_val),
  ord,
@@ -100,7 +101,7 @@ void MiriGenmcShim::handle_assume_block(ThreadId thread_id, AssumeType assume_ty
 
 voidMiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
 constauto pos = inc_pos(thread_id);
-GenMCDriver::handleFence(pos, ord, EventDeps());
+GenMCDriver::handleFence(nullptr, pos, ord, EventDeps());
 }
 
 [[nodiscard]]autoMiriGenmcShim::handle_read_modify_write(
@@ -143,6 +144,7 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
 
 constauto storePos = inc_pos(thread_id);
 constauto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::FaiWrite>(
+nullptr,
  storePos,
 GenmcScalarExt::try_to_sval(old_val),
  ordering,
@@ -210,6 +212,7 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
 
 constauto storePos = inc_pos(thread_id);
 constauto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::CasWrite>(
+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
 constauto 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
 
 autoMiriGenmcShim::handle_free(ThreadId thread_id, uint64_t address) -> bool {
 constauto 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.
 returngetResult().status.has_value();
 }

src/tools/miri/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 (constauto result = GenMCDriver::scheduleNext(threads_action_))
-return SchedulingResult { ExecutionState::Ok, static_cast<int32_t>(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_);
+returnstd::visit(
+ [](auto&& arg) {
+using T = std::decay_t<decltype(arg)>;
+ifconstexpr (std::is_same_v<T, int>)
+return SchedulingResult { ExecutionState::Ok, static_cast<int32_t>(arg) };
+elseifconstexpr (std::is_same_v<T, Blocked>)
+return SchedulingResult { ExecutionState::Blocked, 0 };
+elseifconstexpr (std::is_same_v<T, Error>)
+return SchedulingResult { ExecutionState::Error, 0 };
+elseifconstexpr (std::is_same_v<T, Finished>)
+return SchedulingResult { ExecutionState::Finished, 0 };
+else
+static_assert(false, "non-exhaustive visitor!");
+ },
+ result
+ );
 }
 
 /**** Execution start/end handling ****/

src/tools/miri/genmc-sys/cpp/src/MiriInterface/Mutex.cpp

@@ -60,6 +60,7 @@ auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint
 constbool is_lock_acquired = *ret_val == MUTEX_UNLOCKED;
 if (is_lock_acquired) {
 constauto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::LockCasWrite>(
+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".
 constauto old_val = MUTEX_UNLOCKED;
 constauto load_ret = GenMCDriver::handleLoad<EventLabel::EventLabelKind::TrylockCasRead>(
+nullptr,
  ++currPos,
  old_val,
 SAddr(address),
@@ -115,6 +117,7 @@ auto MiriGenmcShim::handle_mutex_try_lock(ThreadId thread_id, uint64_t address,
  }
 
 constauto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::TrylockCasWrite>(
+nullptr,
  ++currPos,
  old_val,
 SAddr(address),
@@ -136,6 +139,7 @@ auto MiriGenmcShim::handle_mutex_unlock(ThreadId thread_id, uint64_t address, ui
  -> StoreResult {
 constauto pos = inc_pos(thread_id);
 constauto ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::UnlockWrite>(
+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

src/tools/miri/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<std::string> warnings;
+auto config_valid = conf->validate(warnings);
+for (constauto& w : warnings)
+WARN("{}", w);
+if (auto* errors = std::get_if<ConfigErrorList>(&config_valid); errors) {
+for (constauto& e : *errors)
+LOG(VerbosityLevel::Error, "{}", e);
+exit(EUSER);
+ }
 
 // Create the actual driver and Miri-GenMC communication shim.
 auto driver = std::make_unique<MiriGenmcShim>(std::move(conf), mode);

src/tools/miri/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:
 constunsigned 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.
-constauto child_tid = GenMCDriver::handleThreadCreate(pos, child_info, EventDeps());
+constauto 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) {
 constauto pos = inc_pos(thread_id);
 
 // NOTE: Default memory ordering (`Acquire`) used here.
-constauto ret = GenMCDriver::handleThreadJoin(pos, child_id, EventDeps());
+constauto ret = GenMCDriver::handleThreadJoin(nullptr, pos, child_id, EventDeps());
 // If the join failed, decrease the event index again:
 if (!std::holds_alternative<SVal>(ret)) {
 dec_pos(thread_id);
@@ -46,10 +47,10 @@ void MiriGenmcShim::handle_thread_join(ThreadId thread_id, ThreadId child_id) {
 voidMiriGenmcShim::handle_thread_finish(ThreadId thread_id, uint64_t ret_val) {
 constauto 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));
 }
 
 voidMiriGenmcShim::handle_thread_kill(ThreadId thread_id) {
 constauto pos = inc_pos(thread_id);
-GenMCDriver::handleThreadKill(pos);
+GenMCDriver::handleThreadKill(nullptr, pos);
 }

src/tools/miri/genmc-sys/build.rs

@@ -28,7 +28,7 @@ mod downloading {
 /// The GenMC repository the we get our commit from.
 pub(crate)constGENMC_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)constGENMC_COMMIT:&str = "d9527280bb99f1cef64326b1803ffd952e3880df";
+pub(crate)constGENMC_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.
@@ -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.
-fnlink_to_llvm(config_file:&Path) -> (String,String){
-/// Search a string for a line matching `//@VARIABLE_NAME: VARIABLE CONTENT`
-fnextract_value<'a>(input:&'astr,name:&str) -> Option<&'astr>{
- 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
 fncompile_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)

src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp

@@ -220,7 +220,8 @@ struct MiriGenmcShim : private GenMCDriver {
 autohandle_load_reset_if_none(ThreadId tid, std::optional<SVal> old_val, Ts&&... params)
  -> HandleResult<SVal> {
 constauto pos = inc_pos(tid);
-constauto ret = GenMCDriver::handleLoad<k>(pos, old_val, std::forward<Ts>(params)...);
+constauto ret =
+ GenMCDriver::handleLoad<k>(nullptr, pos, old_val, std::forward<Ts>(params)...);
 // If we didn't get a value, we have to reset the index of the current thread.
 if (!std::holds_alternative<SVal>(ret)) {
 dec_pos(tid);

src/tools/miri/genmc-sys/cpp/include/ResultHandling.hpp

@@ -7,14 +7,16 @@
 // GenMC headers:
 #include"Verification/VerificationError.hpp"
 
+#include<format>
+#include<memory>
+#include<sstream>
 #include<string>
 
 /** Information about an error, formatted as a string to avoid having to share an error enum and
  * printing functionality with the Rust side. */
 staticautoformat_error(VerificationError err) -> std::unique_ptr<std::string> {
-auto buf = std::string();
-auto s = llvm::raw_string_ostream(buf);
- s << err;
+ std::stringstream s;
+ s << std::format("{}", err);
 return std::make_unique<std::string>(s.str());
 }
 

src/tools/miri/genmc-sys/cpp/src/MiriInterface/EventHandling.cpp

@@ -34,7 +34,7 @@
 
 voidMiriGenmcShim::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 {
 constauto pos = inc_pos(thread_id);
 constauto ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::Write>(
+nullptr,
  pos,
 GenmcScalarExt::try_to_sval(old_val),
  ord,
@@ -100,7 +101,7 @@ void MiriGenmcShim::handle_assume_block(ThreadId thread_id, AssumeType assume_ty
 
 voidMiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
 constauto pos = inc_pos(thread_id);
-GenMCDriver::handleFence(pos, ord, EventDeps());
+GenMCDriver::handleFence(nullptr, pos, ord, EventDeps());
 }
 
 [[nodiscard]]autoMiriGenmcShim::handle_read_modify_write(
@@ -143,6 +144,7 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
 
 constauto storePos = inc_pos(thread_id);
 constauto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::FaiWrite>(
+nullptr,
  storePos,
 GenmcScalarExt::try_to_sval(old_val),
  ordering,
@@ -210,6 +212,7 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
 
 constauto storePos = inc_pos(thread_id);
 constauto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::CasWrite>(
+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
 constauto 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
 
 autoMiriGenmcShim::handle_free(ThreadId thread_id, uint64_t address) -> bool {
 constauto 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.
 returngetResult().status.has_value();
 }

src/tools/miri/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 (constauto result = GenMCDriver::scheduleNext(threads_action_))
-return SchedulingResult { ExecutionState::Ok, static_cast<int32_t>(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_);
+returnstd::visit(
+ [](auto&& arg) {
+using T = std::decay_t<decltype(arg)>;
+ifconstexpr (std::is_same_v<T, int>)
+return SchedulingResult { ExecutionState::Ok, static_cast<int32_t>(arg) };
+elseifconstexpr (std::is_same_v<T, Blocked>)
+return SchedulingResult { ExecutionState::Blocked, 0 };
+elseifconstexpr (std::is_same_v<T, Error>)
+return SchedulingResult { ExecutionState::Error, 0 };
+elseifconstexpr (std::is_same_v<T, Finished>)
+return SchedulingResult { ExecutionState::Finished, 0 };
+else
+static_assert(false, "non-exhaustive visitor!");
+ },
+ result
+ );
 }
 
 /**** Execution start/end handling ****/

src/tools/miri/genmc-sys/cpp/src/MiriInterface/Mutex.cpp

@@ -60,6 +60,7 @@ auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint
 constbool is_lock_acquired = *ret_val == MUTEX_UNLOCKED;
 if (is_lock_acquired) {
 constauto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::LockCasWrite>(
+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".
 constauto old_val = MUTEX_UNLOCKED;
 constauto load_ret = GenMCDriver::handleLoad<EventLabel::EventLabelKind::TrylockCasRead>(
+nullptr,
  ++currPos,
  old_val,
 SAddr(address),
@@ -115,6 +117,7 @@ auto MiriGenmcShim::handle_mutex_try_lock(ThreadId thread_id, uint64_t address,
  }
 
 constauto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::TrylockCasWrite>(
+nullptr,
  ++currPos,
  old_val,
 SAddr(address),
@@ -136,6 +139,7 @@ auto MiriGenmcShim::handle_mutex_unlock(ThreadId thread_id, uint64_t address, ui
  -> StoreResult {
 constauto pos = inc_pos(thread_id);
 constauto ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::UnlockWrite>(
+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

src/tools/miri/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<std::string> warnings;
+auto config_valid = conf->validate(warnings);
+for (constauto& w : warnings)
+WARN("{}", w);
+if (auto* errors = std::get_if<ConfigErrorList>(&config_valid); errors) {
+for (constauto& e : *errors)
+LOG(VerbosityLevel::Error, "{}", e);
+exit(EUSER);
+ }
 
 // Create the actual driver and Miri-GenMC communication shim.
 auto driver = std::make_unique<MiriGenmcShim>(std::move(conf), mode);

src/tools/miri/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:
 constunsigned 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.
-constauto child_tid = GenMCDriver::handleThreadCreate(pos, child_info, EventDeps());
+constauto 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) {
 constauto pos = inc_pos(thread_id);
 
 // NOTE: Default memory ordering (`Acquire`) used here.
-constauto ret = GenMCDriver::handleThreadJoin(pos, child_id, EventDeps());
+constauto ret = GenMCDriver::handleThreadJoin(nullptr, pos, child_id, EventDeps());
 // If the join failed, decrease the event index again:
 if (!std::holds_alternative<SVal>(ret)) {
 dec_pos(thread_id);
@@ -46,10 +47,10 @@ void MiriGenmcShim::handle_thread_join(ThreadId thread_id, ThreadId child_id) {
 voidMiriGenmcShim::handle_thread_finish(ThreadId thread_id, uint64_t ret_val) {
 constauto 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));
 }
 
 voidMiriGenmcShim::handle_thread_kill(ThreadId thread_id) {
 constauto pos = inc_pos(thread_id);
-GenMCDriver::handleThreadKill(pos);
+GenMCDriver::handleThreadKill(nullptr, pos);
 }

src/tools/miri/genmc-sys/build.rs

@@ -28,7 +28,7 @@ mod downloading {
 /// The GenMC repository the we get our commit from.
 pub(crate)constGENMC_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)constGENMC_COMMIT:&str = "d9527280bb99f1cef64326b1803ffd952e3880df";
+pub(crate)constGENMC_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.
@@ -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.
-fnlink_to_llvm(config_file:&Path) -> (String,String){
-/// Search a string for a line matching `//@VARIABLE_NAME: VARIABLE CONTENT`
-fnextract_value<'a>(input:&'astr,name:&str) -> Option<&'astr>{
- 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
 fncompile_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)

src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp

@@ -220,7 +220,8 @@ struct MiriGenmcShim : private GenMCDriver {
 autohandle_load_reset_if_none(ThreadId tid, std::optional<SVal> old_val, Ts&&... params)
  -> HandleResult<SVal> {
 constauto pos = inc_pos(tid);
-constauto ret = GenMCDriver::handleLoad<k>(pos, old_val, std::forward<Ts>(params)...);
+constauto ret =
+ GenMCDriver::handleLoad<k>(nullptr, pos, old_val, std::forward<Ts>(params)...);
 // If we didn't get a value, we have to reset the index of the current thread.
 if (!std::holds_alternative<SVal>(ret)) {
 dec_pos(tid);

src/tools/miri/genmc-sys/cpp/include/ResultHandling.hpp

@@ -7,14 +7,16 @@
 // GenMC headers:
 #include"Verification/VerificationError.hpp"
 
+#include<format>
+#include<memory>
+#include<sstream>
 #include<string>
 
 /** Information about an error, formatted as a string to avoid having to share an error enum and
  * printing functionality with the Rust side. */
 staticautoformat_error(VerificationError err) -> std::unique_ptr<std::string> {
-auto buf = std::string();
-auto s = llvm::raw_string_ostream(buf);
- s << err;
+ std::stringstream s;
+ s << std::format("{}", err);
 return std::make_unique<std::string>(s.str());
 }
 

src/tools/miri/genmc-sys/cpp/src/MiriInterface/EventHandling.cpp

@@ -34,7 +34,7 @@
 
 voidMiriGenmcShim::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 {
 constauto pos = inc_pos(thread_id);
 constauto ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::Write>(
+nullptr,
  pos,
 GenmcScalarExt::try_to_sval(old_val),
  ord,
@@ -100,7 +101,7 @@ void MiriGenmcShim::handle_assume_block(ThreadId thread_id, AssumeType assume_ty
 
 voidMiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
 constauto pos = inc_pos(thread_id);
-GenMCDriver::handleFence(pos, ord, EventDeps());
+GenMCDriver::handleFence(nullptr, pos, ord, EventDeps());
 }
 
 [[nodiscard]]autoMiriGenmcShim::handle_read_modify_write(
@@ -143,6 +144,7 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
 
 constauto storePos = inc_pos(thread_id);
 constauto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::FaiWrite>(
+nullptr,
  storePos,
 GenmcScalarExt::try_to_sval(old_val),
  ordering,
@@ -210,6 +212,7 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
 
 constauto storePos = inc_pos(thread_id);
 constauto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::CasWrite>(
+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
 constauto 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
 
 autoMiriGenmcShim::handle_free(ThreadId thread_id, uint64_t address) -> bool {
 constauto 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.
 returngetResult().status.has_value();
 }

src/tools/miri/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 (constauto result = GenMCDriver::scheduleNext(threads_action_))
-return SchedulingResult { ExecutionState::Ok, static_cast<int32_t>(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_);
+returnstd::visit(
+ [](auto&& arg) {
+using T = std::decay_t<decltype(arg)>;
+ifconstexpr (std::is_same_v<T, int>)
+return SchedulingResult { ExecutionState::Ok, static_cast<int32_t>(arg) };
+elseifconstexpr (std::is_same_v<T, Blocked>)
+return SchedulingResult { ExecutionState::Blocked, 0 };
+elseifconstexpr (std::is_same_v<T, Error>)
+return SchedulingResult { ExecutionState::Error, 0 };
+elseifconstexpr (std::is_same_v<T, Finished>)
+return SchedulingResult { ExecutionState::Finished, 0 };
+else
+static_assert(false, "non-exhaustive visitor!");
+ },
+ result
+ );
 }
 
 /**** Execution start/end handling ****/

src/tools/miri/genmc-sys/cpp/src/MiriInterface/Mutex.cpp

@@ -60,6 +60,7 @@ auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint
 constbool is_lock_acquired = *ret_val == MUTEX_UNLOCKED;
 if (is_lock_acquired) {
 constauto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::LockCasWrite>(
+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".
 constauto old_val = MUTEX_UNLOCKED;
 constauto load_ret = GenMCDriver::handleLoad<EventLabel::EventLabelKind::TrylockCasRead>(
+nullptr,
  ++currPos,
  old_val,
 SAddr(address),
@@ -115,6 +117,7 @@ auto MiriGenmcShim::handle_mutex_try_lock(ThreadId thread_id, uint64_t address,
  }
 
 constauto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::TrylockCasWrite>(
+nullptr,
  ++currPos,
  old_val,
 SAddr(address),
@@ -136,6 +139,7 @@ auto MiriGenmcShim::handle_mutex_unlock(ThreadId thread_id, uint64_t address, ui
  -> StoreResult {
 constauto pos = inc_pos(thread_id);
 constauto ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::UnlockWrite>(
+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

src/tools/miri/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<std::string> warnings;
+auto config_valid = conf->validate(warnings);
+for (constauto& w : warnings)
+WARN("{}", w);
+if (auto* errors = std::get_if<ConfigErrorList>(&config_valid); errors) {
+for (constauto& e : *errors)
+LOG(VerbosityLevel::Error, "{}", e);
+exit(EUSER);
+ }
 
 // Create the actual driver and Miri-GenMC communication shim.
 auto driver = std::make_unique<MiriGenmcShim>(std::move(conf), mode);

src/tools/miri/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:
 constunsigned 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.
-constauto child_tid = GenMCDriver::handleThreadCreate(pos, child_info, EventDeps());
+constauto 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) {
 constauto pos = inc_pos(thread_id);
 
 // NOTE: Default memory ordering (`Acquire`) used here.
-constauto ret = GenMCDriver::handleThreadJoin(pos, child_id, EventDeps());
+constauto ret = GenMCDriver::handleThreadJoin(nullptr, pos, child_id, EventDeps());
 // If the join failed, decrease the event index again:
 if (!std::holds_alternative<SVal>(ret)) {
 dec_pos(thread_id);
@@ -46,10 +47,10 @@ void MiriGenmcShim::handle_thread_join(ThreadId thread_id, ThreadId child_id) {
 voidMiriGenmcShim::handle_thread_finish(ThreadId thread_id, uint64_t ret_val) {
 constauto 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));
 }
 
 voidMiriGenmcShim::handle_thread_kill(ThreadId thread_id) {
 constauto pos = inc_pos(thread_id);
-GenMCDriver::handleThreadKill(pos);
+GenMCDriver::handleThreadKill(nullptr, pos);
 }

src/tools/miri/genmc-sys/build.rs

@@ -28,7 +28,7 @@ mod downloading {
 /// The GenMC repository the we get our commit from.
 pub(crate)constGENMC_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)constGENMC_COMMIT:&str = "d9527280bb99f1cef64326b1803ffd952e3880df";
+pub(crate)constGENMC_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.
@@ -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.
-fnlink_to_llvm(config_file:&Path) -> (String,String){
-/// Search a string for a line matching `//@VARIABLE_NAME: VARIABLE CONTENT`
-fnextract_value<'a>(input:&'astr,name:&str) -> Option<&'astr>{
- 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
 fncompile_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)

src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp

@@ -220,7 +220,8 @@ struct MiriGenmcShim : private GenMCDriver {
 autohandle_load_reset_if_none(ThreadId tid, std::optional<SVal> old_val, Ts&&... params)
  -> HandleResult<SVal> {
 constauto pos = inc_pos(tid);
-constauto ret = GenMCDriver::handleLoad<k>(pos, old_val, std::forward<Ts>(params)...);
+constauto ret =
+ GenMCDriver::handleLoad<k>(nullptr, pos, old_val, std::forward<Ts>(params)...);
 // If we didn't get a value, we have to reset the index of the current thread.
 if (!std::holds_alternative<SVal>(ret)) {
 dec_pos(tid);

src/tools/miri/genmc-sys/cpp/include/ResultHandling.hpp

@@ -7,14 +7,16 @@
 // GenMC headers:
 #include"Verification/VerificationError.hpp"
 
+#include<format>
+#include<memory>
+#include<sstream>
 #include<string>
 
 /** Information about an error, formatted as a string to avoid having to share an error enum and
  * printing functionality with the Rust side. */
 staticautoformat_error(VerificationError err) -> std::unique_ptr<std::string> {
-auto buf = std::string();
-auto s = llvm::raw_string_ostream(buf);
- s << err;
+ std::stringstream s;
+ s << std::format("{}", err);
 return std::make_unique<std::string>(s.str());
 }
 

src/tools/miri/genmc-sys/cpp/src/MiriInterface/EventHandling.cpp

@@ -34,7 +34,7 @@
 
 voidMiriGenmcShim::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 {
 constauto pos = inc_pos(thread_id);
 constauto ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::Write>(
+nullptr,
  pos,
 GenmcScalarExt::try_to_sval(old_val),
  ord,
@@ -100,7 +101,7 @@ void MiriGenmcShim::handle_assume_block(ThreadId thread_id, AssumeType assume_ty
 
 voidMiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
 constauto pos = inc_pos(thread_id);
-GenMCDriver::handleFence(pos, ord, EventDeps());
+GenMCDriver::handleFence(nullptr, pos, ord, EventDeps());
 }
 
 [[nodiscard]]autoMiriGenmcShim::handle_read_modify_write(
@@ -143,6 +144,7 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
 
 constauto storePos = inc_pos(thread_id);
 constauto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::FaiWrite>(
+nullptr,
  storePos,
 GenmcScalarExt::try_to_sval(old_val),
  ordering,
@@ -210,6 +212,7 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
 
 constauto storePos = inc_pos(thread_id);
 constauto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::CasWrite>(
+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
 constauto 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
 
 autoMiriGenmcShim::handle_free(ThreadId thread_id, uint64_t address) -> bool {
 constauto 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.
 returngetResult().status.has_value();
 }

src/tools/miri/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 (constauto result = GenMCDriver::scheduleNext(threads_action_))
-return SchedulingResult { ExecutionState::Ok, static_cast<int32_t>(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_);
+returnstd::visit(
+ [](auto&& arg) {
+using T = std::decay_t<decltype(arg)>;
+ifconstexpr (std::is_same_v<T, int>)
+return SchedulingResult { ExecutionState::Ok, static_cast<int32_t>(arg) };
+elseifconstexpr (std::is_same_v<T, Blocked>)
+return SchedulingResult { ExecutionState::Blocked, 0 };
+elseifconstexpr (std::is_same_v<T, Error>)
+return SchedulingResult { ExecutionState::Error, 0 };
+elseifconstexpr (std::is_same_v<T, Finished>)
+return SchedulingResult { ExecutionState::Finished, 0 };
+else
+static_assert(false, "non-exhaustive visitor!");
+ },
+ result
+ );
 }
 
 /**** Execution start/end handling ****/

src/tools/miri/genmc-sys/cpp/src/MiriInterface/Mutex.cpp

@@ -60,6 +60,7 @@ auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint
 constbool is_lock_acquired = *ret_val == MUTEX_UNLOCKED;
 if (is_lock_acquired) {
 constauto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::LockCasWrite>(
+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".
 constauto old_val = MUTEX_UNLOCKED;
 constauto load_ret = GenMCDriver::handleLoad<EventLabel::EventLabelKind::TrylockCasRead>(
+nullptr,
  ++currPos,
  old_val,
 SAddr(address),
@@ -115,6 +117,7 @@ auto MiriGenmcShim::handle_mutex_try_lock(ThreadId thread_id, uint64_t address,
  }
 
 constauto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::TrylockCasWrite>(
+nullptr,
  ++currPos,
  old_val,
 SAddr(address),
@@ -136,6 +139,7 @@ auto MiriGenmcShim::handle_mutex_unlock(ThreadId thread_id, uint64_t address, ui
  -> StoreResult {
 constauto pos = inc_pos(thread_id);
 constauto ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::UnlockWrite>(
+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

src/tools/miri/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<std::string> warnings;
+auto config_valid = conf->validate(warnings);
+for (constauto& w : warnings)
+WARN("{}", w);
+if (auto* errors = std::get_if<ConfigErrorList>(&config_valid); errors) {
+for (constauto& e : *errors)
+LOG(VerbosityLevel::Error, "{}", e);
+exit(EUSER);
+ }
 
 // Create the actual driver and Miri-GenMC communication shim.
 auto driver = std::make_unique<MiriGenmcShim>(std::move(conf), mode);

src/tools/miri/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:
 constunsigned 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.
-constauto child_tid = GenMCDriver::handleThreadCreate(pos, child_info, EventDeps());
+constauto 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) {
 constauto pos = inc_pos(thread_id);
 
 // NOTE: Default memory ordering (`Acquire`) used here.
-constauto ret = GenMCDriver::handleThreadJoin(pos, child_id, EventDeps());
+constauto ret = GenMCDriver::handleThreadJoin(nullptr, pos, child_id, EventDeps());
 // If the join failed, decrease the event index again:
 if (!std::holds_alternative<SVal>(ret)) {
 dec_pos(thread_id);
@@ -46,10 +47,10 @@ void MiriGenmcShim::handle_thread_join(ThreadId thread_id, ThreadId child_id) {
 voidMiriGenmcShim::handle_thread_finish(ThreadId thread_id, uint64_t ret_val) {
 constauto 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));
 }
 
 voidMiriGenmcShim::handle_thread_kill(ThreadId thread_id) {
 constauto pos = inc_pos(thread_id);
-GenMCDriver::handleThreadKill(pos);
+GenMCDriver::handleThreadKill(nullptr, pos);
 }

src/tools/miri/genmc-sys/build.rs

@@ -28,7 +28,7 @@ mod downloading {
 /// The GenMC repository the we get our commit from.
 pub(crate)constGENMC_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)constGENMC_COMMIT:&str = "d9527280bb99f1cef64326b1803ffd952e3880df";
+pub(crate)constGENMC_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.
@@ -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.
-fnlink_to_llvm(config_file:&Path) -> (String,String){
-/// Search a string for a line matching `//@VARIABLE_NAME: VARIABLE CONTENT`
-fnextract_value<'a>(input:&'astr,name:&str) -> Option<&'astr>{
- 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
 fncompile_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)

src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp

@@ -220,7 +220,8 @@ struct MiriGenmcShim : private GenMCDriver {
 autohandle_load_reset_if_none(ThreadId tid, std::optional<SVal> old_val, Ts&&... params)
  -> HandleResult<SVal> {
 constauto pos = inc_pos(tid);
-constauto ret = GenMCDriver::handleLoad<k>(pos, old_val, std::forward<Ts>(params)...);
+constauto ret =
+ GenMCDriver::handleLoad<k>(nullptr, pos, old_val, std::forward<Ts>(params)...);
 // If we didn't get a value, we have to reset the index of the current thread.
 if (!std::holds_alternative<SVal>(ret)) {
 dec_pos(tid);

src/tools/miri/genmc-sys/cpp/include/ResultHandling.hpp

@@ -7,14 +7,16 @@
 // GenMC headers:
 #include"Verification/VerificationError.hpp"
 
+#include<format>
+#include<memory>
+#include<sstream>
 #include<string>
 
 /** Information about an error, formatted as a string to avoid having to share an error enum and
  * printing functionality with the Rust side. */
 staticautoformat_error(VerificationError err) -> std::unique_ptr<std::string> {
-auto buf = std::string();
-auto s = llvm::raw_string_ostream(buf);
- s << err;
+ std::stringstream s;
+ s << std::format("{}", err);
 return std::make_unique<std::string>(s.str());
 }
 

src/tools/miri/genmc-sys/cpp/src/MiriInterface/EventHandling.cpp

@@ -34,7 +34,7 @@
 
 voidMiriGenmcShim::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 {
 constauto pos = inc_pos(thread_id);
 constauto ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::Write>(
+nullptr,
  pos,
 GenmcScalarExt::try_to_sval(old_val),
  ord,
@@ -100,7 +101,7 @@ void MiriGenmcShim::handle_assume_block(ThreadId thread_id, AssumeType assume_ty
 
 voidMiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
 constauto pos = inc_pos(thread_id);
-GenMCDriver::handleFence(pos, ord, EventDeps());
+GenMCDriver::handleFence(nullptr, pos, ord, EventDeps());
 }
 
 [[nodiscard]]autoMiriGenmcShim::handle_read_modify_write(
@@ -143,6 +144,7 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
 
 constauto storePos = inc_pos(thread_id);
 constauto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::FaiWrite>(
+nullptr,
  storePos,
 GenmcScalarExt::try_to_sval(old_val),
  ordering,
@@ -210,6 +212,7 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
 
 constauto storePos = inc_pos(thread_id);
 constauto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::CasWrite>(
+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
 constauto 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
 
 autoMiriGenmcShim::handle_free(ThreadId thread_id, uint64_t address) -> bool {
 constauto 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.
 returngetResult().status.has_value();
 }

src/tools/miri/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 (constauto result = GenMCDriver::scheduleNext(threads_action_))
-return SchedulingResult { ExecutionState::Ok, static_cast<int32_t>(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_);
+returnstd::visit(
+ [](auto&& arg) {
+using T = std::decay_t<decltype(arg)>;
+ifconstexpr (std::is_same_v<T, int>)
+return SchedulingResult { ExecutionState::Ok, static_cast<int32_t>(arg) };
+elseifconstexpr (std::is_same_v<T, Blocked>)
+return SchedulingResult { ExecutionState::Blocked, 0 };
+elseifconstexpr (std::is_same_v<T, Error>)
+return SchedulingResult { ExecutionState::Error, 0 };
+elseifconstexpr (std::is_same_v<T, Finished>)
+return SchedulingResult { ExecutionState::Finished, 0 };
+else
+static_assert(false, "non-exhaustive visitor!");
+ },
+ result
+ );
 }
 
 /**** Execution start/end handling ****/

src/tools/miri/genmc-sys/cpp/src/MiriInterface/Mutex.cpp

@@ -60,6 +60,7 @@ auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint
 constbool is_lock_acquired = *ret_val == MUTEX_UNLOCKED;
 if (is_lock_acquired) {
 constauto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::LockCasWrite>(
+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".
 constauto old_val = MUTEX_UNLOCKED;
 constauto load_ret = GenMCDriver::handleLoad<EventLabel::EventLabelKind::TrylockCasRead>(
+nullptr,
  ++currPos,
  old_val,
 SAddr(address),
@@ -115,6 +117,7 @@ auto MiriGenmcShim::handle_mutex_try_lock(ThreadId thread_id, uint64_t address,
  }
 
 constauto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::TrylockCasWrite>(
+nullptr,
  ++currPos,
  old_val,
 SAddr(address),
@@ -136,6 +139,7 @@ auto MiriGenmcShim::handle_mutex_unlock(ThreadId thread_id, uint64_t address, ui
  -> StoreResult {
 constauto pos = inc_pos(thread_id);
 constauto ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::UnlockWrite>(
+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

src/tools/miri/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<std::string> warnings;
+auto config_valid = conf->validate(warnings);
+for (constauto& w : warnings)
+WARN("{}", w);
+if (auto* errors = std::get_if<ConfigErrorList>(&config_valid); errors) {
+for (constauto& e : *errors)
+LOG(VerbosityLevel::Error, "{}", e);
+exit(EUSER);
+ }
 
 // Create the actual driver and Miri-GenMC communication shim.
 auto driver = std::make_unique<MiriGenmcShim>(std::move(conf), mode);

src/tools/miri/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:
 constunsigned 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.
-constauto child_tid = GenMCDriver::handleThreadCreate(pos, child_info, EventDeps());
+constauto 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) {
 constauto pos = inc_pos(thread_id);
 
 // NOTE: Default memory ordering (`Acquire`) used here.
-constauto ret = GenMCDriver::handleThreadJoin(pos, child_id, EventDeps());
+constauto ret = GenMCDriver::handleThreadJoin(nullptr, pos, child_id, EventDeps());
 // If the join failed, decrease the event index again:
 if (!std::holds_alternative<SVal>(ret)) {
 dec_pos(thread_id);
@@ -46,10 +47,10 @@ void MiriGenmcShim::handle_thread_join(ThreadId thread_id, ThreadId child_id) {
 voidMiriGenmcShim::handle_thread_finish(ThreadId thread_id, uint64_t ret_val) {
 constauto 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));
 }
 
 voidMiriGenmcShim::handle_thread_kill(ThreadId thread_id) {
 constauto pos = inc_pos(thread_id);
-GenMCDriver::handleThreadKill(pos);
+GenMCDriver::handleThreadKill(nullptr, pos);
 }

src/tools/miri/genmc-sys/build.rs

@@ -28,7 +28,7 @@ mod downloading {
 /// The GenMC repository the we get our commit from.
 pub(crate)constGENMC_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)constGENMC_COMMIT:&str = "d9527280bb99f1cef64326b1803ffd952e3880df";
+pub(crate)constGENMC_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.
@@ -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.
-fnlink_to_llvm(config_file:&Path) -> (String,String){
-/// Search a string for a line matching `//@VARIABLE_NAME: VARIABLE CONTENT`
-fnextract_value<'a>(input:&'astr,name:&str) -> Option<&'astr>{
- 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
 fncompile_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)

src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp

@@ -220,7 +220,8 @@ struct MiriGenmcShim : private GenMCDriver {
 autohandle_load_reset_if_none(ThreadId tid, std::optional<SVal> old_val, Ts&&... params)
  -> HandleResult<SVal> {
 constauto pos = inc_pos(tid);
-constauto ret = GenMCDriver::handleLoad<k>(pos, old_val, std::forward<Ts>(params)...);
+constauto ret =
+ GenMCDriver::handleLoad<k>(nullptr, pos, old_val, std::forward<Ts>(params)...);
 // If we didn't get a value, we have to reset the index of the current thread.
 if (!std::holds_alternative<SVal>(ret)) {
 dec_pos(tid);

src/tools/miri/genmc-sys/cpp/include/ResultHandling.hpp

@@ -7,14 +7,16 @@
 // GenMC headers:
 #include"Verification/VerificationError.hpp"
 
+#include<format>
+#include<memory>
+#include<sstream>
 #include<string>
 
 /** Information about an error, formatted as a string to avoid having to share an error enum and
  * printing functionality with the Rust side. */
 staticautoformat_error(VerificationError err) -> std::unique_ptr<std::string> {
-auto buf = std::string();
-auto s = llvm::raw_string_ostream(buf);
- s << err;
+ std::stringstream s;
+ s << std::format("{}", err);
 return std::make_unique<std::string>(s.str());
 }
 

src/tools/miri/genmc-sys/cpp/src/MiriInterface/EventHandling.cpp

@@ -34,7 +34,7 @@
 
 voidMiriGenmcShim::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 {
 constauto pos = inc_pos(thread_id);
 constauto ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::Write>(
+nullptr,
  pos,
 GenmcScalarExt::try_to_sval(old_val),
  ord,
@@ -100,7 +101,7 @@ void MiriGenmcShim::handle_assume_block(ThreadId thread_id, AssumeType assume_ty
 
 voidMiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
 constauto pos = inc_pos(thread_id);
-GenMCDriver::handleFence(pos, ord, EventDeps());
+GenMCDriver::handleFence(nullptr, pos, ord, EventDeps());
 }
 
 [[nodiscard]]autoMiriGenmcShim::handle_read_modify_write(
@@ -143,6 +144,7 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
 
 constauto storePos = inc_pos(thread_id);
 constauto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::FaiWrite>(
+nullptr,
  storePos,
 GenmcScalarExt::try_to_sval(old_val),
  ordering,
@@ -210,6 +212,7 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
 
 constauto storePos = inc_pos(thread_id);
 constauto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::CasWrite>(
+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
 constauto 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
 
 autoMiriGenmcShim::handle_free(ThreadId thread_id, uint64_t address) -> bool {
 constauto 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.
 returngetResult().status.has_value();
 }

src/tools/miri/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 (constauto result = GenMCDriver::scheduleNext(threads_action_))
-return SchedulingResult { ExecutionState::Ok, static_cast<int32_t>(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_);
+returnstd::visit(
+ [](auto&& arg) {
+using T = std::decay_t<decltype(arg)>;
+ifconstexpr (std::is_same_v<T, int>)
+return SchedulingResult { ExecutionState::Ok, static_cast<int32_t>(arg) };
+elseifconstexpr (std::is_same_v<T, Blocked>)
+return SchedulingResult { ExecutionState::Blocked, 0 };
+elseifconstexpr (std::is_same_v<T, Error>)
+return SchedulingResult { ExecutionState::Error, 0 };
+elseifconstexpr (std::is_same_v<T, Finished>)
+return SchedulingResult { ExecutionState::Finished, 0 };
+else
+static_assert(false, "non-exhaustive visitor!");
+ },
+ result
+ );
 }
 
 /**** Execution start/end handling ****/

src/tools/miri/genmc-sys/cpp/src/MiriInterface/Mutex.cpp

@@ -60,6 +60,7 @@ auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint
 constbool is_lock_acquired = *ret_val == MUTEX_UNLOCKED;
 if (is_lock_acquired) {
 constauto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::LockCasWrite>(
+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".
 constauto old_val = MUTEX_UNLOCKED;
 constauto load_ret = GenMCDriver::handleLoad<EventLabel::EventLabelKind::TrylockCasRead>(
+nullptr,
  ++currPos,
  old_val,
 SAddr(address),
@@ -115,6 +117,7 @@ auto MiriGenmcShim::handle_mutex_try_lock(ThreadId thread_id, uint64_t address,
  }
 
 constauto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::TrylockCasWrite>(
+nullptr,
  ++currPos,
  old_val,
 SAddr(address),
@@ -136,6 +139,7 @@ auto MiriGenmcShim::handle_mutex_unlock(ThreadId thread_id, uint64_t address, ui
  -> StoreResult {
 constauto pos = inc_pos(thread_id);
 constauto ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::UnlockWrite>(
+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

src/tools/miri/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<std::string> warnings;
+auto config_valid = conf->validate(warnings);
+for (constauto& w : warnings)
+WARN("{}", w);
+if (auto* errors = std::get_if<ConfigErrorList>(&config_valid); errors) {
+for (constauto& e : *errors)
+LOG(VerbosityLevel::Error, "{}", e);
+exit(EUSER);
+ }
 
 // Create the actual driver and Miri-GenMC communication shim.
 auto driver = std::make_unique<MiriGenmcShim>(std::move(conf), mode);

src/tools/miri/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:
 constunsigned 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.
-constauto child_tid = GenMCDriver::handleThreadCreate(pos, child_info, EventDeps());
+constauto 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) {
 constauto pos = inc_pos(thread_id);
 
 // NOTE: Default memory ordering (`Acquire`) used here.
-constauto ret = GenMCDriver::handleThreadJoin(pos, child_id, EventDeps());
+constauto ret = GenMCDriver::handleThreadJoin(nullptr, pos, child_id, EventDeps());
 // If the join failed, decrease the event index again:
 if (!std::holds_alternative<SVal>(ret)) {
 dec_pos(thread_id);
@@ -46,10 +47,10 @@ void MiriGenmcShim::handle_thread_join(ThreadId thread_id, ThreadId child_id) {
 voidMiriGenmcShim::handle_thread_finish(ThreadId thread_id, uint64_t ret_val) {
 constauto 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));
 }
 
 voidMiriGenmcShim::handle_thread_kill(ThreadId thread_id) {
 constauto pos = inc_pos(thread_id);
-GenMCDriver::handleThreadKill(pos);
+GenMCDriver::handleThreadKill(nullptr, pos);
 }