From 19b6ae578b0658115d15848604a28434845bb3e3 Mon Sep 17 00:00:00 2001 From: Frank Busse Date: Fri, 24 Mar 2023 21:14:02 +0000 Subject: new: persistent ptree (-write-ptree) and klee-ptree Introduce three different kinds of process trees: 1. Noop: does nothing (e.g. no allocations for DFS) 2. InMemory: same behaviour as before (e.g. RandomPathSearcher) 3. Persistent: similar to InMemory but writes nodes to ptree.db and tracks information such as branch type, termination type or source location (asm) in nodes. Enabled with -write-ptree ptree.db files can be analysed/plotted with the new "klee-ptree" tool. --- lib/Core/CMakeLists.txt | 1 + lib/Core/Executor.cpp | 23 ++-- lib/Core/Executor.h | 5 +- lib/Core/PTree.cpp | 172 +++++++++++++++++++++++------- lib/Core/PTree.h | 205 ++++++++++++++++++++++++++++-------- lib/Core/PTreeWriter.cpp | 196 ++++++++++++++++++++++++++++++++++ lib/Core/PTreeWriter.h | 46 ++++++++ lib/Core/Searcher.cpp | 23 ++-- lib/Core/Searcher.h | 4 +- lib/Core/SpecialFunctionHandler.cpp | 8 +- lib/Core/UserSearcher.cpp | 12 ++- lib/Core/UserSearcher.h | 1 + 12 files changed, 582 insertions(+), 114 deletions(-) create mode 100644 lib/Core/PTreeWriter.cpp create mode 100644 lib/Core/PTreeWriter.h (limited to 'lib') diff --git a/lib/Core/CMakeLists.txt b/lib/Core/CMakeLists.txt index 9005a1ff..8df3e259 100644 --- a/lib/Core/CMakeLists.txt +++ b/lib/Core/CMakeLists.txt @@ -20,6 +20,7 @@ add_library(kleeCore Memory.cpp MemoryManager.cpp PTree.cpp + PTreeWriter.cpp Searcher.cpp SeedInfo.cpp SpecialFunctionHandler.cpp diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index b4da6a08..8f70540c 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -3639,14 +3639,15 @@ std::string Executor::getAddressInfo(ExecutionState &state, return info.str(); } - -void Executor::terminateState(ExecutionState &state) { +void Executor::terminateState(ExecutionState &state, + StateTerminationType reason) { if (replayKTest && replayPosition!=replayKTest->numObjects) { klee_warning_once(replayKTest, "replay did not consume all objects in test input."); } interpreterHandler->incPathsExplored(); + processTree->setTerminationType(state, reason); std::vector::iterator it = std::find(addedStates.begin(), addedStates.end(), &state); @@ -3690,7 +3691,7 @@ void Executor::terminateStateOnExit(ExecutionState &state) { terminationTypeFileExtension(StateTerminationType::Exit).c_str()); interpreterHandler->incPathsCompleted(); - terminateState(state); + terminateState(state, StateTerminationType::Exit); } void Executor::terminateStateEarly(ExecutionState &state, const Twine &message, @@ -3707,7 +3708,7 @@ void Executor::terminateStateEarly(ExecutionState &state, const Twine &message, terminationTypeFileExtension(reason).c_str()); } - terminateState(state); + terminateState(state, reason); } void Executor::terminateStateEarlyAlgorithm(ExecutionState &state, @@ -3815,7 +3816,7 @@ void Executor::terminateStateOnError(ExecutionState &state, interpreterHandler->processTestCase(state, msg.str().c_str(), file_suffix); } - terminateState(state); + terminateState(state, terminationType); if (shouldExitOn(terminationType)) haltExecution = true; @@ -3848,9 +3849,14 @@ void Executor::terminateStateOnSolverError(ExecutionState &state, } void Executor::terminateStateOnUserError(ExecutionState &state, - const llvm::Twine &message) { + const llvm::Twine &message, + bool writeErr) { ++stats::terminationUserError; - terminateStateOnError(state, message, StateTerminationType::User, ""); + if (writeErr) { + terminateStateOnError(state, message, StateTerminationType::User, ""); + } else { + terminateState(state, StateTerminationType::User); + } } // XXX shoot me @@ -4601,7 +4607,8 @@ void Executor::runFunctionAsMain(Function *f, initializeGlobals(*state); - processTree = std::make_unique(state); + processTree = createPTree(*state, userSearcherRequiresInMemoryPTree(), + *interpreterHandler); run(*state); processTree = nullptr; diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 204638e8..3635de78 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -412,7 +412,7 @@ private: /// Remove state from queue and delete state. This function should only be /// used in the termination functions below. - void terminateState(ExecutionState &state); + void terminateState(ExecutionState &state, StateTerminationType reason); /// Call exit handler and terminate state normally /// (end of execution path) @@ -467,7 +467,8 @@ private: /// Call error handler and terminate state for user errors /// (e.g. wrong usage of klee.h API) void terminateStateOnUserError(ExecutionState &state, - const llvm::Twine &message); + const llvm::Twine &message, + bool writeErr = true); /// bindModuleConstants - Initialize the module constant table. void bindModuleConstants(); diff --git a/lib/Core/PTree.cpp b/lib/Core/PTree.cpp index 6c17e296..c5b640d3 100644 --- a/lib/Core/PTree.cpp +++ b/lib/Core/PTree.cpp @@ -11,49 +11,88 @@ #include "ExecutionState.h" -#include "klee/Expr/Expr.h" +#include "klee/Core/Interpreter.h" #include "klee/Expr/ExprPPrinter.h" +#include "klee/Module/KInstruction.h" #include "klee/Support/OptionCategories.h" #include #include using namespace klee; -using namespace llvm; + +namespace klee { +llvm::cl::OptionCategory + PTreeCat("Process tree related options", + "These options affect the process tree handling."); +} namespace { +llvm::cl::opt CompressProcessTree( + "compress-process-tree", + llvm::cl::desc("Remove intermediate nodes in the process " + "tree whenever possible (default=false)"), + llvm::cl::init(false), llvm::cl::cat(PTreeCat)); + +llvm::cl::opt WritePTree( + "write-ptree", llvm::cl::init(false), + llvm::cl::desc("Write process tree into ptree.db (default=false)"), + llvm::cl::cat(PTreeCat)); +} // namespace -cl::opt - CompressProcessTree("compress-process-tree", - cl::desc("Remove intermediate nodes in the process " - "tree whenever possible (default=false)"), - cl::init(false), cl::cat(MiscCat)); +// PTreeNode -} // namespace +PTreeNode::PTreeNode(PTreeNode *parent, ExecutionState *state) noexcept + : parent{parent}, left{nullptr}, right{nullptr}, state{state} { + state->ptreeNode = this; +} + +// AnnotatedPTreeNode + +AnnotatedPTreeNode::AnnotatedPTreeNode(PTreeNode *parent, + ExecutionState *state) noexcept + : PTreeNode(parent, state) { + id = nextID++; +} -PTree::PTree(ExecutionState *initialState) - : root(PTreeNodePtr(new PTreeNode(nullptr, initialState))) { - initialState->ptreeNode = root.getPointer(); +// NoopPTree + +void NoopPTree::dump(llvm::raw_ostream &os) noexcept { + os << "digraph G {\nTreeNotAvailable [shape=box]\n}"; } -void PTree::attach(PTreeNode *node, ExecutionState *leftState, - ExecutionState *rightState, BranchType reason) { +// InMemoryPTree + +InMemoryPTree::InMemoryPTree(ExecutionState &initialState) noexcept { + root = PTreeNodePtr(createNode(nullptr, &initialState)); + initialState.ptreeNode = root.getPointer(); +} + +PTreeNode *InMemoryPTree::createNode(PTreeNode *parent, ExecutionState *state) { + return new PTreeNode(parent, state); +} + +void InMemoryPTree::attach(PTreeNode *node, ExecutionState *leftState, + ExecutionState *rightState, + BranchType reason) noexcept { assert(node && !node->left.getPointer() && !node->right.getPointer()); assert(node == rightState->ptreeNode && "Attach assumes the right state is the current state"); - node->state = nullptr; - node->left = PTreeNodePtr(new PTreeNode(node, leftState)); + node->left = PTreeNodePtr(createNode(node, leftState)); // The current node inherits the tag uint8_t currentNodeTag = root.getInt(); if (node->parent) currentNodeTag = node->parent->left.getPointer() == node ? node->parent->left.getInt() : node->parent->right.getInt(); - node->right = PTreeNodePtr(new PTreeNode(node, rightState), currentNodeTag); + node->right = PTreeNodePtr(createNode(node, rightState), currentNodeTag); + updateBranchingNode(*node, reason); + node->state = nullptr; } -void PTree::remove(PTreeNode *n) { +void InMemoryPTree::remove(PTreeNode *n) noexcept { assert(!n->left.getPointer() && !n->right.getPointer()); + updateTerminatingNode(*n); do { PTreeNode *p = n->parent; if (p) { @@ -92,17 +131,17 @@ void PTree::remove(PTreeNode *n) { } } -void PTree::dump(llvm::raw_ostream &os) { - ExprPPrinter *pp = ExprPPrinter::create(os); +void InMemoryPTree::dump(llvm::raw_ostream &os) noexcept { + std::unique_ptr pp(ExprPPrinter::create(os)); pp->setNewline("\\l"); - os << "digraph G {\n"; - os << "\tsize=\"10,7.5\";\n"; - os << "\tratio=fill;\n"; - os << "\trotate=90;\n"; - os << "\tcenter = \"true\";\n"; - os << "\tnode [style=\"filled\",width=.1,height=.1,fontname=\"Terminus\"]\n"; - os << "\tedge [arrowsize=.3]\n"; - std::vector stack; + os << "digraph G {\n" + << "\tsize=\"10,7.5\";\n" + << "\tratio=fill;\n" + << "\trotate=90;\n" + << "\tcenter = \"true\";\n" + << "\tnode [style=\"filled\",width=.1,height=.1,fontname=\"Terminus\"]\n" + << "\tedge [arrowsize=.3]\n"; + std::vector stack; stack.push_back(root.getPointer()); while (!stack.empty()) { const PTreeNode *n = stack.back(); @@ -112,24 +151,85 @@ void PTree::dump(llvm::raw_ostream &os) { os << ",fillcolor=green"; os << "];\n"; if (n->left.getPointer()) { - os << "\tn" << n << " -> n" << n->left.getPointer(); - os << " [label=0b" + os << "\tn" << n << " -> n" << n->left.getPointer() << " [label=0b" << std::bitset(n->left.getInt()).to_string() << "];\n"; stack.push_back(n->left.getPointer()); } if (n->right.getPointer()) { - os << "\tn" << n << " -> n" << n->right.getPointer(); - os << " [label=0b" + os << "\tn" << n << " -> n" << n->right.getPointer() << " [label=0b" << std::bitset(n->right.getInt()).to_string() << "];\n"; stack.push_back(n->right.getPointer()); } } os << "}\n"; - delete pp; } -PTreeNode::PTreeNode(PTreeNode *parent, ExecutionState *state) : parent{parent}, state{state} { - state->ptreeNode = this; - left = PTreeNodePtr(nullptr); - right = PTreeNodePtr(nullptr); +std::uint8_t InMemoryPTree::getNextId() noexcept { + static_assert(PtrBitCount <= 8); + std::uint8_t id = 1 << registeredIds++; + if (registeredIds > PtrBitCount) { + klee_error("PTree cannot support more than %d RandomPathSearchers", + PtrBitCount); + } + return id; +} + +// PersistentPTree + +PersistentPTree::PersistentPTree(ExecutionState &initialState, + InterpreterHandler &ih) noexcept + : writer(ih.getOutputFilename("ptree.db")) { + root = PTreeNodePtr(createNode(nullptr, &initialState)); + initialState.ptreeNode = root.getPointer(); +} + +void PersistentPTree::dump(llvm::raw_ostream &os) noexcept { + writer.batchCommit(true); + InMemoryPTree::dump(os); +} + +PTreeNode *PersistentPTree::createNode(PTreeNode *parent, + ExecutionState *state) { + return new AnnotatedPTreeNode(parent, state); +} + +void PersistentPTree::setTerminationType(ExecutionState &state, + StateTerminationType type) { + auto *annotatedNode = llvm::cast(state.ptreeNode); + annotatedNode->kind = type; +} + +void PersistentPTree::updateBranchingNode(PTreeNode &node, BranchType reason) { + auto *annotatedNode = llvm::cast(&node); + const auto &state = *node.state; + const auto prevPC = state.prevPC; + annotatedNode->asmLine = + prevPC && prevPC->info ? prevPC->info->assemblyLine : 0; + annotatedNode->kind = reason; + writer.write(*annotatedNode); +} + +void PersistentPTree::updateTerminatingNode(PTreeNode &node) { + assert(node.state); + auto *annotatedNode = llvm::cast(&node); + const auto &state = *node.state; + const auto prevPC = state.prevPC; + annotatedNode->asmLine = + prevPC && prevPC->info ? prevPC->info->assemblyLine : 0; + annotatedNode->stateID = state.getID(); + writer.write(*annotatedNode); } + +// Factory + +std::unique_ptr klee::createPTree(ExecutionState &initialState, + bool inMemory, + InterpreterHandler &ih) { + if (WritePTree) + return std::make_unique(initialState, ih); + + if (inMemory) + return std::make_unique(initialState); + + return std::make_unique(); +}; diff --git a/lib/Core/PTree.h b/lib/Core/PTree.h index dbee70dd..ab3f0433 100644 --- a/lib/Core/PTree.h +++ b/lib/Core/PTree.h @@ -10,57 +10,170 @@ #ifndef KLEE_PTREE_H #define KLEE_PTREE_H +#include "PTreeWriter.h" +#include "UserSearcher.h" #include "klee/Core/BranchTypes.h" +#include "klee/Core/TerminationTypes.h" #include "klee/Expr/Expr.h" #include "klee/Support/ErrorHandling.h" + #include "llvm/ADT/PointerIntPair.h" +#include "llvm/Support/Casting.h" + +#include +#include namespace klee { - class ExecutionState; - class PTreeNode; - /* PTreeNodePtr is used by the Random Path Searcher object to efficiently - record which PTreeNode belongs to it. PTree is a global structure that - captures all states, whereas a Random Path Searcher might only care about - a subset. The integer part of PTreeNodePtr is a bitmask (a "tag") of which - Random Path Searchers PTreeNode belongs to. */ - constexpr int PtrBitCount = 3; - using PTreeNodePtr = llvm::PointerIntPair; - - class PTreeNode { - public: - PTreeNode *parent = nullptr; - - PTreeNodePtr left; - PTreeNodePtr right; - ExecutionState *state = nullptr; - - PTreeNode(const PTreeNode&) = delete; - PTreeNode(PTreeNode *parent, ExecutionState *state); - ~PTreeNode() = default; - }; - - class PTree { - // Number of registered ID - int registeredIds = 0; - - public: - PTreeNodePtr root; - explicit PTree(ExecutionState *initialState); - ~PTree() = default; - - void attach(PTreeNode *node, ExecutionState *leftState, - ExecutionState *rightState, BranchType reason); - void remove(PTreeNode *node); - void dump(llvm::raw_ostream &os); - std::uint8_t getNextId() { - std::uint8_t id = 1 << registeredIds++; - if (registeredIds > PtrBitCount) { - klee_error("PTree cannot support more than %d RandomPathSearchers", - PtrBitCount); - } - return id; - } - }; -} +class ExecutionState; +class Executor; +class InMemoryPTree; +class InterpreterHandler; +class PTreeNode; +class Searcher; + +/* PTreeNodePtr is used by the Random Path Searcher object to efficiently +record which PTreeNode belongs to it. PTree is a global structure that +captures all states, whereas a Random Path Searcher might only care about +a subset. The integer part of PTreeNodePtr is a bitmask (a "tag") of which +Random Path Searchers PTreeNode belongs to. */ +constexpr std::uint8_t PtrBitCount = 3; +using PTreeNodePtr = llvm::PointerIntPair; + +class PTreeNode { +public: + enum class NodeType : std::uint8_t { Basic, Annotated }; + + PTreeNode *parent{nullptr}; + PTreeNodePtr left; + PTreeNodePtr right; + ExecutionState *state{nullptr}; + + PTreeNode(PTreeNode *parent, ExecutionState *state) noexcept; + virtual ~PTreeNode() = default; + PTreeNode(const PTreeNode &) = delete; + PTreeNode &operator=(PTreeNode const &) = delete; + PTreeNode(PTreeNode &&) = delete; + PTreeNode &operator=(PTreeNode &&) = delete; + + [[nodiscard]] virtual NodeType getType() const { return NodeType::Basic; } + static bool classof(const PTreeNode *N) { return true; } +}; + +class AnnotatedPTreeNode : public PTreeNode { + inline static std::uint32_t nextID{1}; + +public: + std::uint32_t id{0}; + std::uint32_t stateID{0}; + std::uint32_t asmLine{0}; + std::variant kind{BranchType::NONE}; + + AnnotatedPTreeNode(PTreeNode *parent, ExecutionState *state) noexcept; + ~AnnotatedPTreeNode() override = default; + + [[nodiscard]] NodeType getType() const override { return NodeType::Annotated; } + static bool classof(const PTreeNode *N) { + return N->getType() == NodeType::Annotated; + } +}; + +class PTree { +public: + enum class PTreeType : std::uint8_t { Basic, Noop, InMemory, Persistent }; + + /// Branch from PTreeNode and attach states, convention: rightState is + /// parent + virtual void attach(PTreeNode *node, ExecutionState *leftState, + ExecutionState *rightState, BranchType reason) = 0; + /// Dump process tree in .dot format into os (debug) + virtual void dump(llvm::raw_ostream &os) = 0; + /// Remove node from tree + virtual void remove(PTreeNode *node) = 0; + /// Set termination type (on state removal) + virtual void setTerminationType(ExecutionState &state, + StateTerminationType type){} + + virtual ~PTree() = default; + PTree(PTree const &) = delete; + PTree &operator=(PTree const &) = delete; + PTree(PTree &&) = delete; + PTree &operator=(PTree &&) = delete; + + [[nodiscard]] virtual PTreeType getType() const = 0; + static bool classof(const PTreeNode *N) { return true; } + +protected: + explicit PTree() noexcept = default; +}; + +/// @brief A pseudo process tree that does not maintain any nodes. +class NoopPTree final : public PTree { +public: + NoopPTree() noexcept = default; + ~NoopPTree() override = default; + void attach(PTreeNode *node, ExecutionState *leftState, + ExecutionState *rightState, + BranchType reason) noexcept override{} + void dump(llvm::raw_ostream &os) noexcept override; + void remove(PTreeNode *node) noexcept override{} + + [[nodiscard]] PTreeType getType() const override { return PTreeType::Noop; }; + static bool classof(const PTree *T) { return T->getType() == PTreeType::Noop; } +}; + +/// @brief An in-memory process tree required by RandomPathSearcher +class InMemoryPTree : public PTree { +public: + PTreeNodePtr root; + +private: + /// Number of registered IDs ("users", e.g. RandomPathSearcher) + std::uint8_t registeredIds = 0; + + virtual PTreeNode *createNode(PTreeNode *parent, ExecutionState *state); + virtual void updateBranchingNode(PTreeNode &node, BranchType reason){} + virtual void updateTerminatingNode(PTreeNode &node){} + +public: + InMemoryPTree() noexcept = default; + explicit InMemoryPTree(ExecutionState &initialState) noexcept; + ~InMemoryPTree() override = default; + + void attach(PTreeNode *node, ExecutionState *leftState, + ExecutionState *rightState, BranchType reason) noexcept override; + void dump(llvm::raw_ostream &os) noexcept override; + std::uint8_t getNextId() noexcept; + void remove(PTreeNode *node) noexcept override; + + [[nodiscard]] PTreeType getType() const override { return PTreeType::InMemory; }; + static bool classof(const PTree *T) { + return (T->getType() == PTreeType::InMemory) || (T->getType() == PTreeType::Persistent); + } +}; + +/// @brief An in-memory process tree that also writes its nodes into an SQLite +/// database (ptree.db) with a PTreeWriter +class PersistentPTree : public InMemoryPTree { + PTreeWriter writer; + + PTreeNode *createNode(PTreeNode *parent, ExecutionState *state) override; + void updateBranchingNode(PTreeNode &node, BranchType reason) override; + void updateTerminatingNode(PTreeNode &node) override; + +public: + explicit PersistentPTree(ExecutionState &initialState, + InterpreterHandler &ih) noexcept; + ~PersistentPTree() override = default; + void dump(llvm::raw_ostream &os) noexcept override; + void setTerminationType(ExecutionState &state, + StateTerminationType type) override; + + [[nodiscard]] PTreeType getType() const override { return PTreeType::Persistent; }; + static bool classof(const PTree *T) { return T->getType() == PTreeType::Persistent; } +}; + +std::unique_ptr createPTree(ExecutionState &initialState, bool inMemory, + InterpreterHandler &ih); +} // namespace klee #endif /* KLEE_PTREE_H */ diff --git a/lib/Core/PTreeWriter.cpp b/lib/Core/PTreeWriter.cpp new file mode 100644 index 00000000..a8067a5d --- /dev/null +++ b/lib/Core/PTreeWriter.cpp @@ -0,0 +1,196 @@ +//===-- PTreeWriter.cpp ---------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#include "PTreeWriter.h" + +#include "PTree.h" +#include "klee/Support/ErrorHandling.h" +#include "klee/Support/OptionCategories.h" + +#include "llvm/Support/CommandLine.h" + +namespace { +llvm::cl::opt BatchSize( + "ptree-batch-size", llvm::cl::init(100U), + llvm::cl::desc("Number of process tree nodes to batch for writing, " + "see --write-ptree (default=100)"), + llvm::cl::cat(klee::PTreeCat)); +} // namespace + +using namespace klee; + +void prepare_statement(sqlite3 *db, const std::string &query, sqlite3_stmt **stmt) { + int result; +#ifdef SQLITE_PREPARE_PERSISTENT + result = sqlite3_prepare_v3(db, query.c_str(), -1, SQLITE_PREPARE_PERSISTENT, + stmt, nullptr); +#else + result = sqlite3_prepare_v3(db, query.c_str(), -1, 0, stmt, nullptr); +#endif + if (result != SQLITE_OK) { + klee_warning("Process tree database: can't prepare query: %s [%s]", + sqlite3_errmsg(db), query.c_str()); + sqlite3_close(db); + klee_error("Process tree database: can't prepare query: %s", query.c_str()); + } +} + +PTreeWriter::PTreeWriter(const std::string &dbPath) { + // create database file + if (sqlite3_open(dbPath.c_str(), &db) != SQLITE_OK) + klee_error("Can't create process tree database: %s", sqlite3_errmsg(db)); + + // - set options: asynchronous + WAL + char *errMsg = nullptr; + if (sqlite3_exec(db, "PRAGMA synchronous = OFF;", nullptr, nullptr, + &errMsg) != SQLITE_OK) { + klee_warning("Process tree database: can't set option: %s", errMsg); + sqlite3_free(errMsg); + } + if (sqlite3_exec(db, "PRAGMA journal_mode = WAL;", nullptr, nullptr, + &errMsg) != SQLITE_OK) { + klee_warning("Process tree database: can't set option: %s", errMsg); + sqlite3_free(errMsg); + } + + // - create table + std::string query = + "CREATE TABLE IF NOT EXISTS nodes (" + "ID INT PRIMARY KEY, stateID INT, leftID INT, rightID INT," + "asmLine INT, kind INT);"; + char *zErr = nullptr; + if (sqlite3_exec(db, query.c_str(), nullptr, nullptr, &zErr) != SQLITE_OK) { + klee_warning("Process tree database: initialisation error: %s", zErr); + sqlite3_free(zErr); + sqlite3_close(db); + klee_error("Process tree database: initialisation error."); + } + + // create prepared statements + // - insertStmt + query = "INSERT INTO nodes VALUES (?, ?, ?, ?, ?, ?);"; + prepare_statement(db, query, &insertStmt); + // - transactionBeginStmt + query = "BEGIN TRANSACTION"; + prepare_statement(db, query, &transactionBeginStmt); + // - transactionCommitStmt + query = "COMMIT TRANSACTION"; + prepare_statement(db, query, &transactionCommitStmt); + + // begin transaction + if (sqlite3_step(transactionBeginStmt) != SQLITE_DONE) { + klee_warning("Process tree database: can't begin transaction: %s", + sqlite3_errmsg(db)); + } + if (sqlite3_reset(transactionBeginStmt) != SQLITE_OK) { + klee_warning("Process tree database: can't reset transaction: %s", + sqlite3_errmsg(db)); + } +} + +PTreeWriter::~PTreeWriter() { + batchCommit(!flushed); + + // finalize prepared statements + sqlite3_finalize(insertStmt); + sqlite3_finalize(transactionBeginStmt); + sqlite3_finalize(transactionCommitStmt); + + // commit + if (sqlite3_exec(db, "END TRANSACTION", nullptr, nullptr, nullptr) != + SQLITE_OK) { + klee_warning("Process tree database: can't end transaction: %s", + sqlite3_errmsg(db)); + } + + if (sqlite3_close(db) != SQLITE_OK) { + klee_warning("Process tree database: can't close database: %s", + sqlite3_errmsg(db)); + } +} + +void PTreeWriter::batchCommit(bool force) { + ++batch; + if (batch < BatchSize && !force) + return; + + // commit and begin transaction + if (sqlite3_step(transactionCommitStmt) != SQLITE_DONE) { + klee_warning("Process tree database: transaction commit error: %s", + sqlite3_errmsg(db)); + } + + if (sqlite3_reset(transactionCommitStmt) != SQLITE_OK) { + klee_warning("Process tree database: transaction reset error: %s", + sqlite3_errmsg(db)); + } + + if (sqlite3_step(transactionBeginStmt) != SQLITE_DONE) { + klee_warning("Process tree database: transaction begin error: %s", + sqlite3_errmsg(db)); + } + + if (sqlite3_reset(transactionBeginStmt) != SQLITE_OK) { + klee_warning("Process tree database: transaction reset error: %s", + sqlite3_errmsg(db)); + } + + batch = 0; + flushed = true; +} + +void PTreeWriter::write(const AnnotatedPTreeNode &node) { + unsigned rc = 0; + + // bind values (SQLITE_OK is defined as 0 - just check success once at the + // end) + rc |= sqlite3_bind_int64(insertStmt, 1, node.id); + rc |= sqlite3_bind_int(insertStmt, 2, node.stateID); + rc |= sqlite3_bind_int64( + insertStmt, 3, + node.left.getPointer() + ? (static_cast(node.left.getPointer()))->id + : 0); + rc |= sqlite3_bind_int64( + insertStmt, 4, + node.right.getPointer() + ? (static_cast(node.right.getPointer()))->id + : 0); + rc |= sqlite3_bind_int(insertStmt, 5, node.asmLine); + std::uint8_t value{0}; + if (std::holds_alternative(node.kind)) { + value = static_cast(std::get(node.kind)); + } else if (std::holds_alternative(node.kind)) { + value = + static_cast(std::get(node.kind)); + } else { + assert(false && "PTreeWriter: Illegal node kind!"); + } + rc |= sqlite3_bind_int(insertStmt, 6, value); + if (rc != SQLITE_OK) { + // This is either a programming error (e.g. SQLITE_MISUSE) or we ran out of + // resources (e.g. SQLITE_NOMEM). Calling sqlite3_errmsg() after a possible + // successful call above is undefined, hence no error message here. + klee_error("Process tree database: can't persist data for node: %u", + node.id); + } + + // insert + if (sqlite3_step(insertStmt) != SQLITE_DONE) { + klee_warning("Process tree database: can't persist data for node: %u: %s", + node.id, sqlite3_errmsg(db)); + } + + if (sqlite3_reset(insertStmt) != SQLITE_OK) { + klee_warning("Process tree database: error reset node: %u: %s", node.id, + sqlite3_errmsg(db)); + } + + batchCommit(); +} diff --git a/lib/Core/PTreeWriter.h b/lib/Core/PTreeWriter.h new file mode 100644 index 00000000..12709116 --- /dev/null +++ b/lib/Core/PTreeWriter.h @@ -0,0 +1,46 @@ +//===-- PTreeWriter.h -------------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#pragma once + +#include + +#include +#include + +namespace klee { +class AnnotatedPTreeNode; + +/// @brief Writes process tree nodes into an SQLite database +class PTreeWriter { + friend class PersistentPTree; + + ::sqlite3 *db{nullptr}; + ::sqlite3_stmt *insertStmt{nullptr}; + ::sqlite3_stmt *transactionBeginStmt{nullptr}; + ::sqlite3_stmt *transactionCommitStmt{nullptr}; + std::uint32_t batch{0}; + bool flushed{true}; + + /// Writes nodes in batches + void batchCommit(bool force = false); + +public: + explicit PTreeWriter(const std::string &dbPath); + ~PTreeWriter(); + PTreeWriter(const PTreeWriter &other) = delete; + PTreeWriter(PTreeWriter &&other) noexcept = delete; + PTreeWriter &operator=(const PTreeWriter &other) = delete; + PTreeWriter &operator=(PTreeWriter &&other) noexcept = delete; + + /// Write new node into database + void write(const AnnotatedPTreeNode &node); +}; + +} // namespace klee diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp index bf98ebc7..1c57eb4e 100644 --- a/lib/Core/Searcher.cpp +++ b/lib/Core/Searcher.cpp @@ -261,15 +261,18 @@ void WeightedRandomSearcher::printName(llvm::raw_ostream &os) { #define IS_OUR_NODE_VALID(n) \ (((n).getPointer() != nullptr) && (((n).getInt() & idBitMask) != 0)) -RandomPathSearcher::RandomPathSearcher(PTree &processTree, RNG &rng) - : processTree{processTree}, - theRNG{rng}, - idBitMask{processTree.getNextId()} {}; +RandomPathSearcher::RandomPathSearcher(InMemoryPTree *processTree, RNG &rng) + : processTree{processTree}, theRNG{rng}, + idBitMask{ + static_cast(processTree ? processTree->getNextId() : 0)} { + + assert(processTree); +}; ExecutionState &RandomPathSearcher::selectState() { unsigned flips=0, bits=0; - assert(processTree.root.getInt() & idBitMask && "Root should belong to the searcher"); - PTreeNode *n = processTree.root.getPointer(); + assert(processTree->root.getInt() & idBitMask && "Root should belong to the searcher"); + PTreeNode *n = processTree->root.getPointer(); while (!n->state) { if (!IS_OUR_NODE_VALID(n->left)) { assert(IS_OUR_NODE_VALID(n->right) && "Both left and right nodes invalid"); @@ -302,7 +305,7 @@ void RandomPathSearcher::update(ExecutionState *current, childPtr = parent ? ((parent->left.getPointer() == pnode) ? &parent->left : &parent->right) - : &processTree.root; + : &processTree->root; while (pnode && !IS_OUR_NODE_VALID(*childPtr)) { childPtr->setInt(childPtr->getInt() | idBitMask); pnode = parent; @@ -312,7 +315,7 @@ void RandomPathSearcher::update(ExecutionState *current, childPtr = parent ? ((parent->left.getPointer() == pnode) ? &parent->left : &parent->right) - : &processTree.root; + : &processTree->root; } } @@ -325,7 +328,7 @@ void RandomPathSearcher::update(ExecutionState *current, auto childPtr = parent ? ((parent->left.getPointer() == pnode) ? &parent->left : &parent->right) - : &processTree.root; + : &processTree->root; assert(IS_OUR_NODE_VALID(*childPtr) && "Removing pTree child not ours"); childPtr->setInt(childPtr->getInt() & ~idBitMask); pnode = parent; @@ -336,7 +339,7 @@ void RandomPathSearcher::update(ExecutionState *current, } bool RandomPathSearcher::empty() { - return !IS_OUR_NODE_VALID(processTree.root); + return !IS_OUR_NODE_VALID(processTree->root); } void RandomPathSearcher::printName(llvm::raw_ostream &os) { diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h index e399c616..ddd49264 100644 --- a/lib/Core/Searcher.h +++ b/lib/Core/Searcher.h @@ -172,7 +172,7 @@ namespace klee { /// /// The ownership bits are maintained in the update method. class RandomPathSearcher final : public Searcher { - PTree &processTree; + InMemoryPTree *processTree; RNG &theRNG; // Unique bitmask of this searcher @@ -181,7 +181,7 @@ namespace klee { public: /// \param processTree The process tree. /// \param RNG A random number generator. - RandomPathSearcher(PTree &processTree, RNG &rng); + RandomPathSearcher(InMemoryPTree *processTree, RNG &rng); ~RandomPathSearcher() override = default; ExecutionState &selectState() override; diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index 488fba51..4589471c 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -480,12 +480,8 @@ void SpecialFunctionHandler::handleAssume(ExecutionState &state, state.constraints, e, res, state.queryMetaData); assert(success && "FIXME: Unhandled solver failure"); if (res) { - if (SilentKleeAssume) { - executor.terminateState(state); - } else { - executor.terminateStateOnUserError( - state, "invalid klee_assume call (provably false)"); - } + executor.terminateStateOnUserError( + state, "invalid klee_assume call (provably false)", !SilentKleeAssume); } else { executor.addConstraint(state, e); } diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp index 19ac3718..735075f1 100644 --- a/lib/Core/UserSearcher.cpp +++ b/lib/Core/UserSearcher.cpp @@ -100,9 +100,13 @@ bool userSearcherRequiresMD2U() { std::find(CoreSearch.begin(), CoreSearch.end(), Searcher::NURS_QC) != CoreSearch.end()); } +bool userSearcherRequiresInMemoryPTree() { + return std::find(CoreSearch.begin(), CoreSearch.end(), Searcher::RandomPath) != CoreSearch.end(); +} + } // namespace klee -Searcher *getNewSearcher(Searcher::CoreSearchType type, RNG &rng, PTree &processTree) { +Searcher *getNewSearcher(Searcher::CoreSearchType type, RNG &rng, InMemoryPTree *processTree) { Searcher *searcher = nullptr; switch (type) { case Searcher::DFS: searcher = new DFSSearcher(); break; @@ -122,15 +126,15 @@ Searcher *getNewSearcher(Searcher::CoreSearchType type, RNG &rng, PTree &process } Searcher *klee::constructUserSearcher(Executor &executor) { - - Searcher *searcher = getNewSearcher(CoreSearch[0], executor.theRNG, *executor.processTree); + auto *ptree = llvm::dyn_cast(executor.processTree.get()); + Searcher *searcher = getNewSearcher(CoreSearch[0], executor.theRNG, ptree); if (CoreSearch.size() > 1) { std::vector s; s.push_back(searcher); for (unsigned i = 1; i < CoreSearch.size(); i++) - s.push_back(getNewSearcher(CoreSearch[i], executor.theRNG, *executor.processTree)); + s.push_back(getNewSearcher(CoreSearch[i], executor.theRNG, ptree)); searcher = new InterleavedSearcher(s); } diff --git a/lib/Core/UserSearcher.h b/lib/Core/UserSearcher.h index b0df8239..fe75eb6d 100644 --- a/lib/Core/UserSearcher.h +++ b/lib/Core/UserSearcher.h @@ -16,6 +16,7 @@ namespace klee { // XXX gross, should be on demand? bool userSearcherRequiresMD2U(); + bool userSearcherRequiresInMemoryPTree(); void initializeSearchOptions(); -- cgit 1.4.1