about summary refs log tree commit diff homepage
path: root/tools/klee-ptree/main.cpp
diff options
context:
space:
mode:
authorFrank Busse <bb0xfb@gmail.com>2023-03-24 21:14:02 +0000
committerMartinNowack <2443641+MartinNowack@users.noreply.github.com>2024-01-12 12:00:35 +0000
commit19b6ae578b0658115d15848604a28434845bb3e3 (patch)
tree31d52545929760ad725385bd1cdc1153b710fc75 /tools/klee-ptree/main.cpp
parentfc83f06b17221bf5ef20e30d9da1ccff927beb17 (diff)
downloadklee-19b6ae578b0658115d15848604a28434845bb3e3.tar.gz
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.
Diffstat (limited to 'tools/klee-ptree/main.cpp')
-rw-r--r--tools/klee-ptree/main.cpp68
1 files changed, 68 insertions, 0 deletions
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);
+}