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 /lib | |
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 'lib')
-rw-r--r-- | lib/Core/AddressSpace.cpp | 4 | ||||
-rw-r--r-- | lib/Core/AddressSpace.h | 1 | ||||
-rw-r--r-- | lib/Core/ExecutionState.cpp | 6 | ||||
-rw-r--r-- | lib/Core/ExecutionState.h | 172 | ||||
-rw-r--r-- | lib/Core/Executor.cpp | 11 | ||||
-rw-r--r-- | lib/Core/Executor.h | 5 | ||||
-rw-r--r-- | lib/Core/ExecutorUtil.cpp | 7 | ||||
-rw-r--r-- | lib/Core/ImpliedValue.cpp | 2 | ||||
-rw-r--r-- | lib/Core/Memory.cpp | 3 | ||||
-rw-r--r-- | lib/Core/MergeHandler.cpp | 4 | ||||
-rw-r--r-- | lib/Core/MergeHandler.h | 155 | ||||
-rw-r--r-- | lib/Core/PTree.cpp | 3 | ||||
-rw-r--r-- | lib/Core/Searcher.cpp | 14 | ||||
-rw-r--r-- | lib/Core/SeedInfo.cpp | 8 | ||||
-rw-r--r-- | lib/Core/SpecialFunctionHandler.cpp | 9 | ||||
-rw-r--r-- | lib/Core/StatsTracker.cpp | 12 | ||||
-rw-r--r-- | lib/Core/TimingSolver.cpp | 5 | ||||
-rw-r--r-- | lib/Core/UserSearcher.cpp | 6 | ||||
-rw-r--r-- | lib/Module/KModule.cpp | 4 |
19 files changed, 386 insertions, 45 deletions
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 <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/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 <map> #include <set> 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<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/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" |