about summary refs log tree commit diff homepage
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/Core/Context.h2
-rw-r--r--lib/Core/Executor.cpp90
-rw-r--r--lib/Core/Executor.h6
-rw-r--r--lib/Core/SpecialFunctionHandler.cpp8
-rw-r--r--lib/Core/SpecialFunctionHandler.h5
-rw-r--r--lib/Core/StatsTracker.cpp13
-rw-r--r--lib/Module/KModule.cpp128
-rw-r--r--lib/Module/ModuleUtil.cpp706
-rw-r--r--lib/Module/Optimize.cpp5
9 files changed, 430 insertions, 533 deletions
diff --git a/lib/Core/Context.h b/lib/Core/Context.h
index 6c6eb936..e8b48363 100644
--- a/lib/Core/Context.h
+++ b/lib/Core/Context.h
@@ -28,7 +28,7 @@ namespace klee {
     
   public:
     Context() {}
-    
+
     /// initialize - Construct the global Context instance.
     static void initialize(bool IsLittleEndian, Expr::Width PointerWidth);
 
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 24fcea88..3d7eb21d 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -49,22 +49,22 @@
 #include "klee/Internal/System/MemoryUsage.h"
 #include "klee/SolverStats.h"
 
-#include "llvm/IR/Function.h"
+#include "llvm/ADT/SmallPtrSet.h"
+#include "llvm/ADT/StringExtras.h"
 #include "llvm/IR/Attributes.h"
 #include "llvm/IR/BasicBlock.h"
 #include "llvm/IR/Constants.h"
+#include "llvm/IR/DataLayout.h"
 #include "llvm/IR/Function.h"
 #include "llvm/IR/Instructions.h"
 #include "llvm/IR/IntrinsicInst.h"
 #include "llvm/IR/LLVMContext.h"
 #include "llvm/IR/Module.h"
-#include "llvm/IR/DataLayout.h"
 #include "llvm/IR/TypeBuilder.h"
-#include "llvm/ADT/SmallPtrSet.h"
-#include "llvm/ADT/StringExtras.h"
 #include "llvm/Support/CommandLine.h"
 #include "llvm/Support/ErrorHandling.h"
 #include "llvm/Support/FileSystem.h"
+#include "llvm/Support/Path.h"
 #include "llvm/Support/Process.h"
 #include "llvm/Support/raw_ostream.h"
 
@@ -324,8 +324,8 @@ const char *Executor::TerminateReasonNames[] = {
 };
 
 Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,
-    InterpreterHandler *ih)
-    : Interpreter(opts), kmodule(0), interpreterHandler(ih), searcher(0),
+                   InterpreterHandler *ih)
+    : Interpreter(opts), interpreterHandler(ih), searcher(0),
       externalDispatcher(new ExternalDispatcher(ctx)), statsTracker(0),
       pathWriter(0), symPathWriter(0), specialFunctionHandler(0),
       processTree(0), replayKTest(0), replayPath(0), usingSeeds(0),
@@ -393,22 +393,51 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,
   }
 }
 
