diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | tools/klee-ptree/CMakeLists.txt | 16 | ||||
| -rw-r--r-- | tools/klee-ptree/DFSVisitor.cpp | 46 | ||||
| -rw-r--r-- | tools/klee-ptree/DFSVisitor.h | 31 | ||||
| -rw-r--r-- | tools/klee-ptree/Printers.cpp | 266 | ||||
| -rw-r--r-- | tools/klee-ptree/Printers.h | 30 | ||||
| -rw-r--r-- | tools/klee-ptree/Tree.cpp | 208 | ||||
| -rw-r--r-- | tools/klee-ptree/Tree.h | 53 | ||||
| -rw-r--r-- | tools/klee-ptree/main.cpp | 68 | ||||
| -rw-r--r-- | tools/klee/main.cpp | 2 |
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(); |