From 19b6ae578b0658115d15848604a28434845bb3e3 Mon Sep 17 00:00:00 2001 From: Frank Busse Date: Fri, 24 Mar 2023 21:14:02 +0000 Subject: new: persistent ptree (-write-ptree) and klee-ptree Introduce three different kinds of process trees: 1. Noop: does nothing (e.g. no allocations for DFS) 2. InMemory: same behaviour as before (e.g. RandomPathSearcher) 3. Persistent: similar to InMemory but writes nodes to ptree.db and tracks information such as branch type, termination type or source location (asm) in nodes. Enabled with -write-ptree ptree.db files can be analysed/plotted with the new "klee-ptree" tool. --- CMakeLists.txt | 10 + include/klee/Support/OptionCategories.h | 1 + lib/Core/CMakeLists.txt | 1 + lib/Core/Executor.cpp | 23 ++- lib/Core/Executor.h | 5 +- lib/Core/PTree.cpp | 172 +++++++++++++---- lib/Core/PTree.h | 205 +++++++++++++++----- lib/Core/PTreeWriter.cpp | 196 +++++++++++++++++++ lib/Core/PTreeWriter.h | 46 +++++ lib/Core/Searcher.cpp | 23 ++- lib/Core/Searcher.h | 4 +- lib/Core/SpecialFunctionHandler.cpp | 8 +- lib/Core/UserSearcher.cpp | 12 +- lib/Core/UserSearcher.h | 1 + test/CMakeLists.txt | 2 +- test/Feature/KleePtreeBogus.test | 65 +++++++ test/Feature/WritePtree.c | 78 ++++++++ test/Feature/ptree-dbs/duplicated_node.csv | 5 + test/Feature/ptree-dbs/empty_db.csv | 1 + test/Feature/ptree-dbs/invalid_btype.csv | 4 + test/Feature/ptree-dbs/invalid_ttype.csv | 4 + test/Feature/ptree-dbs/loop.csv | 5 + test/Feature/ptree-dbs/missing_after_max.csv | 5 + test/Feature/ptree-dbs/missing_before_max.csv | 5 + test/Feature/ptree-dbs/node_id0.csv | 6 + test/Feature/ptree-dbs/not_a.db | 1 + test/lit.cfg | 9 + test/lit.site.cfg.in | 3 + tools/CMakeLists.txt | 1 + tools/klee-ptree/CMakeLists.txt | 16 ++ tools/klee-ptree/DFSVisitor.cpp | 46 +++++ tools/klee-ptree/DFSVisitor.h | 31 +++ tools/klee-ptree/Printers.cpp | 266 ++++++++++++++++++++++++++ tools/klee-ptree/Printers.h | 30 +++ tools/klee-ptree/Tree.cpp | 208 ++++++++++++++++++++ tools/klee-ptree/Tree.h | 53 +++++ tools/klee-ptree/main.cpp | 68 +++++++ tools/klee/main.cpp | 2 +- unittests/Searcher/CMakeLists.txt | 4 +- unittests/Searcher/SearcherTest.cpp | 26 +-- 40 files changed, 1520 insertions(+), 131 deletions(-) create mode 100644 lib/Core/PTreeWriter.cpp create mode 100644 lib/Core/PTreeWriter.h create mode 100644 test/Feature/KleePtreeBogus.test create mode 100644 test/Feature/WritePtree.c create mode 100644 test/Feature/ptree-dbs/duplicated_node.csv create mode 100644 test/Feature/ptree-dbs/empty_db.csv create mode 100644 test/Feature/ptree-dbs/invalid_btype.csv create mode 100644 test/Feature/ptree-dbs/invalid_ttype.csv create mode 100644 test/Feature/ptree-dbs/loop.csv create mode 100644 test/Feature/ptree-dbs/missing_after_max.csv create mode 100644 test/Feature/ptree-dbs/missing_before_max.csv create mode 100644 test/Feature/ptree-dbs/node_id0.csv create mode 100644 test/Feature/ptree-dbs/not_a.db create mode 100644 tools/klee-ptree/CMakeLists.txt create mode 100644 tools/klee-ptree/DFSVisitor.cpp create mode 100644 tools/klee-ptree/DFSVisitor.h create mode 100644 tools/klee-ptree/Printers.cpp create mode 100644 tools/klee-ptree/Printers.h create mode 100644 tools/klee-ptree/Tree.cpp create mode 100644 tools/klee-ptree/Tree.h create mode 100644 tools/klee-ptree/main.cpp diff --git a/CMakeLists.txt b/CMakeLists.txt index 19e9fc06..4fd68d42 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -310,6 +310,16 @@ if (NOT SQLite3_FOUND) message( FATAL_ERROR "SQLite3 not found, please install" ) endif() +find_program( + SQLITE_CLI + NAMES "sqlite3" + DOC "Path to sqlite3 tool" +) + +if (NOT SQLITE_CLI) + set(SQLITE_CLI "") +endif() + ################################################################################ # Detect libcap ################################################################################ diff --git a/include/klee/Support/OptionCategories.h b/include/klee/Support/OptionCategories.h index 430ff7b1..152241c9 100644 --- a/include/klee/Support/OptionCategories.h +++ b/include/klee/Support/OptionCategories.h @@ -29,6 +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 SeedingCat; extern llvm::cl::OptionCategory SolvingCat; extern llvm::cl::OptionCategory StatsCat; diff --git a/lib/Core/CMakeLists.txt b/lib/Core/CMakeLists.txt index 9005a1ff..8df3e259 100644 --- a/lib/Core/CMakeLists.txt +++ b/lib/Core/CMakeLists.txt @@ -20,6 +20,7 @@ add_library(kleeCore Memory.cpp MemoryManager.cpp PTree.cpp + PTreeWriter.cpp Searcher.cpp SeedInfo.cpp SpecialFunctionHandler.cpp diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index b4da6a08..8f70540c 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -3639,14 +3639,15 @@ std::string Executor::getAddressInfo(ExecutionState &state, return info.str(); } - -void Executor::terminateState(ExecutionState &state) { +void Executor::terminateState(ExecutionState &state, + StateTerminationType reason) { if (replayKTest && replayPosition!=replayKTest->numObjects) { klee_warning_once(replayKTest, "replay did not consume all objects in test input."); } interpreterHandler->incPathsExplored(); + processTree->setTerminationType(state, reason); std::vector::iterator it = std::find(addedStates.begin(), addedStates.end(), &state); @@ -3690,7 +3691,7 @@ void Executor::terminateStateOnExit(ExecutionState &state) { terminationTypeFileExtension(StateTerminationType::Exit).c_str()); interpreterHandler->incPathsCompleted(); - terminateState(state); + terminateState(state, StateTerminationType::Exit); } void Executor::terminateStateEarly(ExecutionState &state, const Twine &message, @@ -3707,7 +3708,7 @@ void Executor::terminateStateEarly(ExecutionState &state, const Twine &message, terminationTypeFileExtension(reason).c_str()); } - terminateState(state); + terminateState(state, reason); } void Executor::terminateStateEarlyAlgorithm(ExecutionState &state, @@ -3815,7 +3816,7 @@ void Executor::terminateStateOnError(ExecutionState &state, interpreterHandler->processTestCase(state, msg.str().c_str(), file_suffix); } - terminateState(state); + terminateState(state, terminationType); if (shouldExitOn(terminationType)) haltExecution = true; @@ -3848,9 +3849,14 @@ void Executor::terminateStateOnSolverError(ExecutionState &state, } void Executor::terminateStateOnUserError(ExecutionState &state, - const llvm::Twine &message) { + const llvm::Twine &message, + bool writeErr) { ++stats::terminationUserError; - terminateStateOnError(state, message, StateTerminationType::User, ""); + if (writeErr) { + terminateStateOnError(state, message, StateTerminationType::User, ""); + } else { + terminateState(state, StateTerminationType::User); + } } // XXX shoot me @@ -4601,7 +4607,8 @@ void Executor::runFunctionAsMain(Function *f, initializeGlobals(*state); - processTree = std::make_unique(state); + processTree = createPTree(*state, userSearcherRequiresInMemoryPTree(), + *interpreterHandler); run(*state); processTree = nullptr; diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 204638e8..3635de78 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -412,7 +412,7 @@ private: /// Remove state from queue and delete state. This function should only be /// used in the termination functions below. - void terminateState(ExecutionState &state); + void terminateState(ExecutionState &state, StateTerminationType reason); /// Call exit handler and terminate state normally /// (end of execution path) @@ -467,7 +467,8 @@ private: /// Call error handler and terminate state for user errors /// (e.g. wrong usage of klee.h API) void terminateStateOnUserError(ExecutionState &state, - const llvm::Twine &message); + const llvm::Twine &message, + bool writeErr = true); /// bindModuleConstants - Initialize the module constant table. void bindModuleConstants(); diff --git a/lib/Core/PTree.cpp b/lib/Core/PTree.cpp index 6c17e296..c5b640d3 100644 --- a/lib/Core/PTree.cpp +++ b/lib/Core/PTree.cpp @@ -11,49 +11,88 @@ #include "ExecutionState.h" -#include "klee/Expr/Expr.h" +#include "klee/Core/Interpreter.h" #include "klee/Expr/ExprPPrinter.h" +#include "klee/Module/KInstruction.h" #include "klee/Support/OptionCategories.h" #include #include using namespace klee; -using namespace llvm; + +namespace klee { +llvm::cl::OptionCategory + PTreeCat("Process tree related options", + "These options affect the process tree handling."); +} namespace { +llvm::cl::opt CompressProcessTree( + "compress-process-tree", + llvm::cl::desc("Remove intermediate nodes in the process " + "tree whenever possible (default=false)"), + llvm::cl::init(false), llvm::cl::cat(PTreeCat)); + +llvm::cl::opt WritePTree( + "write-ptree", llvm::cl::init(false), + llvm::cl::desc("Write process tree into ptree.db (default=false)"), + llvm::cl::cat(PTreeCat)); +} // namespace -cl::opt - CompressProcessTree("compress-process-tree", - cl::desc("Remove intermediate nodes in the process " - "tree whenever possible (default=false)"), - cl::init(false), cl::cat(MiscCat)); +// PTreeNode -} // namespace +PTreeNode::PTreeNode(PTreeNode *parent, ExecutionState *state) noexcept + : parent{parent}, left{nullptr}, right{nullptr}, state{state} { + state->ptreeNode = this; +} + +// AnnotatedPTreeNode + +AnnotatedPTreeNode::AnnotatedPTreeNode(PTreeNode *parent, + ExecutionState *state) noexcept + : PTreeNode(parent, state) { + id = nextID++; +} -PTree::PTree(ExecutionState *initialState) - : root(PTreeNodePtr(new PTreeNode(nullptr, initialState))) { - initialState->ptreeNode = root.getPointer(); +// NoopPTree + +void NoopPTree::dump(llvm::raw_ostream &os) noexcept { + os << "digraph G {\nTreeNotAvailable [shape=box]\n}"; } -void PTree::attach(PTreeNode *node, ExecutionState *leftState, - ExecutionState *rightState, BranchType reason) { +// InMemoryPTree + +InMemoryPTree::InMemoryPTree(ExecutionState &initialState) noexcept { + root = PTreeNodePtr(createNode(nullptr, &initialState)); + initialState.ptreeNode = root.getPointer(); +} + +PTreeNode *InMemoryPTree::createNode(PTreeNode *parent, ExecutionState *state) { + return new PTreeNode(parent, state); +} + +void InMemoryPTree::attach(PTreeNode *node, ExecutionState *leftState, + ExecutionState *rightState, + BranchType reason) noexcept { assert(node && !node->left.getPointer() && !node->right.getPointer()); assert(node == rightState->ptreeNode && "Attach assumes the right state is the current state"); - node->state = nullptr; - node->left = PTreeNodePtr(new PTreeNode(node, leftState)); + node->left = PTreeNodePtr(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(new PTreeNode(node, rightState), currentNodeTag); + node->right = PTreeNodePtr(createNode(node, rightState), currentNodeTag); + updateBranchingNode(*node, reason); + node->state = nullptr; } -void PTree::remove(PTreeNode *n) { +void InMemoryPTree::remove(PTreeNode *n) noexcept { assert(!n->left.getPointer() && !n->right.getPointer()); + updateTerminatingNode(*n); do { PTreeNode *p = n->parent; if (p) { @@ -92,17 +131,17 @@ void PTree::remove(PTreeNode *n) { } } -void PTree::dump(llvm::raw_ostream &os) { - ExprPPrinter *pp = ExprPPrinter::create(os); +void InMemoryPTree::dump(llvm::raw_ostream &os) noexcept { + std::unique_ptr pp(ExprPPrinter::create(os)); pp->setNewline("\\l"); - os << "digraph G {\n"; - os << "\tsize=\"10,7.5\";\n"; - os << "\tratio=fill;\n"; - os << "\trotate=90;\n"; - os << "\tcenter = \"true\";\n"; - os << "\tnode [style=\"filled\",width=.1,height=.1,fontname=\"Terminus\"]\n"; - os << "\tedge [arrowsize=.3]\n"; - std::vector stack; + os << "digraph G {\n" + << "\tsize=\"10,7.5\";\n" + << "\tratio=fill;\n" + << "\trotate=90;\n" + << "\tcenter = \"true\";\n" + << "\tnode [style=\"filled\",width=.1,height=.1,fontname=\"Terminus\"]\n" + << "\tedge [arrowsize=.3]\n"; + std::vector stack; stack.push_back(root.getPointer()); while (!stack.empty()) { const PTreeNode *n = stack.back(); @@ -112,24 +151,85 @@ void PTree::dump(llvm::raw_ostream &os) { os << ",fillcolor=green"; os << "];\n"; if (n->left.getPointer()) { - os << "\tn" << n << " -> n" << n->left.getPointer(); - os << " [label=0b" + os << "\tn" << n << " -> n" << n->left.getPointer() << " [label=0b" << std::bitset(n->left.getInt()).to_string() << "];\n"; stack.push_back(n->left.getPointer()); } if (n->right.getPointer()) { - os << "\tn" << n << " -> n" << n->right.getPointer(); - os << " [label=0b" + os << "\tn" << n << " -> n" << n->right.getPointer() << " [label=0b" << std::bitset(n->right.getInt()).to_string() << "];\n"; stack.push_back(n->right.getPointer()); } } os << "}\n"; - delete pp; } -PTreeNode::PTreeNode(PTreeNode *parent, ExecutionState *state) : parent{parent}, state{state} { - state->ptreeNode = this; - left = PTreeNodePtr(nullptr); - right = PTreeNodePtr(nullptr); +std::uint8_t InMemoryPTree::getNextId() noexcept { + static_assert(PtrBitCount <= 8); + std::uint8_t id = 1 << registeredIds++; + if (registeredIds > PtrBitCount) { + klee_error("PTree cannot support more than %d RandomPathSearchers", + PtrBitCount); + } + return id; +} + +// PersistentPTree + +PersistentPTree::PersistentPTree(ExecutionState &initialState, + InterpreterHandler &ih) noexcept + : writer(ih.getOutputFilename("ptree.db")) { + root = PTreeNodePtr(createNode(nullptr, &initialState)); + initialState.ptreeNode = root.getPointer(); +} + +void PersistentPTree::dump(llvm::raw_ostream &os) noexcept { + writer.batchCommit(true); + InMemoryPTree::dump(os); +} + +PTreeNode *PersistentPTree::createNode(PTreeNode *parent, + ExecutionState *state) { + return new AnnotatedPTreeNode(parent, state); +} + +void PersistentPTree::setTerminationType(ExecutionState &state, + StateTerminationType type) { + auto *annotatedNode = llvm::cast(state.ptreeNode); + annotatedNode->kind = type; +} + +void PersistentPTree::updateBranchingNode(PTreeNode &node, BranchType reason) { + auto *annotatedNode = llvm::cast(&node); + const auto &state = *node.state; + const auto prevPC = state.prevPC; + annotatedNode->asmLine = + prevPC && prevPC->info ? prevPC->info->assemblyLine : 0; + annotatedNode->kind = reason; + writer.write(*annotatedNode); +} + +void PersistentPTree::updateTerminatingNode(PTreeNode &node) { + assert(node.state); + auto *annotatedNode = llvm::cast(&node); + const auto &state = *node.state; + const auto prevPC = state.prevPC; + annotatedNode->asmLine = + prevPC && prevPC->info ? prevPC->info->assemblyLine : 0; + annotatedNode->stateID = state.getID(); + writer.write(*annotatedNode); } + +// Factory + +std::unique_ptr klee::createPTree(ExecutionState &initialState, + bool inMemory, + InterpreterHandler &ih) { + if (WritePTree) + return std::make_unique(initialState, ih); + + if (inMemory) + return std::make_unique(initialState); + + return std::make_unique(); +}; diff --git a/lib/Core/PTree.h b/lib/Core/PTree.h index dbee70dd..ab3f0433 100644 --- a/lib/Core/PTree.h +++ b/lib/Core/PTree.h @@ -10,57 +10,170 @@ #ifndef KLEE_PTREE_H #define KLEE_PTREE_H +#include "PTreeWriter.h" +#include "UserSearcher.h" #include "klee/Core/BranchTypes.h" +#include "klee/Core/TerminationTypes.h" #include "klee/Expr/Expr.h" #include "klee/Support/ErrorHandling.h" + #include "llvm/ADT/PointerIntPair.h" +#include "llvm/Support/Casting.h" + +#include +#include namespace klee { - class ExecutionState; - class PTreeNode; - /* 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. */ - constexpr int PtrBitCount = 3; - using PTreeNodePtr = llvm::PointerIntPair; - - class PTreeNode { - public: - PTreeNode *parent = nullptr; - - PTreeNodePtr left; - PTreeNodePtr right; - ExecutionState *state = nullptr; - - PTreeNode(const PTreeNode&) = delete; - PTreeNode(PTreeNode *parent, ExecutionState *state); - ~PTreeNode() = default; - }; - - class PTree { - // Number of registered ID - int registeredIds = 0; - - public: - PTreeNodePtr root; - explicit PTree(ExecutionState *initialState); - ~PTree() = default; - - void attach(PTreeNode *node, ExecutionState *leftState, - ExecutionState *rightState, BranchType reason); - void remove(PTreeNode *node); - void dump(llvm::raw_ostream &os); - std::uint8_t getNextId() { - std::uint8_t id = 1 << registeredIds++; - if (registeredIds > PtrBitCount) { - klee_error("PTree cannot support more than %d RandomPathSearchers", - PtrBitCount); - } - return id; - } - }; -} +class ExecutionState; +class Executor; +class InMemoryPTree; +class InterpreterHandler; +class PTreeNode; +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. */ +constexpr std::uint8_t PtrBitCount = 3; +using PTreeNodePtr = llvm::PointerIntPair; + +class PTreeNode { +public: + enum class NodeType : std::uint8_t { Basic, Annotated }; + + PTreeNode *parent{nullptr}; + PTreeNodePtr left; + PTreeNodePtr 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; + + [[nodiscard]] virtual NodeType getType() const { return NodeType::Basic; } + static bool classof(const PTreeNode *N) { return true; } +}; + +class AnnotatedPTreeNode : public PTreeNode { + inline static std::uint32_t nextID{1}; + +public: + std::uint32_t id{0}; + std::uint32_t stateID{0}; + std::uint32_t asmLine{0}; + std::variant kind{BranchType::NONE}; + + AnnotatedPTreeNode(PTreeNode *parent, ExecutionState *state) noexcept; + ~AnnotatedPTreeNode() override = default; + + [[nodiscard]] NodeType getType() const override { return NodeType::Annotated; } + static bool classof(const PTreeNode *N) { + return N->getType() == NodeType::Annotated; + } +}; + +class PTree { +public: + enum class PTreeType : std::uint8_t { Basic, Noop, InMemory, Persistent }; + + /// Branch from PTreeNode and attach states, convention: rightState is + /// parent + virtual void attach(PTreeNode *node, ExecutionState *leftState, + ExecutionState *rightState, BranchType reason) = 0; + /// Dump process 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; + /// 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; + + [[nodiscard]] virtual PTreeType getType() const = 0; + static bool classof(const PTreeNode *N) { return true; } + +protected: + explicit PTree() noexcept = default; +}; + +/// @brief A pseudo process tree that does not maintain any nodes. +class NoopPTree final : public PTree { +public: + NoopPTree() noexcept = default; + ~NoopPTree() override = default; + void attach(PTreeNode *node, ExecutionState *leftState, + ExecutionState *rightState, + BranchType reason) noexcept override{} + void dump(llvm::raw_ostream &os) noexcept override; + void remove(PTreeNode *node) noexcept override{} + + [[nodiscard]] PTreeType getType() const override { return PTreeType::Noop; }; + static bool classof(const PTree *T) { return T->getType() == PTreeType::Noop; } +}; + +/// @brief An in-memory process tree required by RandomPathSearcher +class InMemoryPTree : public PTree { +public: + PTreeNodePtr 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){} + +public: + InMemoryPTree() noexcept = default; + explicit InMemoryPTree(ExecutionState &initialState) noexcept; + ~InMemoryPTree() override = default; + + void attach(PTreeNode *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; + + [[nodiscard]] PTreeType getType() const override { return PTreeType::InMemory; }; + static bool classof(const PTree *T) { + return (T->getType() == PTreeType::InMemory) || (T->getType() == PTreeType::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; + + PTreeNode *createNode(PTreeNode *parent, ExecutionState *state) override; + void updateBranchingNode(PTreeNode &node, BranchType reason) override; + void updateTerminatingNode(PTreeNode &node) override; + +public: + explicit PersistentPTree(ExecutionState &initialState, + InterpreterHandler &ih) noexcept; + ~PersistentPTree() 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; } +}; + +std::unique_ptr createPTree(ExecutionState &initialState, bool inMemory, + InterpreterHandler &ih); +} // namespace klee #endif /* KLEE_PTREE_H */ diff --git a/lib/Core/PTreeWriter.cpp b/lib/Core/PTreeWriter.cpp new file mode 100644 index 00000000..a8067a5d --- /dev/null +++ b/lib/Core/PTreeWriter.cpp @@ -0,0 +1,196 @@ +//===-- PTreeWriter.cpp ---------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#include "PTreeWriter.h" + +#include "PTree.h" +#include "klee/Support/ErrorHandling.h" +#include "klee/Support/OptionCategories.h" + +#include "llvm/Support/CommandLine.h" + +namespace { +llvm::cl::opt 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)); +} // namespace + +using namespace klee; + +void prepare_statement(sqlite3 *db, const std::string &query, sqlite3_stmt **stmt) { + int result; +#ifdef SQLITE_PREPARE_PERSISTENT + result = sqlite3_prepare_v3(db, query.c_str(), -1, SQLITE_PREPARE_PERSISTENT, + stmt, nullptr); +#else + 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]", + sqlite3_errmsg(db), query.c_str()); + sqlite3_close(db); + klee_error("Process tree database: can't prepare query: %s", query.c_str()); + } +} + +PTreeWriter::PTreeWriter(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)); + + // - 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); + 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); + sqlite3_free(errMsg); + } + + // - create table + std::string query = + "CREATE TABLE IF NOT EXISTS nodes (" + "ID INT PRIMARY KEY, stateID INT, leftID INT, rightID INT," + "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); + sqlite3_free(zErr); + sqlite3_close(db); + klee_error("Process tree database: initialisation error."); + } + + // create prepared statements + // - insertStmt + query = "INSERT INTO nodes VALUES (?, ?, ?, ?, ?, ?);"; + prepare_statement(db, query, &insertStmt); + // - transactionBeginStmt + query = "BEGIN TRANSACTION"; + prepare_statement(db, query, &transactionBeginStmt); + // - transactionCommitStmt + query = "COMMIT TRANSACTION"; + prepare_statement(db, query, &transactionCommitStmt); + + // begin transaction + if (sqlite3_step(transactionBeginStmt) != SQLITE_DONE) { + klee_warning("Process tree database: can't begin transaction: %s", + sqlite3_errmsg(db)); + } + if (sqlite3_reset(transactionBeginStmt) != SQLITE_OK) { + klee_warning("Process tree database: can't reset transaction: %s", + sqlite3_errmsg(db)); + } +} + +PTreeWriter::~PTreeWriter() { + batchCommit(!flushed); + + // finalize prepared statements + sqlite3_finalize(insertStmt); + sqlite3_finalize(transactionBeginStmt); + sqlite3_finalize(transactionCommitStmt); + + // commit + if (sqlite3_exec(db, "END TRANSACTION", nullptr, nullptr, nullptr) != + SQLITE_OK) { + klee_warning("Process tree database: can't end transaction: %s", + sqlite3_errmsg(db)); + } + + if (sqlite3_close(db) != SQLITE_OK) { + klee_warning("Process tree database: can't close database: %s", + sqlite3_errmsg(db)); + } +} + +void PTreeWriter::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", + sqlite3_errmsg(db)); + } + + if (sqlite3_reset(transactionCommitStmt) != SQLITE_OK) { + klee_warning("Process tree database: transaction reset error: %s", + sqlite3_errmsg(db)); + } + + if (sqlite3_step(transactionBeginStmt) != SQLITE_DONE) { + klee_warning("Process tree database: transaction begin error: %s", + sqlite3_errmsg(db)); + } + + if (sqlite3_reset(transactionBeginStmt) != SQLITE_OK) { + klee_warning("Process tree database: transaction reset error: %s", + sqlite3_errmsg(db)); + } + + batch = 0; + flushed = true; +} + +void PTreeWriter::write(const AnnotatedPTreeNode &node) { + unsigned rc = 0; + + // bind values (SQLITE_OK is defined as 0 - just check success once at the + // end) + rc |= sqlite3_bind_int64(insertStmt, 1, node.id); + rc |= sqlite3_bind_int(insertStmt, 2, node.stateID); + rc |= sqlite3_bind_int64( + insertStmt, 3, + node.left.getPointer() + ? (static_cast(node.left.getPointer()))->id + : 0); + rc |= sqlite3_bind_int64( + insertStmt, 4, + node.right.getPointer() + ? (static_cast(node.right.getPointer()))->id + : 0); + rc |= sqlite3_bind_int(insertStmt, 5, node.asmLine); + std::uint8_t value{0}; + if (std::holds_alternative(node.kind)) { + value = static_cast(std::get(node.kind)); + } else if (std::holds_alternative(node.kind)) { + value = + static_cast(std::get(node.kind)); + } else { + assert(false && "PTreeWriter: 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", + 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)); + } + + if (sqlite3_reset(insertStmt) != SQLITE_OK) { + klee_warning("Process tree database: error reset node: %u: %s", node.id, + sqlite3_errmsg(db)); + } + + batchCommit(); +} diff --git a/lib/Core/PTreeWriter.h b/lib/Core/PTreeWriter.h new file mode 100644 index 00000000..12709116 --- /dev/null +++ b/lib/Core/PTreeWriter.h @@ -0,0 +1,46 @@ +//===-- PTreeWriter.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 + +#include +#include + +namespace klee { +class AnnotatedPTreeNode; + +/// @brief Writes process tree nodes into an SQLite database +class PTreeWriter { + friend class PersistentPTree; + + ::sqlite3 *db{nullptr}; + ::sqlite3_stmt *insertStmt{nullptr}; + ::sqlite3_stmt *transactionBeginStmt{nullptr}; + ::sqlite3_stmt *transactionCommitStmt{nullptr}; + std::uint32_t batch{0}; + bool flushed{true}; + + /// Writes nodes in batches + 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; + + /// Write new node into database + void write(const AnnotatedPTreeNode &node); +}; + +} // namespace klee diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp index bf98ebc7..1c57eb4e 100644 --- a/lib/Core/Searcher.cpp +++ b/lib/Core/Searcher.cpp @@ -261,15 +261,18 @@ void WeightedRandomSearcher::printName(llvm::raw_ostream &os) { #define IS_OUR_NODE_VALID(n) \ (((n).getPointer() != nullptr) && (((n).getInt() & idBitMask) != 0)) -RandomPathSearcher::RandomPathSearcher(PTree &processTree, RNG &rng) - : processTree{processTree}, - theRNG{rng}, - idBitMask{processTree.getNextId()} {}; +RandomPathSearcher::RandomPathSearcher(InMemoryPTree *processTree, RNG &rng) + : processTree{processTree}, theRNG{rng}, + idBitMask{ + static_cast(processTree ? processTree->getNextId() : 0)} { + + assert(processTree); +}; 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(processTree->root.getInt() & idBitMask && "Root should belong to the searcher"); + PTreeNode *n = processTree->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"); @@ -302,7 +305,7 @@ void RandomPathSearcher::update(ExecutionState *current, childPtr = parent ? ((parent->left.getPointer() == pnode) ? &parent->left : &parent->right) - : &processTree.root; + : &processTree->root; while (pnode && !IS_OUR_NODE_VALID(*childPtr)) { childPtr->setInt(childPtr->getInt() | idBitMask); pnode = parent; @@ -312,7 +315,7 @@ void RandomPathSearcher::update(ExecutionState *current, childPtr = parent ? ((parent->left.getPointer() == pnode) ? &parent->left : &parent->right) - : &processTree.root; + : &processTree->root; } } @@ -325,7 +328,7 @@ void RandomPathSearcher::update(ExecutionState *current, auto childPtr = parent ? ((parent->left.getPointer() == pnode) ? &parent->left : &parent->right) - : &processTree.root; + : &processTree->root; assert(IS_OUR_NODE_VALID(*childPtr) && "Removing pTree child not ours"); childPtr->setInt(childPtr->getInt() & ~idBitMask); pnode = parent; @@ -336,7 +339,7 @@ void RandomPathSearcher::update(ExecutionState *current, } bool RandomPathSearcher::empty() { - return !IS_OUR_NODE_VALID(processTree.root); + return !IS_OUR_NODE_VALID(processTree->root); } void RandomPathSearcher::printName(llvm::raw_ostream &os) { diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h index e399c616..ddd49264 100644 --- a/lib/Core/Searcher.h +++ b/lib/Core/Searcher.h @@ -172,7 +172,7 @@ namespace klee { /// /// The ownership bits are maintained in the update method. class RandomPathSearcher final : public Searcher { - PTree &processTree; + InMemoryPTree *processTree; RNG &theRNG; // Unique bitmask of this searcher @@ -181,7 +181,7 @@ namespace klee { public: /// \param processTree The process tree. /// \param RNG A random number generator. - RandomPathSearcher(PTree &processTree, RNG &rng); + RandomPathSearcher(InMemoryPTree *processTree, RNG &rng); ~RandomPathSearcher() override = default; ExecutionState &selectState() override; diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index 488fba51..4589471c 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -480,12 +480,8 @@ void SpecialFunctionHandler::handleAssume(ExecutionState &state, state.constraints, e, res, state.queryMetaData); assert(success && "FIXME: Unhandled solver failure"); if (res) { - if (SilentKleeAssume) { - executor.terminateState(state); - } else { - executor.terminateStateOnUserError( - state, "invalid klee_assume call (provably false)"); - } + executor.terminateStateOnUserError( + state, "invalid klee_assume call (provably false)", !SilentKleeAssume); } else { executor.addConstraint(state, e); } diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp index 19ac3718..735075f1 100644 --- a/lib/Core/UserSearcher.cpp +++ b/lib/Core/UserSearcher.cpp @@ -100,9 +100,13 @@ bool userSearcherRequiresMD2U() { std::find(CoreSearch.begin(), CoreSearch.end(), Searcher::NURS_QC) != CoreSearch.end()); } +bool userSearcherRequiresInMemoryPTree() { + return std::find(CoreSearch.begin(), CoreSearch.end(), Searcher::RandomPath) != CoreSearch.end(); +} + } // namespace klee -Searcher *getNewSearcher(Searcher::CoreSearchType type, RNG &rng, PTree &processTree) { +Searcher *getNewSearcher(Searcher::CoreSearchType type, RNG &rng, InMemoryPTree *processTree) { Searcher *searcher = nullptr; switch (type) { case Searcher::DFS: searcher = new DFSSearcher(); break; @@ -122,15 +126,15 @@ Searcher *getNewSearcher(Searcher::CoreSearchType type, RNG &rng, PTree &process } Searcher *klee::constructUserSearcher(Executor &executor) { - - Searcher *searcher = getNewSearcher(CoreSearch[0], executor.theRNG, *executor.processTree); + auto *ptree = llvm::dyn_cast(executor.processTree.get()); + Searcher *searcher = getNewSearcher(CoreSearch[0], executor.theRNG, ptree); if (CoreSearch.size() > 1) { std::vector s; s.push_back(searcher); for (unsigned i = 1; i < CoreSearch.size(); i++) - s.push_back(getNewSearcher(CoreSearch[i], executor.theRNG, *executor.processTree)); + s.push_back(getNewSearcher(CoreSearch[i], executor.theRNG, ptree)); searcher = new InterleavedSearcher(s); } diff --git a/lib/Core/UserSearcher.h b/lib/Core/UserSearcher.h index b0df8239..fe75eb6d 100644 --- a/lib/Core/UserSearcher.h +++ b/lib/Core/UserSearcher.h @@ -16,6 +16,7 @@ namespace klee { // XXX gross, should be on demand? bool userSearcherRequiresMD2U(); + bool userSearcherRequiresInMemoryPTree(); void initializeSearchOptions(); diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index b4716dae..ae038b80 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-replay kleeRuntest ktest-gen ktest-randgen + DEPENDS klee kleaver klee-ptree klee-replay kleeRuntest ktest-gen ktest-randgen COMMENT "Running system tests" USES_TERMINAL ) diff --git a/test/Feature/KleePtreeBogus.test b/test/Feature/KleePtreeBogus.test new file mode 100644 index 00000000..11fe87c8 --- /dev/null +++ b/test/Feature/KleePtreeBogus.test @@ -0,0 +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: FileCheck -check-prefix=CHECK-CORRUPT -input-file=%t.err %s +CHECK-CORRUPT: Can't 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: 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: FileCheck -check-prefix=CHECK-DUP -input-file=%t.err %s +CHECK-DUP: PTree 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: FileCheck -check-prefix=CHECK-BTYPE -input-file=%t.err %s +CHECK-BTYPE: PTree 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: FileCheck -check-prefix=CHECK-TTYPE -input-file=%t.err %s +CHECK-TTYPE: PTree 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: FileCheck -check-prefix=CHECK-LOOP -input-file=%t.err %s +CHECK-LOOP: PTree 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: 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 + +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: FileCheck -check-prefix=CHECK-MISSB -input-file=%t.err %s +CHECK-MISSB: PTree 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: FileCheck -check-prefix=CHECK-ID0 -input-file=%t.err %s +CHECK-ID0: PTree DB contains illegal node ID (0) + +cleanup +RUN rm -f %t.db diff --git a/test/Feature/WritePtree.c b/test/Feature/WritePtree.c new file mode 100644 index 00000000..e7bf59ce --- /dev/null +++ b/test/Feature/WritePtree.c @@ -0,0 +1,78 @@ +// 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 + +#include "klee/klee.h" + +#include + +int main(void) { + int a = 42; + int c0, c1, c2, c3; + klee_make_symbolic(&c0, sizeof(c0), "c0"); + klee_make_symbolic(&c1, sizeof(c1), "c1"); + klee_make_symbolic(&c2, sizeof(c2), "c2"); + klee_make_symbolic(&c3, sizeof(c3), "c3"); + + if (c0) { + a += 17; + } else { + a -= 4; + } + + if (c1) { + klee_assume(!c1); + } else if (c2) { + char *p = NULL; + p[4711] = '!'; + } else if (c3) { + klee_silent_exit(0); + } else { + return a; + } + + return 0; +} + +// CHECK-BRANCH: branch type,count +// CHECK-BRANCH: Conditional,7 + +// CHECK-DEPTH: depth,count +// CHECK-DEPTH: 3,2 +// CHECK-DEPTH: 4,2 +// CHECK-DEPTH: 5,4 + +// CHECK-INSTR: asm line,branches,terminations,termination types +// CHECK-INSTR-DAG: {{[0-9]+}},0,2,User(2) +// CHECK-INSTR-DAG: {{[0-9]+}},0,2,Ptr(2) +// CHECK-INSTR-DAG: {{[0-9]+}},0,2,SilentExit(2) +// CHECK-INSTR-DAG: {{[0-9]+}},0,2,Exit(2) + +// CHECK-TERM: termination type,count +// CHECK-TERM-DAG: Exit,2 +// CHECK-TERM-DAG: Ptr,2 +// CHECK-TERM-DAG: User,2 +// CHECK-TERM-DAG: SilentExit,2 + +// CHECK-DOT: strict digraph PTree { +// 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]+}}"]; +// CHECK-DOT-DAG: N{{[0-9]+}}[tooltip="Exit\nnode: {{[0-9]+}}\nstate: {{[0-9]+}}\nasm: {{[0-9]+}}",color=green]; +// CHECK-DOT-DAG: N{{[0-9]+}}[tooltip="SilentExit\nnode: {{[0-9]+}}\nstate: {{[0-9]+}}\nasm: {{[0-9]+}}",color=orange]; +// CHECK-DOT-DAG: N{{[0-9]+}}[tooltip="Ptr\nnode: {{[0-9]+}}\nstate: {{[0-9]+}}\nasm: {{[0-9]+}}",color=red]; +// CHECK-DOT-DAG: N{{[0-9]+}}[tooltip="User\nnode: {{[0-9]+}}\nstate: {{[0-9]+}}\nasm: {{[0-9]+}}",color=blue]; +// CHECK-DOT-DAG: N{{[0-9]+}}->{N{{[0-9]+}} N{{[0-9]+}}}; +// CHECK-DOT-DAG: } + +// CHECK-TINFO: nodes: 15 +// CHECK-TINFO: leaf nodes: 8 +// CHECK-TINFO: max. depth: 5 +// CHECK-TINFO: avg. depth: 4.2 diff --git a/test/Feature/ptree-dbs/duplicated_node.csv b/test/Feature/ptree-dbs/duplicated_node.csv new file mode 100644 index 00000000..7882b911 --- /dev/null +++ b/test/Feature/ptree-dbs/duplicated_node.csv @@ -0,0 +1,5 @@ +ID,stateID,leftID,rightID,asmLine,kind +1,0,2,3,44,1 +2,0,0,0,61,36 +3,1,4,2,62,1 +4,1,0,0,63,80 diff --git a/test/Feature/ptree-dbs/empty_db.csv b/test/Feature/ptree-dbs/empty_db.csv new file mode 100644 index 00000000..4dac8a17 --- /dev/null +++ b/test/Feature/ptree-dbs/empty_db.csv @@ -0,0 +1 @@ +ID,stateID,leftID,rightID,asmLine,kind diff --git a/test/Feature/ptree-dbs/invalid_btype.csv b/test/Feature/ptree-dbs/invalid_btype.csv new file mode 100644 index 00000000..01ee428c --- /dev/null +++ b/test/Feature/ptree-dbs/invalid_btype.csv @@ -0,0 +1,4 @@ +ID,stateID,leftID,rightID,asmLine,kind +1,0,2,3,44,123 +2,0,0,0,61,36 +3,1,0,0,61,1 diff --git a/test/Feature/ptree-dbs/invalid_ttype.csv b/test/Feature/ptree-dbs/invalid_ttype.csv new file mode 100644 index 00000000..0d185bee --- /dev/null +++ b/test/Feature/ptree-dbs/invalid_ttype.csv @@ -0,0 +1,4 @@ +ID,stateID,leftID,rightID,asmLine,kind +1,0,2,3,44,1 +2,0,0,0,61,36 +3,1,0,0,61,123 diff --git a/test/Feature/ptree-dbs/loop.csv b/test/Feature/ptree-dbs/loop.csv new file mode 100644 index 00000000..4fc2b9f2 --- /dev/null +++ b/test/Feature/ptree-dbs/loop.csv @@ -0,0 +1,5 @@ +ID,stateID,leftID,rightID,asmLine,kind +1,0,2,3,44,1 +2,0,0,0,61,36 +3,1,4,1,62,1 +4,1,0,0,63,80 diff --git a/test/Feature/ptree-dbs/missing_after_max.csv b/test/Feature/ptree-dbs/missing_after_max.csv new file mode 100644 index 00000000..16e99a35 --- /dev/null +++ b/test/Feature/ptree-dbs/missing_after_max.csv @@ -0,0 +1,5 @@ +ID,stateID,leftID,rightID,asmLine,kind +1,0,2,3,44,1 +2,0,0,0,61,36 +3,1,4,5,62,1 +4,1,0,0,63,80 diff --git a/test/Feature/ptree-dbs/missing_before_max.csv b/test/Feature/ptree-dbs/missing_before_max.csv new file mode 100644 index 00000000..2131ea56 --- /dev/null +++ b/test/Feature/ptree-dbs/missing_before_max.csv @@ -0,0 +1,5 @@ +ID,stateID,leftID,rightID,asmLine,kind +1,0,2,3,44,1 +2,0,0,0,61,36 +3,1,4,5,62,1 +5,1,0,0,63,80 diff --git a/test/Feature/ptree-dbs/node_id0.csv b/test/Feature/ptree-dbs/node_id0.csv new file mode 100644 index 00000000..51a31e49 --- /dev/null +++ b/test/Feature/ptree-dbs/node_id0.csv @@ -0,0 +1,6 @@ +ID,stateID,leftID,rightID,asmLine,kind +0,0,2,3,44,1 +2,0,0,0,61,36 +3,1,4,5,62,1 +4,1,0,0,63,80 +5,2,0,0,63,36 diff --git a/test/Feature/ptree-dbs/not_a.db b/test/Feature/ptree-dbs/not_a.db new file mode 100644 index 00000000..d81cc071 --- /dev/null +++ b/test/Feature/ptree-dbs/not_a.db @@ -0,0 +1 @@ +42 diff --git a/test/lit.cfg b/test/lit.cfg index cb47d3d4..8abf7012 100644 --- a/test/lit.cfg +++ b/test/lit.cfg @@ -116,6 +116,11 @@ config.substitutions.append( ('%libkleeruntest', config.libkleeruntest) ) +# Add a substition for sqlite3 +config.substitutions.append( + ('%sqlite3', os.path.abspath(config.sqlite3)) +) + # Get KLEE and Kleaver specific parameters passed on llvm-lit cmd line # e.g. llvm-lit --param klee_opts=--help klee_extra_params = lit_config.params.get('klee_opts',"") @@ -134,6 +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-replay', 'klee-replay', ''), ('%klee-stats', 'klee-stats', ''), ('%klee-zesti', 'klee-zesti', ''), @@ -233,3 +239,6 @@ config.available_features.add('{}32bit-support'.format('' if config.have_32bit_s config.available_features.add('{}asan'.format('' if config.have_asan else 'not-')) config.available_features.add('{}ubsan'.format('' if config.have_ubsan else 'not-')) config.available_features.add('{}msan'.format('' if config.have_msan else 'not-')) + +# SQLite +config.available_features.add('{}sqlite3'.format('' if config.have_sqlite3 else 'not-')) diff --git a/test/lit.site.cfg.in b/test/lit.site.cfg.in index c7063057..d82b8a2c 100644 --- a/test/lit.site.cfg.in +++ b/test/lit.site.cfg.in @@ -26,6 +26,8 @@ config.cxx = "@NATIVE_CXX@" # test/Concrete/CMakeLists.txt config.O0opt = "-O0 -Xclang -disable-O0-optnone" +config.sqlite3 = "@SQLITE_CLI@" + # Features config.enable_uclibc = True if @SUPPORT_KLEE_UCLIBC@ == 1 else False config.enable_posix_runtime = True if @ENABLE_POSIX_RUNTIME@ == 1 else False @@ -39,6 +41,7 @@ config.have_asan = True if @IS_ASAN_BUILD@ == 1 else False config.have_ubsan = True if @IS_UBSAN_BUILD@ == 1 else False config.have_msan = True if @IS_MSAN_BUILD@ == 1 else False config.have_32bit_support = True if @M32_SUPPORTED@ == 1 else False +config.have_sqlite3 = True if "@SQLITE_CLI@".strip() != "" else False # Add sanitizer list config.environment['LSAN_OPTIONS'] = "suppressions=@KLEE_UTILS_DIR@/sanitizers/lsan.txt" 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 + +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> 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 + +/// @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; + + 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 +#include +#include +#include +#include +#include +#include +#include + +// branches + +void printBranches(const Tree &tree) { + if (tree.nodes.size() <= 1) { + std::cout << "Empty tree.\n"; + return; + } + + std::unordered_map branchTypes; + + DFSVisitor visitor( + tree, + [&branchTypes](std::uint32_t id, Node node, std::uint32_t depth) { + branchTypes[std::get(node.kind)]++; + }, + nullptr); + + // sort output + std::vector> 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 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 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(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(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 terminationTypes; +}; + +void printInstructions(const Tree &tree) { + std::map 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(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 terminations; + + DFSVisitor visitor( + tree, nullptr, + [&terminations](std::uint32_t id, Node node, std::uint32_t depth) { + terminations[std::get(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 + +#include +#include +#include + +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(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(sqlite3_column_int(readStmt, 0)); + const auto stateID = + static_cast(sqlite3_column_int(readStmt, 1)); + const auto left = + static_cast(sqlite3_column_int(readStmt, 2)); + const auto right = + static_cast(sqlite3_column_int(readStmt, 3)); + const auto asmLine = + static_cast(sqlite3_column_int(readStmt, 4)); + const auto tmpKind = + static_cast(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(tmpKind); + } else { + kind = static_cast(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 stack{1}; // root ID + std::unordered_set 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(node.kind) && + static_cast(std::get(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(node.kind)); + const auto branchType = std::get(node.kind); + if (validBranchTypes.count(branchType) == 0) { + std::cerr << "PTree DB contains unknown branch type (" + << (unsigned)static_cast(branchType) + << ") in node " << id << std::endl; + exit(EXIT_FAILURE); + } + } else { + // valid termination types + assert(std::holds_alternative(node.kind)); + const auto terminationType = std::get(node.kind); + if (validTerminationTypes.count(terminationType) == 0 || + terminationType == StateTerminationType::RUNNING) { + std::cerr << "PTree DB contains unknown termination type (" + << (unsigned)static_cast(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 +#include +#include +#include +#include +#include + +inline std::unordered_set validBranchTypes; +inline std::unordered_set validTerminationTypes; +inline std::unordered_map branchTypeNames; +inline std::unordered_map + 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 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 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 +#include +#include + +#include "Printers.h" + +namespace fs = std::filesystem; + +void print_usage() { + std::cout << "Usage: klee-ptree