about summary refs log tree commit diff homepage
path: root/include
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 /include
parent382de941118c12434410df0c5d4e1ecd28e4636f (diff)
downloadklee-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.h173
-rw-r--r--include/klee/MergeHandler.h155
-rw-r--r--include/klee/Module/KModule.h2
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"