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 -------- 8 files changed, 656 insertions(+), 656 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 (limited to 'lib/Core') 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 -- cgit 1.4.1