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

genmc: Build without LLVM; adjust to API changes

Author: RalfJung

genmc-sys/build.rs

@@ -28,7 +28,7 @@ mod downloading {
     /// The GenMC repository the we get our commit from.
     pub(crate) const GENMC_GITHUB_URL: &str = "https://github.com/MPI-SWS/genmc.git";
     /// The GenMC commit we depend on. It must be available on the specified GenMC repository.
-    pub(crate) const GENMC_COMMIT: &str = "d9527280bb99f1cef64326b1803ffd952e3880df";
+    pub(crate) const GENMC_COMMIT: &str = "aa10ed65117c3291524efc19253b5d443a4602ac";
 
     /// Ensure that a local GenMC repo is present and set to the correct commit.
     /// Return the path of the GenMC repo and whether the checked out commit was changed.
@@ -140,51 +140,6 @@ mod downloading {
     }
 }
 
-// FIXME(genmc,llvm): Remove once the LLVM dependency of the GenMC model checker is removed.
-/// The linked LLVM version is in the generated `config.h`` file, which we parse and use to link to LLVM.
-/// Returns c++ compiler definitions required for building with/including LLVM, and the include path for LLVM headers.
-fn link_to_llvm(config_file: &Path) -> (String, String) {
-    /// Search a string for a line matching `//@VARIABLE_NAME: VARIABLE CONTENT`
-    fn extract_value<'a>(input: &'a str, name: &str) -> Option<&'a str> {
-        input
-            .lines()
-            .find_map(|line| line.strip_prefix("//@")?.strip_prefix(name)?.strip_prefix(": "))
-    }
-
-    let file_content = std::fs::read_to_string(&config_file).unwrap_or_else(|err| {
-        panic!("GenMC config file ({}) should exist, but got errror {err:?}", config_file.display())
-    });
-
-    let llvm_definitions = extract_value(&file_content, "LLVM_DEFINITIONS")
-        .expect("Config file should contain LLVM_DEFINITIONS");
-    let llvm_include_dirs = extract_value(&file_content, "LLVM_INCLUDE_DIRS")
-        .expect("Config file should contain LLVM_INCLUDE_DIRS");
-    let llvm_library_dir = extract_value(&file_content, "LLVM_LIBRARY_DIR")
-        .expect("Config file should contain LLVM_LIBRARY_DIR");
-    let llvm_config_path = extract_value(&file_content, "LLVM_CONFIG_PATH")
-        .expect("Config file should contain LLVM_CONFIG_PATH");
-
-    // Add linker search path.
-    let lib_dir = PathBuf::from_str(llvm_library_dir).unwrap();
-    println!("cargo::rustc-link-search=native={}", lib_dir.display());
-
-    // Add libraries to link.
-    let output = std::process::Command::new(llvm_config_path)
-        .arg("--libs") // Print the libraries to link to (space-separated list)
-        .output()
-        .expect("failed to execute llvm-config");
-    let llvm_link_libs =
-        String::try_from(output.stdout).expect("llvm-config output should be a valid string");
-
-    for link_lib in llvm_link_libs.trim().split(" ") {
-        let link_lib =
-            link_lib.strip_prefix("-l").expect("Linker parameter should start with \"-l\"");
-        println!("cargo::rustc-link-lib=dylib={link_lib}");
-    }
-
-    (llvm_definitions.to_string(), llvm_include_dirs.to_string())
-}
-
 /// Build the GenMC model checker library and the Rust-C++ interop library with cxx.rs
 fn compile_cpp_dependencies(genmc_path: &Path, always_configure: bool) {
     // Give each step a separate build directory to prevent interference.
@@ -204,6 +159,7 @@ fn compile_cpp_dependencies(genmc_path: &Path, always_configure: bool) {
         .always_configure(always_configure) // We force running the configure step when the GenMC commit changed.
         .out_dir(genmc_build_dir)
         .profile(GENMC_CMAKE_PROFILE)
+        .define("BUILD_LLI", "OFF")
         .define("GENMC_DEBUG", if enable_genmc_debug { "ON" } else { "OFF" });
 
     // The actual compilation happens here:
@@ -214,19 +170,11 @@ fn compile_cpp_dependencies(genmc_path: &Path, always_configure: bool) {
     println!("cargo::rustc-link-search=native={}", cmake_lib_dir.display());
     println!("cargo::rustc-link-lib=static={GENMC_MODEL_CHECKER}");
 
-    // FIXME(genmc,llvm): Remove once the LLVM dependency of the GenMC model checker is removed.
-    let config_file = genmc_install_dir.join("include").join("genmc").join("config.h");
-    let (llvm_definitions, llvm_include_dirs) = link_to_llvm(&config_file);
-
     // Part 2:
     // Compile the cxx_bridge (the link between the Rust and C++ code).
 
     let genmc_include_dir = genmc_install_dir.join("include").join("genmc");
 
-    // FIXME(genmc,llvm): remove once LLVM dependency is removed.
-    // These definitions are parsed into a cmake list and then printed to the config.h file, so they are ';' separated.
-    let definitions = llvm_definitions.split(";");
-
     // These are all the C++ files we need to compile, which needs to be updated if more C++ files are added to Miri.
     // We use absolute paths since relative paths can confuse IDEs when attempting to go-to-source on a path in a compiler error.
     let cpp_files_base_path = Path::new("cpp/src/");
@@ -244,16 +192,12 @@ fn compile_cpp_dependencies(genmc_path: &Path, always_configure: bool) {
     if enable_genmc_debug {
         bridge.define("ENABLE_GENMC_DEBUG", None);
     }
-    for definition in definitions {
-        bridge.flag(definition);
-    }
     bridge
         .opt_level(2)
         .debug(true) // Same settings that GenMC uses (default for cmake `RelWithDebInfo`)
         .warnings(false) // NOTE: enabling this produces a lot of warnings.
         .std("c++23")
         .include(genmc_include_dir)
-        .include(llvm_include_dirs)
         .include("./cpp/include")
         .files(&cpp_files)
         .out_dir(interface_build_dir)

genmc-sys/cpp/include/MiriInterface.hpp

@@ -220,7 +220,8 @@ struct MiriGenmcShim : private GenMCDriver {
     auto handle_load_reset_if_none(ThreadId tid, std::optional<SVal> old_val, Ts&&... params)
         -> HandleResult<SVal> {
         const auto pos = inc_pos(tid);
-        const auto ret = GenMCDriver::handleLoad<k>(pos, old_val, std::forward<Ts>(params)...);
+        const auto 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);

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. */
 static auto format_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());
 }
 

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

@@ -34,7 +34,7 @@
 
 void MiriGenmcShim::handle_assume_block(ThreadId thread_id, AssumeType assume_type) {
     BUG_ON(getExec().getGraph().isThreadBlocked(thread_id));
-    GenMCDriver::handleAssume(inc_pos(thread_id), assume_type);
+    GenMCDriver::handleAssume(nullptr, inc_pos(thread_id), assume_type);
 }
 
 /**** Memory access handling ****/
@@ -76,6 +76,7 @@ void MiriGenmcShim::handle_assume_block(ThreadId thread_id, AssumeType assume_ty
 ) -> StoreResult {
     const auto pos = inc_pos(thread_id);
     const auto ret = GenMCDriver::handleStore<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
 
 void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
     const auto pos = inc_pos(thread_id);
-    GenMCDriver::handleFence(pos, ord, EventDeps());
+    GenMCDriver::handleFence(nullptr, pos, ord, EventDeps());
 }
 
 [[nodiscard]] auto MiriGenmcShim::handle_read_modify_write(
@@ -143,6 +144,7 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
 
     const auto storePos = inc_pos(thread_id);
     const auto store_ret = GenMCDriver::handleStore<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) {
 
     const auto storePos = inc_pos(thread_id);
     const auto 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
     const auto address_space = AddressSpace::AS_User;
 
     const SVal ret_val = GenMCDriver::handleMalloc(
+        nullptr,
         pos,
         size,
         alignment,
@@ -255,7 +259,7 @@ auto MiriGenmcShim::handle_malloc(ThreadId thread_id, uint64_t size, uint64_t al
 
 auto MiriGenmcShim::handle_free(ThreadId thread_id, uint64_t address) -> bool {
     const auto pos = inc_pos(thread_id);
-    GenMCDriver::handleFree(pos, SAddr(address), EventDeps());
+    GenMCDriver::handleFree(nullptr, pos, SAddr(address), EventDeps());
     // FIXME(genmc): use returned error from `handleFree` once implemented in GenMC.
     return getResult().status.has_value();
 }

genmc-sys/cpp/src/MiriInterface/Exploration.cpp

@@ -22,13 +22,23 @@ auto MiriGenmcShim::schedule_next(
     // a scheduling decision.
     threads_action_[curr_thread_id].kind = curr_thread_next_instr_kind;
 
-    if (const auto result = GenMCDriver::scheduleNext(threads_action_))
-        return SchedulingResult { ExecutionState::Ok, static_cast<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_);
+    return std::visit(
+        [](auto&& arg) {
+            using T = std::decay_t<decltype(arg)>;
+            if constexpr (std::is_same_v<T, int>)
+                return SchedulingResult { ExecutionState::Ok, static_cast<int32_t>(arg) };
+            else if constexpr (std::is_same_v<T, Blocked>)
+                return SchedulingResult { ExecutionState::Blocked, 0 };
+            else if constexpr (std::is_same_v<T, Error>)
+                return SchedulingResult { ExecutionState::Error, 0 };
+            else if constexpr (std::is_same_v<T, Finished>)
+                return SchedulingResult { ExecutionState::Finished, 0 };
+            else
+                static_assert(false, "non-exhaustive visitor!");
+        },
+        result
+    );
 }
 
 /**** Execution start/end handling ****/

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

@@ -60,6 +60,7 @@ auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint
     const bool is_lock_acquired = *ret_val == MUTEX_UNLOCKED;
     if (is_lock_acquired) {
         const auto store_ret = GenMCDriver::handleStore<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".
     const auto old_val = MUTEX_UNLOCKED;
     const auto 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,
     }
 
     const auto 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 {
     const auto pos = inc_pos(thread_id);
     const auto 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

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

genmc-sys/cpp/src/MiriInterface/ThreadManagement.cpp

@@ -19,10 +19,11 @@ void MiriGenmcShim::handle_thread_create(ThreadId thread_id, ThreadId parent_id)
     // FIXME(genmc): for supporting symmetry reduction, these will need to be properly set:
     const unsigned fun_id = 0;
     const SVal arg = SVal(0);
-    const ThreadInfo child_info = ThreadInfo { thread_id, parent_id, fun_id, arg };
+    const ThreadInfo child_info =
+        ThreadInfo { thread_id, parent_id, fun_id, arg, "unknown thread" };
 
     // NOTE: Default memory ordering (`Release`) used here.
-    const auto child_tid = GenMCDriver::handleThreadCreate(pos, child_info, EventDeps());
+    const auto child_tid = GenMCDriver::handleThreadCreate(nullptr, pos, child_info, EventDeps());
     // Sanity check the thread id, which is the index in the `threads_action_` array.
     BUG_ON(child_tid != thread_id || child_tid <= 0 || child_tid != threads_action_.size());
     threads_action_.push_back(Action(ActionKind::Load, Event(child_tid, 0)));
@@ -33,7 +34,7 @@ void MiriGenmcShim::handle_thread_join(ThreadId thread_id, ThreadId child_id) {
     const auto pos = inc_pos(thread_id);
 
     // NOTE: Default memory ordering (`Acquire`) used here.
-    const auto ret = GenMCDriver::handleThreadJoin(pos, child_id, EventDeps());
+    const auto ret = GenMCDriver::handleThreadJoin(nullptr, pos, child_id, EventDeps());
     // If the join failed, decrease the event index again:
     if (!std::holds_alternative<SVal>(ret)) {
         dec_pos(thread_id);
@@ -46,10 +47,10 @@ void MiriGenmcShim::handle_thread_join(ThreadId thread_id, ThreadId child_id) {
 void MiriGenmcShim::handle_thread_finish(ThreadId thread_id, uint64_t ret_val) {
     const auto pos = inc_pos(thread_id);
     // NOTE: Default memory ordering (`Release`) used here.
-    GenMCDriver::handleThreadFinish(pos, SVal(ret_val));
+    GenMCDriver::handleThreadFinish(nullptr, pos, SVal(ret_val));
 }
 
 void MiriGenmcShim::handle_thread_kill(ThreadId thread_id) {
     const auto pos = inc_pos(thread_id);
-    GenMCDriver::handleThreadKill(pos);
+    GenMCDriver::handleThreadKill(nullptr, pos);
 }