diff options
author | Cristian Cadar <c.cadar@imperial.ac.uk> | 2020-04-03 16:07:09 +0100 |
---|---|---|
committer | MartinNowack <2443641+MartinNowack@users.noreply.github.com> | 2020-04-30 09:25:36 +0100 |
commit | e2cbdaeb98168db12aba4abab04eea2416c0931c (patch) | |
tree | cf65881678a00d2e7681ed7aabe66cec9354f891 /include | |
parent | 382de941118c12434410df0c5d4e1ecd28e4636f (diff) | |
download | klee-e2cbdaeb98168db12aba4abab04eea2416c0931c.tar.gz |
Created include/klee/Core directory and moved appropriate files direc\
tly in lib/Core
Diffstat (limited to 'include')
-rw-r--r-- | include/klee/Core/Interpreter.h (renamed from include/klee/Interpreter.h) | 0 | ||||
-rw-r--r-- | include/klee/ExecutionState.h | 173 | ||||
-rw-r--r-- | include/klee/MergeHandler.h | 155 | ||||
-rw-r--r-- | include/klee/Module/KModule.h | 2 |
4 files changed, 1 insertions, 329 deletions
diff --git a/include/klee/Interpreter.h b/include/klee/Core/Interpreter.h index de64030d..de64030d 100644 --- a/include/klee/Interpreter.h +++ b/include/klee/Core/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 <map> -#include <set> -#include <vector> - -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<const MemoryObject *> 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<StackFrame> 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<const std::string *, std::set<unsigned> > 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<std::pair<ref<const MemoryObject>, const Array *>> symbolics; - - /// @brief Set of used array names for this state. Used to avoid collisions. - std::set<std::string> arrayNames; - - // The objects handling the klee_open_merge calls this state ran through - std::vector<ref<MergeHandler> > 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<ref<Expr> > &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<Expr> 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/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<klee::ref<klee::MergeHandler>>` - * 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 <map> -#include <stdint.h> -#include <vector> - -namespace llvm { -class Instruction; -} - -namespace klee { -extern llvm::cl::opt<bool> UseMerge; - -extern llvm::cl::opt<bool> DebugLogMerge; - -extern llvm::cl::opt<bool> 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<ExecutionState *> openStates; - - /// @brief Mapping the different 'klee_close_merge' calls to the states that ran into - /// them - std::map<llvm::Instruction *, std::vector<ExecutionState *> > - 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" |