Reorder linking and optimizations

Link intrinsic library before executing optimizations.
This makes sure that any optimization run by KLEE on the module
is executed for the intrinsic library as well.

Support .ll files as input for KLEE as well.

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);
     }