Initial KLEE checkin.

 - Lots more tweaks, documentation, and web page content is needed,
   but this should compile & work on OS X & Linux.


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72205 91177308-0d34-0410-b5e6-96231b3b80d8

1 files changed, 103 insertions, 0 deletions

diff --git a/lib/Core/PTree.cpp b/lib/Core/PTree.cpp
new file mode 100644
index 00000000..349761cd
--- /dev/null
+++ b/lib/Core/PTree.cpp
@@ -0,0 +1,103 @@
+//===-- PTree.cpp ---------------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "PTree.h"
+
+#include <klee/Expr.h>
+#include <klee/util/ExprPPrinter.h>
+
+#include <vector>
+#include <iostream>
+
+using namespace klee;
+
+  /* *** */
+
+PTree::PTree(const data_type &_root) : root(new Node(0,_root)) {
+}
+
+PTree::~PTree() {}
+
+std::pair<PTreeNode*, PTreeNode*>
+PTree::split(Node *n, 
+             const data_type &leftData, 
+             const data_type &rightData) {
+  assert(n && !n->left && !n->right);
+  n->left = new Node(n, leftData);
+  n->right = new Node(n, rightData);
+  return std::make_pair(n->left, n->right);
+}
+
+void PTree::remove(Node *n) {
+  assert(!n->left && !n->right);
+  do {
+    Node *p = n->parent;
+    delete n;
+    if (p) {
+      if (n == p->left) {
+        p->left = 0;
+      } else {
+        assert(n == p->right);
+        p->right = 0;
+      }
+    }
+    n = p;
+  } while (n && !n->left && !n->right);
+}
+
+void PTree::dump(std::ostream &os) {
+  ExprPPrinter *pp = ExprPPrinter::create(os);
+  pp->setNewline("\\l");
+  os << "digraph G {\n";
+  os << "\tsize=\"10,7.5\";\n";
+  os << "\tratio=fill;\n";
+  os << "\trotate=90;\n";
+  os << "\tcenter = \"true\";\n";
+  os << "\tnode [style=\"filled\",width=.1,height=.1,fontname=\"Terminus\"]\n";
+  os << "\tedge [arrowsize=.3]\n";
+  std::vector<PTree::Node*> stack;
+  stack.push_back(root);
+  while (!stack.empty()) {
+    PTree::Node *n = stack.back();
+    stack.pop_back();
+    if (n->condition.isNull()) {
+      os << "\tn" << n << " [label=\"\"";
+    } else {
+      os << "\tn" << n << " [label=\"";
+      pp->print(n->condition);
+      os << "\",shape=diamond";
+    }
+    if (n->data)
+      os << ",fillcolor=green";
+    os << "];\n";
+    if (n->left) {
+      os << "\tn" << n << " -> n" << n->left << ";\n";
+      stack.push_back(n->left);
+    }
+    if (n->right) {
+      os << "\tn" << n << " -> n" << n->right << ";\n";
+      stack.push_back(n->right);
+    }
+  }
+  os << "}\n";
+  delete pp;
+}
+
+PTreeNode::PTreeNode(PTreeNode *_parent, 
+                     ExecutionState *_data) 
+  : parent(_parent),
+    left(0),
+    right(0),
+    data(_data),
+    condition(0) {
+}
+
+PTreeNode::~PTreeNode() {
+}
+