[Core] Documentation and cleanup

* Removed unused member ShadowObjects in ExecutionState
* Added documentation of members and reorder according to categories

3 files changed, 100 insertions, 55 deletions

diff --git a/include/klee/ExecutionState.h b/include/klee/ExecutionState.h
index 97b700c1..eddf3d4a 100644
--- a/include/klee/ExecutionState.h
+++ b/include/klee/ExecutionState.h
@@ -23,14 +23,14 @@
 #include <vector>
 
 namespace klee {
-  class Array;
-  class CallPathNode;
-  struct Cell;
-  struct KFunction;
-  struct KInstruction;
-  class MemoryObject;
-  class PTreeNode;
-  struct InstructionInfo;
+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);
 
@@ -39,7 +39,7 @@ struct StackFrame {
   KFunction *kf;
   CallPathNode *callPathNode;
 
-  std::vector<const MemoryObject*> allocas;
+  std::vector<const MemoryObject *> allocas;
   Cell *locals;
 
   /// Minimum distance to an uncovered instruction once the function
@@ -61,56 +61,100 @@ struct StackFrame {
   ~StackFrame();
 };
 
+/// @brief ExecutionState representing the one state of execution
 class ExecutionState {
 public:
   typedef std::vector<StackFrame> stack_ty;
 
 private:
   // unsupported, use copy constructor
-  ExecutionState &operator=(const ExecutionState&); 
-  std::map< std::string, std::string > fnAliases;
+  ExecutionState &operator=(const ExecutionState &);
+
+  std::map<std::string, std::string> fnAliases;
 
 public:
-  bool fakeState;
-  unsigned depth;
-  
-  // pc - pointer to current instruction stream
-  KInstIterator pc, prevPC;
+  // Are we currently underconstrained?  Hack: value is size to make fake
+  // objects.
+  unsigned underConstrained;
+
+  /// Execution - Control Flow specific
+
+  /// @brief pointer to instruction to be executed next after the current
+  /// instruction (prevPc)
+  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 in seconds for this state
   mutable double queryCost;
+
+  /// @brief Weight assigned for importance of this state. Can be used for
+  /// searchers to decide
   double weight;
-  AddressSpace addressSpace;
-  TreeOStream pathOS, symPathOS;
+
+  /// @brief Counter how often KLEE branched for this state
+  unsigned depth;
+
+  /// @brief History of complete path: Represents branches taken to reach/create
+  /// this state
+  ///        Includes symbolic-based branches as well.
+  TreeOStream pathOS;
+
+  /// @brief History of symbolic path: Represents branches taken but only
+  /// symbolic ones.
+  TreeOStream symPathOS;
+
+  /// @brief Does not represent a real state just for patching purposes
+  bool fakeState;
+
+  /// @brief Counts how many instructions were executed since the last new
+  /// instruction was covered.
   unsigned instsSinceCovNew;
+
+  /// @brief Flag if new instruction was covered or not in this state
   bool coveredNew;
 
-  /// Disables forking, set by user code.
+  /// @brief Disables forking for this state. Set by user code.
   bool forkDisabled;
 
-  std::map<const std::string*, std::set<unsigned> > coveredLines;
+  /// @brief Set containing which lines in which files are covered by this state
+  std::map<const std::string *, std::set<unsigned> > coveredLines;
+
+  /// @brief Representing pointer to process tree of current state
   PTreeNode *ptreeNode;
 
-  /// ordered list of symbolics: used to generate test cases. 
+  /// ordered list of symbolics: used to generate test cases.
   //
   // FIXME: Move to a shared list structure (not critical).
-  std::vector< std::pair<const MemoryObject*, const Array*> > symbolics;
+  std::vector<std::pair<const MemoryObject *, const Array *> > symbolics;
 
-  /// Set of used array names.  Used to avoid collisions.
+  /// @brief Set of used array names for this state.  Used to avoid collisions.
   std::set<std::string> arrayNames;
 
-  // Used by the checkpoint/rollback methods for fake objects.
-  // FIXME: not freeing things on branch deletion.
-  MemoryMap shadowObjects;
-
-  unsigned incomingBBIndex;
-
   std::string getFnAlias(std::string fn);
   void addFnAlias(std::string old_fn, std::string new_fn);
   void removeFnAlias(std::string fn);
-  
+
 private:
-  ExecutionState() : fakeState(false), ptreeNode(0) {}
+  ExecutionState() : underConstrained(0), fakeState(false), ptreeNode(0) {}
 
 public:
   ExecutionState(KFunction *kf);
@@ -119,24 +163,21 @@ public:
   // use on structure
   ExecutionState(const std::vector<ref<Expr> > &assumptions);
 
-  ExecutionState(const ExecutionState& state);
+  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); 
-  }
+  void addConstraint(ref<Expr> e) { constraints.addConstraint(e); }
 
   bool merge(const ExecutionState &b);
   void dumpStack(llvm::raw_ostream &out) const;
 };
