about summary refs log tree commit diff homepage
path: root/lib/Core/SpecialFunctionHandler.cpp
diff options
context:
space:
mode:
authorFelix Rath <felix.rath@comsys.rwth-aachen.de>2020-05-22 14:09:10 +0200
committerMartinNowack <2443641+MartinNowack@users.noreply.github.com>2020-10-12 11:19:24 +0100
commitc09306ffd894f95be195723327d5b17dca73ebd1 (patch)
tree592773383280012bce8856b28503ab61de0deb98 /lib/Core/SpecialFunctionHandler.cpp
parentd920e049fa955877f772188fdc58cab1b31aabc9 (diff)
downloadklee-c09306ffd894f95be195723327d5b17dca73ebd1.tar.gz
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>
Diffstat (limited to 'lib/Core/SpecialFunctionHandler.cpp')
-rw-r--r--lib/Core/SpecialFunctionHandler.cpp50
1 files changed, 50 insertions, 0 deletions
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) {