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