about summary refs log tree commit diff homepage
path: root/lib/Core
diff options
context:
space:
mode:
authorFrank Busse <bb0xfb@gmail.com>2020-06-16 18:33:26 +0100
committerMartinNowack <2443641+MartinNowack@users.noreply.github.com>2020-06-24 13:48:18 +0100
commita36f7a20afaf6e477846cf72814ebe2c346d87ec (patch)
tree3ce7eeef77ce7b31f077cce68ec178775bd6e18c /lib/Core
parent623d7149dc629af9c8a85fe5d3f841d9deed2192 (diff)
downloadklee-a36f7a20afaf6e477846cf72814ebe2c346d87ec.tar.gz
slightly update ExecutionState, remove holes in struct
Diffstat (limited to 'lib/Core')
-rw-r--r--lib/Core/ExecutionState.cpp45
-rw-r--r--lib/Core/ExecutionState.h62
2 files changed, 49 insertions, 58 deletions
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index 94ac7888..b3719295 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -68,22 +68,20 @@ StackFrame::~StackFrame() {
 ExecutionState::ExecutionState(KFunction *kf) :
     pc(kf->instructions),
     prevPC(pc),
-
     depth(0),
-
+    ptreeNode(nullptr),
+    steppedInstructions(0),
     instsSinceCovNew(0),
     coveredNew(false),
-    forkDisabled(false),
-    ptreeNode(0),
-    steppedInstructions(0){
-  pushFrame(0, kf);
+    forkDisabled(false) {
+  pushFrame(nullptr, kf);
 }
 
-ExecutionState::ExecutionState(const std::vector<ref<Expr> > &assumptions)
-    : constraints(assumptions), ptreeNode(0) {}
+ExecutionState::ExecutionState(const std::vector<ref<Expr>> &assumptions)
+    : constraints(assumptions), ptreeNode(nullptr) {}
 
 ExecutionState::~ExecutionState() {
-  for (auto cur_mergehandler: openMergeStack){
+  for (const auto &cur_mergehandler: openMergeStack){
     cur_mergehandler->removeOpenState(this);
   }
 
@@ -95,33 +93,29 @@ ExecutionState::ExecutionState(const ExecutionState& state):
     prevPC(state.prevPC),
     stack(state.stack),
     incomingBBIndex(state.incomingBBIndex),
-
+    depth(state.depth),
     addressSpace(state.addressSpace),
     constraints(state.constraints),
-
     queryCost(state.queryCost),
-    depth(state.depth),
-
     pathOS(state.pathOS),
     symPathOS(state.symPathOS),
-
-    instsSinceCovNew(state.instsSinceCovNew),
-    coveredNew(state.coveredNew),
-    forkDisabled(state.forkDisabled),
     coveredLines(state.coveredLines),
     ptreeNode(state.ptreeNode),
     symbolics(state.symbolics),
     arrayNames(state.arrayNames),
     openMergeStack(state.openMergeStack),
-    steppedInstructions(state.steppedInstructions) {
-  for (auto cur_mergehandler: openMergeStack)
+    steppedInstructions(state.steppedInstructions),
+    instsSinceCovNew(state.instsSinceCovNew),
+    coveredNew(state.coveredNew),
+    forkDisabled(state.forkDisabled) {
+  for (const auto &cur_mergehandler: openMergeStack)
     cur_mergehandler->addOpenState(this);
 }
 
 ExecutionState *ExecutionState::branch() {
   depth++;
 
-  ExecutionState *falseState = new ExecutionState(*this);
+  auto *falseState = new ExecutionState(*this);
   falseState->coveredNew = false;
   falseState->coveredLines.clear();
 
@@ -129,19 +123,18 @@ ExecutionState *ExecutionState::branch() {
 }
 
 void ExecutionState::pushFrame(KInstIterator caller, KFunction *kf) {
-  stack.push_back(StackFrame(caller,kf));
+  stack.emplace_back(StackFrame(caller, kf));
 }
 
 void ExecutionState::popFrame() {
-  StackFrame &sf = stack.back();
-  for (std::vector<const MemoryObject*>::iterator it = sf.allocas.begin(), 
-         ie = sf.allocas.end(); it != ie; ++it)
-    addressSpace.unbindObject(*it);
+  const StackFrame &sf = stack.back();
+  for (const auto * memoryObject : sf.allocas)
+    addressSpace.unbindObject(memoryObject);
   stack.pop_back();
 }
 
 void ExecutionState::addSymbolic(const MemoryObject *mo, const Array *array) {
-  symbolics.emplace_back(std::make_pair(ref<const MemoryObject>(mo), array));
+  symbolics.emplace_back(ref<const MemoryObject>(mo), array);
 }
 
 /**/
diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h
index f9051195..176ffef6 100644
--- a/lib/Core/ExecutionState.h
+++ b/lib/Core/ExecutionState.h
@@ -65,13 +65,8 @@ struct StackFrame {
 /// @brief ExecutionState representing a path under exploration
 class ExecutionState {
 public:
-  typedef std::vector<StackFrame> stack_ty;
+  using stack_ty = std::vector<StackFrame>;
 
-private:
-  // unsupported, use copy constructor
-  ExecutionState &operator=(const ExecutionState &);
-
-public:
   // Execution - Control Flow specific
 
   /// @brief Pointer to instruction to be executed after the current
@@ -86,10 +81,13 @@ public:
 
   /// @brief Remember from which Basic Block control flow arrived
   /// (i.e. to select the right phi values)
-  unsigned incomingBBIndex;
+  std::uint32_t incomingBBIndex;
 
   // Overall state of the state - Data specific
 
+  /// @brief Exploration depth, i.e., number of times KLEE branched for this state
+  std::uint32_t depth;
+
   /// @brief Address space used by this state (e.g. Global and Heap)
   AddressSpace addressSpace;
 
@@ -101,9 +99,6 @@ public:
   /// @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;
@@ -112,18 +107,8 @@ public:
   /// 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;
+  std::map<const std::string *, std::set<std::uint32_t>> coveredLines;
 
   /// @brief Pointer to the process tree of the current state
   PTreeNode *ptreeNode;
@@ -136,24 +121,37 @@ public:
   /// @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;
+  /// @brief 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
+  /// @brief The numbers of times this state has run through Executor::stepInstruction
   std::uint64_t steppedInstructions;
 
-private:
-  ExecutionState() : ptreeNode(0) {}
+  /// @brief Counts how many instructions were executed since the last new
+  /// instruction was covered.
+  std::uint32_t instsSinceCovNew;
 
-public:
-  ExecutionState(KFunction *kf);
+  /// @brief Whether a new instruction was covered in this state
+  bool coveredNew;
 
+  /// @brief Disables forking for this state. Set by user code
+  bool forkDisabled;
+
+public:
+  // ctors
+  explicit 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);
-
+  explicit ExecutionState(const std::vector<ref<Expr>> &assumptions);
+  // copy ctor
   ExecutionState(const ExecutionState &state);
-
+  // no copy assignment, use copy constructor
+  ExecutionState &operator=(const ExecutionState &) = delete;
+  // no move ctor
+  ExecutionState(ExecutionState &&) noexcept = delete;
+  // no move assignment
+  ExecutionState& operator=(ExecutionState &&) noexcept = delete;
+  // dtor
   ~ExecutionState();
 
   ExecutionState *branch();
@@ -162,7 +160,7 @@ public:
   void popFrame();
 
   void addSymbolic(const MemoryObject *mo, const Array *array);
-  void addConstraint(ref<Expr> e) { constraints.addConstraint(e); }
+  void addConstraint(ref<Expr> e) { constraints.addConstraint(std::move(e)); }
 
   bool merge(const ExecutionState &b);
   void dumpStack(llvm::raw_ostream &out) const;