4 files changed, 24 insertions, 21 deletions

diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index 9004d706..62376db6 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -107,7 +107,7 @@ ExecutionState::ExecutionState(const ExecutionState& state):
     steppedInstructions(state.steppedInstructions),
     instsSinceCovNew(state.instsSinceCovNew),
     unwindingInformation(state.unwindingInformation
-                             ? state.unwindingInformation->cloned()
+                             ? state.unwindingInformation->clone()
                              : nullptr),
     coveredNew(state.coveredNew),
     forkDisabled(state.forkDisabled) {
diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h
index b3560caf..f91790d5 100644
--- a/lib/Core/ExecutionState.h
+++ b/lib/Core/ExecutionState.h
@@ -65,7 +65,8 @@ struct StackFrame {
 };
 
 /// Contains information related to unwinding (Itanium ABI/2-Phase unwinding)
-struct UnwindingInformation {
+class UnwindingInformation {
+public:
   enum class Kind {
     SearchPhase, // first phase
     CleanupPhase // second phase
@@ -84,7 +85,7 @@ public:
       : kind(k), exceptionObject(exceptionObject) {}
   virtual ~UnwindingInformation() = default;
 
-  virtual std::unique_ptr<UnwindingInformation> cloned() const = 0;
+  virtual std::unique_ptr<UnwindingInformation> clone() const = 0;
 };
 
 struct SearchPhaseUnwindingInformation : public UnwindingInformation {
@@ -101,7 +102,7 @@ struct SearchPhaseUnwindingInformation : public UnwindingInformation {
                              UnwindingInformation::Kind::SearchPhase),
         unwindingProgress(unwindingProgress) {}
 
-  std::unique_ptr<UnwindingInformation> cloned() const {
+  std::unique_ptr<UnwindingInformation> clone() const {
     return std::make_unique<SearchPhaseUnwindingInformation>(*this);
   }
 
@@ -132,7 +133,7 @@ struct CleanupPhaseUnwindingInformation : public UnwindingInformation {
         selectorValue(selectorValue),
         catchingStackIndex(catchingStackIndex) {}
 
-  std::unique_ptr<UnwindingInformation> cloned() const {
+  std::unique_ptr<UnwindingInformation> clone() const {
     return std::make_unique<CleanupPhaseUnwindingInformation>(*this);
   }
 
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 64dcee43..2e6f9c89 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -1632,6 +1632,8 @@ void Executor::unwindToNextLandingpad(ExecutionState &state) {
 }
 
 ref<klee::ConstantExpr> Executor::getEhTypeidFor(ref<Expr> type_info) {
+  // FIXME: Handling getEhTypeidFor is non-deterministic and depends on the
+  //        order states have been processed and executed.
   auto eh_type_iterator =
       std::find(std::begin(eh_typeids), std::end(eh_typeids), type_info);
   if (eh_type_iterator == std::end(eh_typeids)) {
@@ -1998,8 +2000,6 @@ 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;
@@ -2021,7 +2021,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
         ++state.pc;
       }
 
-      if (isReturnFromPersonalityFn) {
+      if (ri->getFunction()->getName() == "_klee_eh_cxx_personality") {
         assert(dyn_cast<ConstantExpr>(result) &&
                "result from personality fn must be a concrete value");
 
@@ -3158,15 +3158,22 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     }
 
     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);
+    ref<Expr> exceptionPointer = ExtractExpr::create(arg, 0, Expr::Int64);
+    ref<Expr> selectorValue =
+        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 (!dyn_cast<ConstantExpr>(exceptionPointer) ||
+        !dyn_cast<ConstantExpr>(selectorValue)) {
+      terminateStateOnExecError(
+          state, "resume-instruction called with non constant expression");
+      break;
+    }
+
+    if (!Expr::createIsZero(selectorValue)->isTrue()) {
+      klee_warning("resume-instruction called with non-0 selector value");
     }
 
-    if (!EqExpr::create(expPtr, cui->exceptionObject)->isTrue()) {
+    if (!EqExpr::create(exceptionPointer, cui->exceptionObject)->isTrue()) {
       terminateStateOnExecError(
           state, "resume-instruction called with unexpected exception pointer");
       break;
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index 7144e235..6d54eb22 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -460,13 +460,8 @@ void SpecialFunctionHandler::handleMemalign(ExecutionState &state,
 void SpecialFunctionHandler::handleEhUnwindRaiseExceptionImpl(
     ExecutionState &state, KInstruction *target,
     std::vector<ref<Expr>> &arguments) {
-  if (arguments.size() != 1) {
-    executor.terminateStateOnExecError(
-        state, "Internal Error: Incorrect number of arguments to "
-               "_klee_eh_Unwind_RaiseException_impl, "
-               "should not happen");
-    return;
-  }
+  assert(arguments.size() == 1 &&
+         "invalid number of arguments to _klee_eh_Unwind_RaiseException_impl");
 
   ref<ConstantExpr> exceptionObject = dyn_cast<ConstantExpr>(arguments[0]);
   if (!exceptionObject.get()) {