about summary refs log tree commit diff homepage
path: root/lib
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2020-04-03 16:07:09 +0100
committerMartinNowack <2443641+MartinNowack@users.noreply.github.com>2020-04-30 09:25:36 +0100
commite2cbdaeb98168db12aba4abab04eea2416c0931c (patch)
treecf65881678a00d2e7681ed7aabe66cec9354f891 /lib
parent382de941118c12434410df0c5d4e1ecd28e4636f (diff)
downloadklee-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.cpp4
-rw-r--r--lib/Core/AddressSpace.h1
-rw-r--r--lib/Core/ExecutionState.cpp6
-rw-r--r--lib/Core/ExecutionState.h172
-rw-r--r--lib/Core/Executor.cpp11
-rw-r--r--lib/Core/Executor.h5
-rw-r--r--lib/Core/ExecutorUtil.cpp7
-rw-r--r--lib/Core/ImpliedValue.cpp2
-rw-r--r--lib/Core/Memory.cpp3
-rw-r--r--lib/Core/MergeHandler.cpp4
-rw-r--r--lib/Core/MergeHandler.h155
-rw-r--r--lib/Core/PTree.cpp3
-rw-r--r--lib/Core/Searcher.cpp14
-rw-r--r--lib/Core/SeedInfo.cpp8
-rw-r--r--lib/Core/SpecialFunctionHandler.cpp9
-rw-r--r--lib/Core/StatsTracker.cpp12
-rw-r--r--lib/Core/TimingSolver.cpp5
-rw-r--r--lib/Core/UserSearcher.cpp6
-rw-r--r--lib/Module/KModule.cpp4
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"