diff options
author | Cristian Cadar <c.cadar@imperial.ac.uk> | 2023-12-22 18:22:02 +0200 |
---|---|---|
committer | MartinNowack <2443641+MartinNowack@users.noreply.github.com> | 2024-01-12 12:00:35 +0000 |
commit | 3fa03d12d28658694f2bf2085e8634cc267e3f16 (patch) | |
tree | c775b6d770c98ca310e9caf50c36016f99b81891 /tools | |
parent | 2c8b74cc858793c94e5476b5765e93ee23738702 (diff) | |
download | klee-3fa03d12d28658694f2bf2085e8634cc267e3f16.tar.gz |
Renamed PTree to ExecutionTree (and similar)
Diffstat (limited to 'tools')
-rw-r--r-- | tools/CMakeLists.txt | 2 | ||||
-rw-r--r-- | tools/klee-exec-tree/CMakeLists.txt | 10 | ||||
-rw-r--r-- | tools/klee-exec-tree/DFSVisitor.h | 2 | ||||
-rw-r--r-- | tools/klee-exec-tree/Printers.cpp | 2 | ||||
-rw-r--r-- | tools/klee-exec-tree/Tree.cpp | 33 | ||||
-rw-r--r-- | tools/klee-exec-tree/Tree.h | 8 | ||||
-rw-r--r-- | tools/klee-exec-tree/main.cpp | 4 | ||||
-rw-r--r-- | tools/klee/main.cpp | 9 |
8 files changed, 35 insertions, 35 deletions
diff --git a/tools/CMakeLists.txt b/tools/CMakeLists.txt index 40089c40..8c9128b4 100644 --- a/tools/CMakeLists.txt +++ b/tools/CMakeLists.txt @@ -10,7 +10,7 @@ add_subdirectory(ktest-gen) add_subdirectory(ktest-randgen) add_subdirectory(kleaver) add_subdirectory(klee) -add_subdirectory(klee-ptree) +add_subdirectory(klee-exec-tree) add_subdirectory(klee-replay) add_subdirectory(klee-stats) add_subdirectory(klee-zesti) diff --git a/tools/klee-exec-tree/CMakeLists.txt b/tools/klee-exec-tree/CMakeLists.txt index b5c3fa09..0c473d92 100644 --- a/tools/klee-exec-tree/CMakeLists.txt +++ b/tools/klee-exec-tree/CMakeLists.txt @@ -7,10 +7,10 @@ # #===------------------------------------------------------------------------===# -add_executable(klee-ptree main.cpp Tree.cpp DFSVisitor.cpp Printers.cpp) +add_executable(klee-exec-tree 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}) +target_compile_features(klee-exec-tree PRIVATE cxx_std_17) +target_include_directories(klee-exec-tree PRIVATE ${KLEE_INCLUDE_DIRS} ${SQLite3_INCLUDE_DIRS}) +target_link_libraries(klee-exec-tree PUBLIC ${SQLite3_LIBRARIES}) -install(TARGETS klee-ptree DESTINATION bin) +install(TARGETS klee-exec-tree DESTINATION bin) diff --git a/tools/klee-exec-tree/DFSVisitor.h b/tools/klee-exec-tree/DFSVisitor.h index 60d7b3bd..a61a3ff2 100644 --- a/tools/klee-exec-tree/DFSVisitor.h +++ b/tools/klee-exec-tree/DFSVisitor.h @@ -13,7 +13,7 @@ #include <functional> -/// @brief Traverses a process tree and calls registered callbacks for +/// @brief Traverses an execution tree and calls registered callbacks for /// intermediate and leaf nodes (not the classical Visitor pattern). class DFSVisitor { // void _(node ID, node, depth) diff --git a/tools/klee-exec-tree/Printers.cpp b/tools/klee-exec-tree/Printers.cpp index 950d1b09..70a84017 100644 --- a/tools/klee-exec-tree/Printers.cpp +++ b/tools/klee-exec-tree/Printers.cpp @@ -163,7 +163,7 @@ void printEdges(std::uint32_t id, Node node, std::uint32_t depth) { void printDOT(const Tree &tree) { // header // - style defaults to intermediate nodes - std::cout << "strict digraph PTree {\n" + std::cout << "strict digraph ExecutionTree {\n" "node[shape=point,width=0.15,color=darkgrey];\n" "edge[color=darkgrey];\n\n"; diff --git a/tools/klee-exec-tree/Tree.cpp b/tools/klee-exec-tree/Tree.cpp index 20772600..42b03ba2 100644 --- a/tools/klee-exec-tree/Tree.cpp +++ b/tools/klee-exec-tree/Tree.cpp @@ -20,7 +20,7 @@ Tree::Tree(const std::filesystem::path &path) { ::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::cerr << "Cannot open execution tree database: " << sqlite3_errmsg(db) << std::endl; exit(EXIT_FAILURE); } @@ -31,7 +31,7 @@ Tree::Tree(const std::filesystem::path &path) { "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::cerr << "Cannot prepare read statement: " << sqlite3_errmsg(db) << std::endl; exit(EXIT_FAILURE); } @@ -40,7 +40,7 @@ Tree::Tree(const std::filesystem::path &path) { 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::cerr << "Cannot prepare max statement: " << sqlite3_errmsg(db) << std::endl; exit(EXIT_FAILURE); } @@ -51,7 +51,7 @@ Tree::Tree(const std::filesystem::path &path) { 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; + std::cerr << "Cannot read maximum ID: " << sqlite3_errmsg(db) << std::endl; exit(EXIT_FAILURE); } @@ -74,20 +74,20 @@ Tree::Tree(const std::filesystem::path &path) { // sanity checks: valid indices if (ID == 0) { - std::cerr << "PTree DB contains illegal node ID (0)" << std::endl; + std::cerr << "ExecutionTree 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 " + std::cerr << "ExecutionTree 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): " + std::cerr << "Warning: ExecutionTree DB contains ambiguous node " + "(0 vs. non-0 children): " << ID << std::endl; } @@ -161,9 +161,10 @@ void Tree::sanityCheck() { stack.pop_back(); if (!visited.insert(id).second) { - std::cerr << "PTree DB contains duplicate child reference or circular " - "structure. Affected node: " - << id << std::endl; + std::cerr + << "ExecutionTree DB contains duplicate child reference or circular " + "structure. Affected node: " + << id << std::endl; exit(EXIT_FAILURE); } @@ -173,8 +174,8 @@ void Tree::sanityCheck() { 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; + std::cerr << "ExecutionTree DB references undefined node. Affected node: " + << id << std::endl; exit(EXIT_FAILURE); } @@ -187,7 +188,7 @@ void Tree::sanityCheck() { 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 (" + std::cerr << "ExecutionTree DB contains unknown branch type (" << (unsigned)static_cast<std::uint8_t>(branchType) << ") in node " << id << std::endl; exit(EXIT_FAILURE); @@ -198,7 +199,7 @@ void Tree::sanityCheck() { const auto terminationType = std::get<StateTerminationType>(node.kind); if (validTerminationTypes.count(terminationType) == 0 || terminationType == StateTerminationType::RUNNING) { - std::cerr << "PTree DB contains unknown termination type (" + std::cerr << "ExecutionTree 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-exec-tree/Tree.h b/tools/klee-exec-tree/Tree.h index 65b7baeb..40e04389 100644 --- a/tools/klee-exec-tree/Tree.h +++ b/tools/klee-exec-tree/Tree.h @@ -25,7 +25,7 @@ inline std::unordered_map<BranchType, std::string> branchTypeNames; inline std::unordered_map<StateTerminationType, std::string> terminationTypeNames; -///@brief A Tree node representing a PTreeNode +///@brief A Tree node representing an ExecutionTreeNode struct Node final { std::uint32_t left{0}; std::uint32_t right{0}; @@ -34,7 +34,7 @@ struct Node final { std::variant<BranchType, StateTerminationType> kind{BranchType::NONE}; }; -///@brief An in-memory representation of a complete process tree +///@brief An in-memory representation of a complete execution tree class Tree final { /// Creates branchTypeNames and terminationTypeNames maps static void initialiseTypeNames(); @@ -45,9 +45,9 @@ class Tree final { public: /// sorted vector of Nodes default initialised with BranchType::NONE - std::vector<Node> nodes; // PTree node IDs start with 1! + std::vector<Node> nodes; // ExecutionTree node IDs start with 1! - /// Reads complete ptree.db into memory + /// Reads complete exec-tree.db into memory explicit Tree(const std::filesystem::path &path); ~Tree() = default; }; diff --git a/tools/klee-exec-tree/main.cpp b/tools/klee-exec-tree/main.cpp index 96d2be75..efe28d04 100644 --- a/tools/klee-exec-tree/main.cpp +++ b/tools/klee-exec-tree/main.cpp @@ -16,7 +16,7 @@ namespace fs = std::filesystem; void print_usage() { - std::cout << "Usage: klee-ptree <option> /path[/ptree.db]\n\n" + std::cout << "Usage: klee-exec-tree <option> /path[/exec_tree.db]\n\n" "Options:\n" "\tbranches - print branch statistics in csv format\n" "\tdepths - print depths statistics in csv format\n" @@ -56,7 +56,7 @@ int main(int argc, char *argv[]) { // create tree fs::path path{argv[2]}; if (fs::is_directory(path)) - path /= "ptree.db"; + path /= "exec_tree.db"; if (!fs::exists(path)) { std::cerr << "Cannot open " << path << '\n'; exit(EXIT_FAILURE); diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index ce231967..febeb47f 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -1120,11 +1120,10 @@ int main(int argc, char **argv, char **envp) { atexit(llvm_shutdown); // Call llvm_shutdown() on exit KCommandLine::KeepOnlyCategories( - {&ChecksCat, &DebugCat, &ExtCallsCat, &ExprCat, &LinkCat, - &MemoryCat, &MergeCat, &MiscCat, &ModuleCat, &ReplayCat, - &SearchCat, &SeedingCat, &SolvingCat, &StartCat, &StatsCat, - &TerminationCat, &TestCaseCat, &TestGenCat, &PTreeCat}); - + {&ChecksCat, &DebugCat, &ExtCallsCat, &ExprCat, &LinkCat, + &MemoryCat, &MergeCat, &MiscCat, &ModuleCat, &ReplayCat, + &SearchCat, &SeedingCat, &SolvingCat, &StartCat, &StatsCat, + &TerminationCat, &TestCaseCat, &TestGenCat, &ExecTreeCat, &ExecTreeCat}); llvm::InitializeNativeTarget(); parseArguments(argc, argv); |