diff options
27 files changed, 498 insertions, 457 deletions
diff --git a/include/klee/Support/OptionCategories.h b/include/klee/Support/OptionCategories.h index 152241c9..bee6e52a 100644 --- a/include/klee/Support/OptionCategories.h +++ b/include/klee/Support/OptionCategories.h @@ -29,7 +29,7 @@ namespace klee { extern llvm::cl::OptionCategory MiscCat; extern llvm::cl::OptionCategory ModuleCat; extern llvm::cl::OptionCategory SearchCat; - extern llvm::cl::OptionCategory PTreeCat; + extern llvm::cl::OptionCategory ExecTreeCat; extern llvm::cl::OptionCategory SeedingCat; extern llvm::cl::OptionCategory SolvingCat; extern llvm::cl::OptionCategory StatsCat; diff --git a/lib/Core/CMakeLists.txt b/lib/Core/CMakeLists.txt index 8df3e259..021c3ce7 100644 --- a/lib/Core/CMakeLists.txt +++ b/lib/Core/CMakeLists.txt @@ -13,14 +13,14 @@ add_library(kleeCore Context.cpp CoreStats.cpp ExecutionState.cpp + ExecutionTree.cpp + ExecutionTreeWriter.cpp Executor.cpp ExecutorUtil.cpp ExternalDispatcher.cpp ImpliedValue.cpp Memory.cpp MemoryManager.cpp - PTree.cpp - PTreeWriter.cpp Searcher.cpp SeedInfo.cpp SpecialFunctionHandler.cpp diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h index dbe02fd9..20187166 100644 --- a/lib/Core/ExecutionState.h +++ b/lib/Core/ExecutionState.h @@ -32,10 +32,10 @@ namespace klee { class Array; class CallPathNode; struct Cell; +class ExecutionTreeNode; struct KFunction; struct KInstruction; class MemoryObject; -class PTreeNode; struct InstructionInfo; llvm::raw_ostream &operator<<(llvm::raw_ostream &os, const MemoryMap &mm); @@ -207,9 +207,9 @@ public: /// @brief Set containing which lines in which files are covered by this state std::map<const std::string *, std::set<std::uint32_t>> coveredLines; - /// @brief Pointer to the process tree of the current state - /// Copies of ExecutionState should not copy ptreeNode - PTreeNode *ptreeNode = nullptr; + /// @brief Pointer to the execution tree of the current state + /// Copies of ExecutionState should not copy executionTreeNode + ExecutionTreeNode *executionTreeNode = nullptr; /// @brief Ordered list of symbolics: used to generate test cases. // diff --git a/lib/Core/ExecutionTree.cpp b/lib/Core/ExecutionTree.cpp index c5b640d3..fb4913c7 100644 --- a/lib/Core/ExecutionTree.cpp +++ b/lib/Core/ExecutionTree.cpp @@ -1,4 +1,4 @@ -//===-- PTree.cpp ---------------------------------------------------------===// +//===-- ExecutionTree.cpp -------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // @@ -7,7 +7,7 @@ // //===----------------------------------------------------------------------===// -#include "PTree.h" +#include "ExecutionTree.h" #include "ExecutionState.h" @@ -23,100 +23,105 @@ using namespace klee; namespace klee { llvm::cl::OptionCategory - PTreeCat("Process tree related options", - "These options affect the process tree handling."); + ExecTreeCat("Execution tree related options", + "These options affect the execution tree handling."); } namespace { -llvm::cl::opt<bool> CompressProcessTree( - "compress-process-tree", - llvm::cl::desc("Remove intermediate nodes in the process " +llvm::cl::opt<bool> CompressExecutionTree( + "compress-execution-tree", + llvm::cl::desc("Remove intermediate nodes in the execution " "tree whenever possible (default=false)"), - llvm::cl::init(false), llvm::cl::cat(PTreeCat)); + llvm::cl::init(false), llvm::cl::cat(ExecTreeCat)); -llvm::cl::opt<bool> WritePTree( - "write-ptree", llvm::cl::init(false), - llvm::cl::desc("Write process tree into ptree.db (default=false)"), - llvm::cl::cat(PTreeCat)); +llvm::cl::opt<bool> WriteExecutionTree( + "write-exec-tree", llvm::cl::init(false), + llvm::cl::desc("Write execution tree into exec_tree.db (default=false)"), + llvm::cl::cat(ExecTreeCat)); } // namespace -// PTreeNode +// ExecutionTreeNode -PTreeNode::PTreeNode(PTreeNode *parent, ExecutionState *state) noexcept +ExecutionTreeNode::ExecutionTreeNode(ExecutionTreeNode *parent, + ExecutionState *state) noexcept : parent{parent}, left{nullptr}, right{nullptr}, state{state} { - state->ptreeNode = this; + state->executionTreeNode = this; } -// AnnotatedPTreeNode +// AnnotatedExecutionTreeNode -AnnotatedPTreeNode::AnnotatedPTreeNode(PTreeNode *parent, - ExecutionState *state) noexcept - : PTreeNode(parent, state) { +AnnotatedExecutionTreeNode::AnnotatedExecutionTreeNode( + ExecutionTreeNode *parent, ExecutionState *state) noexcept + : ExecutionTreeNode(parent, state) { id = nextID++; } -// NoopPTree +// NoopExecutionTree -void NoopPTree::dump(llvm::raw_ostream &os) noexcept { +void NoopExecutionTree::dump(llvm::raw_ostream &os) noexcept { os << "digraph G {\nTreeNotAvailable [shape=box]\n}"; } -// InMemoryPTree +// InMemoryExecutionTree -InMemoryPTree::InMemoryPTree(ExecutionState &initialState) noexcept { - root = PTreeNodePtr(createNode(nullptr, &initialState)); - initialState.ptreeNode = root.getPointer(); +InMemoryExecutionTree::InMemoryExecutionTree( + ExecutionState &initialState) noexcept { + root = ExecutionTreeNodePtr(createNode(nullptr, &initialState)); + initialState.executionTreeNode = root.getPointer(); } -PTreeNode *InMemoryPTree::createNode(PTreeNode *parent, ExecutionState *state) { - return new PTreeNode(parent, state); +ExecutionTreeNode *InMemoryExecutionTree::createNode(ExecutionTreeNode *parent, + ExecutionState *state) { + return new ExecutionTreeNode(parent, state); } -void InMemoryPTree::attach(PTreeNode *node, ExecutionState *leftState, - ExecutionState *rightState, - BranchType reason) noexcept { +void InMemoryExecutionTree::attach(ExecutionTreeNode *node, + ExecutionState *leftState, + ExecutionState *rightState, + BranchType reason) noexcept { assert(node && !node->left.getPointer() && !node->right.getPointer()); - assert(node == rightState->ptreeNode && + assert(node == rightState->executionTreeNode && "Attach assumes the right state is the current state"); - node->left = PTreeNodePtr(createNode(node, leftState)); + node->left = ExecutionTreeNodePtr(createNode(node, leftState)); // The current node inherits the tag uint8_t currentNodeTag = root.getInt(); if (node->parent) currentNodeTag = node->parent->left.getPointer() == node ? node->parent->left.getInt() : node->parent->right.getInt(); - node->right = PTreeNodePtr(createNode(node, rightState), currentNodeTag); + node->right = + ExecutionTreeNodePtr(createNode(node, rightState), currentNodeTag); updateBranchingNode(*node, reason); node->state = nullptr; } -void InMemoryPTree::remove(PTreeNode *n) noexcept { +void InMemoryExecutionTree::remove(ExecutionTreeNode *n) noexcept { assert(!n->left.getPointer() && !n->right.getPointer()); updateTerminatingNode(*n); do { - PTreeNode *p = n->parent; + ExecutionTreeNode *p = n->parent; if (p) { if (n == p->left.getPointer()) { - p->left = PTreeNodePtr(nullptr); + p->left = ExecutionTreeNodePtr(nullptr); } else { assert(n == p->right.getPointer()); - p->right = PTreeNodePtr(nullptr); + p->right = ExecutionTreeNodePtr(nullptr); } } delete n; n = p; } while (n && !n->left.getPointer() && !n->right.getPointer()); - if (n && CompressProcessTree) { - // We're now at a node that has exactly one child; we've just deleted the + if (n && CompressExecutionTree) { + // We are now at a node that has exactly one child; we've just deleted the // other one. Eliminate the node and connect its child to the parent // directly (if it's not the root). - PTreeNodePtr child = n->left.getPointer() ? n->left : n->right; - PTreeNode *parent = n->parent; + ExecutionTreeNodePtr child = n->left.getPointer() ? n->left : n->right; + ExecutionTreeNode *parent = n->parent; child.getPointer()->parent = parent; if (!parent) { - // We're at the root. + // We are at the root root = child; } else { if (n == parent->left.getPointer()) { @@ -131,7 +136,7 @@ void InMemoryPTree::remove(PTreeNode *n) noexcept { } } -void InMemoryPTree::dump(llvm::raw_ostream &os) noexcept { +void InMemoryExecutionTree::dump(llvm::raw_ostream &os) noexcept { std::unique_ptr<ExprPPrinter> pp(ExprPPrinter::create(os)); pp->setNewline("\\l"); os << "digraph G {\n" @@ -141,10 +146,10 @@ void InMemoryPTree::dump(llvm::raw_ostream &os) noexcept { << "\tcenter = \"true\";\n" << "\tnode [style=\"filled\",width=.1,height=.1,fontname=\"Terminus\"]\n" << "\tedge [arrowsize=.3]\n"; - std::vector<const PTreeNode *> stack; + std::vector<const ExecutionTreeNode *> stack; stack.push_back(root.getPointer()); while (!stack.empty()) { - const PTreeNode *n = stack.back(); + const ExecutionTreeNode *n = stack.back(); stack.pop_back(); os << "\tn" << n << " [shape=diamond"; if (n->state) @@ -164,43 +169,46 @@ void InMemoryPTree::dump(llvm::raw_ostream &os) noexcept { os << "}\n"; } -std::uint8_t InMemoryPTree::getNextId() noexcept { +std::uint8_t InMemoryExecutionTree::getNextId() noexcept { static_assert(PtrBitCount <= 8); std::uint8_t id = 1 << registeredIds++; if (registeredIds > PtrBitCount) { - klee_error("PTree cannot support more than %d RandomPathSearchers", + klee_error("ExecutionTree cannot support more than %d RandomPathSearchers", PtrBitCount); } return id; } -// PersistentPTree +// PersistentExecutionTree -PersistentPTree::PersistentPTree(ExecutionState &initialState, - InterpreterHandler &ih) noexcept - : writer(ih.getOutputFilename("ptree.db")) { - root = PTreeNodePtr(createNode(nullptr, &initialState)); - initialState.ptreeNode = root.getPointer(); +PersistentExecutionTree::PersistentExecutionTree( + ExecutionState &initialState, InterpreterHandler &ih) noexcept + : writer(ih.getOutputFilename("exec_tree.db")) { + root = ExecutionTreeNodePtr(createNode(nullptr, &initialState)); + initialState.executionTreeNode = root.getPointer(); } -void PersistentPTree::dump(llvm::raw_ostream &os) noexcept { +void PersistentExecutionTree::dump(llvm::raw_ostream &os) noexcept { writer.batchCommit(true); - InMemoryPTree::dump(os); + InMemoryExecutionTree::dump(os); } -PTreeNode *PersistentPTree::createNode(PTreeNode *parent, - ExecutionState *state) { - return new AnnotatedPTreeNode(parent, state); +ExecutionTreeNode * +PersistentExecutionTree::createNode(ExecutionTreeNode *parent, + ExecutionState *state) { + return new AnnotatedExecutionTreeNode(parent, state); } -void PersistentPTree::setTerminationType(ExecutionState &state, - StateTerminationType type) { - auto *annotatedNode = llvm::cast<AnnotatedPTreeNode>(state.ptreeNode); +void PersistentExecutionTree::setTerminationType(ExecutionState &state, + StateTerminationType type) { + auto *annotatedNode = + llvm::cast<AnnotatedExecutionTreeNode>(state.executionTreeNode); annotatedNode->kind = type; } -void PersistentPTree::updateBranchingNode(PTreeNode &node, BranchType reason) { - auto *annotatedNode = llvm::cast<AnnotatedPTreeNode>(&node); +void PersistentExecutionTree::updateBranchingNode(ExecutionTreeNode &node, + BranchType reason) { + auto *annotatedNode = llvm::cast<AnnotatedExecutionTreeNode>(&node); const auto &state = *node.state; const auto prevPC = state.prevPC; annotatedNode->asmLine = @@ -209,9 +217,9 @@ void PersistentPTree::updateBranchingNode(PTreeNode &node, BranchType reason) { writer.write(*annotatedNode); } -void PersistentPTree::updateTerminatingNode(PTreeNode &node) { +void PersistentExecutionTree::updateTerminatingNode(ExecutionTreeNode &node) { assert(node.state); - auto *annotatedNode = llvm::cast<AnnotatedPTreeNode>(&node); + auto *annotatedNode = llvm::cast<AnnotatedExecutionTreeNode>(&node); const auto &state = *node.state; const auto prevPC = state.prevPC; annotatedNode->asmLine = @@ -222,14 +230,14 @@ void PersistentPTree::updateTerminatingNode(PTreeNode &node) { // Factory -std::unique_ptr<PTree> klee::createPTree(ExecutionState &initialState, - bool inMemory, - InterpreterHandler &ih) { - if (WritePTree) - return std::make_unique<PersistentPTree>(initialState, ih); +std::unique_ptr<ExecutionTree> +klee::createExecutionTree(ExecutionState &initialState, bool inMemory, + InterpreterHandler &ih) { + if (WriteExecutionTree) + return std::make_unique<PersistentExecutionTree>(initialState, ih); if (inMemory) - return std::make_unique<InMemoryPTree>(initialState); + return std::make_unique<InMemoryExecutionTree>(initialState); - return std::make_unique<NoopPTree>(); + return std::make_unique<NoopExecutionTree>(); }; diff --git a/lib/Core/ExecutionTree.h b/lib/Core/ExecutionTree.h index ab3f0433..cd28a85c 100644 --- a/lib/Core/ExecutionTree.h +++ b/lib/Core/ExecutionTree.h @@ -1,4 +1,4 @@ -//===-- PTree.h -------------------------------------------------*- C++ -*-===// +//===-- ExecutionTree.h -----------------------------------------*- C++ -*-===// // // The KLEE Symbolic Virtual Machine // @@ -7,10 +7,10 @@ // //===----------------------------------------------------------------------===// -#ifndef KLEE_PTREE_H -#define KLEE_PTREE_H +#ifndef KLEE_EXECUTION_TREE_H +#define KLEE_EXECUTION_TREE_H -#include "PTreeWriter.h" +#include "ExecutionTreeWriter.h" #include "UserSearcher.h" #include "klee/Core/BranchTypes.h" #include "klee/Core/TerminationTypes.h" @@ -26,40 +26,41 @@ namespace klee { class ExecutionState; class Executor; -class InMemoryPTree; +class InMemoryExecutionTree; class InterpreterHandler; -class PTreeNode; +class ExecutionTreeNode; class Searcher; -/* PTreeNodePtr is used by the Random Path Searcher object to efficiently -record which PTreeNode belongs to it. PTree is a global structure that -captures all states, whereas a Random Path Searcher might only care about -a subset. The integer part of PTreeNodePtr is a bitmask (a "tag") of which -Random Path Searchers PTreeNode belongs to. */ +/* ExecutionTreeNodePtr is used by the Random Path Searcher object to +efficiently record which ExecutionTreeNode belongs to it. ExecutionTree is a +global structure that captures all states, whereas a Random Path Searcher might +only care about a subset. The integer part of ExecutionTreeNodePtr is a bitmask +(a "tag") of which Random Path Searchers ExecutionTreeNode belongs to. */ constexpr std::uint8_t PtrBitCount = 3; -using PTreeNodePtr = llvm::PointerIntPair<PTreeNode *, PtrBitCount, uint8_t>; +using ExecutionTreeNodePtr = + llvm::PointerIntPair<ExecutionTreeNode *, PtrBitCount, uint8_t>; -class PTreeNode { +class ExecutionTreeNode { public: enum class NodeType : std::uint8_t { Basic, Annotated }; - PTreeNode *parent{nullptr}; - PTreeNodePtr left; - PTreeNodePtr right; + ExecutionTreeNode *parent{nullptr}; + ExecutionTreeNodePtr left; + ExecutionTreeNodePtr right; ExecutionState *state{nullptr}; - PTreeNode(PTreeNode *parent, ExecutionState *state) noexcept; - virtual ~PTreeNode() = default; - PTreeNode(const PTreeNode &) = delete; - PTreeNode &operator=(PTreeNode const &) = delete; - PTreeNode(PTreeNode &&) = delete; - PTreeNode &operator=(PTreeNode &&) = delete; + ExecutionTreeNode(ExecutionTreeNode *parent, ExecutionState *state) noexcept; + virtual ~ExecutionTreeNode() = default; + ExecutionTreeNode(const ExecutionTreeNode &) = delete; + ExecutionTreeNode &operator=(ExecutionTreeNode const &) = delete; + ExecutionTreeNode(ExecutionTreeNode &&) = delete; + ExecutionTreeNode &operator=(ExecutionTreeNode &&) = delete; [[nodiscard]] virtual NodeType getType() const { return NodeType::Basic; } - static bool classof(const PTreeNode *N) { return true; } + static bool classof(const ExecutionTreeNode *N) { return true; } }; -class AnnotatedPTreeNode : public PTreeNode { +class AnnotatedExecutionTreeNode : public ExecutionTreeNode { inline static std::uint32_t nextID{1}; public: @@ -68,112 +69,135 @@ public: std::uint32_t asmLine{0}; std::variant<BranchType, StateTerminationType> kind{BranchType::NONE}; - AnnotatedPTreeNode(PTreeNode *parent, ExecutionState *state) noexcept; - ~AnnotatedPTreeNode() override = default; + AnnotatedExecutionTreeNode(ExecutionTreeNode *parent, + ExecutionState *state) noexcept; + ~AnnotatedExecutionTreeNode() override = default; [[nodiscard]] NodeType getType() const override { return NodeType::Annotated; } - static bool classof(const PTreeNode *N) { + + static bool classof(const ExecutionTreeNode *N) { return N->getType() == NodeType::Annotated; } }; -class PTree { +class ExecutionTree { public: - enum class PTreeType : std::uint8_t { Basic, Noop, InMemory, Persistent }; - - /// Branch from PTreeNode and attach states, convention: rightState is + enum class ExecutionTreeType : std::uint8_t { + Basic, + Noop, + InMemory, + Persistent + }; + + /// Branch from ExecutionTreeNode and attach states, convention: rightState is /// parent - virtual void attach(PTreeNode *node, ExecutionState *leftState, + virtual void attach(ExecutionTreeNode *node, ExecutionState *leftState, ExecutionState *rightState, BranchType reason) = 0; - /// Dump process tree in .dot format into os (debug) + /// Dump execution tree in .dot format into os (debug) virtual void dump(llvm::raw_ostream &os) = 0; /// Remove node from tree - virtual void remove(PTreeNode *node) = 0; + virtual void remove(ExecutionTreeNode *node) = 0; /// Set termination type (on state removal) virtual void setTerminationType(ExecutionState &state, StateTerminationType type){} - virtual ~PTree() = default; - PTree(PTree const &) = delete; - PTree &operator=(PTree const &) = delete; - PTree(PTree &&) = delete; - PTree &operator=(PTree &&) = delete; + virtual ~ExecutionTree() = default; + ExecutionTree(ExecutionTree const &) = delete; + ExecutionTree &operator=(ExecutionTree const &) = delete; + ExecutionTree(ExecutionTree &&) = delete; + ExecutionTree &operator=(ExecutionTree &&) = delete; - [[nodiscard]] virtual PTreeType getType() const = 0; - static bool classof(const PTreeNode *N) { return true; } + [[nodiscard]] virtual ExecutionTreeType getType() const = 0; + static bool classof(const ExecutionTreeNode *N) { return true; } protected: - explicit PTree() noexcept = default; + explicit ExecutionTree() noexcept = default; }; -/// @brief A pseudo process tree that does not maintain any nodes. -class NoopPTree final : public PTree { +/// @brief A pseudo execution tree that does not maintain any nodes. +class NoopExecutionTree final : public ExecutionTree { public: - NoopPTree() noexcept = default; - ~NoopPTree() override = default; - void attach(PTreeNode *node, ExecutionState *leftState, - ExecutionState *rightState, - BranchType reason) noexcept override{} + NoopExecutionTree() noexcept = default; + ~NoopExecutionTree() override = default; + void attach(ExecutionTreeNode *node, ExecutionState *leftState, + ExecutionState *rightState, BranchType reason) noexcept override {} void dump(llvm::raw_ostream &os) noexcept override; - void remove(PTreeNode *node) noexcept override{} + void remove(ExecutionTreeNode *node) noexcept override {} - [[nodiscard]] PTreeType getType() const override { return PTreeType::Noop; }; - static bool classof(const PTree *T) { return T->getType() == PTreeType::Noop; } + [[nodiscard]] ExecutionTreeType getType() const override { + return ExecutionTreeType::Noop; + }; + + static bool classof(const ExecutionTree *T) { + return T->getType() == ExecutionTreeType::Noop; + } }; -/// @brief An in-memory process tree required by RandomPathSearcher -class InMemoryPTree : public PTree { +/// @brief An in-memory execution tree required by RandomPathSearcher +class InMemoryExecutionTree : public ExecutionTree { public: - PTreeNodePtr root; + ExecutionTreeNodePtr root; private: /// Number of registered IDs ("users", e.g. RandomPathSearcher) std::uint8_t registeredIds = 0; - virtual PTreeNode *createNode(PTreeNode *parent, ExecutionState *state); - virtual void updateBranchingNode(PTreeNode &node, BranchType reason){} - virtual void updateTerminatingNode(PTreeNode &node){} + virtual ExecutionTreeNode *createNode(ExecutionTreeNode *parent, + ExecutionState *state); + virtual void updateBranchingNode(ExecutionTreeNode &node, BranchType reason) {} + virtual void updateTerminatingNode(ExecutionTreeNode &node) {} public: - InMemoryPTree() noexcept = default; - explicit InMemoryPTree(ExecutionState &initialState) noexcept; - ~InMemoryPTree() override = default; + InMemoryExecutionTree() noexcept = default; + explicit InMemoryExecutionTree(ExecutionState &initialState) noexcept; + ~InMemoryExecutionTree() override = default; - void attach(PTreeNode *node, ExecutionState *leftState, + void attach(ExecutionTreeNode *node, ExecutionState *leftState, ExecutionState *rightState, BranchType reason) noexcept override; void dump(llvm::raw_ostream &os) noexcept override; std::uint8_t getNextId() noexcept; - void remove(PTreeNode *node) noexcept override; + void remove(ExecutionTreeNode *node) noexcept override; - [[nodiscard]] PTreeType getType() const override { return PTreeType::InMemory; }; - static bool classof(const PTree *T) { - return (T->getType() == PTreeType::InMemory) || (T->getType() == PTreeType::Persistent); + [[nodiscard]] ExecutionTreeType getType() const override { + return ExecutionTreeType::InMemory; + }; + + static bool classof(const ExecutionTree *T) { + return (T->getType() == ExecutionTreeType::InMemory) || + (T->getType() == ExecutionTreeType::Persistent); } }; -/// @brief An in-memory process tree that also writes its nodes into an SQLite -/// database (ptree.db) with a PTreeWriter -class PersistentPTree : public InMemoryPTree { - PTreeWriter writer; +/// @brief An in-memory execution tree that also writes its nodes into an SQLite +/// database (exec_tree.db) with a ExecutionTreeWriter +class PersistentExecutionTree : public InMemoryExecutionTree { + ExecutionTreeWriter writer; - PTreeNode *createNode(PTreeNode *parent, ExecutionState *state) override; - void updateBranchingNode(PTreeNode &node, BranchType reason) override; - void updateTerminatingNode(PTreeNode &node) override; + ExecutionTreeNode *createNode(ExecutionTreeNode *parent, + ExecutionState *state) override; + void updateBranchingNode(ExecutionTreeNode &node, BranchType reason) override; + void updateTerminatingNode(ExecutionTreeNode &node) override; public: - explicit PersistentPTree(ExecutionState &initialState, - InterpreterHandler &ih) noexcept; - ~PersistentPTree() override = default; + explicit PersistentExecutionTree(ExecutionState &initialState, + InterpreterHandler &ih) noexcept; + ~PersistentExecutionTree() override = default; void dump(llvm::raw_ostream &os) noexcept override; void setTerminationType(ExecutionState &state, StateTerminationType type) override; - [[nodiscard]] PTreeType getType() const override { return PTreeType::Persistent; }; - static bool classof(const PTree *T) { return T->getType() == PTreeType::Persistent; } + [[nodiscard]] ExecutionTreeType getType() const override { + return ExecutionTreeType::Persistent; + }; + + static bool classof(const ExecutionTree *T) { + return T->getType() == ExecutionTreeType::Persistent; + } }; -std::unique_ptr<PTree> createPTree(ExecutionState &initialState, bool inMemory, - InterpreterHandler &ih); +std::unique_ptr<ExecutionTree> createExecutionTree(ExecutionState &initialState, + bool inMemory, + InterpreterHandler &ih); } // namespace klee -#endif /* KLEE_PTREE_H */ +#endif /* KLEE_EXECUTION_TREE_H */ diff --git a/lib/Core/ExecutionTreeWriter.cpp b/lib/Core/ExecutionTreeWriter.cpp index a8067a5d..10cd5c27 100644 --- a/lib/Core/ExecutionTreeWriter.cpp +++ b/lib/Core/ExecutionTreeWriter.cpp @@ -1,4 +1,4 @@ -//===-- PTreeWriter.cpp ---------------------------------------------------===// +//===-- ExecutionTreeWriter.cpp -------------------------------------------===// // // The KLEE Symbolic Virtual Machine // @@ -7,9 +7,9 @@ // //===----------------------------------------------------------------------===// -#include "PTreeWriter.h" +#include "ExecutionTreeWriter.h" -#include "PTree.h" +#include "ExecutionTree.h" #include "klee/Support/ErrorHandling.h" #include "klee/Support/OptionCategories.h" @@ -18,9 +18,9 @@ namespace { llvm::cl::opt<unsigned> BatchSize( "ptree-batch-size", llvm::cl::init(100U), - llvm::cl::desc("Number of process tree nodes to batch for writing, " - "see --write-ptree (default=100)"), - llvm::cl::cat(klee::PTreeCat)); + llvm::cl::desc("Number of execution tree nodes to batch for writing, " + "see --write-execution-tree (default=100)"), + llvm::cl::cat(klee::ExecTreeCat)); } // namespace using namespace klee; @@ -34,28 +34,29 @@ void prepare_statement(sqlite3 *db, const std::string &query, sqlite3_stmt **stm result = sqlite3_prepare_v3(db, query.c_str(), -1, 0, stmt, nullptr); #endif if (result != SQLITE_OK) { - klee_warning("Process tree database: can't prepare query: %s [%s]", + klee_warning("Execution tree database: cannot prepare query: %s [%s]", sqlite3_errmsg(db), query.c_str()); sqlite3_close(db); - klee_error("Process tree database: can't prepare query: %s", query.c_str()); + klee_error("Execution tree database: cannot prepare query: %s", + query.c_str()); } } -PTreeWriter::PTreeWriter(const std::string &dbPath) { +ExecutionTreeWriter::ExecutionTreeWriter(const std::string &dbPath) { // create database file if (sqlite3_open(dbPath.c_str(), &db) != SQLITE_OK) - klee_error("Can't create process tree database: %s", sqlite3_errmsg(db)); + klee_error("Cannot create execution tree database: %s", sqlite3_errmsg(db)); // - set options: asynchronous + WAL char *errMsg = nullptr; if (sqlite3_exec(db, "PRAGMA synchronous = OFF;", nullptr, nullptr, &errMsg) != SQLITE_OK) { - klee_warning("Process tree database: can't set option: %s", errMsg); + klee_warning("Execution tree database: cannot set option: %s", errMsg); sqlite3_free(errMsg); } if (sqlite3_exec(db, "PRAGMA journal_mode = WAL;", nullptr, nullptr, &errMsg) != SQLITE_OK) { - klee_warning("Process tree database: can't set option: %s", errMsg); + klee_warning("Execution tree database: cannot set option: %s", errMsg); sqlite3_free(errMsg); } @@ -66,10 +67,10 @@ PTreeWriter::PTreeWriter(const std::string &dbPath) { "asmLine INT, kind INT);"; char *zErr = nullptr; if (sqlite3_exec(db, query.c_str(), nullptr, nullptr, &zErr) != SQLITE_OK) { - klee_warning("Process tree database: initialisation error: %s", zErr); + klee_warning("Execution tree database: initialisation error: %s", zErr); sqlite3_free(zErr); sqlite3_close(db); - klee_error("Process tree database: initialisation error."); + klee_error("Execution tree database: initialisation error."); } // create prepared statements @@ -85,16 +86,16 @@ PTreeWriter::PTreeWriter(const std::string &dbPath) { // begin transaction if (sqlite3_step(transactionBeginStmt) != SQLITE_DONE) { - klee_warning("Process tree database: can't begin transaction: %s", + klee_warning("Execution tree database: cannot begin transaction: %s", sqlite3_errmsg(db)); } if (sqlite3_reset(transactionBeginStmt) != SQLITE_OK) { - klee_warning("Process tree database: can't reset transaction: %s", + klee_warning("Execution tree database: cannot reset transaction: %s", sqlite3_errmsg(db)); } } -PTreeWriter::~PTreeWriter() { +ExecutionTreeWriter::~ExecutionTreeWriter() { batchCommit(!flushed); // finalize prepared statements @@ -105,39 +106,39 @@ PTreeWriter::~PTreeWriter() { // commit if (sqlite3_exec(db, "END TRANSACTION", nullptr, nullptr, nullptr) != SQLITE_OK) { - klee_warning("Process tree database: can't end transaction: %s", + klee_warning("Execution tree database: cannot end transaction: %s", sqlite3_errmsg(db)); } if (sqlite3_close(db) != SQLITE_OK) { - klee_warning("Process tree database: can't close database: %s", + klee_warning("Execution tree database: cannot close database: %s", sqlite3_errmsg(db)); } } -void PTreeWriter::batchCommit(bool force) { +void ExecutionTreeWriter::batchCommit(bool force) { ++batch; if (batch < BatchSize && !force) return; // commit and begin transaction if (sqlite3_step(transactionCommitStmt) != SQLITE_DONE) { - klee_warning("Process tree database: transaction commit error: %s", + klee_warning("Execution tree database: transaction commit error: %s", sqlite3_errmsg(db)); } if (sqlite3_reset(transactionCommitStmt) != SQLITE_OK) { - klee_warning("Process tree database: transaction reset error: %s", + klee_warning("Execution tree database: transaction reset error: %s", sqlite3_errmsg(db)); } if (sqlite3_step(transactionBeginStmt) != SQLITE_DONE) { - klee_warning("Process tree database: transaction begin error: %s", + klee_warning("Execution tree database: transaction begin error: %s", sqlite3_errmsg(db)); } if (sqlite3_reset(transactionBeginStmt) != SQLITE_OK) { - klee_warning("Process tree database: transaction reset error: %s", + klee_warning("Execution tree database: transaction reset error: %s", sqlite3_errmsg(db)); } @@ -145,7 +146,7 @@ void PTreeWriter::batchCommit(bool force) { flushed = true; } -void PTreeWriter::write(const AnnotatedPTreeNode &node) { +void ExecutionTreeWriter::write(const AnnotatedExecutionTreeNode &node) { unsigned rc = 0; // bind values (SQLITE_OK is defined as 0 - just check success once at the @@ -155,12 +156,12 @@ void PTreeWriter::write(const AnnotatedPTreeNode &node) { rc |= sqlite3_bind_int64( insertStmt, 3, node.left.getPointer() - ? (static_cast<AnnotatedPTreeNode *>(node.left.getPointer()))->id + ? (static_cast<AnnotatedExecutionTreeNode *>(node.left.getPointer()))->id : 0); rc |= sqlite3_bind_int64( insertStmt, 4, node.right.getPointer() - ? (static_cast<AnnotatedPTreeNode *>(node.right.getPointer()))->id + ? (static_cast<AnnotatedExecutionTreeNode *>(node.right.getPointer()))->id : 0); rc |= sqlite3_bind_int(insertStmt, 5, node.asmLine); std::uint8_t value{0}; @@ -170,25 +171,26 @@ void PTreeWriter::write(const AnnotatedPTreeNode &node) { value = static_cast<std::uint8_t>(std::get<StateTerminationType>(node.kind)); } else { - assert(false && "PTreeWriter: Illegal node kind!"); + assert(false && "ExecutionTreeWriter: Illegal node kind!"); } rc |= sqlite3_bind_int(insertStmt, 6, value); if (rc != SQLITE_OK) { // This is either a programming error (e.g. SQLITE_MISUSE) or we ran out of // resources (e.g. SQLITE_NOMEM). Calling sqlite3_errmsg() after a possible // successful call above is undefined, hence no error message here. - klee_error("Process tree database: can't persist data for node: %u", + klee_error("Execution tree database: cannot persist data for node: %u", node.id); } // insert if (sqlite3_step(insertStmt) != SQLITE_DONE) { - klee_warning("Process tree database: can't persist data for node: %u: %s", - node.id, sqlite3_errmsg(db)); + klee_warning( + "Execution tree database: cannot persist data for node: %u: %s", + node.id, sqlite3_errmsg(db)); } if (sqlite3_reset(insertStmt) != SQLITE_OK) { - klee_warning("Process tree database: error reset node: %u: %s", node.id, + klee_warning("Execution tree database: error reset node: %u: %s", node.id, sqlite3_errmsg(db)); } diff --git a/lib/Core/ExecutionTreeWriter.h b/lib/Core/ExecutionTreeWriter.h index 12709116..d78ad0b1 100644 --- a/lib/Core/ExecutionTreeWriter.h +++ b/lib/Core/ExecutionTreeWriter.h @@ -1,4 +1,4 @@ -//===-- PTreeWriter.h -------------------------------------------*- C++ -*-===// +//===-- ExecutionTreeWriter.h -----------------------------------*- C++ -*-===// // // The KLEE Symbolic Virtual Machine // @@ -15,11 +15,11 @@ #include <string> namespace klee { -class AnnotatedPTreeNode; +class AnnotatedExecutionTreeNode; -/// @brief Writes process tree nodes into an SQLite database -class PTreeWriter { - friend class PersistentPTree; +/// @brief Writes execution tree nodes into an SQLite database +class ExecutionTreeWriter { + friend class PersistentExecutionTree; ::sqlite3 *db{nullptr}; ::sqlite3_stmt *insertStmt{nullptr}; @@ -32,15 +32,15 @@ class PTreeWriter { void batchCommit(bool force = false); public: - explicit PTreeWriter(const std::string &dbPath); - ~PTreeWriter(); - PTreeWriter(const PTreeWriter &other) = delete; - PTreeWriter(PTreeWriter &&other) noexcept = delete; - PTreeWriter &operator=(const PTreeWriter &other) = delete; - PTreeWriter &operator=(PTreeWriter &&other) noexcept = delete; + explicit ExecutionTreeWriter(const std::string &dbPath); + ~ExecutionTreeWriter(); + ExecutionTreeWriter(const ExecutionTreeWriter &other) = delete; + ExecutionTreeWriter(ExecutionTreeWriter &&other) noexcept = delete; + ExecutionTreeWriter &operator=(const ExecutionTreeWriter &other) = delete; + ExecutionTreeWriter &operator=(ExecutionTreeWriter &&other) noexcept = delete; /// Write new node into database - void write(const AnnotatedPTreeNode &node); + void write(const AnnotatedExecutionTreeNode &node); }; } // namespace klee diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 8f70540c..cf6ce777 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -13,12 +13,12 @@ #include "Context.h" #include "CoreStats.h" #include "ExecutionState.h" +#include "ExecutionTree.h" #include "ExternalDispatcher.h" #include "GetElementPtrTypeIterator.h" #include "ImpliedValue.h" #include "Memory.h" #include "MemoryManager.h" -#include "PTree.h" #include "Searcher.h" #include "SeedInfo.h" #include "SpecialFunctionHandler.h" @@ -469,8 +469,8 @@ cl::opt<bool> DebugCheckForImpliedValues( } // namespace // XXX hack -extern "C" unsigned dumpStates, dumpPTree; -unsigned dumpStates = 0, dumpPTree = 0; +extern "C" unsigned dumpStates, dumpExecutionTree; +unsigned dumpStates = 0, dumpExecutionTree = 0; Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts, InterpreterHandler *ih) @@ -918,7 +918,7 @@ void Executor::branch(ExecutionState &state, ExecutionState *ns = es->branch(); addedStates.push_back(ns); result.push_back(ns); - processTree->attach(es->ptreeNode, ns, es, reason); + executionTree->attach(es->executionTreeNode, ns, es, reason); } } @@ -1189,7 +1189,7 @@ Executor::StatePair Executor::fork(ExecutionState ¤t, ref<Expr> condition, } } - processTree->attach(current.ptreeNode, falseState, trueState, reason); + executionTree->attach(current.executionTreeNode, falseState, trueState, reason); stats::incBranchStat(reason, 1); if (pathWriter) { @@ -3355,7 +3355,7 @@ void Executor::updateStates(ExecutionState *current) { seedMap.find(es); if (it3 != seedMap.end()) seedMap.erase(it3); - processTree->remove(es->ptreeNode); + executionTree->remove(es->executionTreeNode); delete es; } removedStates.clear(); @@ -3522,7 +3522,8 @@ void Executor::run(ExecutionState &initialState) { executeInstruction(state, ki); timers.invoke(); if (::dumpStates) dumpStates(); - if (::dumpPTree) dumpPTree(); + if (::dumpExecutionTree) + dumpExecutionTree(); updateStates(&state); if ((stats::instructions % 1000) == 0) { @@ -3571,7 +3572,8 @@ void Executor::run(ExecutionState &initialState) { executeInstruction(state, ki); timers.invoke(); if (::dumpStates) dumpStates(); - if (::dumpPTree) dumpPTree(); + if (::dumpExecutionTree) + dumpExecutionTree(); updateStates(&state); @@ -3647,7 +3649,7 @@ void Executor::terminateState(ExecutionState &state, } interpreterHandler->incPathsExplored(); - processTree->setTerminationType(state, reason); + executionTree->setTerminationType(state, reason); std::vector<ExecutionState *>::iterator it = std::find(addedStates.begin(), addedStates.end(), &state); @@ -3662,7 +3664,7 @@ void Executor::terminateState(ExecutionState &state, if (it3 != seedMap.end()) seedMap.erase(it3); addedStates.erase(it); - processTree->remove(state.ptreeNode); + executionTree->remove(state.executionTreeNode); delete &state; } } @@ -4607,10 +4609,10 @@ void Executor::runFunctionAsMain(Function *f, initializeGlobals(*state); - processTree = createPTree(*state, userSearcherRequiresInMemoryPTree(), - *interpreterHandler); + executionTree = createExecutionTree( + *state, userSearcherRequiresInMemoryExecutionTree(), *interpreterHandler); run(*state); - processTree = nullptr; + executionTree = nullptr; // hack to clear memory objects memory = nullptr; @@ -4840,18 +4842,17 @@ int *Executor::getErrnoLocation(const ExecutionState &state) const { #endif } - -void Executor::dumpPTree() { - if (!::dumpPTree) return; +void Executor::dumpExecutionTree() { + if (!::dumpExecutionTree) + return; char name[32]; - snprintf(name, sizeof(name),"ptree%08d.dot", (int) stats::instructions); + snprintf(name, sizeof(name), "exec_tree%08d.dot", (int)stats::instructions); auto os = interpreterHandler->openOutputFile(name); - if (os) { - processTree->dump(*os); - } + if (os) + executionTree->dump(*os); - ::dumpPTree = 0; + ::dumpExecutionTree = 0; } void Executor::dumpStates() { diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 3635de78..f7f84101 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -57,38 +57,36 @@ namespace llvm { class Value; } -namespace klee { - class Array; - struct Cell; - class ExecutionState; - class ExternalDispatcher; - class Expr; - class InstructionInfoTable; - class KCallable; - struct KFunction; - struct KInstruction; - class KInstIterator; - class KModule; - class MemoryManager; - class MemoryObject; - class ObjectState; - class PTree; - class Searcher; - class SeedInfo; - class SpecialFunctionHandler; - struct StackFrame; - class StatsTracker; - class TimingSolver; - class TreeStreamWriter; - class MergeHandler; - class MergingSearcher; - template<class T> class ref; - - - - /// \todo Add a context object to keep track of data only live - /// during an instruction step. Should contain addedStates, - /// removedStates, and haltExecution, among others. +namespace klee { +class Array; +struct Cell; +class ExecutionState; +class ExternalDispatcher; +class Expr; +class InstructionInfoTable; +class KCallable; +struct KFunction; +struct KInstruction; +class KInstIterator; +class KModule; +class MemoryManager; +class MemoryObject; +class ObjectState; +class ExecutionTree; +class Searcher; +class SeedInfo; +class SpecialFunctionHandler; +struct StackFrame; +class StatsTracker; +class TimingSolver; +class TreeStreamWriter; +class MergeHandler; +class MergingSearcher; +template <class T> class ref; + +/// \todo Add a context object to keep track of data only live +/// during an instruction step. Should contain addedStates, +/// removedStates, and haltExecution, among others. class Executor : public Interpreter { friend class OwningSearcher; @@ -117,7 +115,7 @@ private: TreeStreamWriter *pathWriter, *symPathWriter; SpecialFunctionHandler *specialFunctionHandler; TimerGroup timers; - std::unique_ptr<PTree> processTree; + std::unique_ptr<ExecutionTree> executionTree; /// Used to track states that have been added during the current /// instructions step. @@ -501,7 +499,7 @@ private: /// Only for debug purposes; enable via debugger or klee-control void dumpStates(); - void dumpPTree(); + void dumpExecutionTree(); public: Executor(llvm::LLVMContext &ctx, const InterpreterOptions &opts, @@ -576,7 +574,7 @@ public: MergingSearcher *getMergingSearcher() const { return mergingSearcher; }; void setMergingSearcher(MergingSearcher *ms) { mergingSearcher = ms; }; }; - -} // End klee namespace + +} // namespace klee #endif /* KLEE_EXECUTOR_H */ diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp index 1c57eb4e..e94511ea 100644 --- a/lib/Core/Searcher.cpp +++ b/lib/Core/Searcher.cpp @@ -11,9 +11,9 @@ #include "CoreStats.h" #include "ExecutionState.h" +#include "ExecutionTree.h" #include "Executor.h" #include "MergeHandler.h" -#include "PTree.h" #include "StatsTracker.h" #include "klee/ADT/DiscretePDF.h" @@ -261,18 +261,17 @@ void WeightedRandomSearcher::printName(llvm::raw_ostream &os) { #define IS_OUR_NODE_VALID(n) \ (((n).getPointer() != nullptr) && (((n).getInt() & idBitMask) != 0)) -RandomPathSearcher::RandomPathSearcher(InMemoryPTree *processTree, RNG &rng) - : processTree{processTree}, theRNG{rng}, - idBitMask{ - static_cast<uint8_t>(processTree ? processTree->getNextId() : 0)} { - - assert(processTree); +RandomPathSearcher::RandomPathSearcher(InMemoryExecutionTree *executionTree, RNG &rng) + : executionTree{executionTree}, theRNG{rng}, + idBitMask{static_cast<uint8_t>(executionTree ? executionTree->getNextId() : 0)} { + assert(executionTree); }; ExecutionState &RandomPathSearcher::selectState() { unsigned flips=0, bits=0; - assert(processTree->root.getInt() & idBitMask && "Root should belong to the searcher"); - PTreeNode *n = processTree->root.getPointer(); + assert(executionTree->root.getInt() & idBitMask && + "Root should belong to the searcher"); + ExecutionTreeNode *n = executionTree->root.getPointer(); while (!n->state) { if (!IS_OUR_NODE_VALID(n->left)) { assert(IS_OUR_NODE_VALID(n->right) && "Both left and right nodes invalid"); @@ -300,46 +299,47 @@ void RandomPathSearcher::update(ExecutionState *current, const std::vector<ExecutionState *> &removedStates) { // insert states for (auto es : addedStates) { - PTreeNode *pnode = es->ptreeNode, *parent = pnode->parent; - PTreeNodePtr *childPtr; + ExecutionTreeNode *etnode = es->executionTreeNode, *parent = etnode->parent; + ExecutionTreeNodePtr *childPtr; - childPtr = parent ? ((parent->left.getPointer() == pnode) ? &parent->left - : &parent->right) - : &processTree->root; - while (pnode && !IS_OUR_NODE_VALID(*childPtr)) { + childPtr = parent ? ((parent->left.getPointer() == etnode) ? &parent->left + : &parent->right) + : &executionTree->root; + while (etnode && !IS_OUR_NODE_VALID(*childPtr)) { childPtr->setInt(childPtr->getInt() | idBitMask); - pnode = parent; - if (pnode) - parent = pnode->parent; + etnode = parent; + if (etnode) + parent = etnode->parent; childPtr = parent - ? ((parent->left.getPointer() == pnode) ? &parent->left - : &parent->right) - : &processTree->root; + ? ((parent->left.getPointer() == etnode) ? &parent->left + : &parent->right) + : &executionTree->root; } } // remove states for (auto es : removedStates) { - PTreeNode *pnode = es->ptreeNode, *parent = pnode->parent; + ExecutionTreeNode *etnode = es->executionTreeNode, *parent = etnode->parent; - while (pnode && !IS_OUR_NODE_VALID(pnode->left) && - !IS_OUR_NODE_VALID(pnode->right)) { + while (etnode && !IS_OUR_NODE_VALID(etnode->left) && + !IS_OUR_NODE_VALID(etnode->right)) { auto childPtr = - parent ? ((parent->left.getPointer() == pnode) ? &parent->left - : &parent->right) - : &processTree->root; - assert(IS_OUR_NODE_VALID(*childPtr) && "Removing pTree child not ours"); + parent ? ((parent->left.getPointer() == etnode) ? &parent->left + : &parent->right) + : &executionTree->root; + assert(IS_OUR_NODE_VALID(*childPtr) && + "Removing executionTree child not ours"); childPtr->setInt(childPtr->getInt() & ~idBitMask); - pnode = parent; - if (pnode) - parent = pnode->parent; + etnode = parent; + if (etnode) + parent = etnode->parent; } } } bool RandomPathSearcher::empty() { - return !IS_OUR_NODE_VALID(processTree->root); + return !IS_OUR_NODE_VALID(executionTree->root); } void RandomPathSearcher::printName(llvm::raw_ostream &os) { diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h index ddd49264..36efe67a 100644 --- a/lib/Core/Searcher.h +++ b/lib/Core/Searcher.h @@ -11,7 +11,7 @@ #define KLEE_SEARCHER_H #include "ExecutionState.h" -#include "PTree.h" +#include "ExecutionTree.h" #include "klee/ADT/RNG.h" #include "klee/System/Time.h" @@ -89,10 +89,11 @@ namespace klee { void printName(llvm::raw_ostream &os) override; }; - /// BFSSearcher implements breadth-first exploration. When KLEE branches multiple - /// times for a single instruction, all new states have the same depth. Keep in - /// mind that the process tree (PTree) is a binary tree and hence the depth of - /// a state in that tree and its branch depth during BFS are different. + /// BFSSearcher implements breadth-first exploration. When KLEE branches + /// multiple times for a single instruction, all new states have the same + /// depth. Keep in mind that the execution tree (ExecutionTree) is a binary + /// tree and hence the depth of a state in that tree and its branch depth + /// during BFS are different. class BFSSearcher final : public Searcher { std::deque<ExecutionState*> states; @@ -156,32 +157,35 @@ namespace klee { void printName(llvm::raw_ostream &os) override; }; - /// RandomPathSearcher performs a random walk of the PTree to select a state. - /// PTree is a global data structure, however, a searcher can sometimes only - /// select from a subset of all states (depending on the update calls). + /// RandomPathSearcher performs a random walk of the ExecutionTree to select a + /// state. ExecutionTree is a global data structure, however, a searcher can + /// sometimes only select from a subset of all states (depending on the update + /// calls). /// - /// To support this, RandomPathSearcher has a subgraph view of PTree, in that it - /// only walks the PTreeNodes that it "owns". Ownership is stored in the - /// getInt method of the PTreeNodePtr class (which hides it in the pointer itself). + /// To support this, RandomPathSearcher has a subgraph view of ExecutionTree, + /// in that it only walks the ExecutionTreeNodes that it "owns". Ownership is + /// stored in the getInt method of the ExecutionTreeNodePtr class (which hides + /// it in the pointer itself). /// - /// The current implementation of PTreeNodePtr supports only 3 instances of the - /// RandomPathSearcher. This is because the current PTreeNodePtr implementation - /// conforms to C++ and only steals the last 3 alignment bits. This restriction - /// could be relaxed slightly by an architecture-specific implementation of - /// PTreeNodePtr that also steals the top bits of the pointer. + /// The current implementation of ExecutionTreeNodePtr supports only 3 + /// instances of the RandomPathSearcher. This is because the current + /// ExecutionTreeNodePtr implementation conforms to C++ and only steals the + /// last 3 alignment bits. This restriction could be relaxed slightly by an + /// architecture-specific implementation of ExecutionTreeNodePtr that also + /// steals the top bits of the pointer. /// /// The ownership bits are maintained in the update method. class RandomPathSearcher final : public Searcher { - InMemoryPTree *processTree; + InMemoryExecutionTree *executionTree; RNG &theRNG; // Unique bitmask of this searcher const uint8_t idBitMask; public: - /// \param processTree The process tree. + /// \param executionTree The execution tree. /// \param RNG A random number generator. - RandomPathSearcher(InMemoryPTree *processTree, RNG &rng); + RandomPathSearcher(InMemoryExecutionTree *executionTree, RNG &rng); ~RandomPathSearcher() override = default; ExecutionState &selectState() override; diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp index 735075f1..7e0fd31f 100644 --- a/lib/Core/UserSearcher.cpp +++ b/lib/Core/UserSearcher.cpp @@ -100,19 +100,20 @@ bool userSearcherRequiresMD2U() { std::find(CoreSearch.begin(), CoreSearch.end(), Searcher::NURS_QC) != CoreSearch.end()); } -bool userSearcherRequiresInMemoryPTree() { +bool userSearcherRequiresInMemoryExecutionTree() { return std::find(CoreSearch.begin(), CoreSearch.end(), Searcher::RandomPath) != CoreSearch.end(); } } // namespace klee -Searcher *getNewSearcher(Searcher::CoreSearchType type, RNG &rng, InMemoryPTree *processTree) { +Searcher *getNewSearcher(Searcher::CoreSearchType type, RNG &rng, + InMemoryExecutionTree *executionTree) { Searcher *searcher = nullptr; switch (type) { case Searcher::DFS: searcher = new DFSSearcher(); break; case Searcher::BFS: searcher = new BFSSearcher(); break; case Searcher::RandomState: searcher = new RandomSearcher(rng); break; - case Searcher::RandomPath: searcher = new RandomPathSearcher(processTree, rng); break; + case Searcher::RandomPath: searcher = new RandomPathSearcher(executionTree, rng); break; case Searcher::NURS_CovNew: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::CoveringNew, rng); break; case Searcher::NURS_MD2U: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::MinDistToUncovered, rng); break; case Searcher::NURS_Depth: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::Depth, rng); break; @@ -126,15 +127,16 @@ Searcher *getNewSearcher(Searcher::CoreSearchType type, RNG &rng, InMemoryPTree } Searcher *klee::constructUserSearcher(Executor &executor) { - auto *ptree = llvm::dyn_cast<InMemoryPTree>(executor.processTree.get()); - Searcher *searcher = getNewSearcher(CoreSearch[0], executor.theRNG, ptree); + auto *etree = + llvm::dyn_cast<InMemoryExecutionTree>(executor.executionTree.get()); + Searcher *searcher = getNewSearcher(CoreSearch[0], executor.theRNG, etree); if (CoreSearch.size() > 1) { std::vector<Searcher *> s; s.push_back(searcher); for (unsigned i = 1; i < CoreSearch.size(); i++) - s.push_back(getNewSearcher(CoreSearch[i], executor.theRNG, ptree)); + s.push_back(getNewSearcher(CoreSearch[i], executor.theRNG, etree)); searcher = new InterleavedSearcher(s); } diff --git a/lib/Core/UserSearcher.h b/lib/Core/UserSearcher.h index fe75eb6d..af582455 100644 --- a/lib/Core/UserSearcher.h +++ b/lib/Core/UserSearcher.h @@ -16,7 +16,7 @@ namespace klee { // XXX gross, should be on demand? bool userSearcherRequiresMD2U(); - bool userSearcherRequiresInMemoryPTree(); + bool userSearcherRequiresInMemoryExecutionTree(); void initializeSearchOptions(); diff --git a/scripts/klee-control b/scripts/klee-control index 0a918b42..e9d22db6 100755 --- a/scripts/klee-control +++ b/scripts/klee-control @@ -77,7 +77,7 @@ def main(): if opts.dumpStates: execCmd(pid, "p dumpStates = 1", opts) if opts.dumpTree: - execCmd(pid, "p dumpPTree = 1", opts) + execCmd(pid, "p dumpExecutionTree = 1", opts) if opts.stopForking: execCmd(pid, 'p stop_forking()', opts) if opts.haltExecution: diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index ae038b80..a7d748c6 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -147,7 +147,7 @@ file(GENERATE add_custom_target(systemtests COMMAND "${LIT_TOOL}" ${LIT_ARGS} "${CMAKE_CURRENT_BINARY_DIR}" - DEPENDS klee kleaver klee-ptree klee-replay kleeRuntest ktest-gen ktest-randgen + DEPENDS klee kleaver klee-exec-tree klee-replay kleeRuntest ktest-gen ktest-randgen COMMENT "Running system tests" USES_TERMINAL ) diff --git a/test/Feature/KleeExecTreeBogus.test b/test/Feature/KleeExecTreeBogus.test index 11fe87c8..5926d128 100644 --- a/test/Feature/KleeExecTreeBogus.test +++ b/test/Feature/KleeExecTreeBogus.test @@ -1,65 +1,65 @@ REQUIRES: sqlite3 fail on broken db (not sqlite) -RUN: not %klee-ptree tree-info %S/ptree-dbs/not_a.db 2> %t.err +RUN: not %klee-exec-tree tree-info %S/exec-tree-dbs/not_a.db 2> %t.err RUN: FileCheck -check-prefix=CHECK-CORRUPT -input-file=%t.err %s -CHECK-CORRUPT: Can't prepare read statement: file is not a database +CHECK-CORRUPT: Cannot prepare read statement: file is not a database empty tree RUN: rm -f %t.db -RUN: %sqlite3 -separator ',' %t.db ".import %S/ptree-dbs/empty_db.csv nodes" -RUN: %klee-ptree tree-info %t.db > %t.err +RUN: %sqlite3 -separator ',' %t.db ".import %S/exec-tree-dbs/empty_db.csv nodes" +RUN: %klee-exec-tree tree-info %t.db > %t.err RUN: FileCheck -check-prefix=CHECK-EMPTY -input-file=%t.err %s CHECK-EMPTY: Empty tree. fail on tree with duplicate node IDs RUN: rm -f %t.db -RUN: %sqlite3 -separator ',' %t.db ".import %S/ptree-dbs/duplicated_node.csv nodes" -RUN: not %klee-ptree tree-info %t.db 2> %t.err +RUN: %sqlite3 -separator ',' %t.db ".import %S/exec-tree-dbs/duplicated_node.csv nodes" +RUN: not %klee-exec-tree tree-info %t.db 2> %t.err RUN: FileCheck -check-prefix=CHECK-DUP -input-file=%t.err %s -CHECK-DUP: PTree DB contains duplicate child reference or circular structure. Affected node: 2 +CHECK-DUP: ExecutionTree DB contains duplicate child reference or circular structure. Affected node: 2 fail on invalid branch type RUN: rm -f %t.db -RUN: %sqlite3 -separator ',' %t.db ".import %S/ptree-dbs/invalid_btype.csv nodes" -RUN: not %klee-ptree tree-info %t.db 2> %t.err +RUN: %sqlite3 -separator ',' %t.db ".import %S/exec-tree-dbs/invalid_btype.csv nodes" +RUN: not %klee-exec-tree tree-info %t.db 2> %t.err RUN: FileCheck -check-prefix=CHECK-BTYPE -input-file=%t.err %s -CHECK-BTYPE: PTree DB contains unknown branch type (123) in node 1 +CHECK-BTYPE: ExecutionTree DB contains unknown branch type (123) in node 1 fail on invalid termination type RUN: rm -f %t.db -RUN: %sqlite3 -separator ',' %t.db ".import %S/ptree-dbs/invalid_ttype.csv nodes" -RUN: not %klee-ptree tree-info %t.db 2> %t.err +RUN: %sqlite3 -separator ',' %t.db ".import %S/exec-tree-dbs/invalid_ttype.csv nodes" +RUN: not %klee-exec-tree tree-info %t.db 2> %t.err RUN: FileCheck -check-prefix=CHECK-TTYPE -input-file=%t.err %s -CHECK-TTYPE: PTree DB contains unknown termination type (123) in node 3 +CHECK-TTYPE: ExecutionTree DB contains unknown termination type (123) in node 3 fail on tree with looping nodes RUN: rm -f %t.db -RUN: %sqlite3 -separator ',' %t.db ".import %S/ptree-dbs/loop.csv nodes" -RUN: not %klee-ptree tree-info %t.db 2> %t.err +RUN: %sqlite3 -separator ',' %t.db ".import %S/exec-tree-dbs/loop.csv nodes" +RUN: not %klee-exec-tree tree-info %t.db 2> %t.err RUN: FileCheck -check-prefix=CHECK-LOOP -input-file=%t.err %s -CHECK-LOOP: PTree DB contains duplicate child reference or circular structure. Affected node: 1 +CHECK-LOOP: ExecutionTree DB contains duplicate child reference or circular structure. Affected node: 1 fail on tree with missing node (child node ID > max. ID) RUN: rm -f %t.db -RUN: %sqlite3 -separator ',' %t.db ".import %S/ptree-dbs/missing_after_max.csv nodes" -RUN: not %klee-ptree tree-info %t.db 2> %t.err +RUN: %sqlite3 -separator ',' %t.db ".import %S/exec-tree-dbs/missing_after_max.csv nodes" +RUN: not %klee-exec-tree tree-info %t.db 2> %t.err RUN: FileCheck -check-prefix=CHECK-MISSA -input-file=%t.err %s -CHECK-MISSA: PTree DB contains references to non-existing nodes (> max. ID) in node 3 +CHECK-MISSA: ExecutionTree DB contains references to non-existing nodes (> max. ID) in node 3 fail on tree with missing node (child node ID < max. ID) RUN: rm -f %t.db -RUN: %sqlite3 -separator ',' %t.db ".import %S/ptree-dbs/missing_before_max.csv nodes" -RUN: not %klee-ptree tree-info %t.db 2> %t.err +RUN: %sqlite3 -separator ',' %t.db ".import %S/exec-tree-dbs/missing_before_max.csv nodes" +RUN: not %klee-exec-tree tree-info %t.db 2> %t.err RUN: FileCheck -check-prefix=CHECK-MISSB -input-file=%t.err %s -CHECK-MISSB: PTree DB references undefined node. Affected node: 4 +CHECK-MISSB: ExecutionTree DB references undefined node. Affected node: 4 fail on illegal node ID (0) RUN: rm -f %t.db -RUN: %sqlite3 -separator ',' %t.db ".import %S/ptree-dbs/node_id0.csv nodes" -RUN: not %klee-ptree tree-info %t.db 2> %t.err +RUN: %sqlite3 -separator ',' %t.db ".import %S/exec-tree-dbs/node_id0.csv nodes" +RUN: not %klee-exec-tree tree-info %t.db 2> %t.err RUN: FileCheck -check-prefix=CHECK-ID0 -input-file=%t.err %s -CHECK-ID0: PTree DB contains illegal node ID (0) +CHECK-ID0: ExecutionTree DB contains illegal node ID (0) cleanup RUN rm -f %t.db diff --git a/test/Feature/WriteExecutionTree.c b/test/Feature/WriteExecutionTree.c index e7bf59ce..42f531a5 100644 --- a/test/Feature/WriteExecutionTree.c +++ b/test/Feature/WriteExecutionTree.c @@ -1,13 +1,13 @@ // RUN: %clang %s -emit-llvm %O0opt -g -c -o %t.bc // RUN: rm -rf %t.klee-out -// RUN: %klee -write-ptree --output-dir=%t.klee-out %t.bc -// RUN: %klee-ptree branches %t.klee-out/ptree.db | FileCheck --check-prefix=CHECK-BRANCH %s -// RUN: %klee-ptree depths %t.klee-out | FileCheck --check-prefix=CHECK-DEPTH %s -// RUN: %klee-ptree instructions %t.klee-out | FileCheck --check-prefix=CHECK-INSTR %s -// RUN: %klee-ptree terminations %t.klee-out | FileCheck --check-prefix=CHECK-TERM %s -// RUN: %klee-ptree tree-dot %t.klee-out | FileCheck --check-prefix=CHECK-DOT %s -// RUN: %klee-ptree tree-info %t.klee-out | FileCheck --check-prefix=CHECK-TINFO %s -// RUN: not %klee-ptree dot %t.klee-out/ptree-doesnotexist.db +// RUN: %klee -write-exec-tree --output-dir=%t.klee-out %t.bc +// RUN: %klee-exec-tree branches %t.klee-out/exec_tree.db | FileCheck --check-prefix=CHECK-BRANCH %s +// RUN: %klee-exec-tree depths %t.klee-out | FileCheck --check-prefix=CHECK-DEPTH %s +// RUN: %klee-exec-tree instructions %t.klee-out | FileCheck --check-prefix=CHECK-INSTR %s +// RUN: %klee-exec-tree terminations %t.klee-out | FileCheck --check-prefix=CHECK-TERM %s +// RUN: %klee-exec-tree tree-dot %t.klee-out | FileCheck --check-prefix=CHECK-DOT %s +// RUN: %klee-exec-tree tree-info %t.klee-out | FileCheck --check-prefix=CHECK-TINFO %s +// RUN: not %klee-exec-tree dot %t.klee-out/exec-tree-doesnotexist.db #include "klee/klee.h" @@ -61,7 +61,7 @@ int main(void) { // CHECK-TERM-DAG: User,2 // CHECK-TERM-DAG: SilentExit,2 -// CHECK-DOT: strict digraph PTree { +// CHECK-DOT: strict digraph ExecutionTree { // CHECK-DOT: node[shape=point,width=0.15,color=darkgrey]; // CHECK-DOT: edge[color=darkgrey]; // CHECK-DOT-DAG: N{{[0-9]+}}[tooltip="Conditional\nnode: {{[0-9]+}}\nstate: 0\nasm: {{[0-9]+}}"]; diff --git a/test/lit.cfg b/test/lit.cfg index 8abf7012..52869d34 100644 --- a/test/lit.cfg +++ b/test/lit.cfg @@ -139,7 +139,7 @@ if len(kleaver_extra_params) != 0: # If a tool's name is a prefix of another, the longer name has # to come first, e.g., klee-replay should come before klee subs = [ ('%kleaver', 'kleaver', kleaver_extra_params), - ('%klee-ptree', 'klee-ptree', ''), + ('%klee-exec-tree', 'klee-exec-tree', ''), ('%klee-replay', 'klee-replay', ''), ('%klee-stats', 'klee-stats', ''), ('%klee-zesti', 'klee-zesti', ''), 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); diff --git a/unittests/Searcher/SearcherTest.cpp b/unittests/Searcher/SearcherTest.cpp index f9089615..8b3ba7df 100644 --- a/unittests/Searcher/SearcherTest.cpp +++ b/unittests/Searcher/SearcherTest.cpp @@ -10,10 +10,10 @@ #include "gtest/gtest.h" -#include "klee/ADT/RNG.h" #include "Core/ExecutionState.h" -#include "Core/PTree.h" +#include "Core/ExecutionTree.h" #include "Core/Searcher.h" +#include "klee/ADT/RNG.h" #include "llvm/Support/raw_ostream.h" @@ -24,10 +24,10 @@ namespace { TEST(SearcherTest, RandomPath) { // First state ExecutionState es; - InMemoryPTree processTree(es); + InMemoryExecutionTree executionTree(es); RNG rng; - RandomPathSearcher rp(&processTree, rng); + RandomPathSearcher rp(&executionTree, rng); EXPECT_TRUE(rp.empty()); rp.update(nullptr, {&es}, {}); @@ -36,7 +36,8 @@ TEST(SearcherTest, RandomPath) { // Two states ExecutionState es1(es); - processTree.attach(es.ptreeNode, &es1, &es, BranchType::Conditional); + executionTree.attach(es.executionTreeNode, &es1, &es, + BranchType::Conditional); rp.update(&es, {&es1}, {}); // Random path seed dependant @@ -50,27 +51,28 @@ TEST(SearcherTest, RandomPath) { } rp.update(&es, {&es1}, {&es}); - processTree.remove(es.ptreeNode); + executionTree.remove(es.executionTreeNode); for (int i = 0; i < 100; i++) { EXPECT_EQ(&rp.selectState(), &es1); } rp.update(&es1, {}, {&es1}); - processTree.remove(es1.ptreeNode); + executionTree.remove(es1.executionTreeNode); EXPECT_TRUE(rp.empty()); } TEST(SearcherTest, TwoRandomPath) { // Root state ExecutionState root; - InMemoryPTree processTree(root); + InMemoryExecutionTree executionTree(root); ExecutionState es(root); - processTree.attach(root.ptreeNode, &es, &root, BranchType::Conditional); + executionTree.attach(root.executionTreeNode, &es, &root, + BranchType::Conditional); RNG rng, rng1; - RandomPathSearcher rp(&processTree, rng); - RandomPathSearcher rp1(&processTree, rng1); + RandomPathSearcher rp(&executionTree, rng); + RandomPathSearcher rp1(&executionTree, rng1); EXPECT_TRUE(rp.empty()); EXPECT_TRUE(rp1.empty()); @@ -81,7 +83,8 @@ TEST(SearcherTest, TwoRandomPath) { // Two states ExecutionState es1(es); - processTree.attach(es.ptreeNode, &es1, &es, BranchType::Conditional); + executionTree.attach(es.executionTreeNode, &es1, &es, + BranchType::Conditional); rp.update(&es, {}, {}); rp1.update(nullptr, {&es1}, {}); @@ -101,49 +104,50 @@ TEST(SearcherTest, TwoRandomPath) { } rp1.update(&es, {}, {&es}); - processTree.remove(es.ptreeNode); + executionTree.remove(es.executionTreeNode); EXPECT_TRUE(rp1.empty()); EXPECT_EQ(&rp.selectState(), &es1); rp.update(&es1, {}, {&es1}); - processTree.remove(es1.ptreeNode); + executionTree.remove(es1.executionTreeNode); EXPECT_TRUE(rp.empty()); EXPECT_TRUE(rp1.empty()); - processTree.remove(root.ptreeNode); + executionTree.remove(root.executionTreeNode); } TEST(SearcherTest, TwoRandomPathDot) { - std::stringstream modelPTreeDot; - PTreeNode *rootPNode, *rightLeafPNode, *esParentPNode, *es1LeafPNode, - *esLeafPNode; + std::stringstream modelExecutionTreeDot; + ExecutionTreeNode *rootExecutionTreeNode, *rightLeafExecutionTreeNode, + *esParentExecutionTreeNode, *es1LeafExecutionTreeNode, + *esLeafExecutionTreeNode; // Root state ExecutionState root; - InMemoryPTree processTree(root); - rootPNode = root.ptreeNode; + InMemoryExecutionTree executionTree(root); + rootExecutionTreeNode = root.executionTreeNode; ExecutionState es(root); - processTree.attach(root.ptreeNode, &es, &root, BranchType::NONE); - rightLeafPNode = root.ptreeNode; - esParentPNode = es.ptreeNode; + executionTree.attach(root.executionTreeNode, &es, &root, BranchType::NONE); + rightLeafExecutionTreeNode = root.executionTreeNode; + esParentExecutionTreeNode = es.executionTreeNode; RNG rng; - RandomPathSearcher rp(&processTree, rng); - RandomPathSearcher rp1(&processTree, rng); + RandomPathSearcher rp(&executionTree, rng); + RandomPathSearcher rp1(&executionTree, rng); rp.update(nullptr, {&es}, {}); ExecutionState es1(es); - processTree.attach(es.ptreeNode, &es1, &es, BranchType::NONE); - esLeafPNode = es.ptreeNode; - es1LeafPNode = es1.ptreeNode; + executionTree.attach(es.executionTreeNode, &es1, &es, BranchType::NONE); + esLeafExecutionTreeNode = es.executionTreeNode; + es1LeafExecutionTreeNode = es1.executionTreeNode; rp.update(&es, {}, {}); rp1.update(nullptr, {&es1}, {}); - // Compare PTree to model PTree - modelPTreeDot + // Compare ExecutionTree to model ExecutionTree + modelExecutionTreeDot << "digraph G {\n" << "\tsize=\"10,7.5\";\n" << "\tratio=fill;\n" @@ -151,30 +155,29 @@ TEST(SearcherTest, TwoRandomPathDot) { << "\tcenter = \"true\";\n" << "\tnode [style=\"filled\",width=.1,height=.1,fontname=\"Terminus\"]\n" << "\tedge [arrowsize=.3]\n" - << "\tn" << rootPNode << " [shape=diamond];\n" - << "\tn" << rootPNode << " -> n" << esParentPNode << " [label=0b011];\n" - << "\tn" << rootPNode << " -> n" << rightLeafPNode << " [label=0b000];\n" - << "\tn" << rightLeafPNode << " [shape=diamond,fillcolor=green];\n" - << "\tn" << esParentPNode << " [shape=diamond];\n" - << "\tn" << esParentPNode << " -> n" << es1LeafPNode - << " [label=0b010];\n" - << "\tn" << esParentPNode << " -> n" << esLeafPNode << " [label=0b001];\n" - << "\tn" << esLeafPNode << " [shape=diamond,fillcolor=green];\n" - << "\tn" << es1LeafPNode << " [shape=diamond,fillcolor=green];\n" + << "\tn" << rootExecutionTreeNode << " [shape=diamond];\n" + << "\tn" << rootExecutionTreeNode << " -> n" << esParentExecutionTreeNode << " [label=0b011];\n" + << "\tn" << rootExecutionTreeNode << " -> n" << rightLeafExecutionTreeNode << " [label=0b000];\n" + << "\tn" << rightLeafExecutionTreeNode << " [shape=diamond,fillcolor=green];\n" + << "\tn" << esParentExecutionTreeNode << " [shape=diamond];\n" + << "\tn" << esParentExecutionTreeNode << " -> n" << es1LeafExecutionTreeNode << " [label=0b010];\n" + << "\tn" << esParentExecutionTreeNode << " -> n" << esLeafExecutionTreeNode << " [label=0b001];\n" + << "\tn" << esLeafExecutionTreeNode << " [shape=diamond,fillcolor=green];\n" + << "\tn" << es1LeafExecutionTreeNode << " [shape=diamond,fillcolor=green];\n" << "}\n"; - std::string pTreeDot; - llvm::raw_string_ostream pTreeDotStream(pTreeDot); - processTree.dump(pTreeDotStream); - EXPECT_EQ(modelPTreeDot.str(), pTreeDotStream.str()); + std::string executionTreeDot; + llvm::raw_string_ostream executionTreeDotStream(executionTreeDot); + executionTree.dump(executionTreeDotStream); + EXPECT_EQ(modelExecutionTreeDot.str(), executionTreeDotStream.str()); rp.update(&es, {&es1}, {&es}); rp1.update(nullptr, {&es}, {&es1}); rp1.update(&es, {}, {&es}); - processTree.remove(es.ptreeNode); + executionTree.remove(es.executionTreeNode); - modelPTreeDot.str(""); - modelPTreeDot + modelExecutionTreeDot.str(""); + modelExecutionTreeDot << "digraph G {\n" << "\tsize=\"10,7.5\";\n" << "\tratio=fill;\n" @@ -182,33 +185,32 @@ TEST(SearcherTest, TwoRandomPathDot) { << "\tcenter = \"true\";\n" << "\tnode [style=\"filled\",width=.1,height=.1,fontname=\"Terminus\"]\n" << "\tedge [arrowsize=.3]\n" - << "\tn" << rootPNode << " [shape=diamond];\n" - << "\tn" << rootPNode << " -> n" << esParentPNode << " [label=0b001];\n" - << "\tn" << rootPNode << " -> n" << rightLeafPNode << " [label=0b000];\n" - << "\tn" << rightLeafPNode << " [shape=diamond,fillcolor=green];\n" - << "\tn" << esParentPNode << " [shape=diamond];\n" - << "\tn" << esParentPNode << " -> n" << es1LeafPNode - << " [label=0b001];\n" - << "\tn" << es1LeafPNode << " [shape=diamond,fillcolor=green];\n" + << "\tn" << rootExecutionTreeNode << " [shape=diamond];\n" + << "\tn" << rootExecutionTreeNode << " -> n" << esParentExecutionTreeNode << " [label=0b001];\n" + << "\tn" << rootExecutionTreeNode << " -> n" << rightLeafExecutionTreeNode << " [label=0b000];\n" + << "\tn" << rightLeafExecutionTreeNode << " [shape=diamond,fillcolor=green];\n" + << "\tn" << esParentExecutionTreeNode << " [shape=diamond];\n" + << "\tn" << esParentExecutionTreeNode << " -> n" << es1LeafExecutionTreeNode << " [label=0b001];\n" + << "\tn" << es1LeafExecutionTreeNode << " [shape=diamond,fillcolor=green];\n" << "}\n"; - pTreeDot = ""; - processTree.dump(pTreeDotStream); - EXPECT_EQ(modelPTreeDot.str(), pTreeDotStream.str()); - processTree.remove(es1.ptreeNode); - processTree.remove(root.ptreeNode); + executionTreeDot = ""; + executionTree.dump(executionTreeDotStream); + EXPECT_EQ(modelExecutionTreeDot.str(), executionTreeDotStream.str()); + executionTree.remove(es1.executionTreeNode); + executionTree.remove(root.executionTreeNode); } TEST(SearcherDeathTest, TooManyRandomPaths) { // First state ExecutionState es; - InMemoryPTree processTree(es); - processTree.remove(es.ptreeNode); // Need to remove to avoid leaks + InMemoryExecutionTree executionTree(es); + executionTree.remove(es.executionTreeNode); // Need to remove to avoid leaks RNG rng; - RandomPathSearcher rp(&processTree, rng); - RandomPathSearcher rp1(&processTree, rng); - RandomPathSearcher rp2(&processTree, rng); - ASSERT_DEATH({ RandomPathSearcher rp3(&processTree, rng); }, ""); + RandomPathSearcher rp(&executionTree, rng); + RandomPathSearcher rp1(&executionTree, rng); + RandomPathSearcher rp2(&executionTree, rng); + ASSERT_DEATH({ RandomPathSearcher rp3(&executionTree, rng); }, ""); } } |