From 2c8b74cc858793c94e5476b5765e93ee23738702 Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Thu, 14 Dec 2023 22:15:57 +0000 Subject: Rename files from PTree to ExecutionTree (and similar) --- lib/Core/ExecutionTree.cpp | 235 +++++++++++++++++++ lib/Core/ExecutionTree.h | 179 +++++++++++++++ lib/Core/ExecutionTreeWriter.cpp | 196 ++++++++++++++++ lib/Core/ExecutionTreeWriter.h | 46 ++++ lib/Core/PTree.cpp | 235 ------------------- lib/Core/PTree.h | 179 --------------- lib/Core/PTreeWriter.cpp | 196 ---------------- lib/Core/PTreeWriter.h | 46 ---- test/Feature/KleeExecTreeBogus.test | 65 ++++++ test/Feature/KleePtreeBogus.test | 65 ------ test/Feature/WriteExecutionTree.c | 78 +++++++ test/Feature/WritePtree.c | 78 ------- test/Feature/exec-tree-dbs/duplicated_node.csv | 5 + test/Feature/exec-tree-dbs/empty_db.csv | 1 + test/Feature/exec-tree-dbs/invalid_btype.csv | 4 + test/Feature/exec-tree-dbs/invalid_ttype.csv | 4 + test/Feature/exec-tree-dbs/loop.csv | 5 + test/Feature/exec-tree-dbs/missing_after_max.csv | 5 + test/Feature/exec-tree-dbs/missing_before_max.csv | 5 + test/Feature/exec-tree-dbs/node_id0.csv | 6 + test/Feature/exec-tree-dbs/not_a.db | 1 + 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 - tools/klee-exec-tree/CMakeLists.txt | 16 ++ tools/klee-exec-tree/DFSVisitor.cpp | 46 ++++ tools/klee-exec-tree/DFSVisitor.h | 31 +++ tools/klee-exec-tree/Printers.cpp | 266 ++++++++++++++++++++++ tools/klee-exec-tree/Printers.h | 30 +++ tools/klee-exec-tree/Tree.cpp | 208 +++++++++++++++++ tools/klee-exec-tree/Tree.h | 53 +++++ tools/klee-exec-tree/main.cpp | 68 ++++++ 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 ------ 46 files changed, 1553 insertions(+), 1553 deletions(-) create mode 100644 lib/Core/ExecutionTree.cpp create mode 100644 lib/Core/ExecutionTree.h create mode 100644 lib/Core/ExecutionTreeWriter.cpp create mode 100644 lib/Core/ExecutionTreeWriter.h delete mode 100644 lib/Core/PTree.cpp delete mode 100644 lib/Core/PTree.h delete mode 100644 lib/Core/PTreeWriter.cpp delete mode 100644 lib/Core/PTreeWriter.h create mode 100644 test/Feature/KleeExecTreeBogus.test delete mode 100644 test/Feature/KleePtreeBogus.test create mode 100644 test/Feature/WriteExecutionTree.c delete mode 100644 test/Feature/WritePtree.c create mode 100644 test/Feature/exec-tree-dbs/duplicated_node.csv create mode 100644 test/Feature/exec-tree-dbs/empty_db.csv create mode 100644 test/Feature/exec-tree-dbs/invalid_btype.csv create mode 100644 test/Feature/exec-tree-dbs/invalid_ttype.csv create mode 100644 test/Feature/exec-tree-dbs/loop.csv create mode 100644 test/Feature/exec-tree-dbs/missing_after_max.csv create mode 100644 test/Feature/exec-tree-dbs/missing_before_max.csv create mode 100644 test/Feature/exec-tree-dbs/node_id0.csv create mode 100644 test/Feature/exec-tree-dbs/not_a.db delete mode 100644 test/Feature/ptree-dbs/duplicated_node.csv delete mode 100644 test/Feature/ptree-dbs/empty_db.csv delete mode 100644 test/Feature/ptree-dbs/invalid_btype.csv delete mode 100644 test/Feature/ptree-dbs/invalid_ttype.csv delete mode 100644 test/Feature/ptree-dbs/loop.csv delete mode 100644 test/Feature/ptree-dbs/missing_after_max.csv delete mode 100644 test/Feature/ptree-dbs/missing_before_max.csv delete mode 100644 test/Feature/ptree-dbs/node_id0.csv delete mode 100644 test/Feature/ptree-dbs/not_a.db create mode 100644 tools/klee-exec-tree/CMakeLists.txt create mode 100644 tools/klee-exec-tree/DFSVisitor.cpp create mode 100644 tools/klee-exec-tree/DFSVisitor.h create mode 100644 tools/klee-exec-tree/Printers.cpp create mode 100644 tools/klee-exec-tree/Printers.h create mode 100644 tools/klee-exec-tree/Tree.cpp create mode 100644 tools/klee-exec-tree/Tree.h create mode 100644 tools/klee-exec-tree/main.cpp delete mode 100644 tools/klee-ptree/CMakeLists.txt delete mode 100644 tools/klee-ptree/DFSVisitor.cpp delete mode 100644 tools/klee-ptree/DFSVisitor.h delete mode 100644 tools/klee-ptree/Printers.cpp delete mode 100644 tools/klee-ptree/Printers.h delete mode 100644 tools/klee-ptree/Tree.cpp delete mode 100644 tools/klee-ptree/Tree.h delete mode 100644 tools/klee-ptree/main.cpp diff --git a/lib/Core/ExecutionTree.cpp b/lib/Core/ExecutionTree.cpp new file mode 100644 index 00000000..c5b640d3 --- /dev/null +++ b/lib/Core/ExecutionTree.cpp @@ -0,0 +1,235 @@ +//===-- PTree.cpp ---------------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#include "PTree.h" + +#include "ExecutionState.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; + +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 + +// PTreeNode + +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++; +} + +// NoopPTree + +void NoopPTree::dump(llvm::raw_ostream &os) noexcept { + os << "digraph G {\nTreeNotAvailable [shape=box]\n}"; +} + +// 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->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(createNode(node, rightState), currentNodeTag); + updateBranchingNode(*node, reason); + node->state = nullptr; +} + +void InMemoryPTree::remove(PTreeNode *n) noexcept { + assert(!n->left.getPointer() && !n->right.getPointer()); + updateTerminatingNode(*n); + do { + PTreeNode *p = n->parent; + if (p) { + if (n == p->left.getPointer()) { + p->left = PTreeNodePtr(nullptr); + } else { + assert(n == p->right.getPointer()); + p->right = PTreeNodePtr(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 + // 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; + + child.getPointer()->parent = parent; + if (!parent) { + // We're at the root. + root = child; + } else { + if (n == parent->left.getPointer()) { + parent->left = child; + } else { + assert(n == parent->right.getPointer()); + parent->right = child; + } + } + + delete n; + } +} + +void InMemoryPTree::dump(llvm::raw_ostream &os) noexcept { + std::unique_ptr pp(ExprPPrinter::create(os)); + pp->setNewline("\\l"); + 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(); + stack.pop_back(); + os << "\tn" << n << " [shape=diamond"; + if (n->state) + os << ",fillcolor=green"; + os << "];\n"; + if (n->left.getPointer()) { + 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() << " [label=0b" + << std::bitset(n->right.getInt()).to_string() << "];\n"; + stack.push_back(n->right.getPointer()); + } + } + os << "}\n"; +} + +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/ExecutionTree.h b/lib/Core/ExecutionTree.h new file mode 100644 index 00000000..ab3f0433 --- /dev/null +++ b/lib/Core/ExecutionTree.h @@ -0,0 +1,179 @@ +//===-- PTree.h -------------------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#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 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/ExecutionTreeWriter.cpp b/lib/Core/ExecutionTreeWriter.cpp new file mode 100644 index 00000000..a8067a5d --- /dev/null +++ b/lib/Core/ExecutionTreeWriter.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/ExecutionTreeWriter.h b/lib/Core/ExecutionTreeWriter.h new file mode 100644 index 00000000..12709116 --- /dev/null +++ b/lib/Core/ExecutionTreeWriter.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/PTree.cpp b/lib/Core/PTree.cpp deleted file mode 100644 index c5b640d3..00000000 --- a/lib/Core/PTree.cpp +++ /dev/null @@ -1,235 +0,0 @@ -//===-- PTree.cpp ---------------------------------------------------------===// -// -// The KLEE Symbolic Virtual Machine -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. -// -//===----------------------------------------------------------------------===// - -#include "PTree.h" - -#include "ExecutionState.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; - -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 - -// PTreeNode - -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++; -} - -// NoopPTree - -void NoopPTree::dump(llvm::raw_ostream &os) noexcept { - os << "digraph G {\nTreeNotAvailable [shape=box]\n}"; -} - -// 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->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(createNode(node, rightState), currentNodeTag); - updateBranchingNode(*node, reason); - node->state = nullptr; -} - -void InMemoryPTree::remove(PTreeNode *n) noexcept { - assert(!n->left.getPointer() && !n->right.getPointer()); - updateTerminatingNode(*n); - do { - PTreeNode *p = n->parent; - if (p) { - if (n == p->left.getPointer()) { - p->left = PTreeNodePtr(nullptr); - } else { - assert(n == p->right.getPointer()); - p->right = PTreeNodePtr(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 - // 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; - - child.getPointer()->parent = parent; - if (!parent) { - // We're at the root. - root = child; - } else { - if (n == parent->left.getPointer()) { - parent->left = child; - } else { - assert(n == parent->right.getPointer()); - parent->right = child; - } - } - - delete n; - } -} - -void InMemoryPTree::dump(llvm::raw_ostream &os) noexcept { - std::unique_ptr pp(ExprPPrinter::create(os)); - pp->setNewline("\\l"); - 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(); - stack.pop_back(); - os << "\tn" << n << " [shape=diamond"; - if (n->state) - os << ",fillcolor=green"; - os << "];\n"; - if (n->left.getPointer()) { - 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() << " [label=0b" - << std::bitset(n->right.getInt()).to_string() << "];\n"; - stack.push_back(n->right.getPointer()); - } - } - os << "}\n"; -} - -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 deleted file mode 100644 index ab3f0433..00000000 --- a/lib/Core/PTree.h +++ /dev/null @@ -1,179 +0,0 @@ -//===-- PTree.h -------------------------------------------------*- C++ -*-===// -// -// The KLEE Symbolic Virtual Machine -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. -// -//===----------------------------------------------------------------------===// - -#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 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 deleted file mode 100644 index a8067a5d..00000000 --- a/lib/Core/PTreeWriter.cpp +++ /dev/null @@ -1,196 +0,0 @@ -//===-- 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 deleted file mode 100644 index 12709116..00000000 --- a/lib/Core/PTreeWriter.h +++ /dev/null @@ -1,46 +0,0 @@ -//===-- 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/test/Feature/KleeExecTreeBogus.test b/test/Feature/KleeExecTreeBogus.test new file mode 100644 index 00000000..11fe87c8 --- /dev/null +++ b/test/Feature/KleeExecTreeBogus.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/KleePtreeBogus.test b/test/Feature/KleePtreeBogus.test deleted file mode 100644 index 11fe87c8..00000000 --- a/test/Feature/KleePtreeBogus.test +++ /dev/null @@ -1,65 +0,0 @@ -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/WriteExecutionTree.c b/test/Feature/WriteExecutionTree.c new file mode 100644 index 00000000..e7bf59ce --- /dev/null +++ b/test/Feature/WriteExecutionTree.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/WritePtree.c b/test/Feature/WritePtree.c deleted file mode 100644 index e7bf59ce..00000000 --- a/test/Feature/WritePtree.c +++ /dev/null @@ -1,78 +0,0 @@ -// 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/exec-tree-dbs/duplicated_node.csv b/test/Feature/exec-tree-dbs/duplicated_node.csv new file mode 100644 index 00000000..7882b911 --- /dev/null +++ b/test/Feature/exec-tree-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/exec-tree-dbs/empty_db.csv b/test/Feature/exec-tree-dbs/empty_db.csv new file mode 100644 index 00000000..4dac8a17 --- /dev/null +++ b/test/Feature/exec-tree-dbs/empty_db.csv @@ -0,0 +1 @@ +ID,stateID,leftID,rightID,asmLine,kind diff --git a/test/Feature/exec-tree-dbs/invalid_btype.csv b/test/Feature/exec-tree-dbs/invalid_btype.csv new file mode 100644 index 00000000..01ee428c --- /dev/null +++ b/test/Feature/exec-tree-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/exec-tree-dbs/invalid_ttype.csv b/test/Feature/exec-tree-dbs/invalid_ttype.csv new file mode 100644 index 00000000..0d185bee --- /dev/null +++ b/test/Feature/exec-tree-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/exec-tree-dbs/loop.csv b/test/Feature/exec-tree-dbs/loop.csv new file mode 100644 index 00000000..4fc2b9f2 --- /dev/null +++ b/test/Feature/exec-tree-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/exec-tree-dbs/missing_after_max.csv b/test/Feature/exec-tree-dbs/missing_after_max.csv new file mode 100644 index 00000000..16e99a35 --- /dev/null +++ b/test/Feature/exec-tree-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/exec-tree-dbs/missing_before_max.csv b/test/Feature/exec-tree-dbs/missing_before_max.csv new file mode 100644 index 00000000..2131ea56 --- /dev/null +++ b/test/Feature/exec-tree-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/exec-tree-dbs/node_id0.csv b/test/Feature/exec-tree-dbs/node_id0.csv new file mode 100644 index 00000000..51a31e49 --- /dev/null +++ b/test/Feature/exec-tree-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/exec-tree-dbs/not_a.db b/test/Feature/exec-tree-dbs/not_a.db new file mode 100644 index 00000000..d81cc071 --- /dev/null +++ b/test/Feature/exec-tree-dbs/not_a.db @@ -0,0 +1 @@ +42 diff --git a/test/Feature/ptree-dbs/duplicated_node.csv b/test/Feature/ptree-dbs/duplicated_node.csv deleted file mode 100644 index 7882b911..00000000 --- a/test/Feature/ptree-dbs/duplicated_node.csv +++ /dev/null @@ -1,5 +0,0 @@ -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 deleted file mode 100644 index 4dac8a17..00000000 --- a/test/Feature/ptree-dbs/empty_db.csv +++ /dev/null @@ -1 +0,0 @@ -ID,stateID,leftID,rightID,asmLine,kind diff --git a/test/Feature/ptree-dbs/invalid_btype.csv b/test/Feature/ptree-dbs/invalid_btype.csv deleted file mode 100644 index 01ee428c..00000000 --- a/test/Feature/ptree-dbs/invalid_btype.csv +++ /dev/null @@ -1,4 +0,0 @@ -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 deleted file mode 100644 index 0d185bee..00000000 --- a/test/Feature/ptree-dbs/invalid_ttype.csv +++ /dev/null @@ -1,4 +0,0 @@ -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 deleted file mode 100644 index 4fc2b9f2..00000000 --- a/test/Feature/ptree-dbs/loop.csv +++ /dev/null @@ -1,5 +0,0 @@ -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 deleted file mode 100644 index 16e99a35..00000000 --- a/test/Feature/ptree-dbs/missing_after_max.csv +++ /dev/null @@ -1,5 +0,0 @@ -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 deleted file mode 100644 index 2131ea56..00000000 --- a/test/Feature/ptree-dbs/missing_before_max.csv +++ /dev/null @@ -1,5 +0,0 @@ -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 deleted file mode 100644 index 51a31e49..00000000 --- a/test/Feature/ptree-dbs/node_id0.csv +++ /dev/null @@ -1,6 +0,0 @@ -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 deleted file mode 100644 index d81cc071..00000000 --- a/test/Feature/ptree-dbs/not_a.db +++ /dev/null @@ -1 +0,0 @@ -42 diff --git a/tools/klee-exec-tree/CMakeLists.txt b/tools/klee-exec-tree/CMakeLists.txt new file mode 100644 index 00000000..b5c3fa09 --- /dev/null +++ b/tools/klee-exec-tree/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-exec-tree/DFSVisitor.cpp b/tools/klee-exec-tree/DFSVisitor.cpp new file mode 100644 index 00000000..c87afc3e --- /dev/null +++ b/tools/klee-exec-tree/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-exec-tree/DFSVisitor.h b/tools/klee-exec-tree/DFSVisitor.h new file mode 100644 index 00000000..60d7b3bd --- /dev/null +++ b/tools/klee-exec-tree/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-exec-tree/Printers.cpp b/tools/klee-exec-tree/Printers.cpp new file mode 100644 index 00000000..950d1b09 --- /dev/null +++ b/tools/klee-exec-tree/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-exec-tree/Printers.h b/tools/klee-exec-tree/Printers.h new file mode 100644 index 00000000..d20db4a1 --- /dev/null +++ b/tools/klee-exec-tree/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-exec-tree/Tree.cpp b/tools/klee-exec-tree/Tree.cpp new file mode 100644 index 00000000..20772600 --- /dev/null +++ b/tools/klee-exec-tree/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-exec-tree/Tree.h b/tools/klee-exec-tree/Tree.h new file mode 100644 index 00000000..65b7baeb --- /dev/null +++ b/tools/klee-exec-tree/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-exec-tree/main.cpp b/tools/klee-exec-tree/main.cpp new file mode 100644 index 00000000..96d2be75 --- /dev/null +++ b/tools/klee-exec-tree/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