1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
|
//===-- 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>
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(llvm::raw_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() {
}
|
