From e2cbdaeb98168db12aba4abab04eea2416c0931c Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Fri, 3 Apr 2020 16:07:09 +0100 Subject: Created include/klee/Core directory and moved appropriate files direc\ tly in lib/Core --- include/klee/Core/Interpreter.h | 167 ++++++++++++++++++++++++++++++++++++++ include/klee/ExecutionState.h | 173 ---------------------------------------- include/klee/Interpreter.h | 167 -------------------------------------- include/klee/MergeHandler.h | 155 ----------------------------------- include/klee/Module/KModule.h | 2 +- 5 files changed, 168 insertions(+), 496 deletions(-) create mode 100644 include/klee/Core/Interpreter.h delete mode 100644 include/klee/ExecutionState.h delete mode 100644 include/klee/Interpreter.h delete mode 100644 include/klee/MergeHandler.h (limited to 'include') diff --git a/include/klee/Core/Interpreter.h b/include/klee/Core/Interpreter.h new file mode 100644 index 00000000..de64030d --- /dev/null +++ b/include/klee/Core/Interpreter.h @@ -0,0 +1,167 @@ +//===-- Interpreter.h - Abstract Execution Engine Interface -----*- 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_INTERPRETER_H +#define KLEE_INTERPRETER_H + +#include +#include +#include +#include +#include + +struct KTest; + +namespace llvm { +class Function; +class LLVMContext; +class Module; +class raw_ostream; +class raw_fd_ostream; +} + +namespace klee { +class ExecutionState; +class Interpreter; +class TreeStreamWriter; + +class InterpreterHandler { +public: + InterpreterHandler() {} + virtual ~InterpreterHandler() {} + + virtual llvm::raw_ostream &getInfoStream() const = 0; + + virtual std::string getOutputFilename(const std::string &filename) = 0; + virtual std::unique_ptr openOutputFile(const std::string &filename) = 0; + + virtual void incPathsExplored() = 0; + + virtual void processTestCase(const ExecutionState &state, + const char *err, + const char *suffix) = 0; +}; + +class Interpreter { +public: + /// ModuleOptions - Module level options which can be set when + /// registering a module with the interpreter. + struct ModuleOptions { + std::string LibraryDir; + std::string EntryPoint; + bool Optimize; + bool CheckDivZero; + bool CheckOvershift; + + ModuleOptions(const std::string &_LibraryDir, + const std::string &_EntryPoint, bool _Optimize, + bool _CheckDivZero, bool _CheckOvershift) + : LibraryDir(_LibraryDir), EntryPoint(_EntryPoint), Optimize(_Optimize), + CheckDivZero(_CheckDivZero), CheckOvershift(_CheckOvershift) {} + }; + + enum LogType + { + STP, //.CVC (STP's native language) + KQUERY, //.KQUERY files (kQuery native language) + SMTLIB2 //.SMT2 files (SMTLIB version 2 files) + }; + + /// InterpreterOptions - Options varying the runtime behavior during + /// interpretation. + struct InterpreterOptions { + /// A frequency at which to make concrete reads return constrained + /// symbolic values. This is used to test the correctness of the + /// symbolic execution on concrete programs. + unsigned MakeConcreteSymbolic; + + InterpreterOptions() + : MakeConcreteSymbolic(false) + {} + }; + +protected: + const InterpreterOptions interpreterOpts; + + Interpreter(const InterpreterOptions &_interpreterOpts) + : interpreterOpts(_interpreterOpts) + {} + +public: + virtual ~Interpreter() {} + + static Interpreter *create(llvm::LLVMContext &ctx, + const InterpreterOptions &_interpreterOpts, + InterpreterHandler *ih); + + /// Register the module to be executed. + /// \param modules A list of modules that should form the final + /// module + /// \return The final module after it has been optimized, checks + /// inserted, and modified for interpretation. + virtual llvm::Module * + setModule(std::vector> &modules, + const ModuleOptions &opts) = 0; + + // supply a tree stream writer which the interpreter will use + // to record the concrete path (as a stream of '0' and '1' bytes). + virtual void setPathWriter(TreeStreamWriter *tsw) = 0; + + // supply a tree stream writer which the interpreter will use + // to record the symbolic path (as a stream of '0' and '1' bytes). + virtual void setSymbolicPathWriter(TreeStreamWriter *tsw) = 0; + + // supply a test case to replay from. this can be used to drive the + // interpretation down a user specified path. use null to reset. + virtual void setReplayKTest(const struct KTest *out) = 0; + + // supply a list of branch decisions specifying which direction to + // take on forks. this can be used to drive the interpretation down + // a user specified path. use null to reset. + virtual void setReplayPath(const std::vector *path) = 0; + + // supply a set of symbolic bindings that will be used as "seeds" + // for the search. use null to reset. + virtual void useSeeds(const std::vector *seeds) = 0; + + virtual void runFunctionAsMain(llvm::Function *f, + int argc, + char **argv, + char **envp) = 0; + + /*** Runtime options ***/ + + virtual void setHaltExecution(bool value) = 0; + + virtual void setInhibitForking(bool value) = 0; + + virtual void prepareForEarlyExit() = 0; + + /*** State accessor methods ***/ + + virtual unsigned getPathStreamID(const ExecutionState &state) = 0; + + virtual unsigned getSymbolicPathStreamID(const ExecutionState &state) = 0; + + virtual void getConstraintLog(const ExecutionState &state, + std::string &res, + LogType logFormat = STP) = 0; + + virtual bool getSymbolicSolution(const ExecutionState &state, + std::vector< + std::pair > > + &res) = 0; + + virtual void getCoveredLines(const ExecutionState &state, + std::map > &res) = 0; +}; + +} // End klee namespace + +#endif /* KLEE_INTERPRETER_H */ diff --git a/include/klee/ExecutionState.h b/include/klee/ExecutionState.h deleted file mode 100644 index b5625a00..00000000 --- a/include/klee/ExecutionState.h +++ /dev/null @@ -1,173 +0,0 @@ -//===-- ExecutionState.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_EXECUTIONSTATE_H -#define KLEE_EXECUTIONSTATE_H - -#include "klee/Expr/Constraints.h" -#include "klee/Expr/Expr.h" -#include "klee/ADT/TreeStream.h" -#include "klee/System/Time.h" -#include "klee/MergeHandler.h" - -// FIXME: We do not want to be exposing these? :( -#include "../../lib/Core/AddressSpace.h" -#include "klee/Module/KInstIterator.h" - -#include -#include -#include - -namespace klee { -class Array; -class CallPathNode; -struct Cell; -struct KFunction; -struct KInstruction; -class MemoryObject; -class PTreeNode; -struct InstructionInfo; - -llvm::raw_ostream &operator<<(llvm::raw_ostream &os, const MemoryMap &mm); - -struct StackFrame { - KInstIterator caller; - KFunction *kf; - CallPathNode *callPathNode; - - std::vector allocas; - Cell *locals; - - /// Minimum distance to an uncovered instruction once the function - /// returns. This is not a good place for this but is used to - /// quickly compute the context sensitive minimum distance to an - /// uncovered instruction. This value is updated by the StatsTracker - /// periodically. - unsigned minDistToUncoveredOnReturn; - - // For vararg functions: arguments not passed via parameter are - // stored (packed tightly) in a local (alloca) memory object. This - // is set up to match the way the front-end generates vaarg code (it - // does not pass vaarg through as expected). VACopy is lowered inside - // of intrinsic lowering. - MemoryObject *varargs; - - StackFrame(KInstIterator caller, KFunction *kf); - StackFrame(const StackFrame &s); - ~StackFrame(); -}; - -/// @brief ExecutionState representing a path under exploration -class ExecutionState { -public: - typedef std::vector stack_ty; - -private: - // unsupported, use copy constructor - ExecutionState &operator=(const ExecutionState &); - -public: - // Execution - Control Flow specific - - /// @brief Pointer to instruction to be executed after the current - /// instruction - KInstIterator pc; - - /// @brief Pointer to instruction which is currently executed - KInstIterator prevPC; - - /// @brief Stack representing the current instruction stream - stack_ty stack; - - /// @brief Remember from which Basic Block control flow arrived - /// (i.e. to select the right phi values) - unsigned incomingBBIndex; - - // Overall state of the state - Data specific - - /// @brief Address space used by this state (e.g. Global and Heap) - AddressSpace addressSpace; - - /// @brief Constraints collected so far - ConstraintManager constraints; - - /// Statistics and information - - /// @brief Costs for all queries issued for this state, in seconds - mutable time::Span queryCost; - - /// @brief Exploration depth, i.e., number of times KLEE branched for this state - unsigned depth; - - /// @brief History of complete path: represents branches taken to - /// reach/create this state (both concrete and symbolic) - TreeOStream pathOS; - - /// @brief History of symbolic path: represents symbolic branches - /// taken to reach/create this state - TreeOStream symPathOS; - - /// @brief Counts how many instructions were executed since the last new - /// instruction was covered. - unsigned instsSinceCovNew; - - /// @brief Whether a new instruction was covered in this state - bool coveredNew; - - /// @brief Disables forking for this state. Set by user code - bool forkDisabled; - - /// @brief Set containing which lines in which files are covered by this state - std::map > coveredLines; - - /// @brief Pointer to the process tree of the current state - PTreeNode *ptreeNode; - - /// @brief Ordered list of symbolics: used to generate test cases. - // - // FIXME: Move to a shared list structure (not critical). - std::vector, const Array *>> symbolics; - - /// @brief Set of used array names for this state. Used to avoid collisions. - std::set arrayNames; - - // The objects handling the klee_open_merge calls this state ran through - std::vector > openMergeStack; - - // The numbers of times this state has run through Executor::stepInstruction - std::uint64_t steppedInstructions; - -private: - ExecutionState() : ptreeNode(0) {} - -public: - ExecutionState(KFunction *kf); - - // XXX total hack, just used to make a state so solver can - // use on structure - ExecutionState(const std::vector > &assumptions); - - ExecutionState(const ExecutionState &state); - - ~ExecutionState(); - - ExecutionState *branch(); - - void pushFrame(KInstIterator caller, KFunction *kf); - void popFrame(); - - void addSymbolic(const MemoryObject *mo, const Array *array); - void addConstraint(ref e) { constraints.addConstraint(e); } - - bool merge(const ExecutionState &b); - void dumpStack(llvm::raw_ostream &out) const; -}; -} - -#endif /* KLEE_EXECUTIONSTATE_H */ diff --git a/include/klee/Interpreter.h b/include/klee/Interpreter.h deleted file mode 100644 index de64030d..00000000 --- a/include/klee/Interpreter.h +++ /dev/null @@ -1,167 +0,0 @@ -//===-- Interpreter.h - Abstract Execution Engine Interface -----*- 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_INTERPRETER_H -#define KLEE_INTERPRETER_H - -#include -#include -#include -#include -#include - -struct KTest; - -namespace llvm { -class Function; -class LLVMContext; -class Module; -class raw_ostream; -class raw_fd_ostream; -} - -namespace klee { -class ExecutionState; -class Interpreter; -class TreeStreamWriter; - -class InterpreterHandler { -public: - InterpreterHandler() {} - virtual ~InterpreterHandler() {} - - virtual llvm::raw_ostream &getInfoStream() const = 0; - - virtual std::string getOutputFilename(const std::string &filename) = 0; - virtual std::unique_ptr openOutputFile(const std::string &filename) = 0; - - virtual void incPathsExplored() = 0; - - virtual void processTestCase(const ExecutionState &state, - const char *err, - const char *suffix) = 0; -}; - -class Interpreter { -public: - /// ModuleOptions - Module level options which can be set when - /// registering a module with the interpreter. - struct ModuleOptions { - std::string LibraryDir; - std::string EntryPoint; - bool Optimize; - bool CheckDivZero; - bool CheckOvershift; - - ModuleOptions(const std::string &_LibraryDir, - const std::string &_EntryPoint, bool _Optimize, - bool _CheckDivZero, bool _CheckOvershift) - : LibraryDir(_LibraryDir), EntryPoint(_EntryPoint), Optimize(_Optimize), - CheckDivZero(_CheckDivZero), CheckOvershift(_CheckOvershift) {} - }; - - enum LogType - { - STP, //.CVC (STP's native language) - KQUERY, //.KQUERY files (kQuery native language) - SMTLIB2 //.SMT2 files (SMTLIB version 2 files) - }; - - /// InterpreterOptions - Options varying the runtime behavior during - /// interpretation. - struct InterpreterOptions { - /// A frequency at which to make concrete reads return constrained - /// symbolic values. This is used to test the correctness of the - /// symbolic execution on concrete programs. - unsigned MakeConcreteSymbolic; - - InterpreterOptions() - : MakeConcreteSymbolic(false) - {} - }; - -protected: - const InterpreterOptions interpreterOpts; - - Interpreter(const InterpreterOptions &_interpreterOpts) - : interpreterOpts(_interpreterOpts) - {} - -public: - virtual ~Interpreter() {} - - static Interpreter *create(llvm::LLVMContext &ctx, - const InterpreterOptions &_interpreterOpts, - InterpreterHandler *ih); - - /// Register the module to be executed. - /// \param modules A list of modules that should form the final - /// module - /// \return The final module after it has been optimized, checks - /// inserted, and modified for interpretation. - virtual llvm::Module * - setModule(std::vector> &modules, - const ModuleOptions &opts) = 0; - - // supply a tree stream writer which the interpreter will use - // to record the concrete path (as a stream of '0' and '1' bytes). - virtual void setPathWriter(TreeStreamWriter *tsw) = 0; - - // supply a tree stream writer which the interpreter will use - // to record the symbolic path (as a stream of '0' and '1' bytes). - virtual void setSymbolicPathWriter(TreeStreamWriter *tsw) = 0; - - // supply a test case to replay from. this can be used to drive the - // interpretation down a user specified path. use null to reset. - virtual void setReplayKTest(const struct KTest *out) = 0; - - // supply a list of branch decisions specifying which direction to - // take on forks. this can be used to drive the interpretation down - // a user specified path. use null to reset. - virtual void setReplayPath(const std::vector *path) = 0; - - // supply a set of symbolic bindings that will be used as "seeds" - // for the search. use null to reset. - virtual void useSeeds(const std::vector *seeds) = 0; - - virtual void runFunctionAsMain(llvm::Function *f, - int argc, - char **argv, - char **envp) = 0; - - /*** Runtime options ***/ - - virtual void setHaltExecution(bool value) = 0; - - virtual void setInhibitForking(bool value) = 0; - - virtual void prepareForEarlyExit() = 0; - - /*** State accessor methods ***/ - - virtual unsigned getPathStreamID(const ExecutionState &state) = 0; - - virtual unsigned getSymbolicPathStreamID(const ExecutionState &state) = 0; - - virtual void getConstraintLog(const ExecutionState &state, - std::string &res, - LogType logFormat = STP) = 0; - - virtual bool getSymbolicSolution(const ExecutionState &state, - std::vector< - std::pair > > - &res) = 0; - - virtual void getCoveredLines(const ExecutionState &state, - std::map > &res) = 0; -}; - -} // End klee namespace - -#endif /* KLEE_INTERPRETER_H */ diff --git a/include/klee/MergeHandler.h b/include/klee/MergeHandler.h deleted file mode 100644 index 48b67467..00000000 --- a/include/klee/MergeHandler.h +++ /dev/null @@ -1,155 +0,0 @@ -//===-- MergeHandler.h --------------------------------------------*- C++ -*-===// -// -// The KLEE Symbolic Virtual Machine -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. -// -//===----------------------------------------------------------------------===// - -/** - * @file MergeHandler.h - * @brief Implementation of the region based merging - * - * ## Basic usage: - * - * @code{.cpp} - * klee_open_merge(); - * - * code containing branches etc. - * - * klee_close_merge(); - * @endcode - * - * Will lead to all states that forked from the state that executed the - * klee_open_merge() being merged in the klee_close_merge(). This allows for - * fine-grained regions to be specified for merging. - * - * # Implementation Structure - * - * The main part of the new functionality is implemented in the class - * klee::MergeHandler. The Special Function Handler generates an instance of - * this class every time a state runs into a klee_open_merge() call. - * - * This instance is appended to a `std::vector>` - * in the ExecutionState that passed the merge open point. This stack is also - * copied during forks. We use a stack instead of a single instance to support - * nested merge regions. - * - * Once a state runs into a `klee_close_merge()`, the Special Function Handler - * notifies the top klee::MergeHandler in the state's stack, pauses the state - * from scheduling, and tries to merge it with all other states that already - * arrived at the same close merge point. This top instance is then popped from - * the stack, resulting in a decrease of the ref count of the - * klee::MergeHandler. - * - * Since the only references to this MergeHandler are in the stacks of - * the ExecutionStates currently in the merging region, once the ref count - * reaches zero, every state which ran into the same `klee_open_merge()` is now - * paused and waiting to be merged. The destructor of the MergeHandler - * then continues the scheduling of the corresponding paused states. - * - * # Non-blocking State Merging - * - * This feature adds functionality to the BoundedMergingSearcher that will - * prioritize (e.g., immediately schedule) states running inside a bounded-merge - * region once a state has reached a corresponding klee_close_merge() call. The - * goal is to quickly gather all states inside the merging region in order to - * release the waiting states. However, states that are running for more than - * twice the mean number of instructions compared to the states that are already - * waiting, will not be prioritized anymore. - * - * Once no more states are available for prioritizing, but there are states - * waiting to be released, these states (which have already been merged as good as - * possible) will be continued without waiting for the remaining states. When a - * remaining state now enters a close-merge point, it will again wait for the - * other states, or until the 'timeout' is reached. -*/ - -#ifndef KLEE_MERGEHANDLER_H -#define KLEE_MERGEHANDLER_H - -#include "klee/util/Ref.h" -#include "llvm/Support/CommandLine.h" -#include -#include -#include - -namespace llvm { -class Instruction; -} - -namespace klee { -extern llvm::cl::opt UseMerge; - -extern llvm::cl::opt DebugLogMerge; - -extern llvm::cl::opt DebugLogIncompleteMerge; - -class Executor; -class ExecutionState; - -/// @brief Represents one `klee_open_merge()` call. -/// Handles merging of states that branched from it -class MergeHandler { -private: - Executor *executor; - - /// @brief The instruction count when the state ran into the klee_open_merge - uint64_t openInstruction; - - /// @brief The average number of instructions between the open and close merge of each - /// state that has finished so far - double closedMean; - - /// @brief Number of states that are tracked by this MergeHandler, that ran - /// into a relevant klee_close_merge - unsigned closedStateCount; - - /// @brief Get distance of state from the openInstruction - unsigned getInstructionDistance(ExecutionState *es); - - /// @brief States that ran through the klee_open_merge, but not yet into a - /// corresponding klee_close_merge - std::vector openStates; - - /// @brief Mapping the different 'klee_close_merge' calls to the states that ran into - /// them - std::map > - reachedCloseMerge; - -public: - - /// @brief Called when a state runs into a 'klee_close_merge()' call - void addClosedState(ExecutionState *es, llvm::Instruction *mp); - - /// @brief Return state that should be prioritized to complete this merge - ExecutionState *getPrioritizeState(); - - /// @brief Add state to the 'openStates' vector - void addOpenState(ExecutionState *es); - - /// @brief Remove state from the 'openStates' vector - void removeOpenState(ExecutionState *es); - - /// @brief True, if any states have run into 'klee_close_merge()' and have - /// not been released yet - bool hasMergedStates(); - - /// @brief Immediately release the merged states that have run into a - /// 'klee_merge_close()' - void releaseStates(); - - // Return the mean time it takes for a state to get from klee_open_merge to - // klee_close_merge - double getMean(); - - /// @brief Required by klee::ref-managed objects - class ReferenceCounter _refCount; - - MergeHandler(Executor *_executor, ExecutionState *es); - ~MergeHandler(); -}; -} - -#endif /* KLEE_MERGEHANDLER_H */ diff --git a/include/klee/Module/KModule.h b/include/klee/Module/KModule.h index 89606e2e..9c24cb31 100644 --- a/include/klee/Module/KModule.h +++ b/include/klee/Module/KModule.h @@ -11,7 +11,7 @@ #define KLEE_KMODULE_H #include "klee/Config/Version.h" -#include "klee/Interpreter.h" +#include "klee/Core/Interpreter.h" #include "llvm/ADT/ArrayRef.h" -- cgit 1.4.1