new: persistent ptree (-write-ptree) and klee-ptree

Introduce three different kinds of process trees:
1. Noop: does nothing (e.g. no allocations for DFS)
2. InMemory: same behaviour as before (e.g. RandomPathSearcher)
3. Persistent: similar to InMemory but writes nodes to ptree.db
     and tracks information such as branch type, termination
     type or source location (asm) in nodes. Enabled with
     -write-ptree

ptree.db files can be analysed/plotted with the new "klee-ptree"
tool.

10 files changed, 720 insertions, 1 deletions

diff --git a/tools/CMakeLists.txt b/tools/CMakeLists.txt
index b641885c..40089c40 100644
--- a/tools/CMakeLists.txt
+++ b/tools/CMakeLists.txt
@@ -10,6 +10,7 @@ add_subdirectory(ktest-gen)
 add_subdirectory(ktest-randgen)
 add_subdirectory(kleaver)
 add_subdirectory(klee)
+add_subdirectory(klee-ptree)
 add_subdirectory(klee-replay)
 add_subdirectory(klee-stats)
 add_subdirectory(klee-zesti)
diff --git a/tools/klee-ptree/CMakeLists.txt b/tools/klee-ptree/CMakeLists.txt
new file mode 100644
index 00000000..b5c3fa09
--- /dev/null
+++ b/tools/klee-ptree/CMakeLists.txt
@@ -0,0 +1,16 @@
+#===------------------------------------------------------------------------===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+
+add_executable(klee-ptree main.cpp Tree.cpp DFSVisitor.cpp Printers.cpp)
+
+target_compile_features(klee-ptree PRIVATE cxx_std_17)
+target_include_directories(klee-ptree PRIVATE ${KLEE_INCLUDE_DIRS} ${SQLite3_INCLUDE_DIRS})
+target_link_libraries(klee-ptree PUBLIC ${SQLite3_LIBRARIES})
+
+install(TARGETS klee-ptree DESTINATION bin)
diff --git a/tools/klee-ptree/DFSVisitor.cpp b/tools/klee-ptree/DFSVisitor.cpp
new file mode 100644
index 00000000..c87afc3e
--- /dev/null
+++ b/tools/klee-ptree/DFSVisitor.cpp
@@ -0,0 +1,46 @@
+//===-- DFSVisitor.cpp ------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "DFSVisitor.h"
+
+#include <utility>
+
+DFSVisitor::DFSVisitor(const Tree &tree, callbackT cb_intermediate,
+                       callbackT cb_leaf) noexcept
+    : tree{tree},
+      cb_intermediate{std::move(cb_intermediate)}, cb_leaf{std::move(cb_leaf)} {
+  run();
+}
+
+void DFSVisitor::run() const noexcept {
+  // empty tree
+  if (tree.nodes.size() <= 1)
+    return;
+
+  std::vector<std::tuple<std::uint32_t, std::uint32_t>> stack{
+      {1, 1}}; // (id, depth)
+  while (!stack.empty()) {
+    std::uint32_t id, depth;
+    std::tie(id, depth) = stack.back();
+    stack.pop_back();
+    const auto &node = tree.nodes[id];
+
+    if (node.left || node.right) {
+      if (cb_intermediate)
+        cb_intermediate(id, node, depth);
+      if (node.right)
+        stack.emplace_back(node.right, depth + 1);
+      if (node.left)
+        stack.emplace_back(node.left, depth + 1);
+    } else {
+      if (cb_leaf)
+        cb_leaf(id, node, depth);
+    }
+  }
+}
diff --git a/tools/klee-ptree/DFSVisitor.h b/tools/klee-ptree/DFSVisitor.h
new file mode 100644
index 00000000..60d7b3bd
--- /dev/null
+++ b/tools/klee-ptree/DFSVisitor.h
@@ -0,0 +1,31 @@
+//===-- DFSVisitor.h --------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#pragma once
+
+#include "Tree.h"
+
+#include <functional>
+
+/// @brief Traverses a process tree and calls registered callbacks for
+/// intermediate and leaf nodes (not the classical Visitor pattern).
+class DFSVisitor {
+  // void _(node ID, node, depth)
+  using callbackT = std::function<void(std::uint32_t, Node, std::uint32_t)>;
+
+  const Tree &tree;
+  callbackT cb_intermediate;
+  callbackT cb_leaf;
+  void run() const noexcept;
+
+public:
+  DFSVisitor(const Tree &tree, callbackT cb_intermediate,
+             callbackT cb_leaf) noexcept;
+  ~DFSVisitor() = default;
+};
diff --git a/tools/klee-ptree/Printers.cpp b/tools/klee-ptree/Printers.cpp
new file mode 100644
index 00000000..950d1b09
--- /dev/null
+++ b/tools/klee-ptree/Printers.cpp
@@ -0,0 +1,266 @@
+//===-- Printers.cpp --------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "Printers.h"
+
+#include "DFSVisitor.h"
+#include "klee/Core/BranchTypes.h"
+#include "klee/Core/TerminationTypes.h"
+
+#include <algorithm>
+#include <array>
+#include <cstdlib>
+#include <iostream>
+#include <map>
+#include <string>
+#include <string_view>
+#include <unordered_map>
+
+// branches
+
+void printBranches(const Tree &tree) {
+  if (tree.nodes.size() <= 1) {
+    std::cout << "Empty tree.\n";
+    return;
+  }
+
+  std::unordered_map<BranchType, std::uint32_t> branchTypes;
+
+  DFSVisitor visitor(
+      tree,
+      [&branchTypes](std::uint32_t id, Node node, std::uint32_t depth) {
+        branchTypes[std::get<BranchType>(node.kind)]++;
+      },
+      nullptr);
+
+  // sort output
+  std::vector<std::pair<BranchType, std::uint32_t>> sortedBranchTypes(
+      branchTypes.begin(), branchTypes.end());
+  std::sort(sortedBranchTypes.begin(), sortedBranchTypes.end(),
+            [](const auto &lhs, const auto &rhs) {
+              return (lhs.second > rhs.second) ||
+                     (lhs.second == rhs.second && lhs.first < rhs.first);
+            });
+
+  std::cout << "branch type,count\n";
+  for (const auto &[branchType, count] : sortedBranchTypes)
+    std::cout << branchTypeNames[branchType] << ',' << count << '\n';
+}
+
+// depths
+
+struct DepthInfo {
+  std::vector<std::uint32_t> depths;
+  std::uint32_t maxDepth{0};
+  std::uint32_t noLeaves{0};
+  std::uint32_t noNodes{0};
+};
+
+DepthInfo getDepthInfo(const Tree &tree) {
+  DepthInfo I;
+
+  DFSVisitor visitor(
+      tree,
+      [&](std::uint32_t id, Node node, std::uint32_t depth) { ++I.noNodes; },
+      [&I](std::uint32_t id, Node node, std::uint32_t depth) {
+        ++I.noLeaves;
+        ++I.noNodes;
+        if (depth > I.maxDepth)
+          I.maxDepth = depth;
+        if (depth >= I.depths.size())
+          I.depths.resize(depth + 1, 0);
+        ++I.depths[depth];
+      });
+
+  return I;
+}
+
+void printDepths(const Tree &tree) {
+  if (tree.nodes.size() <= 1) {
+    std::cout << "Empty tree.\n";
+    return;
+  }
+
+  const auto DI = getDepthInfo(tree);
+  std::cout << "depth,count\n";
+  for (size_t depth = 1; depth <= DI.maxDepth; ++depth) {
+    auto count = DI.depths[depth];
+    if (count)
+      std::cout << depth << ',' << count << '\n';
+  }
+}
+
+// dot
+
+std::array<std::string, 6> NodeColours = {"green", "orange",   "red",
+                                          "blue",  "darkblue", "darkgrey"};
+
+std::string_view terminationTypeColour(StateTerminationType type) {
+  // Exit
+  if (type == StateTerminationType::Exit)
+    return NodeColours[0];
+
+  // Early
+  if ((StateTerminationType::EXIT < type &&
+       type <= StateTerminationType::EARLY) ||
+      (StateTerminationType::EXECERR < type &&
+       type <= StateTerminationType::END)) {
+    return NodeColours[1];
+  }
+
+  // Program error
+  if (StateTerminationType::SOLVERERR < type &&
+      type <= StateTerminationType::PROGERR)
+    return NodeColours[2];
+
+  // User error
+  if (StateTerminationType::PROGERR < type &&
+      type <= StateTerminationType::USERERR)
+    return NodeColours[3];
+
+  // Execution/Solver error
+  if ((StateTerminationType::USERERR < type &&
+       type <= StateTerminationType::EXECERR) ||
+      (StateTerminationType::EARLY < type &&
+       type <= StateTerminationType::SOLVERERR))
+    return NodeColours[4];
+
+  return NodeColours[5];
+}
+
+void printIntermediateNode(std::uint32_t id, Node node, std::uint32_t depth) {
+  std::cout << 'N' << id << '[' << "tooltip=\""
+            << branchTypeNames[std::get<BranchType>(node.kind)] << "\\n"
+            << "node: " << id << "\\nstate: " << node.stateID
+            << "\\nasm: " << node.asmLine << "\"];\n";
+}
+
+void printLeafNode(std::uint32_t id, Node node, std::uint32_t depth) {
+  const auto terminationType = std::get<StateTerminationType>(node.kind);
+  const auto colour = terminationTypeColour(terminationType);
+  std::cout << 'N' << id << '[' << "tooltip=\""
+            << terminationTypeNames[terminationType] << "\\n"
+            << "node: " << id << "\\nstate: " << node.stateID
+            << "\\nasm: " << node.asmLine << "\",color=" << colour << "];\n";
+}
+
+void printEdges(std::uint32_t id, Node node, std::uint32_t depth) {
+  std::cout << 'N' << id << "->{";
+  if (node.left && node.right) {
+    std::cout << 'N' << node.left << " N" << node.right;
+  } else {
+    std::cout << 'N' << (node.left ? node.left : node.right);
+  }
+  std::cout << "};\n";
+}
+
+void printDOT(const Tree &tree) {
+  // header
+  // - style defaults to intermediate nodes
+  std::cout << "strict digraph PTree {\n"
+               "node[shape=point,width=0.15,color=darkgrey];\n"
+               "edge[color=darkgrey];\n\n";
+
+  // nodes
+  // - change colour for leaf nodes
+  // - attach branch and location info as tooltips
+  DFSVisitor nodeVisitor(tree, printIntermediateNode, printLeafNode);
+
+  // edges
+  DFSVisitor edgeVisitor(tree, printEdges, nullptr);
+
+  // footer
+  std::cout << '}' << std::endl;
+}
+
+// instructions
+
+struct Info {
+  std::uint32_t noBranches{0};
+  std::uint32_t noTerminations{0};
+  std::map<StateTerminationType, std::uint32_t> terminationTypes;
+};
+
+void printInstructions(const Tree &tree) {
+  std::map<std::uint32_t, Info> asmInfo;
+
+  DFSVisitor visitor(
+      tree,
+      [&asmInfo](std::uint32_t id, Node node, std::uint32_t depth) {
+        asmInfo[node.asmLine].noBranches++;
+      },
+      [&asmInfo](std::uint32_t id, Node node, std::uint32_t depth) {
+        auto &info = asmInfo[node.asmLine];
+        info.noTerminations++;
+        info.terminationTypes[std::get<StateTerminationType>(node.kind)]++;
+      });
+
+  std::cout << "asm line,branches,terminations,termination types\n";
+  for (const auto &[asmLine, info] : asmInfo) {
+    std::cout << asmLine << ',' << info.noBranches << ',' << info.noTerminations
+              << ',';
+    std::string sep{""};
+    for (const auto &[terminationType, count] : info.terminationTypes) {
+      std::cout << sep << terminationTypeNames[terminationType] << '(' << count
+                << ')';
+      sep = ";";
+    }
+    std::cout << '\n';
+  }
+}
+
+// terminations
+
+void printTerminations(const Tree &tree) {
+  if (tree.nodes.size() <= 1) {
+    std::cout << "Empty tree.\n";
+    return;
+  }
+
+  std::map<StateTerminationType, std::uint32_t> terminations;
+
+  DFSVisitor visitor(
+      tree, nullptr,
+      [&terminations](std::uint32_t id, Node node, std::uint32_t depth) {
+        terminations[std::get<StateTerminationType>(node.kind)]++;
+      });
+
+  std::cout << "termination type,count\n";
+  for (const auto &[terminationType, count] : terminations)
+    std::cout << terminationTypeNames[terminationType] << ',' << count << '\n';
+}
+
+// tree info
+
+void printTreeInfo(const Tree &tree) {
+  if (tree.nodes.size() <= 1) {
+    std::cout << "Empty tree.\n";
+    return;
+  }
+
+  const auto DI = getDepthInfo(tree);
+
+  // determine average depth
+  std::uint64_t sum{0};
+  for (size_t depth = 1; depth <= DI.maxDepth; ++depth) {
+    auto count = DI.depths[depth];
+    if (count)
+      sum += count * depth;
+  }
+  double avgDepth = (double)sum / DI.noLeaves;
+
+  std::cout << "nodes: " << DI.noNodes << '\n'
+            << "leaf nodes: " << DI.noLeaves
+            << (DI.noNodes && (DI.noLeaves != DI.noNodes / 2 + 1)
+                    ? " (not a binary tree?!)"
+                    : "")
+            << '\n'
+            << "max. depth: " << DI.maxDepth << '\n'
+            << "avg. depth: " << std::setprecision(2) << avgDepth << '\n';
+}
diff --git a/tools/klee-ptree/Printers.h b/tools/klee-ptree/Printers.h
new file mode 100644
index 00000000..d20db4a1
--- /dev/null
+++ b/tools/klee-ptree/Printers.h
@@ -0,0 +1,30 @@
+//===-- Printers.h ----------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#pragma once
+
+#include "Tree.h"
+
+/// print branch types in csv format
+void printBranches(const Tree &tree);
+
+/// print depths in csv format
+void printDepths(const Tree &tree);
+
+/// print tree in dot format
+void printDOT(const Tree &tree);
+
+/// print instruction information in csv format
+void printInstructions(const Tree &tree);
+
+/// print termination types in csv format
+void printTerminations(const Tree &tree);
+
+/// print tree/node information
+void printTreeInfo(const Tree &tree);
diff --git a/tools/klee-ptree/Tree.cpp b/tools/klee-ptree/Tree.cpp
new file mode 100644
index 00000000..20772600
--- /dev/null
+++ b/tools/klee-ptree/Tree.cpp
@@ -0,0 +1,208 @@
+//===-- Tree.cpp ------------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "Tree.h"
+
+#include <sqlite3.h>
+
+#include <cassert>
+#include <cstdlib>
+#include <iostream>
+
+Tree::Tree(const std::filesystem::path &path) {
+  // open db
+  ::sqlite3 *db;
+  if (sqlite3_open_v2(path.c_str(), &db, SQLITE_OPEN_READONLY, nullptr) !=
+      SQLITE_OK) {
+    std::cerr << "Can't open process tree database: " << sqlite3_errmsg(db)
+              << std::endl;
+    exit(EXIT_FAILURE);
+  }
+
+  // initialise prepared statement
+  ::sqlite3_stmt *readStmt;
+  std::string query{
+      "SELECT ID, stateID, leftID, rightID, asmLine, kind FROM nodes;"};
+  if (sqlite3_prepare_v3(db, query.c_str(), -1, SQLITE_PREPARE_PERSISTENT,
+                         &readStmt, nullptr) != SQLITE_OK) {
+    std::cerr << "Can't prepare read statement: " << sqlite3_errmsg(db)
+              << std::endl;
+    exit(EXIT_FAILURE);
+  }
+
+  ::sqlite3_stmt *maxStmt;
+  query = "SELECT MAX(ID) FROM nodes;";
+  if (sqlite3_prepare_v3(db, query.c_str(), -1, SQLITE_PREPARE_PERSISTENT,
+                         &maxStmt, nullptr) != SQLITE_OK) {
+    std::cerr << "Can't prepare max statement: " << sqlite3_errmsg(db)
+              << std::endl;
+    exit(EXIT_FAILURE);
+  }
+
+  // read max id
+  int rc;
+  std::uint64_t maxID;
+  if ((rc = sqlite3_step(maxStmt)) == SQLITE_ROW) {
+    maxID = static_cast<std::uint32_t>(sqlite3_column_int(maxStmt, 0));
+  } else {
+    std::cerr << "Can't read maximum ID: " << sqlite3_errmsg(db) << std::endl;
+    exit(EXIT_FAILURE);
+  }
+
+  // reserve space
+  nodes.resize(maxID + 1, {});
+
+  // read rows into vector
+  while ((rc = sqlite3_step(readStmt)) == SQLITE_ROW) {
+    const auto ID = static_cast<std::uint32_t>(sqlite3_column_int(readStmt, 0));
+    const auto stateID =
+        static_cast<std::uint32_t>(sqlite3_column_int(readStmt, 1));
+    const auto left =
+        static_cast<std::uint32_t>(sqlite3_column_int(readStmt, 2));
+    const auto right =
+        static_cast<std::uint32_t>(sqlite3_column_int(readStmt, 3));
+    const auto asmLine =
+        static_cast<std::uint32_t>(sqlite3_column_int(readStmt, 4));
+    const auto tmpKind =
+        static_cast<std::uint8_t>(sqlite3_column_int(readStmt, 5));
+
+    // sanity checks: valid indices
+    if (ID == 0) {
+      std::cerr << "PTree DB contains illegal node ID (0)" << std::endl;
+      exit(EXIT_FAILURE);
+    }
+
+    if (left > maxID || right > maxID) {
+      std::cerr << "PTree DB contains references to non-existing nodes (> max. "
+                   "ID) in node "
+                << ID << std::endl;
+      exit(EXIT_FAILURE);
+    }
+
+    if ((left == 0 && right != 0) || (left != 0 && right == 0)) {
+      std::cerr << "Warning: PTree DB contains ambiguous node (0 vs. non-0 "
+                   "children): "
+                << ID << std::endl;
+    }
+
+    // determine node kind (branch or leaf node)
+    decltype(Node::kind) kind;
+    if (left == 0 && right == 0) {
+      kind = static_cast<StateTerminationType>(tmpKind);
+    } else {
+      kind = static_cast<BranchType>(tmpKind);
+    }
+
+    // store children
+    nodes[ID] = {.left = left,
+                 .right = right,
+                 .stateID = stateID,
+                 .asmLine = asmLine,
+                 .kind = kind};
+  }
+
+  if (rc != SQLITE_DONE) {
+    std::cerr << "Error while reading database: " << sqlite3_errmsg(db)
+              << std::endl;
+    exit(EXIT_FAILURE);
+  }
+
+  // close db
+  sqlite3_finalize(maxStmt);
+  sqlite3_finalize(readStmt);
+  sqlite3_close(db);
+
+  // initialise global sets/maps and sanity check
+  initialiseValidTypes();
+  sanityCheck();
+  initialiseTypeNames();
+}
+
+void Tree::initialiseTypeNames() {
+// branch types
+#undef BTYPE
+#define BTYPE(Name, I) branchTypeNames[BranchType::Name] = #Name;
+  BRANCH_TYPES
+
+// termination types
+#undef TTYPE
+#define TTYPE(Name, I, S)                                                      \
+  terminationTypeNames[StateTerminationType::Name] = #Name;
+  TERMINATION_TYPES
+}
+
+void Tree::initialiseValidTypes() {
+// branch types
+#undef BTYPE
+#define BTYPE(Name, I) validBranchTypes.insert(BranchType::Name);
+  BRANCH_TYPES
+
+// termination types
+#undef TTYPE
+#define TTYPE(Name, I, S)                                                      \
+  validTerminationTypes.insert(StateTerminationType::Name);
+  TERMINATION_TYPES
+}
+
+void Tree::sanityCheck() {
+  if (nodes.size() <= 1) // [0] is unused
+    return;
+
+  std::vector<std::uint32_t> stack{1}; // root ID
+  std::unordered_set<std::uint32_t> visited;
+  while (!stack.empty()) {
+    const auto id = stack.back();
+    stack.pop_back();
+
+    if (!visited.insert(id).second) {
+      std::cerr << "PTree DB contains duplicate child reference or circular "
+                   "structure. Affected node: "
+                << id << std::endl;
+      exit(EXIT_FAILURE);
+    }
+
+    const auto &node = nodes[id];
+
+    // default constructed "gap" in vector
+    if (!node.left && !node.right &&
+        std::holds_alternative<BranchType>(node.kind) &&
+        static_cast<std::uint8_t>(std::get<BranchType>(node.kind)) == 0u) {
+      std::cerr << "PTree DB references undefined node. Affected node: " << id
+                << std::endl;
+      exit(EXIT_FAILURE);
+    }
+
+    if (node.left || node.right) {
+      if (node.right)
+        stack.push_back(node.right);
+      if (node.left)
+        stack.push_back(node.left);
+      // valid branch types
+      assert(std::holds_alternative<BranchType>(node.kind));
+      const auto branchType = std::get<BranchType>(node.kind);
+      if (validBranchTypes.count(branchType) == 0) {
+        std::cerr << "PTree DB contains unknown branch type ("
+                  << (unsigned)static_cast<std::uint8_t>(branchType)
+                  << ") in node " << id << std::endl;
+        exit(EXIT_FAILURE);
+      }
+    } else {
+      // valid termination types
+      assert(std::holds_alternative<StateTerminationType>(node.kind));
+      const auto terminationType = std::get<StateTerminationType>(node.kind);
+      if (validTerminationTypes.count(terminationType) == 0 ||
+          terminationType == StateTerminationType::RUNNING) {
+        std::cerr << "PTree DB contains unknown termination type ("
+                  << (unsigned)static_cast<std::uint8_t>(terminationType)
+                  << ") in node " << id << std::endl;
+        exit(EXIT_FAILURE);
+      }
+    }
+  }
+}
diff --git a/tools/klee-ptree/Tree.h b/tools/klee-ptree/Tree.h
new file mode 100644
index 00000000..65b7baeb
--- /dev/null
+++ b/tools/klee-ptree/Tree.h
@@ -0,0 +1,53 @@
+//===-- Tree.h --------------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#pragma once
+
+#include "klee/Core/BranchTypes.h"
+#include "klee/Core/TerminationTypes.h"
+
+#include <filesystem>
+#include <string>
+#include <unordered_map>
+#include <unordered_set>
+#include <variant>
+#include <vector>
+
+inline std::unordered_set<BranchType> validBranchTypes;
+inline std::unordered_set<StateTerminationType> validTerminationTypes;
+inline std::unordered_map<BranchType, std::string> branchTypeNames;
+inline std::unordered_map<StateTerminationType, std::string>
+    terminationTypeNames;
+
+///@brief A Tree node representing a PTreeNode
+struct Node final {
+  std::uint32_t left{0};
+  std::uint32_t right{0};
+  std::uint32_t stateID{0};
+  std::uint32_t asmLine{0};
+  std::variant<BranchType, StateTerminationType> kind{BranchType::NONE};
+};
+
+///@brief An in-memory representation of a complete process tree
+class Tree final {
+  /// Creates branchTypeNames and terminationTypeNames maps
+  static void initialiseTypeNames();
+  /// Creates validBranchTypes and validTerminationTypes sets
+  static void initialiseValidTypes();
+  /// Checks tree properties (e.g. valid branch/termination types)
+  void sanityCheck();
+
+public:
+  /// sorted vector of Nodes default initialised with BranchType::NONE
+  std::vector<Node> nodes; // PTree node IDs start with 1!
+
+  /// Reads complete ptree.db into memory
+  explicit Tree(const std::filesystem::path &path);
+  ~Tree() = default;
+};
diff --git a/tools/klee-ptree/main.cpp b/tools/klee-ptree/main.cpp
new file mode 100644
index 00000000..96d2be75
--- /dev/null
+++ b/tools/klee-ptree/main.cpp
@@ -0,0 +1,68 @@
+//===-- main.cpp ------------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include <cstdlib>
+#include <filesystem>
+#include <iostream>
+
+#include "Printers.h"
+
+namespace fs = std::filesystem;
+
+void print_usage() {
+  std::cout << "Usage: klee-ptree <option> /path[/ptree.db]\n\n"
+               "Options:\n"
+               "\tbranches     -  print branch statistics in csv format\n"
+               "\tdepths       -  print depths statistics in csv format\n"
+               "\tinstructions -  print asm line summary in csv format\n"
+               "\tterminations -  print termination statistics in csv format\n"
+               "\ttree-dot     -  print tree in dot format\n"
+               "\ttree-info    -  print tree statistics"
+               "\n";
+}
+
+int main(int argc, char *argv[]) {
+  if (argc != 3) {
+    print_usage();
+    exit(EXIT_FAILURE);
+  }
+
+  // parse options
+  void (*action)(const Tree &);
+  std::string option(argv[1]);
+  if (option == "branches") {
+    action = printBranches;
+  } else if (option == "instructions") {
+    action = printInstructions;
+  } else if (option == "depths") {
+    action = printDepths;
+  } else if (option == "terminations") {
+    action = printTerminations;
+  } else if (option == "tree-dot") {
+    action = printDOT;
+  } else if (option == "tree-info") {
+    action = printTreeInfo;
+  } else {
+    print_usage();
+    exit(EXIT_FAILURE);
+  }
+
+  // create tree
+  fs::path path{argv[2]};
+  if (fs::is_directory(path))
+    path /= "ptree.db";
+  if (!fs::exists(path)) {
+    std::cerr << "Cannot open " << path << '\n';
+    exit(EXIT_FAILURE);
+  }
+  Tree tree(path);
+
+  // print results
+  action(tree);
+}
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index a3062d24..ce231967 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -1123,7 +1123,7 @@ int main(int argc, char **argv, char **envp) {
      {&ChecksCat,      &DebugCat,    &ExtCallsCat, &ExprCat,   &LinkCat,
       &MemoryCat,      &MergeCat,    &MiscCat,     &ModuleCat, &ReplayCat,
       &SearchCat,      &SeedingCat,  &SolvingCat,  &StartCat,  &StatsCat,
-      &TerminationCat, &TestCaseCat, &TestGenCat});
+      &TerminationCat, &TestCaseCat, &TestGenCat,  &PTreeCat});
 
   llvm::InitializeNativeTarget();