1 files changed, 105 insertions, 81 deletions

diff --git a/lib/Core/ExecutionTree.h b/lib/Core/ExecutionTree.h
index ab3f0433..cd28a85c 100644
--- a/lib/Core/ExecutionTree.h
+++ b/lib/Core/ExecutionTree.h
@@ -1,4 +1,4 @@
-//===-- PTree.h -------------------------------------------------*- C++ -*-===//
+//===-- ExecutionTree.h -----------------------------------------*- C++ -*-===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
@@ -7,10 +7,10 @@
 //
 //===----------------------------------------------------------------------===//
 
-#ifndef KLEE_PTREE_H
-#define KLEE_PTREE_H
+#ifndef KLEE_EXECUTION_TREE_H
+#define KLEE_EXECUTION_TREE_H
 
-#include "PTreeWriter.h"
+#include "ExecutionTreeWriter.h"
 #include "UserSearcher.h"
 #include "klee/Core/BranchTypes.h"
 #include "klee/Core/TerminationTypes.h"
@@ -26,40 +26,41 @@
 namespace klee {
 class ExecutionState;
 class Executor;
-class InMemoryPTree;
+class InMemoryExecutionTree;
 class InterpreterHandler;
-class PTreeNode;
+class ExecutionTreeNode;
 class Searcher;
 
-/* PTreeNodePtr is used by the Random Path Searcher object to efficiently
-record which PTreeNode belongs to it. PTree is a global structure that
-captures all  states, whereas a Random Path Searcher might only care about
-a subset. The integer part of PTreeNodePtr is a bitmask (a "tag") of which
-Random Path Searchers PTreeNode belongs to. */
+/* ExecutionTreeNodePtr is used by the Random Path Searcher object to
+efficiently record which ExecutionTreeNode belongs to it. ExecutionTree is a
+global structure that captures all  states, whereas a Random Path Searcher might
+only care about a subset. The integer part of ExecutionTreeNodePtr is a bitmask
+(a "tag") of which Random Path Searchers ExecutionTreeNode belongs to. */
 constexpr std::uint8_t PtrBitCount = 3;
-using PTreeNodePtr = llvm::PointerIntPair<PTreeNode *, PtrBitCount, uint8_t>;
+using ExecutionTreeNodePtr =
+    llvm::PointerIntPair<ExecutionTreeNode *, PtrBitCount, uint8_t>;
 
-class PTreeNode {
+class ExecutionTreeNode {
 public:
   enum class NodeType : std::uint8_t { Basic, Annotated };
 
-  PTreeNode *parent{nullptr};
-  PTreeNodePtr left;
-  PTreeNodePtr right;
+  ExecutionTreeNode *parent{nullptr};
+  ExecutionTreeNodePtr left;
+  ExecutionTreeNodePtr right;
   ExecutionState *state{nullptr};
 
-  PTreeNode(PTreeNode *parent, ExecutionState *state) noexcept;
-  virtual ~PTreeNode() = default;
-  PTreeNode(const PTreeNode &) = delete;
-  PTreeNode &operator=(PTreeNode const &) = delete;
-  PTreeNode(PTreeNode &&) = delete;
-  PTreeNode &operator=(PTreeNode &&) = delete;
+  ExecutionTreeNode(ExecutionTreeNode *parent, ExecutionState *state) noexcept;
+  virtual ~ExecutionTreeNode() = default;
+  ExecutionTreeNode(const ExecutionTreeNode &) = delete;
+  ExecutionTreeNode &operator=(ExecutionTreeNode const &) = delete;
+  ExecutionTreeNode(ExecutionTreeNode &&) = delete;
+  ExecutionTreeNode &operator=(ExecutionTreeNode &&) = delete;
 
   [[nodiscard]] virtual NodeType getType() const { return NodeType::Basic; }
-  static bool classof(const PTreeNode *N) { return true; }
+  static bool classof(const ExecutionTreeNode *N) { return true; }
 };
 
-class AnnotatedPTreeNode : public PTreeNode {
+class AnnotatedExecutionTreeNode : public ExecutionTreeNode {
   inline static std::uint32_t nextID{1};
 
 public:
@@ -68,112 +69,135 @@ public:
   std::uint32_t asmLine{0};
   std::variant<BranchType, StateTerminationType> kind{BranchType::NONE};
 
-  AnnotatedPTreeNode(PTreeNode *parent, ExecutionState *state) noexcept;
-  ~AnnotatedPTreeNode() override = default;
+  AnnotatedExecutionTreeNode(ExecutionTreeNode *parent,
+                             ExecutionState *state) noexcept;
+  ~AnnotatedExecutionTreeNode() override = default;
 
   [[nodiscard]] NodeType getType() const override { return NodeType::Annotated; }
-  static bool classof(const PTreeNode *N) {
+
+  static bool classof(const ExecutionTreeNode *N) {
     return N->getType() == NodeType::Annotated;
   }
 };
 
-class PTree {
+class ExecutionTree {
 public:
-  enum class PTreeType : std::uint8_t { Basic, Noop, InMemory, Persistent };
-
-  /// Branch from PTreeNode and attach states, convention: rightState is
+  enum class ExecutionTreeType : std::uint8_t {
+    Basic,
+    Noop,
+    InMemory,
+    Persistent
+  };
+
+  /// Branch from ExecutionTreeNode and attach states, convention: rightState is
   /// parent
-  virtual void attach(PTreeNode *node, ExecutionState *leftState,
+  virtual void attach(ExecutionTreeNode *node, ExecutionState *leftState,
                       ExecutionState *rightState, BranchType reason) = 0;
-  /// Dump process tree in .dot format into os (debug)
+  /// Dump execution tree in .dot format into os (debug)
   virtual void dump(llvm::raw_ostream &os) = 0;
   /// Remove node from tree
-  virtual void remove(PTreeNode *node) = 0;
+  virtual void remove(ExecutionTreeNode *node) = 0;
   /// Set termination type (on state removal)
   virtual void setTerminationType(ExecutionState &state,
                                   StateTerminationType type){}
 
-  virtual ~PTree() = default;
-  PTree(PTree const &) = delete;
-  PTree &operator=(PTree const &) = delete;
-  PTree(PTree &&) = delete;
-  PTree &operator=(PTree &&) = delete;
+  virtual ~ExecutionTree() = default;
+  ExecutionTree(ExecutionTree const &) = delete;
+  ExecutionTree &operator=(ExecutionTree const &) = delete;
+  ExecutionTree(ExecutionTree &&) = delete;
+  ExecutionTree &operator=(ExecutionTree &&) = delete;
 
-  [[nodiscard]] virtual PTreeType getType() const = 0;
-  static bool classof(const PTreeNode *N) { return true; }
+  [[nodiscard]] virtual ExecutionTreeType getType() const = 0;
+  static bool classof(const ExecutionTreeNode *N) { return true; }
 
 protected:
-  explicit PTree() noexcept = default;
+  explicit ExecutionTree() noexcept = default;
 };
 
-/// @brief A pseudo process tree that does not maintain any nodes.
-class NoopPTree final : public PTree {
+/// @brief A pseudo execution tree that does not maintain any nodes.
+class NoopExecutionTree final : public ExecutionTree {
 public:
-  NoopPTree() noexcept = default;
-  ~NoopPTree() override = default;
-  void attach(PTreeNode *node, ExecutionState *leftState,
-              ExecutionState *rightState,
-              BranchType reason) noexcept override{}
+  NoopExecutionTree() noexcept = default;
+  ~NoopExecutionTree() override = default;
+  void attach(ExecutionTreeNode *node, ExecutionState *leftState,
+              ExecutionState *rightState, BranchType reason) noexcept override {}
   void dump(llvm::raw_ostream &os) noexcept override;
-  void remove(PTreeNode *node) noexcept override{}
+  void remove(ExecutionTreeNode *node) noexcept override {}
 
-  [[nodiscard]] PTreeType getType() const override { return PTreeType::Noop; };
-  static bool classof(const PTree *T) { return T->getType() == PTreeType::Noop; }
+  [[nodiscard]] ExecutionTreeType getType() const override {
+    return ExecutionTreeType::Noop;
+  };
+
+  static bool classof(const ExecutionTree *T) {
+    return T->getType() == ExecutionTreeType::Noop;
+  }
 };
 
-/// @brief An in-memory process tree required by RandomPathSearcher
-class InMemoryPTree : public PTree {
+/// @brief An in-memory execution tree required by RandomPathSearcher
+class InMemoryExecutionTree : public ExecutionTree {
 public:
-  PTreeNodePtr root;
+  ExecutionTreeNodePtr root;
 
 private:
   /// Number of registered IDs ("users", e.g. RandomPathSearcher)
   std::uint8_t registeredIds = 0;
 
-  virtual PTreeNode *createNode(PTreeNode *parent, ExecutionState *state);
-  virtual void updateBranchingNode(PTreeNode &node, BranchType reason){}
-  virtual void updateTerminatingNode(PTreeNode &node){}
+  virtual ExecutionTreeNode *createNode(ExecutionTreeNode *parent,
+                                        ExecutionState *state);
+  virtual void updateBranchingNode(ExecutionTreeNode &node, BranchType reason) {}
+  virtual void updateTerminatingNode(ExecutionTreeNode &node) {}
 
 public:
-  InMemoryPTree() noexcept = default;
-  explicit InMemoryPTree(ExecutionState &initialState) noexcept;
-  ~InMemoryPTree() override = default;
+  InMemoryExecutionTree() noexcept = default;
+  explicit InMemoryExecutionTree(ExecutionState &initialState) noexcept;
+  ~InMemoryExecutionTree() override = default;
 
-  void attach(PTreeNode *node, ExecutionState *leftState,
+  void attach(ExecutionTreeNode *node, ExecutionState *leftState,
               ExecutionState *rightState, BranchType reason) noexcept override;
   void dump(llvm::raw_ostream &os) noexcept override;
   std::uint8_t getNextId() noexcept;
-  void remove(PTreeNode *node) noexcept override;
+  void remove(ExecutionTreeNode *node) noexcept override;
 
-  [[nodiscard]] PTreeType getType() const override { return PTreeType::InMemory; };
-  static bool classof(const PTree *T) {
-    return (T->getType() == PTreeType::InMemory) || (T->getType() == PTreeType::Persistent);
+  [[nodiscard]] ExecutionTreeType getType() const override {
+    return ExecutionTreeType::InMemory;
+  };
+
+  static bool classof(const ExecutionTree *T) {
+    return (T->getType() == ExecutionTreeType::InMemory) ||
+           (T->getType() == ExecutionTreeType::Persistent);
   }
 };
 
-/// @brief An in-memory process tree that also writes its nodes into an SQLite
-/// database (ptree.db) with a PTreeWriter
-class PersistentPTree : public InMemoryPTree {
-  PTreeWriter writer;
+/// @brief An in-memory execution tree that also writes its nodes into an SQLite
+/// database (exec_tree.db) with a ExecutionTreeWriter
+class PersistentExecutionTree : public InMemoryExecutionTree {
+  ExecutionTreeWriter writer;
 
-  PTreeNode *createNode(PTreeNode *parent, ExecutionState *state) override;
-  void updateBranchingNode(PTreeNode &node, BranchType reason) override;
-  void updateTerminatingNode(PTreeNode &node) override;
+  ExecutionTreeNode *createNode(ExecutionTreeNode *parent,
+                                ExecutionState *state) override;
+  void updateBranchingNode(ExecutionTreeNode &node, BranchType reason) override;
+  void updateTerminatingNode(ExecutionTreeNode &node) override;
 
 public:
-  explicit PersistentPTree(ExecutionState &initialState,
-                           InterpreterHandler &ih) noexcept;
-  ~PersistentPTree() override = default;
+  explicit PersistentExecutionTree(ExecutionState &initialState,
+                                   InterpreterHandler &ih) noexcept;
+  ~PersistentExecutionTree() override = default;
   void dump(llvm::raw_ostream &os) noexcept override;
   void setTerminationType(ExecutionState &state,
                           StateTerminationType type) override;
 
-  [[nodiscard]] PTreeType getType() const override { return PTreeType::Persistent; };
-  static bool classof(const PTree *T) { return T->getType() == PTreeType::Persistent; }
+  [[nodiscard]] ExecutionTreeType getType() const override {
+    return ExecutionTreeType::Persistent;
+  };
+
+  static bool classof(const ExecutionTree *T) {
+    return T->getType() == ExecutionTreeType::Persistent;
+  }
 };
 
-std::unique_ptr<PTree> createPTree(ExecutionState &initialState, bool inMemory,
-                                   InterpreterHandler &ih);
+std::unique_ptr<ExecutionTree> createExecutionTree(ExecutionState &initialState,
+                                                   bool inMemory,
+                                                   InterpreterHandler &ih);
 } // namespace klee
 
-#endif /* KLEE_PTREE_H */
+#endif /* KLEE_EXECUTION_TREE_H */