+llvm::Module *
+Executor::setModule(std::vector<std::unique_ptr<llvm::Module>> &modules,
+                    const ModuleOptions &opts) {
+  assert(!kmodule && !modules.empty() &&
+         "can only register one module"); // XXX gross
 
-const Module *Executor::setModule(llvm::Module *module, 
-                                  const ModuleOptions &opts) {
-  assert(!kmodule && module && "can only register one module"); // XXX gross
-  
-  kmodule = new KModule(module);
+  kmodule = std::unique_ptr<KModule>(new KModule());
 
-  // Initialize the context.
-  DataLayout *TD = kmodule->targetData;
-  Context::initialize(TD->isLittleEndian(),
-                      (Expr::Width) TD->getPointerSizeInBits());
+  // Preparing the final module happens in multiple stages
+
+  // Link with KLEE intrinsics library before running any optimizations
+  SmallString<128> LibPath(opts.LibraryDir);
+  llvm::sys::path::append(LibPath, "libkleeRuntimeIntrinsic.bca");
+  std::string error;
+  if (!klee::loadFile(LibPath.str(), modules[0]->getContext(), modules,
+                      error)) {
+    klee_error("Could not load KLEE intrinsic file %s", LibPath.c_str());
+  }
 
+  // 1.) Link the modules together
+  while (kmodule->link(modules, opts.EntryPoint)) {
+    // 2.) Apply different instrumentation
+    kmodule->instrument(opts);
+  }
+
+  // 3.) Optimise and prepare for KLEE
+
+  // Create a list of functions that should be preserved if used
+  std::vector<const char *> preservedFunctions;
   specialFunctionHandler = new SpecialFunctionHandler(*this);
+  specialFunctionHandler->prepare(preservedFunctions);
+
+  preservedFunctions.push_back(opts.EntryPoint.c_str());
+
+  // Preserve the free-standing library calls
+  preservedFunctions.push_back("memset");
+  preservedFunctions.push_back("memcpy");
+  preservedFunctions.push_back("memcmp");
+  preservedFunctions.push_back("memmove");
+
+  kmodule->optimiseAndPrepare(opts, preservedFunctions);
+
+  // 4.) Manifest the module
+  kmodule->manifest(interpreterHandler, StatsTracker::useStatistics());
 
-  specialFunctionHandler->prepare();
-  kmodule->prepare(opts, interpreterHandler);
   specialFunctionHandler->bind();
 
   if (StatsTracker::useStatistics() || userSearcherRequiresMD2U()) {
@@ -417,8 +446,13 @@ const Module *Executor::setModule(llvm::Module *module,
                        interpreterHandler->getOutputFilename("assembly.ll"),
                        userSearcherRequiresMD2U());
   }
-  
-  return module;
+
+  // Initialize the context.
+  DataLayout *TD = kmodule->targetData.get();
+  Context::initialize(TD->isLittleEndian(),
+                      (Expr::Width)TD->getPointerSizeInBits());
+
+  return kmodule->module.get();
 }
 
 Executor::~Executor() {
@@ -428,7 +462,6 @@ Executor::~Executor() {
   delete specialFunctionHandler;
   delete statsTracker;
   delete solver;
-  delete kmodule;
   while(!timers.empty()) {
     delete timers.back();
     timers.pop_back();
@@ -441,7 +474,7 @@ Executor::~Executor() {
 void Executor::initializeGlobalObject(ExecutionState &state, ObjectState *os,
                                       const Constant *c, 
                                       unsigned offset) {
-  DataLayout *targetData = kmodule->targetData;
+  const auto targetData = kmodule->targetData.get();
   if (const ConstantVector *cp = dyn_cast<ConstantVector>(c)) {
     unsigned elementSize =
       targetData->getTypeStoreSize(cp->getType()->getElementType());
@@ -501,7 +534,7 @@ MemoryObject * Executor::addExternalObject(ExecutionState &state,
 extern void *__dso_handle __attribute__ ((__weak__));
 
 void Executor::initializeGlobals(ExecutionState &state) {
-  Module *m = kmodule->module;
+  Module *m = kmodule->module.get();
 
   if (m->getModuleInlineAsm() != "")
     klee_warning("executable has module level assembly (ignoring)");
@@ -1400,9 +1433,8 @@ Function* Executor::getTargetFunction(Value *calledVal, ExecutionState &state) {
 #endif
       std::string alias = state.getFnAlias(gv->getName());
       if (alias != "") {
-        llvm::Module* currModule = kmodule->module;
         GlobalValue *old_gv = gv;
-        gv = currModule->getNamedValue(alias);
+        gv = kmodule->module->getNamedValue(alias);
         if (!gv) {
           klee_error("Function %s(), alias for %s not found!\n", alias.c_str(),
                      old_gv->getName().str().c_str());
@@ -1738,7 +1770,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     Function *f = getTargetFunction(fp, state);
 
     // Skip debug intrinsics, we can't evaluate their metadata arguments.
-    if (f && isDebugIntrinsic(f, kmodule))
+    if (f && isDebugIntrinsic(f, kmodule.get()))
       break;
 
     if (isa<InlineAsm>(fp)) {
@@ -2595,14 +2627,14 @@ void Executor::bindInstructionConstants(KInstruction *KI) {
 }
 
 void Executor::bindModuleConstants() {
-  for (std::vector<KFunction*>::iterator it = kmodule->functions.begin(), 
-         ie = kmodule->functions.end(); it != ie; ++it) {
-    KFunction *kf = *it;
+  for (auto &kfp : kmodule->functions) {
+    KFunction *kf = kfp.get();
     for (unsigned i=0; i<kf->numInstructions; ++i)
       bindInstructionConstants(kf->instructions[i]);
   }
 
-  kmodule->constantTable = new Cell[kmodule->constants.size()];
+  kmodule->constantTable =
+      std::unique_ptr<Cell[]>(new Cell[kmodule->constants.size()]);
   for (unsigned i=0; i<kmodule->constants.size(); ++i) {
     Cell &c = kmodule->constantTable[i];
     c.value = evalConstant(kmodule->constants[i]);
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index a0174ab7..6ad5e987 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -120,7 +120,7 @@ private:
 
   class TimerInfo;
 
-  KModule *kmodule;
+  std::unique_ptr<KModule> kmodule;
   InterpreterHandler *interpreterHandler;
   Searcher *searcher;
 
@@ -491,8 +491,8 @@ public:
     replayPosition = 0;
   }
 
-  virtual const llvm::Module *
-  setModule(llvm::Module *module, const ModuleOptions &opts);
+  llvm::Module *setModule(std::vector<std::unique_ptr<llvm::Module>> &modules,
+                          const ModuleOptions &opts) override;
 
   virtual void useSeeds(const std::vector<struct KTest *> *seeds) { 
     usingSeeds = seeds;
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index 11a73da3..62526c94 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -169,18 +169,18 @@ int SpecialFunctionHandler::size() {
 SpecialFunctionHandler::SpecialFunctionHandler(Executor &_executor) 
   : executor(_executor) {}
 
-
-void SpecialFunctionHandler::prepare() {
+void SpecialFunctionHandler::prepare(
+    std::vector<const char *> &preservedFunctions) {
   unsigned N = size();
 
   for (unsigned i=0; i<N; ++i) {
     HandlerInfo &hi = handlerInfo[i];
     Function *f = executor.kmodule->module->getFunction(hi.name);
-    
+
     // No need to create if the function doesn't exist, since it cannot
     // be called in that case.
-  
     if (f && (!hi.doNotOverride || f->isDeclaration())) {
+      preservedFunctions.push_back(hi.name);
       // Make sure NoReturn attribute is set, for optimization and
       // coverage counting.
       if (hi.doesNotReturn)
diff --git a/lib/Core/SpecialFunctionHandler.h b/lib/Core/SpecialFunctionHandler.h
index b11a4974..f99a212f 100644
--- a/lib/Core/SpecialFunctionHandler.h
+++ b/lib/Core/SpecialFunctionHandler.h
@@ -77,7 +77,10 @@ namespace klee {
     /// prepared for execution. At the moment this involves deleting
     /// unused function bodies and marking intrinsics with appropriate
     /// flags for use in optimizations.
-    void prepare();
+    ///
+    /// @param preservedFunctions contains all the function names which should
+    /// be preserved during optimization
+    void prepare(std::vector<const char *> &preservedFunctions);
 
     /// Initialize the internal handler map after the module has been
     /// prepared for execution.
diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp
index f2a989e2..725cfd56 100644
--- a/lib/Core/StatsTracker.cpp
+++ b/lib/Core/StatsTracker.cpp
@@ -195,7 +195,7 @@ StatsTracker::StatsTracker(Executor &_executor, std::string _objectFilename,
         "--istats-write-after-instructions cannot be enabled at the same "
         "time.");
 
-  KModule *km = executor.kmodule;
+  KModule *km = executor.kmodule.get();
 
   if (!sys::path::is_absolute(objectFilename)) {
     SmallString<128> current(objectFilename);
@@ -219,9 +219,8 @@ StatsTracker::StatsTracker(Executor &_executor, std::string _objectFilename,
   if (OutputIStats)
     theStatisticManager->useIndexedStats(km->infos->getMaxID());
 
-  for (std::vector<KFunction*>::iterator it = km->functions.begin(), 
-         ie = km->functions.end(); it != ie; ++it) {
-    KFunction *kf = *it;
+  for (auto &kfp : km->functions) {
+    KFunction *kf = kfp.get();
     kf->trackCoverage = 1;
 
     for (unsigned i=0; i<kf->numInstructions; ++i) {
@@ -469,7 +468,7 @@ void StatsTracker::updateStateStatistics(uint64_t addend) {
 }
 
 void StatsTracker::writeIStats() {
-  Module *m = executor.kmodule->module;
+  const auto m = executor.kmodule->module.get();
   uint64_t istatsMask = 0;
   llvm::raw_fd_ostream &of = *istatsFile;
   
@@ -666,8 +665,8 @@ uint64_t klee::computeMinDistToUncovered(const KInstruction *ki,
 }
 
 void StatsTracker::computeReachableUncovered() {
-  KModule *km = executor.kmodule;
-  Module *m = km->module;
+  KModule *km = executor.kmodule.get();
+  const auto m = km->module.get();
   static bool init = true;
   const InstructionInfoTable &infos = *km->infos;
   StatisticManager &sm = *theStatisticManager;
diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp
index 75e71c0a..d185f687 100644
--- a/lib/Module/KModule.cpp
+++ b/lib/Module/KModule.cpp
@@ -29,9 +29,12 @@
 #include "llvm/IR/DataLayout.h"
 
 #if LLVM_VERSION_CODE < LLVM_VERSION(3, 5)
+#include "llvm/Analysis/Verifier.h"
+#include "llvm/Linker.h"
 #include "llvm/Support/CallSite.h"
 #else
 #include "llvm/IR/CallSite.h"
+#include "llvm/Linker/Linker.h"
 #endif
 
 #include "klee/Internal/Module/LLVMPassManager.h"
@@ -81,33 +84,10 @@ namespace {
                               cl::desc("Print functions whose address is taken."));
 }
 
-KModule::KModule(Module *_module) 
-  : module(_module),
-    targetData(new DataLayout(module)),
-    infos(0),
-    constantTable(0) {
-}
-
-KModule::~KModule() {
-  delete[] constantTable;
-  delete infos;
-
-  for (std::vector<KFunction*>::iterator it = functions.begin(), 
-         ie = functions.end(); it != ie; ++it)
-    delete *it;
-
-  for (std::map<const llvm::Constant*, KConstant*>::iterator it=constantMap.begin(),
-      itE=constantMap.end(); it!=itE;++it)
-    delete it->second;
-
-  delete targetData;
-  delete module;
-}
-
 /***/
 
 namespace llvm {
-extern void Optimize(Module *, const std::string &EntryPoint);
+extern void Optimize(Module *, llvm::ArrayRef<const char *> preservedFunctions);
 }
 
 // what a hack
@@ -194,14 +174,31 @@ void KModule::addInternalFunction(const char* functionName){
   internalFunctions.insert(internalFunction);
 }
 
-void KModule::prepare(const Interpreter::ModuleOptions &opts,
-                      InterpreterHandler *ih) {
+bool KModule::link(std::vector<std::unique_ptr<llvm::Module>> &modules,
+                   const std::string &entryPoint) {
+  auto numRemainingModules = modules.size();
+  // Add the currently active module to the list of linkables
+  modules.push_back(std::move(module));
+  std::string error;
+  module = std::unique_ptr<llvm::Module>(
+      klee::linkModules(modules, entryPoint, error));
+  if (!module)
+    klee_error("Could not link KLEE files %s", error.c_str());
+
+  targetData = std::unique_ptr<llvm::DataLayout>(new DataLayout(module.get()));
+
+  // Check if we linked anything
+  return modules.size() != numRemainingModules;
+}
+
+void KModule::instrument(const Interpreter::ModuleOptions &opts) {
   // Inject checks prior to optimization... we also perform the
   // invariant transformations that we will end up doing later so that
   // optimize is seeing what is as close as possible to the final
   // module.
   LegacyLLVMPassManagerTy pm;
   pm.add(new RaiseAsmPass());
+
   // This pass will scalarize as much code as possible so that the Executor
   // does not need to handle operands of vector type for most instructions
   // other than InsertElementInst and ExtractElementInst.
@@ -214,21 +211,13 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts,
 
   pm.add(new IntrinsicCleanerPass(*targetData));
   pm.run(*module);
+}
 
+void KModule::optimiseAndPrepare(
+    const Interpreter::ModuleOptions &opts,
+    llvm::ArrayRef<const char *> preservedFunctions) {
   if (opts.Optimize)
-    Optimize(module, opts.EntryPoint);
-
-  // FIXME: Missing force import for various math functions.
-
-  // FIXME: Find a way that we can test programs without requiring
-  // this to be linked in, it makes low level debugging much more
-  // annoying.
-
-  SmallString<128> LibPath(opts.LibraryDir);
-  llvm::sys::path::append(LibPath,
-      "kleeRuntimeIntrinsic.bc"
-    );
-  module = linkWithLibrary(module, LibPath.str());
+    Optimize(module.get(), preservedFunctions);
 
   // Add internal functions which are not used to check if instructions
   // have been already visited
@@ -237,10 +226,9 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts,
   if (opts.CheckOvershift)
     addInternalFunction("klee_overshift_check");
 
-
   // Needs to happen after linking (since ctors/dtors can be modified)
   // and optimization (since global optimization can rewrite lists).
-  injectStaticConstructorsAndDestructors(module);
+  injectStaticConstructorsAndDestructors(module.get());
 
   // Finally, run the passes that maintain invariants we expect during
   // interpretation. We run the intrinsic cleaner just in case we
@@ -268,74 +256,69 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts,
   if (!operandTypeCheckPass->checkPassed()) {
     klee_error("Unexpected instruction operand types detected");
   }
+}
 
-  if (OutputSource) {
+void KModule::manifest(InterpreterHandler *ih, bool forceSourceOutput) {
+  if (OutputSource || forceSourceOutput) {
     std::unique_ptr<llvm::raw_fd_ostream> os(ih->openOutputFile("assembly.ll"));
     assert(os && !os->has_error() && "unable to open source output");
     *os << *module;
   }
 
   if (OutputModule) {
-    llvm::raw_fd_ostream *f = ih->openOutputFile("final.bc");
-    WriteBitcodeToFile(module, *f);
-    delete f;
+    std::unique_ptr<llvm::raw_fd_ostream> f(ih->openOutputFile("final.bc"));
+    WriteBitcodeToFile(module.get(), *f);
   }
 
   /* Build shadow structures */
 
-  infos = new InstructionInfoTable(module);  
-  
-  for (Module::iterator it = module->begin(), ie = module->end();
-       it != ie; ++it) {
-    if (it->isDeclaration())
+  infos = std::unique_ptr<InstructionInfoTable>(
+      new InstructionInfoTable(module.get()));
+
+  for (auto &Function : *module) {
+    if (Function.isDeclaration())
       continue;
 
-    Function *fn = &*it;
-    KFunction *kf = new KFunction(fn, this);
-    
+    auto kf = std::unique_ptr<KFunction>(new KFunction(&Function, this));
+
     for (unsigned i=0; i<kf->numInstructions; ++i) {
       KInstruction *ki = kf->instructions[i];
       ki->info = &infos->getInfo(ki->inst);
     }
 
-    functions.push_back(kf);
-    functionMap.insert(std::make_pair(fn, kf));
+    functionMap.insert(std::make_pair(&Function, kf.get()));
+    functions.push_back(std::move(kf));
   }
 
   /* Compute various interesting properties */
 
-  for (std::vector<KFunction*>::iterator it = functions.begin(), 
-         ie = functions.end(); it != ie; ++it) {
-    KFunction *kf = *it;
+  for (auto &kf : functions) {
     if (functionEscapes(kf->function))
       escapingFunctions.insert(kf->function);
   }
 
   if (DebugPrintEscapingFunctions && !escapingFunctions.empty()) {
     llvm::errs() << "KLEE: escaping functions: [";
-    for (std::set<Function*>::iterator it = escapingFunctions.begin(), 
-         ie = escapingFunctions.end(); it != ie; ++it) {
-      llvm::errs() << (*it)->getName() << ", ";
-    }
+    for (auto &Function : escapingFunctions)
+      llvm::errs() << Function->getName() << ", ";
     llvm::errs() << "]\n";
   }
 }
 
 KConstant* KModule::getKConstant(const Constant *c) {
-  std::map<const llvm::Constant*, KConstant*>::iterator it = constantMap.find(c);
+  auto it = constantMap.find(c);
   if (it != constantMap.end())
-    return it->second;
+    return it->second.get();
   return NULL;
 }
 
 unsigned KModule::getConstantID(Constant *c, KInstruction* ki) {
-  KConstant *kc = getKConstant(c);
-  if (kc)
+  if (KConstant *kc = getKConstant(c))
     return kc->id;  
 
   unsigned id = constants.size();
-  kc = new KConstant(c, id, ki);
-  constantMap.insert(std::make_pair(c, kc));
+  auto kc = std::unique_ptr<KConstant>(new KConstant(c, id, ki));
+  constantMap.insert(std::make_pair(c, std::move(kc)));
   constants.push_back(c);
   return id;
 }
@@ -379,11 +362,10 @@ KFunction::KFunction(llvm::Function *_function,
     numArgs(function->arg_size()),
     numInstructions(0),
     trackCoverage(true) {
-  for (llvm::Function::iterator bbit = function->begin(), 
-         bbie = function->end(); bbit != bbie; ++bbit) {
-    BasicBlock *bb = &*bbit;
-    basicBlockEntry[bb] = numInstructions;
-    numInstructions += bb->size();
+  // Assign unique instruction IDs to each basic block
+  for (auto &BasicBlock : *function) {
+    basicBlockEntry[&BasicBlock] = numInstructions;
+    numInstructions += BasicBlock.size();
   }
 
   instructions = new KInstruction*[numInstructions];
diff --git a/lib/Module/ModuleUtil.cpp b/lib/Module/ModuleUtil.cpp
index b07d3d2f..4f2fdf19 100644
--- a/lib/Module/ModuleUtil.cpp
+++ b/lib/Module/ModuleUtil.cpp
@@ -14,26 +14,33 @@
 #include "klee/Internal/Support/ErrorHandling.h"
 #include "../Core/SpecialFunctionHandler.h"
 
-#include "llvm/IRReader/IRReader.h"
 #include "llvm/IR/Function.h"
 #include "llvm/IR/Instructions.h"
 #include "llvm/IR/IntrinsicInst.h"
 #include "llvm/IR/LLVMContext.h"
 #include "llvm/IR/Module.h"
 #include "llvm/IR/ValueSymbolTable.h"
+#include "llvm/IRReader/IRReader.h"
 #include "llvm/Object/Archive.h"
-#include "llvm/Object/ObjectFile.h"
 #include "llvm/Object/Error.h"
+#include "llvm/Object/ObjectFile.h"
+#include "llvm/Support/DataStream.h"
 #include "llvm/Support/FileSystem.h"
 #include "llvm/Support/SourceMgr.h"
-#include "llvm/Support/DataStream.h"
 
 #if LLVM_VERSION_CODE < LLVM_VERSION(3, 5)
-#include "llvm/Linker.h"
+#include "llvm/Analysis/Verifier.h"
 #include "llvm/Assembly/AssemblyAnnotationWriter.h"
+#include "llvm/Linker.h"
 #else
-#include "llvm/Linker/Linker.h"
 #include "llvm/IR/AssemblyAnnotationWriter.h"
+#include "llvm/IR/Verifier.h"
+#include "llvm/Linker/Linker.h"
+#endif
+
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6)
+#include "llvm/IR/DiagnosticInfo.h"
+#include "llvm/IR/DiagnosticPrinter.h"
 #endif
 
 #include "llvm/Analysis/ValueTracking.h"
@@ -42,9 +49,12 @@
 #include "llvm/Support/raw_ostream.h"
 #include "llvm/Support/Path.h"
 
+#include "klee/Internal/Module/LLVMPassManager.h"
+
+#include <algorithm>
+#include <fstream>
 #include <map>
 #include <set>
-#include <fstream>
 #include <sstream>
 #include <string>
 
@@ -71,23 +81,27 @@ GetAllUndefinedSymbols(Module *M, std::set<std::string> &UndefinedSymbols) {
   std::set<std::string> DefinedSymbols;
   UndefinedSymbols.clear();
   KLEE_DEBUG_WITH_TYPE("klee_linker",
-                       dbgs() << "*** Computing undefined symbols ***\n");
-
-  for (Module::iterator I = M->begin(), E = M->end(); I != E; ++I)
-    if (I->hasName()) {
-      if (I->isDeclaration())
-        UndefinedSymbols.insert(I->getName());
-      else if (!I->hasLocalLinkage()) {
+                       dbgs() << "*** Computing undefined symbols for "
+                              << M->getModuleIdentifier() << " ***\n");
+
+  for (auto const &Function : *M) {
+    if (Function.hasName()) {
+      if (Function.isDeclaration())
+        UndefinedSymbols.insert(Function.getName());
+      else if (!Function.hasLocalLinkage()) {
 #if LLVM_VERSION_CODE < LLVM_VERSION(3, 5)
-            assert(!I->hasDLLImportLinkage() && "Found dllimported non-external symbol!");
+        assert(!Function.hasDLLImportLinkage() &&
+               "Found dllimported non-external symbol!");
 #else
-            assert(!I->hasDLLImportStorageClass() && "Found dllimported non-external symbol!");
+        assert(!Function.hasDLLImportStorageClass() &&
+               "Found dllimported non-external symbol!");
 #endif
-        DefinedSymbols.insert(I->getName());
+        DefinedSymbols.insert(Function.getName());
       }
     }
+  }
 
-  for (Module::global_iterator I = M->global_begin(), E = M->global_end();
+  for (Module::const_global_iterator I = M->global_begin(), E = M->global_end();
        I != E; ++I)
     if (I->hasName()) {
       if (I->isDeclaration())
@@ -102,7 +116,7 @@ GetAllUndefinedSymbols(Module *M, std::set<std::string> &UndefinedSymbols) {
       }
     }
 
-  for (Module::alias_iterator I = M->alias_begin(), E = M->alias_end();
+  for (Module::const_alias_iterator I = M->alias_begin(), E = M->alias_end();
        I != E; ++I)
     if (I->hasName())
       DefinedSymbols.insert(I->getName());
@@ -114,8 +128,7 @@ GetAllUndefinedSymbols(Module *M, std::set<std::string> &UndefinedSymbols) {
   for (std::set<std::string>::iterator I = UndefinedSymbols.begin();
        I != UndefinedSymbols.end(); ++I )
   {
-    if (DefinedSymbols.count(*I))
-    {
+    if (DefinedSymbols.find(*I) != DefinedSymbols.end()) {
       SymbolsToRemove.push_back(*I);
       continue;
     }
@@ -135,385 +148,126 @@ GetAllUndefinedSymbols(Module *M, std::set<std::string> &UndefinedSymbols) {
                          dbgs() << "Symbol " << *I << " is undefined.\n");
   }
 
-  // Remove KLEE intrinsics from set of undefined symbols
-  for (SpecialFunctionHandler::const_iterator sf = SpecialFunctionHandler::begin(),
-       se = SpecialFunctionHandler::end(); sf != se; ++sf)
-  {
-    if (UndefinedSymbols.find(sf->name) == UndefinedSymbols.end())
-      continue;
-
-    SymbolsToRemove.push_back(sf->name);
-    KLEE_DEBUG_WITH_TYPE("klee_linker",
-                         dbgs() << "KLEE intrinsic " << sf->name <<
-                         " has will be removed from undefined symbols"<< "\n");
-  }
-
   // Now remove the symbols from undefined set.
-  for (size_t i = 0, j = SymbolsToRemove.size(); i < j; ++i )
-    UndefinedSymbols.erase(SymbolsToRemove[i]);
+  for (auto const &symbol : SymbolsToRemove)
+    UndefinedSymbols.erase(symbol);
 
   KLEE_DEBUG_WITH_TYPE("klee_linker",
                        dbgs() << "*** Finished computing undefined symbols ***\n");
 }
 
-
-/*!  A helper function for linkBCA() which cleans up
- *   memory allocated by that function.
- */
-static void CleanUpLinkBCA(std::vector<Module*> &archiveModules)
-{
-  for (std::vector<Module*>::iterator I = archiveModules.begin(), E = archiveModules.end();
-      I != E; ++I)
-  {
-    delete (*I);
-  }
-}
-
-/*! A helper function for klee::linkWithLibrary() that links in an archive of bitcode
- *  modules into a composite bitcode module
- *
- *  \param[in] archive Archive of bitcode modules
- *  \param[in,out] composite The bitcode module to link against the archive
- *  \param[out] errorMessage Set to an error message if linking fails
- *
- *  \return True if linking succeeds otherwise false
- */
-static bool linkBCA(object::Archive* archive, Module* composite, std::string& errorMessage)
-{
-  llvm::raw_string_ostream SS(errorMessage);
-  std::vector<Module*> archiveModules;
-
-  // Is this efficient? Could we use StringRef instead?
-  std::set<std::string> undefinedSymbols;
-  GetAllUndefinedSymbols(composite, undefinedSymbols);
-
-  if (undefinedSymbols.size() == 0)
-  {
-    // Nothing to do
-    KLEE_DEBUG_WITH_TYPE("klee_linker", dbgs() << "No undefined symbols. Not linking anything in!\n");
-    return true;
-  }
-
-  KLEE_DEBUG_WITH_TYPE("klee_linker", dbgs() << "Loading modules\n");
-  // Load all bitcode files in to memory so we can examine their symbols
-#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5)
-  for (object::Archive::child_iterator AI = archive->child_begin(),
-       AE = archive->child_end(); AI != AE; ++AI)
-#else
-  for (object::Archive::child_iterator AI = archive->begin_children(),
-       AE = archive->end_children(); AI != AE; ++AI)
-#endif
-  {
-
-    StringRef memberName;
-#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5)
-    ErrorOr<StringRef> memberNameErr = AI->getName();
-    std::error_code ec = memberNameErr.getError();
-    if (!ec) {
-      memberName = memberNameErr.get();
-#else
-    error_code ec = AI->getName(memberName);
-
-    if ( ec == errc::success )
-    {
-#endif
-      KLEE_DEBUG_WITH_TYPE("klee_linker", dbgs() << "Loading archive member " << memberName << "\n");
-    }
-    else
-    {
-      errorMessage="Archive member does not have a name!\n";
-      return false;
-    }
-
-#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5)
-    ErrorOr<std::unique_ptr<llvm::object::Binary> > child = AI->getAsBinary();
-    ec = child.getError();
-#else
-    OwningPtr<object::Binary> child;
-    ec = AI->getAsBinary(child);
-#endif
-    if (ec) {
-      // If we can't open as a binary object file its hopefully a bitcode file
+static bool linkTwoModules(llvm::Module *Dest,
+                           std::unique_ptr<llvm::Module> Src,
+                           std::string &errorMsg) {
 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6)
-      ErrorOr<MemoryBufferRef> buff = AI->getMemoryBufferRef();
-      ec = buff.getError();
-#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 5)
-      ErrorOr<std::unique_ptr<MemoryBuffer> > buffErr = AI->getMemoryBuffer();
-      std::unique_ptr<MemoryBuffer> buff = nullptr;
-      ec = buffErr.getError();
-      if (!ec)
-        buff = std::move(buffErr.get());
+  raw_string_ostream Stream(errorMsg);
+  DiagnosticPrinterRawOStream DP(Stream);
+  auto linkResult = Linker::LinkModules(
+      Dest, Src.release(), [&](const DiagnosticInfo &DI) { DI.print(DP); });
 #else
-      OwningPtr<MemoryBuffer> buff; // Once this is destroyed will Module still be valid??
-      ec = AI->getMemoryBuffer(buff);
+  auto linkResult = Linker::LinkModules(Dest, Src.release(),
+                                        Linker::DestroySource, &errorMsg);
 #endif
-      if (ec) {
-        SS << "Failed to get MemoryBuffer: " <<ec.message();
-        SS.flush();
-        return false;
-      }
-
-      if (buff)
-      {
-        Module *Result = 0;
-        // FIXME: Maybe load bitcode file lazily? Then if we need to link, materialise the module
-#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5)
-#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 7)
-        ErrorOr<std::unique_ptr<Module> > resultErr =
-#else
-        ErrorOr<Module *> resultErr =
-#endif
-	    parseBitcodeFile(buff.get(), composite->getContext());
-        ec = resultErr.getError();
-        if (ec)
-          errorMessage = ec.message();
-        else
-#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 7)
-          Result = resultErr->release();
-#else
-          Result = resultErr.get();
-#endif
-#else
-        Result = ParseBitcodeFile(buff.get(), composite->getContext(),
-	    &errorMessage);
-#endif
-        if(!Result)
-        {
-          SS << "Loading module failed : " << errorMessage << "\n";
-          SS.flush();
-          return false;
-        }
-        archiveModules.push_back(Result);
-      }
-      else
-      {
-        errorMessage="Buffer was NULL!";
-        return false;
-      }
-
-    }
-    else if (child.get()->isObject())
-    {
-      SS << "Object file " << child.get()->getFileName().data() <<
-            " in archive is not supported";
-      SS.flush();
-      return false;
-    }
-    else
-    {
-      SS << "Loading archive child with error "<< ec.message();
-      SS.flush();
-      return false;
-    }
-
-  }
-
-  KLEE_DEBUG_WITH_TYPE("klee_linker", dbgs() << "Loaded " << archiveModules.size() << " modules\n");
 
+  return !linkResult;
+}
 
-  std::set<std::string> previouslyUndefinedSymbols;
+std::unique_ptr<llvm::Module>
+klee::linkModules(std::vector<std::unique_ptr<llvm::Module>> &modules,
+                  llvm::StringRef entryFunction, std::string &errorMsg) {
+  assert(!modules.empty() && "modules list should not be empty");
 
-  // Walk through the modules looking for definitions of undefined symbols
-  // if we find a match we should link that module in.
-  unsigned int passCounter=0;
-  do
-  {
-    unsigned int modulesLoadedOnPass=0;
-    previouslyUndefinedSymbols = undefinedSymbols;
+  if (entryFunction.empty()) {
+    // If no entry function is provided, link all modules together into one
+    std::unique_ptr<llvm::Module> composite = std::move(modules.back());
+    modules.pop_back();
 
-    for (size_t i = 0, j = archiveModules.size(); i < j; ++i)
-    {
-      // skip empty archives
-      if (archiveModules[i] == 0)
+    // Just link all modules together
+    for (auto &module : modules) {
+      if (linkTwoModules(composite.get(), std::move(module), errorMsg))
         continue;
-      Module * M = archiveModules[i];
-      // Look for the undefined symbols in the composite module
-      for (std::set<std::string>::iterator S = undefinedSymbols.begin(), SE = undefinedSymbols.end();
-         S != SE; ++S)
-      {
-
-        // FIXME: We aren't handling weak symbols here!
-        // However the algorithm used in LLVM3.2 didn't seem to either
-        // so maybe it doesn't matter?
-
-        if ( GlobalValue* GV = dyn_cast_or_null<GlobalValue>(M->getValueSymbolTable().lookup(*S)))
-        {
-          if (GV->isDeclaration()) continue; // Not a definition
-
-          KLEE_DEBUG_WITH_TYPE("klee_linker", dbgs() << "Found " << GV->getName() <<
-              " in " << M->getModuleIdentifier() << "\n");
-
-#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6)
-          if (Linker::LinkModules(composite, M))
-#else
-          if (Linker::LinkModules(composite, M, Linker::DestroySource, &errorMessage))
-#endif
-          {
-            // Linking failed
-            SS << "Linking archive module with composite failed:" << errorMessage;
-            SS.flush();
-            CleanUpLinkBCA(archiveModules);
-            return false;
-          }
-          else
-          {
-            // Link succeed, now clean up
-            modulesLoadedOnPass++;
-            KLEE_DEBUG_WITH_TYPE("klee_linker", dbgs() << "Linking succeeded.\n");
-
-            delete M;
-            archiveModules[i] = 0;
-
-            // We need to recompute the undefined symbols in the composite module
-            // after linking
-            GetAllUndefinedSymbols(composite, undefinedSymbols);
-
-            break; // Look for symbols in next module
-          }
 
-        }
-      }
+      // Linking failed
+      errorMsg = "Linking archive module with composite failed:" + errorMsg;
+      return nullptr;
     }
 
-    passCounter++;
-    KLEE_DEBUG_WITH_TYPE("klee_linker", dbgs() << "Completed " << passCounter <<
-                " linker passes.\n" << modulesLoadedOnPass <<
-                " modules loaded on the last pass\n");
-  } while (undefinedSymbols != previouslyUndefinedSymbols); // Iterate until we reach a fixed point
-
-
-  // What's left in archiveModules we don't want to link in so free it
-  CleanUpLinkBCA(archiveModules);
-
-  return true;
+    // clean up every module as we already linked in every module
+    modules.clear();
+    return composite;
+  }
 
-}
+  // Starting from the module containing the entry function, resolve unresolved
+  // dependencies recursively
 
 
-Module *klee::linkWithLibrary(Module *module,
-                              const std::string &libraryName) {
-  KLEE_DEBUG_WITH_TYPE("klee_linker", dbgs() << "Linking file " << libraryName << "\n");
-  if (!sys::fs::exists(libraryName)) {
-    klee_error("Link with library %s failed. No such file.",
-        libraryName.c_str());
+  // search for the module containing the entry function
+  std::unique_ptr<llvm::Module> composite;
+  for (auto &module : modules) {
+    if (!module || !module->getNamedValue(entryFunction))
+      continue;
+    if (composite) {
+      errorMsg =
+          "Function " + entryFunction.str() +
+          " defined in different modules (" + module->getModuleIdentifier() +
+          " already defined in: " + composite->getModuleIdentifier() + ")";
+      return nullptr;
+    }
+    composite = std::move(module);
   }
 
-#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5)
-  ErrorOr<std::unique_ptr<MemoryBuffer> > bufferErr =
-      MemoryBuffer::getFile(libraryName);
-  std::error_code ec = bufferErr.getError();
-#else
-  OwningPtr<MemoryBuffer> Buffer;
-  error_code ec = MemoryBuffer::getFile(libraryName,Buffer);
-#endif
-  if (ec) {
-    klee_error("Link with library %s failed: %s", libraryName.c_str(),
-        ec.message().c_str());
+  // fail if not found
+  if (!composite) {
+    errorMsg = "'" + entryFunction.str() + "' function not found in module.";
+    return nullptr;
   }
 
-#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6)
-  MemoryBufferRef Buffer = bufferErr.get()->getMemBufferRef();
-#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 5)
-  MemoryBuffer *Buffer = bufferErr->get();
-#endif
-
-#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6)
-  sys::fs::file_magic magic = sys::fs::identify_magic(Buffer.getBuffer());
-#else
-  sys::fs::file_magic magic = sys::fs::identify_magic(Buffer->getBuffer());
-#endif
-
-  LLVMContext &Context = module->getContext();
-  std::string ErrorMessage;
-
-  if (magic == sys::fs::file_magic::bitcode) {
-    Module *Result = 0;
-#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5)
-#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 7)
-    ErrorOr<std::unique_ptr<Module> > ResultErr =
-#else
-    ErrorOr<Module *> ResultErr =
-#endif
-	parseBitcodeFile(Buffer, Context);
-    if ((ec = ResultErr.getError())) {
-      ErrorMessage = ec.message();
-#else
-    Result = ParseBitcodeFile(Buffer.get(), Context, &ErrorMessage);
-    if (!Result) {
-#endif
-      klee_error("Link with library %s failed: %s", libraryName.c_str(),
-          ErrorMessage.c_str());
-    }
+  while (true) {
+    std::set<std::string> undefinedSymbols;
+    GetAllUndefinedSymbols(composite.get(), undefinedSymbols);
 
-#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 7)
-    Result = ResultErr->release();
-#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 5)
-    Result = ResultErr.get();
-#endif
+    // Stop in nothing is undefined
+    if (undefinedSymbols.empty())
+      break;
 
-#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6)
-    if (Linker::LinkModules(module, Result)) {
-      ErrorMessage = "linking error";
-#else
-    if (Linker::LinkModules(module, Result, Linker::DestroySource, &ErrorMessage)) {
-#endif
-      klee_error("Link with library %s failed: %s", libraryName.c_str(),
-          ErrorMessage.c_str());
-    }
-
-// unique_ptr owns the Module, we don't have to delete it
-#if LLVM_VERSION_CODE < LLVM_VERSION(3, 7)
-    delete Result;
-#endif
+    bool merged = false;
+    for (auto &module : modules) {
+      if (!module)
+        continue;
 
-  } else if (magic == sys::fs::file_magic::archive) {
-#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6)
-    ErrorOr<std::unique_ptr<object::Binary> > arch =
-        object::createBinary(Buffer, &Context);
-    ec = arch.getError();
-#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 5)
-    ErrorOr<object::Binary *> arch =
-        object::createBinary(std::move(bufferErr.get()), &Context);
-    ec = arch.getError();
-#else
-    OwningPtr<object::Binary> arch;
-    ec = object::createBinary(Buffer.take(), arch);
-#endif
-    if (ec)
-      klee_error("Link with library %s failed: %s", libraryName.c_str(),
-          ec.message().c_str());
+      for (auto symbol : undefinedSymbols) {
+        GlobalValue *GV =
+            dyn_cast_or_null<GlobalValue>(module->getNamedValue(symbol));
+        if (!GV || GV->isDeclaration())
+          continue;
 
-#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6)
-    if (object::Archive *a = dyn_cast<object::Archive>(arch->get())) {
-#else
-    if (object::Archive *a = dyn_cast<object::Archive>(arch.get())) {
-#endif
-      // Handle in helper
-      if (!linkBCA(a, module, ErrorMessage))
-        klee_error("Link with library %s failed: %s", libraryName.c_str(),
-            ErrorMessage.c_str());
-    }
-    else {
-    	klee_error("Link with library %s failed: Cast to archive failed", libraryName.c_str());
+        // Found symbol, therefore merge in module
+        KLEE_DEBUG_WITH_TYPE("klee_linker",
+                             dbgs() << "Found " << GV->getName() << " in "
+                                    << module->getModuleIdentifier() << "\n");
+        if (linkTwoModules(composite.get(), std::move(module), errorMsg)) {
+          module = nullptr;
+          merged = true;
+          break;
+        }
+        // Linking failed
+        errorMsg = "Linking archive module with composite failed:" + errorMsg;
+        return nullptr;
+      }
     }
+    if (!merged)
+      break;
+  }
 
-  } else if (magic.is_object()) {
-#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5)
-    std::unique_ptr<object::Binary> obj;
-#else
-    OwningPtr<object::Binary> obj;
-#endif
-    if (obj.get()->isObject()) {
-      klee_warning("Link with library: Object file %s in archive %s found. "
-          "Currently not supported.",
-          obj.get()->getFileName().data(), libraryName.c_str());
-    }
-  } else {
-    klee_error("Link with library %s failed: Unrecognized file type.",
-        libraryName.c_str());
+  // Condense the module array
+  std::vector<std::unique_ptr<llvm::Module>> LeftoverModules;
+  for (auto &module : modules) {
+    if (module)
+      LeftoverModules.emplace_back(std::move(module));
   }
 
-  return module;
+  modules.swap(LeftoverModules);
+  return composite;
 }
 
 Function *klee::getDirectCallTarget(CallSite cs, bool moduleIsFullyLinked) {
@@ -582,69 +336,197 @@ bool klee::functionEscapes(const Function *f) {
   return !valueIsOnlyCalled(f);
 }
 
-#if LLVM_VERSION_CODE < LLVM_VERSION(3, 5)
+bool klee::loadFile(const std::string &fileName, LLVMContext &context,
+                    std::vector<std::unique_ptr<llvm::Module>> &modules,
+                    std::string &errorMsg) {
+  KLEE_DEBUG_WITH_TYPE("klee_loader", dbgs()
+                                          << "Load file " << fileName << "\n");
 
-Module *klee::loadModule(LLVMContext &ctx, const std::string &path, std::string &errorMsg) {
-    OwningPtr<MemoryBuffer> bufferPtr;
-    error_code ec = MemoryBuffer::getFileOrSTDIN(path.c_str(), bufferPtr);
-    if (ec) {
-        errorMsg = ec.message();
-        return 0;
-    }
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5)
+  ErrorOr<std::unique_ptr<MemoryBuffer>> bufferErr =
+      MemoryBuffer::getFileOrSTDIN(fileName);
+  std::error_code ec = bufferErr.getError();
+#else
+  OwningPtr<MemoryBuffer> Buffer;
+  error_code ec = MemoryBuffer::getFileOrSTDIN(fileName, Buffer);
+#endif
+  if (ec) {
+    klee_error("Loading file %s failed: %s", fileName.c_str(),
+               ec.message().c_str());
+  }
+
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6)
+  MemoryBufferRef Buffer = bufferErr.get()->getMemBufferRef();
+#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 5)
+  MemoryBuffer *Buffer = bufferErr->get();
+#endif
 
-    Module *module = getLazyBitcodeModule(bufferPtr.get(), ctx, &errorMsg);
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6)
+  sys::fs::file_magic magic = sys::fs::identify_magic(Buffer.getBuffer());
+#else
+  sys::fs::file_magic magic = sys::fs::identify_magic(Buffer->getBuffer());
+#endif
 
+  if (magic == sys::fs::file_magic::bitcode) {
+    SMDiagnostic Err;
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6)
+    std::unique_ptr<llvm::Module> module(parseIR(Buffer, Err, context));
+#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 5)
+    std::unique_ptr<llvm::Module> module(ParseIR(Buffer, Err, context));
+#else
+    std::unique_ptr<llvm::Module> module(ParseIR(Buffer.take(), Err, context));
+#endif
     if (!module) {
-        return 0;
-    }
-    if (module->MaterializeAllPermanently(&errorMsg)) {
-        delete module;
-        return 0;
+      klee_error("Loading file %s failed: %s", fileName.c_str(),
+                 Err.getMessage().str().c_str());
     }
+    modules.push_back(std::move(module));
+    return true;
+  }
 
-    // In the case of success LLVM will take ownership of the module.
-    // Therefore we need to take ownership away from the `bufferPtr` otherwise the
-    // allocated memory will be deleted twice.
-    bufferPtr.take();
+  if (magic == sys::fs::file_magic::archive) {
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6)
+    ErrorOr<std::unique_ptr<object::Binary>> archOwner =
+        object::createBinary(Buffer, &context);
+    ec = archOwner.getError();
+    llvm::object::Binary *arch = archOwner.get().get();
+#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 5)
+    ErrorOr<object::Binary *> archOwner =
+        object::createBinary(std::move(bufferErr.get()), &context);
+    ec = archOwner.getError();
+    llvm::object::Binary *arch = archOwner.get();
+#else
+    OwningPtr<object::Binary> archOwner;
+    ec = object::createBinary(Buffer.take(), archOwner);
+    llvm::object::Binary *arch = archOwner.get();
+#endif
+    if (ec)
+      klee_error("Loading file %s failed: %s", fileName.c_str(),
+                 ec.message().c_str());
 
-    errorMsg = "";
-    return module;
-}
+    if (auto archive = dyn_cast<object::Archive>(arch)) {
+// Load all bitcode files into memory
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5)
+      for (object::Archive::child_iterator AI = archive->child_begin(),
+                                           AE = archive->child_end();
+           AI != AE; ++AI)
+#else
+      for (object::Archive::child_iterator AI = archive->begin_children(),
+                                           AE = archive->end_children();
+           AI != AE; ++AI)
+#endif
+      {
 
+        StringRef memberName;
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5)
+        ErrorOr<StringRef> memberNameErr = AI->getName();
+        std::error_code ec = memberNameErr.getError();
+        if (!ec) {
+          memberName = memberNameErr.get();
 #else
+        error_code ec = AI->getName(memberName);
 
-Module *klee::loadModule(LLVMContext &ctx, const std::string &path, std::string &errorMsg) {
-  auto buffer = MemoryBuffer::getFileOrSTDIN(path.c_str());
-  if (!buffer) {
-    errorMsg = buffer.getError().message().c_str();
-    return nullptr;
-  }
+        if (ec == errc::success) {
+#endif
+          KLEE_DEBUG_WITH_TYPE("klee_linker", dbgs()
+                                                  << "Loading archive member "
+                                                  << memberName << "\n");
+        } else {
+          errorMsg = "Archive member does not have a name!\n";
+          return false;
+        }
 
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5)
+        ErrorOr<std::unique_ptr<llvm::object::Binary>> child =
+            AI->getAsBinary();
+        ec = child.getError();
+#else
+        OwningPtr<object::Binary> child;
+        ec = AI->getAsBinary(child);
+#endif
+        if (ec) {
+// If we can't open as a binary object file its hopefully a bitcode file
 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6)
-  auto errorOrModule = getLazyBitcodeModule(std::move(buffer.get()), ctx);
+          ErrorOr<MemoryBufferRef> buff = AI->getMemoryBufferRef();
+          ec = buff.getError();
+#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 5)
+          ErrorOr<std::unique_ptr<MemoryBuffer>> buffErr =
+              AI->getMemoryBuffer();
+          std::unique_ptr<MemoryBuffer> buff = nullptr;
+          ec = buffErr.getError();
+          if (!ec)
+            buff = std::move(buffErr.get());
 #else
-  auto errorOrModule = getLazyBitcodeModule(buffer->get(), ctx);
+        OwningPtr<MemoryBuffer> buff;
+        ec = AI->getMemoryBuffer(buff);
 #endif
+          if (ec) {
+            errorMsg = "Failed to get MemoryBuffer: " + ec.message();
+            return false;
+          }
 
-  if (!errorOrModule) {
-    errorMsg = errorOrModule.getError().message().c_str();
-    return nullptr;
-  }
-  // The module has taken ownership of the MemoryBuffer so release it
-  // from the std::unique_ptr
-  buffer->release();
-#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 7)
-  auto module = errorOrModule->release();
+          if (buff) {
+            // FIXME: Maybe load bitcode file lazily? Then if we need to link,
+            // materialise
+            // the module
+            SMDiagnostic Err;
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6)
+            std::unique_ptr<llvm::Module> module =
+                parseIR(buff.get(), Err, context);
+#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 5)
+            std::unique_ptr<llvm::Module> module(
+                ParseIR(buff.get(), Err, context));
 #else
-  auto module = *errorOrModule;
+          std::unique_ptr<llvm::Module> module(
+              ParseIR(buff.take(), Err, context));
 #endif
+            if (!module) {
+              klee_error("Loading file %s failed: %s", fileName.c_str(),
+                         Err.getMessage().str().c_str());
+            }
+
+            modules.push_back(std::move(module));
+          } else {
+            errorMsg = "Buffer was NULL!";
+            return false;
+          }
 
-  if (auto ec = module->materializeAllPermanently()) {
-    errorMsg = ec.message();
-    return nullptr;
+        } else if (child.get()->isObject()) {
+          errorMsg = "Object file " + child.get()->getFileName().str() +
+                     " in archive is not supported";
+          return false;
+        } else {
+          errorMsg = "Loading archive child with error " + ec.message();
+          return false;
+        }
+      }
+    }
+    return true;
   }
+  if (magic.is_object()) {
+    errorMsg = "Loading file " + fileName +
+               " Object file as input is currently not supported";
+    return false;
+  }
+  // This might still be an assembly file. Let's try to parse it.
+  SMDiagnostic Err;
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6)
+  std::unique_ptr<llvm::Module> module(parseIR(Buffer, Err, context));
+#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 5)
+  std::unique_ptr<llvm::Module> module(ParseIR(Buffer, Err, context));
+#else
+std::unique_ptr<llvm::Module> module(ParseIR(Buffer.take(), Err, context));
+#endif
+  if (!module) {
+    klee_error("Loading file %s failed: Unrecognized file type.",
+               fileName.c_str());
+  }
+  modules.push_back(std::move(module));
+  return true;
+}
 
-  errorMsg = "";
-  return module;
+void klee::checkModule(llvm::Module *m) {
+  LegacyLLVMPassManagerTy pm;
+  pm.add(createVerifierPass());
+  pm.run(*m);
 }
-#endif
diff --git a/lib/Module/Optimize.cpp b/lib/Module/Optimize.cpp
index 64e4863f..18c56cc2 100644
--- a/lib/Module/Optimize.cpp
+++ b/lib/Module/Optimize.cpp
@@ -144,7 +144,7 @@ static void AddStandardCompilePasses(klee::LegacyLLVMPassManagerTy &PM) {
 /// Optimize - Perform link time optimizations. This will run the scalar
 /// optimizations, any loaded plugin-optimization modules, and then the
 /// inter-procedural optimizations if applicable.
-void Optimize(Module *M, const std::string &EntryPoint) {
+void Optimize(Module *M, llvm::ArrayRef<const char *> preservedFunctions) {
 
   // Instantiate the pass manager to organize the passes.
   klee::LegacyLLVMPassManagerTy Passes;
@@ -174,8 +174,7 @@ void Optimize(Module *M, const std::string &EntryPoint) {
     // for a main function.  If main is defined, mark all other functions
     // internal.
     if (!DisableInternalize) {
-      ModulePass *pass = createInternalizePass(
-          std::vector<const char *>(1, EntryPoint.c_str()));
+      ModulePass *pass = createInternalizePass(preservedFunctions);
       addPass(Passes, pass);
     }