From c09306ffd894f95be195723327d5b17dca73ebd1 Mon Sep 17 00:00:00 2001
From: Felix Rath <felix.rath@comsys.rwth-aachen.de>
Date: Fri, 22 May 2020 14:09:10 +0200
Subject: Implemented support for C++ Exceptions
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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>
---
 lib/Core/SpecialFunctionHandler.cpp | 50 +++++++++++++++++++++++++++++++++++++
 1 file changed, 50 insertions(+)

(limited to 'lib/Core/SpecialFunctionHandler.cpp')

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) {
-- 
cgit 1.4.1