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.

1 files changed, 294 insertions, 412 deletions

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