From 4d901507be04ff557f94d590a65e7924405f3c1c Mon Sep 17 00:00:00 2001 From: Ryan Zmuda Date: Tue, 18 Aug 2026 12:06:26 -0400 Subject: [PATCH] klee: consume frozen binary facts --- klee/lib/Core/CMakeLists.txt | 2 - klee/lib/Core/Executor.cpp | 6 +-- klee/tools/klee/main.cpp | 49 +++++++------------ .../resolve_facts_llvm/BinaryLLVMFacts.hpp | 12 +++++ 4 files changed, 32 insertions(+), 37 deletions(-) diff --git a/klee/lib/Core/CMakeLists.txt b/klee/lib/Core/CMakeLists.txt index be5d458ad..021c3ce73 100644 --- a/klee/lib/Core/CMakeLists.txt +++ b/klee/lib/Core/CMakeLists.txt @@ -35,8 +35,6 @@ target_link_libraries(kleeCore PRIVATE kleaverSolver kleaverExpr kleeSupport - libreach - resolve_facts_llvm ) llvm_config(kleeCore "${USE_LLVM_SHARED}" core executionengine mcjit native support) diff --git a/klee/lib/Core/Executor.cpp b/klee/lib/Core/Executor.cpp index cc5bbe6b6..aae0bc952 100644 --- a/klee/lib/Core/Executor.cpp +++ b/klee/lib/Core/Executor.cpp @@ -56,8 +56,6 @@ #include "klee/System/MemoryUsage.h" #include "klee/System/Time.h" -#include "resolve_facts_llvm/resolve_facts_llvm.hpp" - #include "llvm/ADT/SmallPtrSet.h" #include "llvm/ADT/StringExtras.h" #include "llvm/IR/Attributes.h" @@ -2115,9 +2113,7 @@ void Executor::transferToBasicBlock(BasicBlock *dst, BasicBlock *src, goto cont; } } - const auto bb_id = resolve::facts.addNode(*dst); - - klee_warning(("pruning state: " + std::to_string(bb_id)).c_str()); + klee_warning("pruning state"); // For debugging // std::cout << "call stack: " << std::endl; diff --git a/klee/tools/klee/main.cpp b/klee/tools/klee/main.cpp index 986888980..e9e2e1558 100644 --- a/klee/tools/klee/main.cpp +++ b/klee/tools/klee/main.cpp @@ -26,8 +26,7 @@ #include "reach/distmap.hpp" #include "reach/facts.hpp" -#include "reach/graph.hpp" -#include "resolve_facts_llvm/resolve_facts_llvm.hpp" +#include "resolve_facts_llvm/binary_facts_llvm.hpp" #include "klee/Support/CompilerWarning.h" DISABLE_WARNING_PUSH @@ -64,7 +63,6 @@ DISABLE_WARNING_POP #include #include #include -#include #include using namespace llvm; @@ -654,13 +652,12 @@ void build_distmap_blacklist_for_module const std::unordered_set &bl, std::unordered_map &distMap, std::unordered_set &blackList, + const resolve::BinaryLLVMFacts &facts, const llvm::Module &M) { for (const Function &F : M) { for (const BasicBlock &BB : F) { for (const Instruction &I : BB) { - const auto iid = resolve::facts.addNode(I); - const auto mid = resolve::facts.getModuleId(I); - const auto id = std::make_pair(mid, iid); + const auto id = facts.getId(I); if (dm.find(id) != dm.end()) { distMap[&I] = dm.at(id); @@ -674,17 +671,12 @@ void build_distmap_blacklist_for_module } // Search for function node id that matches name -std::optional findMatchingFunctionNodeId(const reach_facts::database &db, - const std::string functionName) { - //std::regex pattern(".*/__uClibc_main.c:f" + functionName); - // "/challenge/app/src/libc/misc/internals/__uClibc_main.c:ftarget" - std::vector matches; - for (const auto &[node_id, node_type] : db.node_type) { - if (node_type == resolve_facts::NodeType::Function && db.name.at(node_id).ends_with(functionName)) { - matches.push_back(node_id); - } - } - if (!matches.size()) { +std::optional +findMatchingFunctionNodeId(const facts_rs::FactsBuf *facts, + const std::string &functionName) { + const auto matches = + reach_facts::find_functions_by_name_suffix(facts, functionName); + if (matches.empty()) { return {}; } if (matches.size() > 1) { @@ -706,27 +698,23 @@ bool KleeHandler::buildDistMapAndBlackList return false; } + resolve::BinaryLLVMFacts facts; for (const auto &M : loadedModules) { - resolve::getModuleFacts(*M); + resolve::getBinaryModuleFacts(facts, *M); } - resolve::getModuleFacts(*mainModule); - - const auto fcts = resolve::facts; - - auto json = fcts.serialize(); - - auto facts = std::istringstream(json); - const reach_facts::database db = reach_facts::load(facts, graph::CFG_LOAD_OPTIONS); + resolve::getBinaryModuleFacts(facts, *mainModule); + const auto serialized = facts.serialize(); // Map target name to node ID - const auto targetNodeId_opt = findMatchingFunctionNodeId(db, targetFunctionName); + const auto targetNodeId_opt = + findMatchingFunctionNodeId(serialized.get(), targetFunctionName); if (!targetNodeId_opt.has_value()) { klee_warning("no matching node ID for target function %s", targetFunctionName.c_str()); return false; } const auto targetNodeId = targetNodeId_opt.value(); - const auto dm_bl = distmap::gen(db, targetNodeId); + const auto dm_bl = distmap::gen(serialized.get(), targetNodeId); const auto &dm = dm_bl.distmap; const auto &bl = dm_bl.blacklist; @@ -738,9 +726,10 @@ bool KleeHandler::buildDistMapAndBlackList // } for (const auto &M : loadedModules) { - build_distmap_blacklist_for_module(dm, bl, distMap, blackList, *M); + build_distmap_blacklist_for_module(dm, bl, distMap, blackList, facts, *M); } - build_distmap_blacklist_for_module(dm, bl, distMap, blackList, *mainModule); + build_distmap_blacklist_for_module(dm, bl, distMap, blackList, facts, + *mainModule); // std::cout << "distMap.size() = " << distMap.size() << std::endl // << "blackList.size() = " << blackList.size() << std::endl; diff --git a/resolve-facts/include/resolve_facts_llvm/BinaryLLVMFacts.hpp b/resolve-facts/include/resolve_facts_llvm/BinaryLLVMFacts.hpp index 40595e4a5..2a30ffc9d 100644 --- a/resolve-facts/include/resolve_facts_llvm/BinaryLLVMFacts.hpp +++ b/resolve-facts/include/resolve_facts_llvm/BinaryLLVMFacts.hpp @@ -20,6 +20,7 @@ #include #include #include +#include namespace resolve { @@ -36,6 +37,8 @@ class BinarySerializedFacts { BinarySerializedFacts(const BinarySerializedFacts &) = delete; BinarySerializedFacts &operator=(const BinarySerializedFacts &) = delete; + const facts_rs::FactsBuf *get() const { return buf; } + llvm::ArrayRef bytes() const { return {facts_rs::facts_buf_data(buf), facts_rs::facts_buf_len(buf)}; } @@ -99,6 +102,15 @@ class BinaryLLVMFacts { BinaryLLVMFacts(const BinaryLLVMFacts &) = delete; BinaryLLVMFacts &operator=(const BinaryLLVMFacts &) = delete; + std::pair + getId(const llvm::Instruction &instruction) const { + const auto module = moduleHandles.find(instruction.getModule()); + const auto node = instructionIDs.find(&instruction); + assert(module != moduleHandles.end()); + assert(node != instructionIDs.end()); + return {module->second, node->second}; + } + BinaryNodeId addNode(const llvm::Module &M) { addModule(M); return 0;