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 +- lib/Core/AddressSpace.cpp | 4 +- lib/Core/AddressSpace.h | 1 + lib/Core/ExecutionState.cpp | 6 +- lib/Core/ExecutionState.h | 172 +++++++++++++++++++++++++++++++++++ lib/Core/Executor.cpp | 11 ++- lib/Core/Executor.h | 5 +- lib/Core/ExecutorUtil.cpp | 7 +- lib/Core/ImpliedValue.cpp | 2 +- lib/Core/Memory.cpp | 3 +- lib/Core/MergeHandler.cpp | 4 +- lib/Core/MergeHandler.h | 155 ++++++++++++++++++++++++++++++++ lib/Core/PTree.cpp | 3 +- lib/Core/Searcher.cpp | 14 +-- lib/Core/SeedInfo.cpp | 8 +- lib/Core/SpecialFunctionHandler.cpp | 9 +- lib/Core/StatsTracker.cpp | 12 +-- lib/Core/TimingSolver.cpp | 5 +- lib/Core/UserSearcher.cpp | 6 +- lib/Module/KModule.cpp | 4 +- tools/klee/main.cpp | 14 +-- 25 files changed, 561 insertions(+), 548 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 create mode 100644 lib/Core/ExecutionState.h create mode 100644 lib/Core/MergeHandler.h 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" diff --git a/lib/Core/AddressSpace.cpp b/lib/Core/AddressSpace.cpp index e006d4d0..114e9c8b 100644 --- a/lib/Core/AddressSpace.cpp +++ b/lib/Core/AddressSpace.cpp @@ -8,13 +8,15 @@ //===----------------------------------------------------------------------===// #include "AddressSpace.h" -#include "CoreStats.h" + #include "Memory.h" #include "TimingSolver.h" #include "klee/Expr/Expr.h" #include "klee/TimerStatIncrementer.h" +#include "CoreStats.h" + using namespace klee; /// diff --git a/lib/Core/AddressSpace.h b/lib/Core/AddressSpace.h index bcd4b13d..4df8d5f0 100644 --- a/lib/Core/AddressSpace.h +++ b/lib/Core/AddressSpace.h @@ -11,6 +11,7 @@ #define KLEE_ADDRESSSPACE_H #include "Memory.h" + #include "klee/Expr/Expr.h" #include "klee/ADT/ImmutableMap.h" #include "klee/System/Time.h" diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index e526a5fa..94ac7888 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -7,16 +7,16 @@ // //===----------------------------------------------------------------------===// -#include "Memory.h" +#include "ExecutionState.h" -#include "klee/ExecutionState.h" +#include "Memory.h" #include "klee/Expr/Expr.h" #include "klee/Module/Cell.h" #include "klee/Module/InstructionInfoTable.h" #include "klee/Module/KInstruction.h" #include "klee/Module/KModule.h" -#include "klee/OptionCategories.h" +#include "klee/Support/OptionCategories.h" #include "llvm/IR/Function.h" #include "llvm/Support/CommandLine.h" diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h new file mode 100644 index 00000000..f9051195 --- /dev/null +++ b/lib/Core/ExecutionState.h @@ -0,0 +1,172 @@ +//===-- 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 "AddressSpace.h" +#include "MergeHandler.h" + +#include "klee/ADT/TreeStream.h" +#include "klee/Expr/Constraints.h" +#include "klee/Expr/Expr.h" +#include "klee/Module/KInstIterator.h" +#include "klee/System/Time.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/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 74965625..693ac006 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -24,6 +24,8 @@ #include "TimingSolver.h" #include "UserSearcher.h" +#include "klee/ADT/KTest.h" +#include "klee/ADT/RNG.h" #include "klee/Common.h" #include "klee/Config/Version.h" #include "klee/Core/Interpreter.h" @@ -33,22 +35,19 @@ #include "klee/Expr/ExprPPrinter.h" #include "klee/Expr/ExprSMTLIBPrinter.h" #include "klee/Expr/ExprUtil.h" -#include "klee/ADT/KTest.h" -#include "klee/ADT/RNG.h" #include "klee/Module/Cell.h" #include "klee/Module/InstructionInfoTable.h" #include "klee/Module/KInstruction.h" #include "klee/Module/KModule.h" +#include "klee/OptionCategories.h" +#include "klee/Solver/SolverCmdLine.h" +#include "klee/Solver/SolverStats.h" #include "klee/Support/ErrorHandling.h" #include "klee/Support/FileHandling.h" #include "klee/Support/FloatEvaluation.h" #include "klee/Support/ModuleUtil.h" #include "klee/System/MemoryUsage.h" #include "klee/System/Time.h" -#include "klee/Interpreter.h" -#include "klee/OptionCategories.h" -#include "klee/Solver/SolverCmdLine.h" -#include "klee/Solver/SolverStats.h" #include "klee/TimerStatIncrementer.h" #include "klee/util/GetElementPtrTypeIterator.h" diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index cd6b173a..2cb97d66 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -15,14 +15,15 @@ #ifndef KLEE_EXECUTOR_H #define KLEE_EXECUTOR_H -#include "klee/ExecutionState.h" +#include "ExecutionState.h" + +#include "klee/Core/Interpreter.h" #include "klee/Expr/ArrayCache.h" #include "klee/Expr/ArrayExprOptimizer.h" #include "klee/Module/Cell.h" #include "klee/Module/KInstruction.h" #include "klee/Module/KModule.h" #include "klee/System/Time.h" -#include "klee/Interpreter.h" #include "llvm/ADT/Twine.h" #include "llvm/Support/raw_ostream.h" diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp index 1e5fc7b0..867e76a6 100644 --- a/lib/Core/ExecutorUtil.cpp +++ b/lib/Core/ExecutorUtil.cpp @@ -7,16 +7,15 @@ // //===----------------------------------------------------------------------===// -#include "Executor.h" - #include "Context.h" +#include "Executor.h" #include "klee/Config/Version.h" +#include "klee/Core/Interpreter.h" #include "klee/Expr/Expr.h" #include "klee/Module/KModule.h" -#include "klee/Support/ErrorHandling.h" -#include "klee/Interpreter.h" #include "klee/Solver/Solver.h" +#include "klee/Support/ErrorHandling.h" #include "llvm/IR/Constants.h" #include "llvm/IR/DataLayout.h" diff --git a/lib/Core/ImpliedValue.cpp b/lib/Core/ImpliedValue.cpp index 8be796d1..a09e4b7c 100644 --- a/lib/Core/ImpliedValue.cpp +++ b/lib/Core/ImpliedValue.cpp @@ -14,8 +14,8 @@ #include "klee/Expr/Constraints.h" #include "klee/Expr/Expr.h" #include "klee/Expr/ExprUtil.h" -#include "klee/Support/IntEvaluation.h" // FIXME: Use APInt #include "klee/Solver/Solver.h" +#include "klee/Support/IntEvaluation.h" // FIXME: Use APInt #include #include diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp index e369dd1a..b93373b8 100644 --- a/lib/Core/Memory.cpp +++ b/lib/Core/Memory.cpp @@ -12,11 +12,12 @@ #include "Context.h" #include "MemoryManager.h" +#include "klee/ADT/BitArray.h" #include "klee/Expr/ArrayCache.h" #include "klee/Expr/Expr.h" -#include "klee/Support/ErrorHandling.h" #include "klee/OptionCategories.h" #include "klee/Solver/Solver.h" +#include "klee/Support/ErrorHandling.h" #include "klee/util/BitArray.h" #include "llvm/IR/Function.h" diff --git a/lib/Core/MergeHandler.cpp b/lib/Core/MergeHandler.cpp index 7a683e84..578b1b51 100644 --- a/lib/Core/MergeHandler.cpp +++ b/lib/Core/MergeHandler.cpp @@ -7,12 +7,12 @@ // //===----------------------------------------------------------------------===// -#include "klee/MergeHandler.h" +#include "MergeHandler.h" #include "CoreStats.h" +#include "ExecutionState.h" #include "Executor.h" #include "Searcher.h" -#include "klee/ExecutionState.h" namespace klee { diff --git a/lib/Core/MergeHandler.h b/lib/Core/MergeHandler.h new file mode 100644 index 00000000..48b67467 --- /dev/null +++ b/lib/Core/MergeHandler.h @@ -0,0 +1,155 @@ +//===-- 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/lib/Core/PTree.cpp b/lib/Core/PTree.cpp index 91a6d883..6c10e0cc 100644 --- a/lib/Core/PTree.cpp +++ b/lib/Core/PTree.cpp @@ -9,7 +9,8 @@ #include "PTree.h" -#include "klee/ExecutionState.h" +#include "ExecutionState.h" + #include "klee/Expr/Expr.h" #include "klee/Expr/ExprPPrinter.h" diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp index 87ef98ad..d8119e49 100644 --- a/lib/Core/Searcher.cpp +++ b/lib/Core/Searcher.cpp @@ -10,21 +10,23 @@ #include "Searcher.h" #include "CoreStats.h" +#include "ExecutionState.h" #include "Executor.h" +#include "MergeHandler.h" #include "PTree.h" #include "StatsTracker.h" -#include "klee/ExecutionState.h" -#include "klee/MergeHandler.h" -#include "klee/Statistics.h" +#include "klee/ADT/DiscretePDF.h" +#include "klee/ADT/RNG.h" +#include "klee/Statistics/Statistics.h" #include "klee/Module/InstructionInfoTable.h" #include "klee/Module/KInstruction.h" #include "klee/Module/KModule.h" -#include "klee/ADT/DiscretePDF.h" -#include "klee/ADT/RNG.h" +#include "klee/Statistics.h" +#include "klee/Support/ErrorHandling.h" #include "klee/Support/ModuleUtil.h" #include "klee/System/Time.h" -#include "klee/Support/ErrorHandling.h" + #include "llvm/IR/CallSite.h" #include "llvm/IR/Constants.h" #include "llvm/IR/Instructions.h" diff --git a/lib/Core/SeedInfo.cpp b/lib/Core/SeedInfo.cpp index 7c3957d2..423e9861 100644 --- a/lib/Core/SeedInfo.cpp +++ b/lib/Core/SeedInfo.cpp @@ -7,14 +7,16 @@ // //===----------------------------------------------------------------------===// -#include "Memory.h" #include "SeedInfo.h" + +#include "ExecutionState.h" +#include "Memory.h" #include "TimingSolver.h" -#include "klee/ExecutionState.h" + +#include "klee/ADT/KTest.h" #include "klee/Expr/Expr.h" #include "klee/Expr/ExprUtil.h" -#include "klee/ADT/KTest.h" #include "klee/Support/ErrorHandling.h" using namespace klee; diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index 1d6db7e0..52beb89d 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -9,20 +9,21 @@ #include "SpecialFunctionHandler.h" +#include "ExecutionState.h" #include "Executor.h" #include "Memory.h" #include "MemoryManager.h" +#include "MergeHandler.h" #include "Searcher.h" #include "TimingSolver.h" -#include "klee/ExecutionState.h" #include "klee/Module/KInstruction.h" #include "klee/Module/KModule.h" -#include "klee/Support/Debug.h" -#include "klee/Support/ErrorHandling.h" -#include "klee/MergeHandler.h" #include "klee/OptionCategories.h" #include "klee/Solver/SolverCmdLine.h" +#include "klee/Support/Debug.h" +#include "klee/Support/ErrorHandling.h" +#include "klee/Support/OptionCategories.h" #include "llvm/ADT/Twine.h" #include "llvm/IR/DataLayout.h" diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp index fba20cdd..81db25e3 100644 --- a/lib/Core/StatsTracker.cpp +++ b/lib/Core/StatsTracker.cpp @@ -9,16 +9,18 @@ #include "StatsTracker.h" -#include "klee/ExecutionState.h" -#include "klee/Statistics.h" +#include "ExecutionState.h" + #include "klee/Config/Version.h" + #include "klee/Module/InstructionInfoTable.h" -#include "klee/Module/KModule.h" #include "klee/Module/KInstruction.h" +#include "klee/Module/KModule.h" +#include "klee/Solver/SolverStats.h" +#include "klee/Statistics/Statistics.h" +#include "klee/Support/ErrorHandling.h" #include "klee/Support/ModuleUtil.h" #include "klee/System/MemoryUsage.h" -#include "klee/Support/ErrorHandling.h" -#include "klee/Solver/SolverStats.h" #include "CallPathManager.h" #include "CoreStats.h" diff --git a/lib/Core/TimingSolver.cpp b/lib/Core/TimingSolver.cpp index 0bd2fe57..ee829a35 100644 --- a/lib/Core/TimingSolver.cpp +++ b/lib/Core/TimingSolver.cpp @@ -9,8 +9,11 @@ #include "TimingSolver.h" +#include "ExecutionState.h" + #include "klee/Config/Version.h" -#include "klee/ExecutionState.h" +#include "klee/Statistics/Statistics.h" +#include "klee/Statistics/TimerStatIncrementer.h" #include "klee/Solver/Solver.h" #include "klee/Statistics.h" #include "klee/TimerStatIncrementer.h" diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp index a7982115..8dc32a40 100644 --- a/lib/Core/UserSearcher.cpp +++ b/lib/Core/UserSearcher.cpp @@ -9,12 +9,12 @@ #include "UserSearcher.h" -#include "Searcher.h" #include "Executor.h" +#include "MergeHandler.h" +#include "Searcher.h" -#include "klee/Support/ErrorHandling.h" -#include "klee/MergeHandler.h" #include "klee/Solver/SolverCmdLine.h" +#include "klee/Support/ErrorHandling.h" #include "llvm/Support/CommandLine.h" diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp index 4377d4af..e6c06594 100644 --- a/lib/Module/KModule.cpp +++ b/lib/Module/KModule.cpp @@ -12,15 +12,15 @@ #include "Passes.h" #include "klee/Config/Version.h" +#include "klee/Core/Interpreter.h" #include "klee/Module/Cell.h" #include "klee/Module/InstructionInfoTable.h" #include "klee/Module/KInstruction.h" #include "klee/Module/KModule.h" +#include "klee/OptionCategories.h" #include "klee/Support/Debug.h" #include "klee/Support/ErrorHandling.h" #include "klee/Support/ModuleUtil.h" -#include "klee/Interpreter.h" -#include "klee/OptionCategories.h" #if LLVM_VERSION_CODE >= LLVM_VERSION(4, 0) #include "llvm/Bitcode/BitcodeWriter.h" diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index 209f67b2..06273879 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -9,21 +9,20 @@ // //===----------------------------------------------------------------------===// -#include "klee/Config/Version.h" -#include "klee/ExecutionState.h" -#include "klee/Expr/Expr.h" #include "klee/ADT/KTest.h" #include "klee/ADT/TreeStream.h" +#include "klee/Config/Version.h" +#include "klee/Core/Interpreter.h" +#include "klee/Expr/Expr.h" +#include "klee/OptionCategories.h" +#include "klee/Solver/SolverCmdLine.h" +#include "klee/Statistics.h" #include "klee/Support/Debug.h" #include "klee/Support/ErrorHandling.h" #include "klee/Support/FileHandling.h" #include "klee/Support/ModuleUtil.h" #include "klee/Support/PrintVersion.h" #include "klee/System/Time.h" -#include "klee/Interpreter.h" -#include "klee/OptionCategories.h" -#include "klee/Solver/SolverCmdLine.h" -#include "klee/Statistics.h" #include "llvm/IR/Constants.h" #include "llvm/IR/IRBuilder.h" @@ -293,6 +292,7 @@ namespace { namespace klee { extern cl::opt MaxTime; +class ExecutionState; } /***/ -- cgit 1.4.1