1 files changed, 81 insertions, 0 deletions
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;