From baa7bff33bc9e69bdd4f0d6621b9c06ff82e11b4 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 29 Jan 2014 17:18:22 +0000 Subject: When using KLEE's built-in Bitcode archive linker do not consider KLEE intrinsics as undefined symbols --- lib/Module/ModuleUtil.cpp | 23 +++++++++++++++++++---- 1 file changed, 19 insertions(+), 4 deletions(-) (limited to 'lib/Module') diff --git a/lib/Module/ModuleUtil.cpp b/lib/Module/ModuleUtil.cpp index 1881c817..54cc0429 100644 --- a/lib/Module/ModuleUtil.cpp +++ b/lib/Module/ModuleUtil.cpp @@ -11,6 +11,7 @@ #include "klee/Config/Version.h" // FIXME: This does not belong here. #include "../Core/Common.h" +#include "../Core/SpecialFunctionHandler.h" #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) #include "llvm/Bitcode/ReaderWriter.h" @@ -103,6 +104,7 @@ GetAllUndefinedSymbols(Module *M, std::set &UndefinedSymbols) { if (I->hasName()) DefinedSymbols.insert(I->getName()); + // Prune out any defined symbols from the undefined symbols set // and other symbols we don't want to treat as an undefined symbol for (std::set::iterator I = UndefinedSymbols.begin(); @@ -124,15 +126,28 @@ GetAllUndefinedSymbols(Module *M, std::set &UndefinedSymbols) { continue; } + // Remove KLEE intrinsics from set of undefined symbols + bool kleeIntrinsicStripped=false; + for (SpecialFunctionHandler::const_iterator sf = SpecialFunctionHandler::begin(), + se = SpecialFunctionHandler::end(); sf != se; ++sf) + { + if (*I == sf->name) + { + DEBUG_WITH_TYPE("klee_linker", dbgs() << "KLEE intrinsic " << sf->name << + " has been removed from undefined symbols"<< "\n"); + UndefinedSymbols.erase(I++); + kleeIntrinsicStripped=true; + break; + } + } + + if (kleeIntrinsicStripped) continue; + // Symbol really is undefined DEBUG_WITH_TYPE("klee_linker", dbgs() << "Symbol " << *I << " is undefined.\n"); ++I; // Keep this symbol in the undefined symbols list } - // FIXME: Remove KLEE special functions - // from the list of undefined symbols. HandlerInfo in SpecialFunctionHandler - // needs to be moved so we can use it here. - DEBUG_WITH_TYPE("klee_linker", dbgs() << "*** Finished computing undefined symbols ***\n"); } -- cgit 1.4.1