-
 }
 
 #endif
diff --git a/include/klee/Internal/Module/KInstruction.h b/include/klee/Internal/Module/KInstruction.h
index fc86070b..62f514ff 100644
--- a/include/klee/Internal/Module/KInstruction.h
+++ b/include/klee/Internal/Module/KInstruction.h
@@ -50,7 +50,7 @@ namespace klee {
     std::vector< std::pair<unsigned, uint64_t> > indices;
 
     /// offset - A constant offset to add to the pointer operand to execute the
-    /// insturction.
+    /// instruction.
     uint64_t offset;
   };
 }
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index 5d32c936..1dc08624 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -66,13 +66,16 @@ StackFrame::~StackFrame() {
 
 /***/
 
-ExecutionState::ExecutionState(KFunction *kf) 
-  : fakeState(false),
-    depth(0),
+ExecutionState::ExecutionState(KFunction *kf) :
+    underConstrained(0),
     pc(kf->instructions),
     prevPC(pc),
+
     queryCost(0.), 
     weight(1),
+    depth(0),
+
+    fakeState(false),
     instsSinceCovNew(0),
     coveredNew(false),
     forkDisabled(false),
@@ -80,12 +83,9 @@ ExecutionState::ExecutionState(KFunction *kf)
   pushFrame(0, kf);
 }
 
-ExecutionState::ExecutionState(const std::vector<ref<Expr> > &assumptions) 
-  : fakeState(true),
-    constraints(assumptions),
-    queryCost(0.),
-    ptreeNode(0) {
-}
+ExecutionState::ExecutionState(const std::vector<ref<Expr> > &assumptions)
+    : underConstrained(0), constraints(assumptions), queryCost(0.),
+      fakeState(true), ptreeNode(0) {}
 
 ExecutionState::~ExecutionState() {
   for (unsigned int i=0; i<symbolics.size(); i++)
@@ -100,28 +100,32 @@ ExecutionState::~ExecutionState() {
   while (!stack.empty()) popFrame();
 }
 
-ExecutionState::ExecutionState(const ExecutionState& state)
-  : fnAliases(state.fnAliases),
-    fakeState(state.fakeState),
-    depth(state.depth),
+ExecutionState::ExecutionState(const ExecutionState& state):
+    fnAliases(state.fnAliases),
+    underConstrained(state.underConstrained),
     pc(state.pc),
     prevPC(state.prevPC),
     stack(state.stack),
+    incomingBBIndex(state.incomingBBIndex),
+
+    addressSpace(state.addressSpace),
     constraints(state.constraints),
+
     queryCost(state.queryCost),
     weight(state.weight),
-    addressSpace(state.addressSpace),
+    depth(state.depth),
+
     pathOS(state.pathOS),
     symPathOS(state.symPathOS),
+
+    fakeState(state.fakeState),
     instsSinceCovNew(state.instsSinceCovNew),
     coveredNew(state.coveredNew),
     forkDisabled(state.forkDisabled),
     coveredLines(state.coveredLines),
     ptreeNode(state.ptreeNode),
     symbolics(state.symbolics),
-    arrayNames(state.arrayNames),
-    shadowObjects(state.shadowObjects),
-    incomingBBIndex(state.incomingBBIndex)
+    arrayNames(state.arrayNames)
 {
   for (unsigned int i=0; i<symbolics.size(); i++)
     symbolics[i].first->refCount++;