Implemented support for C++ Exceptions

We implement the Itanium ABI unwinding base-API, and leave the
C++-specific parts to libcxxabi.

Co-authored-by: Lukas Wölfer <lukas.woelfer@rwth-aachen.de>

8 files changed, 570 insertions, 23 deletions

diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index 5dfabe9e..9004d706 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -106,6 +106,9 @@ ExecutionState::ExecutionState(const ExecutionState& state):
     openMergeStack(state.openMergeStack),
     steppedInstructions(state.steppedInstructions),
     instsSinceCovNew(state.instsSinceCovNew),
+    unwindingInformation(state.unwindingInformation
+                             ? state.unwindingInformation->cloned()
+                             : nullptr),
     coveredNew(state.coveredNew),
     forkDisabled(state.forkDisabled) {
   for (const auto &cur_mergehandler: openMergeStack)
diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h
index 7be69ea7..b3560caf 100644
--- a/lib/Core/ExecutionState.h
+++ b/lib/Core/ExecutionState.h
@@ -21,6 +21,7 @@
 #include "klee/System/Time.h"
 
 #include <map>
+#include <memory>
 #include <set>
 #include <vector>
 
@@ -63,6 +64,83 @@ struct StackFrame {
   ~StackFrame();
 };
 
+/// Contains information related to unwinding (Itanium ABI/2-Phase unwinding)
+struct UnwindingInformation {
+  enum class Kind {
+    SearchPhase, // first phase
+    CleanupPhase // second phase
+  };
+
+private:
+  const Kind kind;
+
+public:
+  // _Unwind_Exception* of the thrown exception, used in both phases
+  ref<ConstantExpr> exceptionObject;
+
+  Kind getKind() const { return kind; }
+
+  explicit UnwindingInformation(ref<ConstantExpr> exceptionObject, Kind k)
+      : kind(k), exceptionObject(exceptionObject) {}
+  virtual ~UnwindingInformation() = default;
+
+  virtual std::unique_ptr<UnwindingInformation> cloned() const = 0;
+};
+
+struct SearchPhaseUnwindingInformation : public UnwindingInformation {
+  // Keeps track of the stack index we have so far unwound to.
+  std::size_t unwindingProgress;
+
+  // MemoryObject that contains a serialized version of the last executed
+  // landingpad, so we can clean it up after the personality fn returns.
+  MemoryObject *serializedLandingpad = nullptr;
+
+  SearchPhaseUnwindingInformation(ref<ConstantExpr> exceptionObject,
+                                  std::size_t const unwindingProgress)
+      : UnwindingInformation(exceptionObject,
+                             UnwindingInformation::Kind::SearchPhase),
+        unwindingProgress(unwindingProgress) {}
+
+  std::unique_ptr<UnwindingInformation> cloned() const {
+    return std::make_unique<SearchPhaseUnwindingInformation>(*this);
+  }
+
+  static bool classof(const UnwindingInformation *u) {
+    return u->getKind() == UnwindingInformation::Kind::SearchPhase;
+  }
+};
+
+struct CleanupPhaseUnwindingInformation : public UnwindingInformation {
+  // Phase 1 will try to find a catching landingpad.
+  // Phase 2 will unwind up to this landingpad or return from
+  // _Unwind_RaiseException if none was found.
+
+  // The selector value of the catching landingpad that was found
+  // during the search phase.
+  ref<ConstantExpr> selectorValue;
+
+  // Used to know when we have to stop unwinding and to
+  // ensure that unwinding stops at the frame for which
+  // we first found a handler in the search phase.
+  const std::size_t catchingStackIndex;
+
+  CleanupPhaseUnwindingInformation(ref<ConstantExpr> exceptionObject,
+                                   ref<ConstantExpr> selectorValue,
+                                   const std::size_t catchingStackIndex)
+      : UnwindingInformation(exceptionObject,
+                             UnwindingInformation::Kind::CleanupPhase),
+        selectorValue(selectorValue),
+        catchingStackIndex(catchingStackIndex) {}
+
+  std::unique_ptr<UnwindingInformation> cloned() const {
+    return std::make_unique<CleanupPhaseUnwindingInformation>(*this);
+  }
+
+  static bool classof(const UnwindingInformation *u) {
+    return u->getKind() == UnwindingInformation::Kind::CleanupPhase;
+  }
+};
+
 /// @brief ExecutionState representing a path under exploration
 class ExecutionState {
 #ifdef KLEE_UNITTEST
@@ -141,6 +219,9 @@ public:
   /// instruction was covered.
   std::uint32_t instsSinceCovNew;
 
+  /// @brief Keep track of unwinding state while unwinding, otherwise empty
+  std::unique_ptr<UnwindingInformation> unwindingInformation;
+
   /// @brief the global state counter
   static std::uint32_t nextID;
 
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index de35710f..64dcee43 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -65,6 +65,7 @@
 #include "llvm/IR/IntrinsicInst.h"
 #include "llvm/IR/LLVMContext.h"
 #include "llvm/IR/Module.h"
+#include "llvm/IR/Operator.h"
 #include "llvm/Support/CommandLine.h"
 #include "llvm/Support/ErrorHandling.h"
 #include "llvm/Support/FileSystem.h"
@@ -80,10 +81,12 @@ typedef unsigned TypeSize;
 #include <algorithm>
 #include <cassert>
 #include <cerrno>
+#include <cstring>
 #include <cxxabi.h>
 #include <fstream>
 #include <iomanip>
 #include <iosfwd>
+#include <limits>
 #include <sstream>
 #include <string>
 #include <sys/mman.h>
@@ -284,6 +287,10 @@ cl::list<Executor::TerminateReason> ExitOnErrorType(
         clEnumValN(Executor::ReportError, "ReportError",
                    "klee_report_error called"),
         clEnumValN(Executor::User, "User", "Wrong klee_* functions invocation"),
+        clEnumValN(Executor::UncaughtException, "UncaughtException",
+                   "Exception was not caught"),
+        clEnumValN(Executor::UnexpectedException, "UnexpectedException",
+                   "An unexpected exception was thrown"),
         clEnumValN(Executor::Unhandled, "Unhandled",
                    "Unhandled instruction hit") KLEE_LLVM_CL_VAL_END),
     cl::ZeroOrMore,
@@ -433,6 +440,8 @@ const char *Executor::TerminateReasonNames[] = {
   [ ReadOnly ] = "readonly",
   [ ReportError ] = "reporterror",
   [ User ] = "user",
+  [ UncaughtException ] = "uncaught_exception",
+  [ UnexpectedException ] = "unexpected_exception",
   [ Unhandled ] = "xxx",
 };
 
@@ -1407,6 +1416,235 @@ static inline const llvm::fltSemantics *fpWidthToSemantics(unsigned width) {
   }
 }
 
+MemoryObject *Executor::serializeLandingpad(ExecutionState &state,
+                                            const llvm::LandingPadInst &lpi,
+                                            bool &stateTerminated) {
+  stateTerminated = false;
+
+  std::vector<unsigned char> serialized;
+
+  for (unsigned current_clause_id = 0; current_clause_id < lpi.getNumClauses();
+       ++current_clause_id) {
+    llvm::Constant *current_clause = lpi.getClause(current_clause_id);
+    if (lpi.isCatch(current_clause_id)) {
+      // catch-clause
+      serialized.push_back(0);
+
+      std::uint64_t ti_addr = 0;
+
+      llvm::BitCastOperator *clause_bitcast =
+          dyn_cast<llvm::BitCastOperator>(current_clause);
+      if (clause_bitcast) {
+        llvm::GlobalValue *clause_type =
+            dyn_cast<GlobalValue>(clause_bitcast->getOperand(0));
+
+        ti_addr = globalAddresses[clause_type]->getZExtValue();
+      } else if (current_clause->isNullValue()) {
+        ti_addr = 0;
+      } else {
+        terminateStateOnError(
+            state, "Internal: Clause is not a bitcast or null (catch-all)",
+            Exec);
+        stateTerminated = true;
+        return nullptr;
+      }
+      const std::size_t old_size = serialized.size();
+      serialized.resize(old_size + 8);
+      memcpy(serialized.data() + old_size, &ti_addr, sizeof(ti_addr));
+    } else if (lpi.isFilter(current_clause_id)) {
+      if (current_clause->isNullValue()) {
+        // special handling for a catch-all filter clause, i.e., "[0 x i8*]"
+        // for this case we serialize 1 element..
+        serialized.push_back(1);
+        // which is a 64bit-wide 0.
+        serialized.resize(serialized.size() + 8, 0);
+      } else {
+        llvm::ConstantArray const *ca =
+            cast<llvm::ConstantArray>(current_clause);
+
+        // serialize `num_elements+1` as unsigned char
+        unsigned const num_elements = ca->getNumOperands();
+        unsigned char serialized_num_elements = 0;
+
+        if (num_elements >=
+            std::numeric_limits<decltype(serialized_num_elements)>::max()) {
+          terminateStateOnError(
+              state, "Internal: too many elements in landingpad filter", Exec);
+          stateTerminated = true;
+          return nullptr;
+        }
+
+        serialized_num_elements = num_elements;
+        serialized.push_back(serialized_num_elements + 1);
+
+        // serialize the exception-types occurring in this filter-clause
+        for (llvm::Value const *v : ca->operands()) {
+          llvm::BitCastOperator const *bitcast =
+              dyn_cast<llvm::BitCastOperator>(v);
+          if (!bitcast) {
+            terminateStateOnError(state,
+                                  "Internal: expected value inside a "
+                                  "filter-clause to be a bitcast",
+                                  Exec);
+            stateTerminated = true;
+            return nullptr;
+          }
+
+          llvm::GlobalValue const *clause_value =
+              dyn_cast<GlobalValue>(bitcast->getOperand(0));
+          if (!clause_value) {
+            terminateStateOnError(state,
+                                  "Internal: expected value inside a "
+                                  "filter-clause bitcast to be a GlobalValue",
+                                  Exec);
+            stateTerminated = true;
+            return nullptr;
+          }
+
+          std::uint64_t const ti_addr =
+              globalAddresses[clause_value]->getZExtValue();
+
+          const std::size_t old_size = serialized.size();
+          serialized.resize(old_size + 8);
+          memcpy(serialized.data() + old_size, &ti_addr, sizeof(ti_addr));
+        }
+      }
+    }
+  }
+
+  MemoryObject *mo =
+      memory->allocate(serialized.size(), true, false, nullptr, 1);
+  ObjectState *os = bindObjectInState(state, mo, false);
+  for (unsigned i = 0; i < serialized.size(); i++) {
+    os->write8(i, serialized[i]);
+  }
+
+  return mo;
+}
+
+void Executor::unwindToNextLandingpad(ExecutionState &state) {
+  UnwindingInformation *ui = state.unwindingInformation.get();
+  assert(ui && "unwinding without unwinding information");
+
+  std::size_t startIndex;
+  std::size_t lowestStackIndex;
+  bool popFrames;
+
+  if (auto *sui = dyn_cast<SearchPhaseUnwindingInformation>(ui)) {
+    startIndex = sui->unwindingProgress;
+    lowestStackIndex = 0;
+    popFrames = false;
+  } else if (auto *cui = dyn_cast<CleanupPhaseUnwindingInformation>(ui)) {
+    startIndex = state.stack.size() - 1;
+    lowestStackIndex = cui->catchingStackIndex;
+    popFrames = true;
+  } else {
+    assert(false && "invalid UnwindingInformation subclass");
+  }
+
+  for (std::size_t i = startIndex; i > lowestStackIndex; i--) {
+    auto const &sf = state.stack.at(i);
+
+    Instruction *inst = sf.caller ? sf.caller->inst : nullptr;
+
+    if (popFrames) {
+      state.popFrame();
+      if (statsTracker != nullptr) {
+        statsTracker->framePopped(state);
+      }
+    }
+
+    if (InvokeInst *invoke = dyn_cast<InvokeInst>(inst)) {
+      // we found the next invoke instruction in the call stack, handle it
+      // depending on the current phase.
+      if (auto *sui = dyn_cast<SearchPhaseUnwindingInformation>(ui)) {
+        // in the search phase, run personality function to check if this
+        // landingpad catches the exception
+
+        LandingPadInst *lpi = invoke->getUnwindDest()->getLandingPadInst();
+        assert(lpi && "unwind target of an invoke instruction did not lead to "
+                      "a landingpad");
+
+        // check if this is a pure cleanup landingpad first
+        if (lpi->isCleanup() && lpi->getNumClauses() == 0) {
+          // pure cleanup lpi, this can't be a handler, so skip it
+          continue;
+        }
+
+        bool stateTerminated = false;
+        MemoryObject *clauses_mo =
+            serializeLandingpad(state, *lpi, stateTerminated);
+        assert((stateTerminated != bool(clauses_mo)) &&
+               "illegal serializeLandingpad result");
+
+        if (stateTerminated) {
+          return;
+        }
+
+        assert(sui->serializedLandingpad == nullptr &&
+               "serializedLandingpad should be reset");
+        sui->serializedLandingpad = clauses_mo;
+
+        llvm::Function *personality_fn =
+            kmodule->module->getFunction("_klee_eh_cxx_personality");
+        KFunction *kf = kmodule->functionMap[personality_fn];
+
+        state.pushFrame(state.prevPC, kf);
+        state.pc = kf->instructions;
+        bindArgument(kf, 0, state, sui->exceptionObject);
+        bindArgument(kf, 1, state, clauses_mo->getSizeExpr());
+        bindArgument(kf, 2, state, clauses_mo->getBaseExpr());
+
+        if (statsTracker) {
+          statsTracker->framePushed(state,
+                                    &state.stack[state.stack.size() - 2]);
+        }
+
+        // make sure we remember our search progress afterwards
+        sui->unwindingProgress = i - 1;
+      } else {
+        // in the cleanup phase, redirect control flow
+        transferToBasicBlock(invoke->getUnwindDest(), invoke->getParent(),
+                             state);
+      }
+
+      // we are done, stop search/unwinding here
+      return;
+    }
+  }
+
+  // no further invoke instruction/landingpad found
+  if (isa<SearchPhaseUnwindingInformation>(ui)) {
+    // in phase 1, simply stop unwinding. this will return
+    // control flow back to _Unwind_RaiseException, which will
+    // return the correct error.
+
+    // clean up unwinding state
+    state.unwindingInformation.reset();
+  } else {
+    // in phase 2, this represent a situation that should
+    // not happen, as we only progressed to phase 2 because
+    // we found a handler in phase 1.
+    // therefore terminate the state.
+    terminateStateOnExecError(state,
+                              "Missing landingpad in phase 2 of unwinding");
+  }
+}
+
+ref<klee::ConstantExpr> Executor::getEhTypeidFor(ref<Expr> type_info) {
+  auto eh_type_iterator =
+      std::find(std::begin(eh_typeids), std::end(eh_typeids), type_info);
+  if (eh_type_iterator == std::end(eh_typeids)) {
+    eh_typeids.push_back(type_info);
+    eh_type_iterator = std::prev(std::end(eh_typeids));
+  }
+  // +1 because typeids must always be positive, so they can be distinguished
+  // from 'no landingpad clause matched' which has value 0
+  auto res = ConstantExpr::create(eh_type_iterator - std::begin(eh_typeids) + 1,
+                                  Expr::Int32);
+  return res;
+}
+
 void Executor::executeCall(ExecutionState &state, KInstruction *ki, Function *f,
                            std::vector<ref<Expr>> &arguments) {
   Instruction *i = ki->inst;
@@ -1500,6 +1738,12 @@ void Executor::executeCall(ExecutionState &state, KInstruction *ki, Function *f,
       }
       break;
     }
+
+    case Intrinsic::eh_typeid_for: {
+      bindLocal(ki, state, getEhTypeidFor(arguments.at(0)));
+      break;
+    }
+
     case Intrinsic::vaend:
       // va_end is a noop for the interpreter.
       //
@@ -1518,8 +1762,15 @@ void Executor::executeCall(ExecutionState &state, KInstruction *ki, Function *f,
       return;
     }
 
-    if (InvokeInst *ii = dyn_cast<InvokeInst>(i))
-      transferToBasicBlock(ii->getNormalDest(), i->getParent(), state);
+    // __cxa_throw & _rethrow are already handled in their
+    // SpecialFunctionHandlers and have already been redirected to their unwind
+    // destinations, so we must not transfer them to their regular targets.
+    if (InvokeInst *ii = dyn_cast<InvokeInst>(i)) {
+      if (f->getName() != std::string("__cxa_throw") &&
+          f->getName() != std::string("__cxa_rethrow")) {
+        transferToBasicBlock(ii->getNormalDest(), i->getParent(), state);
+      }
+    }
   } else {
     // Check if maximum stack size was reached.
     // We currently only count the number of stack frames
@@ -1747,6 +1998,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     Instruction *caller = kcaller ? kcaller->inst : 0;
     bool isVoidReturn = (ri->getNumOperands() == 0);
     ref<Expr> result = ConstantExpr::alloc(0, Expr::Bool);
+    bool isReturnFromPersonalityFn =
+        ri->getFunction()->getName() == "_klee_eh_cxx_personality";
     
     if (!isVoidReturn) {
       result = eval(ki, 0, state).value;
@@ -1768,6 +2021,40 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
         ++state.pc;
       }
 
+      if (isReturnFromPersonalityFn) {
+        assert(dyn_cast<ConstantExpr>(result) &&
+               "result from personality fn must be a concrete value");
+
+        auto *sui = dyn_cast_or_null<SearchPhaseUnwindingInformation>(
+            state.unwindingInformation.get());
+        assert(sui && "return from personality function outside of "
+                      "search phase unwinding");
+
+        // unbind the MO we used to pass the serialized landingpad
+        state.addressSpace.unbindObject(sui->serializedLandingpad);
+        sui->serializedLandingpad = nullptr;
+
+        if (result->isZero()) {
+          // this lpi doesn't handle the exception, continue the search
+          unwindToNextLandingpad(state);
+        } else {
+          // a clause (or a catch-all clause or filter clause) matches:
+          // remember the stack index and switch to cleanup phase
+          state.unwindingInformation =
+              std::make_unique<CleanupPhaseUnwindingInformation>(
+                  sui->exceptionObject, cast<ConstantExpr>(result),
+                  sui->unwindingProgress);
+          // this pointer is now invalidated
+          sui = nullptr;
+          // continue the unwinding process (which will now start with the
+          // cleanup phase)
+          unwindToNextLandingpad(state);
+        }
+
+        // never return normally from the personality fn
+        break;
+      }
+
       if (!isVoidReturn) {
         Type *t = caller->getType();
         if (t != Type::getVoidTy(i->getContext())) {
@@ -2858,6 +3145,79 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     // instructions.
     terminateStateOnExecError(state, "Unexpected ShuffleVector instruction");
     break;
+
+  case Instruction::Resume: {
+    auto *cui = dyn_cast_or_null<CleanupPhaseUnwindingInformation>(
+        state.unwindingInformation.get());
+
+    if (!cui) {
+      terminateStateOnExecError(
+          state,
+          "resume-instruction executed outside of cleanup phase unwinding");
+      break;
+    }
+
+    ref<Expr> arg = eval(ki, 0, state).value;
+    ref<Expr> expPtr = ExtractExpr::create(arg, 0, Expr::Int64);
+    ref<Expr> selector = ExtractExpr::create(arg, Expr::Int64, Expr::Int32);
+
+    if (!Expr::createIsZero(selector)->isTrue()) {
+      llvm::errs() << "resume-instruction called with non-0 selector value '"
+                   << selector << "'\n";
+    }
+
+    if (!EqExpr::create(expPtr, cui->exceptionObject)->isTrue()) {
+      terminateStateOnExecError(
+          state, "resume-instruction called with unexpected exception pointer");
+      break;
+    }
+
+    unwindToNextLandingpad(state);
+    break;
+  }
+
+  case Instruction::LandingPad: {
+    auto *cui = dyn_cast_or_null<CleanupPhaseUnwindingInformation>(
+        state.unwindingInformation.get());
+
+    if (!cui) {
+      terminateStateOnExecError(
+          state, "Executing landing pad but not in unwinding phase 2");
+      break;
+    }
+
+    ref<ConstantExpr> exceptionPointer = cui->exceptionObject;
+    ref<ConstantExpr> selectorValue;
+
+    // check on which frame we are currently
+    if (state.stack.size() - 1 == cui->catchingStackIndex) {
+      // we are in the target stack frame, return the selector value
+      // that was returned by the personality fn in phase 1 and stop unwinding.
+      selectorValue = cui->selectorValue;
+
+      // stop unwinding by cleaning up our unwinding information.
+      state.unwindingInformation.reset();
+
+      // this would otherwise now be a dangling pointer
+      cui = nullptr;
+    } else {
+      // we are not yet at the target stack frame. the landingpad might have
+      // a cleanup clause or not, anyway, we give it the selector value "0",
+      // which represents a cleanup, and expect it to handle it.
+      // This is explicitly allowed by LLVM, see
+      // https://llvm.org/docs/ExceptionHandling.html#id18
+      selectorValue = ConstantExpr::create(0, Expr::Int32);
+    }
+
+    // we have to return a {i8*, i32}
+    ref<Expr> result = ConcatExpr::create(
+        ZExtExpr::create(selectorValue, Expr::Int32), exceptionPointer);
+
+    bindLocal(ki, state, result);
+
+    break;
+  }
+
   case Instruction::AtomicRMW:
     terminateStateOnExecError(state, "Unexpected Atomic instruction, should be "
                                      "lowered by LowerAtomicInstructionPass");
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 25a874cd..30d1dd92 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -42,6 +42,7 @@ namespace llvm {
   class BasicBlock;
   class BranchInst;
   class CallInst;
+  class LandingPadInst;
   class Constant;
   class ConstantExpr;
   class Function;
@@ -109,7 +110,9 @@ public:
     ReadOnly,
     ReportError,
     User,
-    Unhandled
+    UncaughtException,
+    UnexpectedException,
+    Unhandled,
   };
 
   /// The random number generator.
@@ -219,6 +222,12 @@ private:
   /// `nullptr` if merging is disabled
   MergingSearcher *mergingSearcher = nullptr;
 
+  /// Typeids used during exception handling
+  std::vector<ref<Expr>> eh_typeids;
+
+  /// Return the typeid corresponding to a certain `type_info`
+  ref<ConstantExpr> getEhTypeidFor(ref<Expr> type_info);
+
   llvm::Function* getTargetFunction(llvm::Value *calledVal,
                                     ExecutionState &state);
   
@@ -304,7 +313,17 @@ private:
   void executeFree(ExecutionState &state,
                    ref<Expr> address,
                    KInstruction *target = 0);
-  
+
+  /// Serialize a landingpad instruction so it can be handled by the
+  /// libcxxabi-runtime
+  MemoryObject *serializeLandingpad(ExecutionState &state,
+                                    const llvm::LandingPadInst &lpi,
+                                    bool &stateTerminated);
+
+  /// Unwind the given state until it hits a landingpad. This is used
+  /// for exception handling.
+  void unwindToNextLandingpad(ExecutionState &state);
+
   void executeCall(ExecutionState &state, 
                    KInstruction *ki,
                    llvm::Function *f,
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index 57f059a4..a36d4324 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -15,6 +15,7 @@
 #include "MemoryManager.h"
 #include "MergeHandler.h"
 #include "Searcher.h"
+#include "StatsTracker.h"
 #include "TimingSolver.h"
 
 #include "klee/Module/KInstruction.h"
@@ -26,6 +27,7 @@
 
 #include "llvm/ADT/Twine.h"
 #include "llvm/IR/DataLayout.h"
+#include "llvm/IR/Instructions.h"
 #include "llvm/IR/Module.h"
 
 #include <errno.h>
@@ -112,6 +114,7 @@ static SpecialFunctionHandler::HandlerInfo handlerInfo[] = {
   add("malloc", handleMalloc, true),
   add("memalign", handleMemalign, true),
   add("realloc", handleRealloc, true),
+  add("_klee_eh_Unwind_RaiseException_impl", handleEhUnwindRaiseExceptionImpl, false),
 
   // operator delete[](void*)
   add("_ZdaPv", handleDeleteArray, false),
@@ -136,6 +139,7 @@ static SpecialFunctionHandler::HandlerInfo handlerInfo[] = {
   add("__ubsan_handle_sub_overflow", handleSubOverflow, false),
   add("__ubsan_handle_mul_overflow", handleMulOverflow, false),
   add("__ubsan_handle_divrem_overflow", handleDivRemOverflow, false),
+  add("klee_eh_typeid_for", handleEhTypeid, true),
 
 #undef addDNR
 #undef add
@@ -453,6 +457,52 @@ void SpecialFunctionHandler::handleMemalign(ExecutionState &state,
                         alignment);
 }
 
+void SpecialFunctionHandler::handleEhUnwindRaiseExceptionImpl(
+    ExecutionState &state, KInstruction *target,
+    std::vector<ref<Expr>> &arguments) {
+  if (arguments.size() != 1) {
+    executor.terminateStateOnError(
+        state,
+        "Internal Error: Incorrect number of arguments to "
+        "_klee_eh_Unwind_RaiseException_impl, "
+        "should not happen",
+        Executor::Unhandled);
+    return;
+  }
+
+  ref<ConstantExpr> exceptionObject = dyn_cast<ConstantExpr>(arguments[0]);
+  if (!exceptionObject.get()) {
+    executor.terminateStateOnError(state,
+                                   "Internal error: Symbolic exception pointer",
+                                   Executor::Unhandled);
+    return;
+  }
+
+  if (isa_and_nonnull<SearchPhaseUnwindingInformation>(
+          state.unwindingInformation)) {
+    executor.terminateStateOnError(
+        state,
+        "Internal error: Unwinding restarted during an ongoing search phase",
+        Executor::Unhandled);
+    return;
+  }
+
+  state.unwindingInformation =
+      std::make_unique<SearchPhaseUnwindingInformation>(exceptionObject,
+                                                        state.stack.size() - 1);
+
+  executor.unwindToNextLandingpad(state);
+}
+
+void SpecialFunctionHandler::handleEhTypeid(ExecutionState &state,
+                                            KInstruction *target,
+                                            std::vector<ref<Expr>> &arguments) {
+  assert(arguments.size() == 1 &&
+         "invalid number of arguments to klee_eh_typeid_for");
+
+  executor.bindLocal(target, state, executor.getEhTypeidFor(arguments[0]));
+}
+
 void SpecialFunctionHandler::handleAssume(ExecutionState &state,
                             KInstruction *target,
                             std::vector<ref<Expr> > &arguments) {
diff --git a/lib/Core/SpecialFunctionHandler.h b/lib/Core/SpecialFunctionHandler.h
index 0ad04049..3db650d7 100644
--- a/lib/Core/SpecialFunctionHandler.h
+++ b/lib/Core/SpecialFunctionHandler.h
@@ -119,6 +119,8 @@ namespace klee {
     HANDLER(handleMakeSymbolic);
     HANDLER(handleMalloc);
     HANDLER(handleMemalign);
+    HANDLER(handleEhUnwindRaiseExceptionImpl);
+    HANDLER(handleEhTypeid);
     HANDLER(handleMarkGlobal);
     HANDLER(handleOpenMerge);
     HANDLER(handleCloseMerge);
diff --git a/lib/Module/IntrinsicCleaner.cpp b/lib/Module/IntrinsicCleaner.cpp
index 030a75ca..cd93b3ec 100644
--- a/lib/Module/IntrinsicCleaner.cpp
+++ b/lib/Module/IntrinsicCleaner.cpp
@@ -364,7 +364,6 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b, Module &M) {
 #if LLVM_VERSION_CODE >= LLVM_VERSION(7, 0)
       case Intrinsic::dbg_label:
 #endif
-      case Intrinsic::eh_typeid_for:
       case Intrinsic::exp2:
       case Intrinsic::exp:
       case Intrinsic::expect:
@@ -400,6 +399,11 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b, Module &M) {
         dirty = true;
         break;
 
+      case Intrinsic::eh_typeid_for: {
+        // Don't lower this, we need it for exception handling
+        break;
+      }
+
         // Warn about any unrecognized intrinsics.
       default: {
         const Function *Callee = ii->getCalledFunction();
diff --git a/lib/Module/ModuleUtil.cpp b/lib/Module/ModuleUtil.cpp
index f4cc3048..2316ef45 100644
--- a/lib/Module/ModuleUtil.cpp
+++ b/lib/Module/ModuleUtil.cpp
@@ -203,41 +203,69 @@ klee::linkModules(std::vector<std::unique_ptr<llvm::Module>> &modules,
     return nullptr;
   }
 
-  while (true) {
+  auto containsUsedSymbols = [](const llvm::Module *module) {
+    GlobalValue *GV =
+        dyn_cast_or_null<GlobalValue>(module->getNamedValue("llvm.used"));
+    if (!GV)
+      return false;
+    KLEE_DEBUG_WITH_TYPE("klee_linker", dbgs() << "Used attribute in "
+                                               << module->getModuleIdentifier()
+                                               << '\n');
+    return true;
+  };
+
+  for (auto &module : modules) {
+    if (!module || !containsUsedSymbols(module.get()))
+      continue;
+    if (!linkTwoModules(composite.get(), std::move(module), errorMsg)) {
+      // Linking failed
+      errorMsg = "Linking module containing '__attribute__((used))'"
+                 " symbols with composite failed:" +
+                 errorMsg;
+      return nullptr;
+    }
+    module = nullptr;
+  }
+
+  bool symbolsLinked = true;
+  while (symbolsLinked) {
+    symbolsLinked = false;
     std::set<std::string> undefinedSymbols;
     GetAllUndefinedSymbols(composite.get(), undefinedSymbols);
+    auto hasRequiredDefinition = [&undefinedSymbols](
+                                     const llvm::Module *module) {
+      for (auto symbol : undefinedSymbols) {
+        GlobalValue *GV =
+            dyn_cast_or_null<GlobalValue>(module->getNamedValue(symbol));
+        if (GV && !GV->isDeclaration()) {
+          KLEE_DEBUG_WITH_TYPE("klee_linker",
+                               dbgs() << "Found " << GV->getName() << " in "
+                                      << module->getModuleIdentifier() << "\n");
+          return true;
+        }
+      }
+      return false;
+    };
 
     // Stop in nothing is undefined
     if (undefinedSymbols.empty())
       break;
 
-    bool merged = false;
     for (auto &module : modules) {
       if (!module)
         continue;
 
-      for (auto symbol : undefinedSymbols) {
-        GlobalValue *GV =
-            dyn_cast_or_null<GlobalValue>(module->getNamedValue(symbol));
-        if (!GV || GV->isDeclaration())
-          continue;
+      if (!hasRequiredDefinition(module.get()))
+        continue;
 
-        // 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;
-        }
+      if (!linkTwoModules(composite.get(), std::move(module), errorMsg)) {
         // Linking failed
         errorMsg = "Linking archive module with composite failed:" + errorMsg;
         return nullptr;
       }
+      module = nullptr;
+      symbolsLinked = true;
     }
-    if (!merged)
-      break;
   }
 
   // Condense the module array