add ExecutionState IDs

* add getID()/setID()
* use ExecutionStateIDCompare in Executor::states set
* output state id in .err files

4 files changed, 29 insertions, 7 deletions

diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index b3719295..7b600003 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -41,6 +41,10 @@ cl::opt<bool> DebugLogStateMerge(
 
 /***/
 
+std::uint32_t ExecutionState::nextID = 1;
+
+/***/
+
 StackFrame::StackFrame(KInstIterator _caller, KFunction *_kf)
   : caller(_caller), kf(_kf), callPathNode(0), 
     minDistToUncoveredOnReturn(0), varargs(0) {
@@ -75,6 +79,7 @@ ExecutionState::ExecutionState(KFunction *kf) :
     coveredNew(false),
     forkDisabled(false) {
   pushFrame(nullptr, kf);
+  setID();
 }
 
 ExecutionState::ExecutionState(const std::vector<ref<Expr>> &assumptions)
@@ -116,6 +121,7 @@ ExecutionState *ExecutionState::branch() {
   depth++;
 
   auto *falseState = new ExecutionState(*this);
+  falseState->setID();
   falseState->coveredNew = false;
   falseState->coveredLines.clear();
 
diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h
index 176ffef6..e7332472 100644
--- a/lib/Core/ExecutionState.h
+++ b/lib/Core/ExecutionState.h
@@ -131,6 +131,12 @@ public:
   /// instruction was covered.
   std::uint32_t instsSinceCovNew;
 
+  /// @brief the global state counter
+  static std::uint32_t nextID;
+
+  /// @brief the state id
+  std::uint32_t id {0};
+
   /// @brief Whether a new instruction was covered in this state
   bool coveredNew;
 
@@ -138,7 +144,7 @@ public:
   bool forkDisabled;
 
 public:
-  // ctors
+  // only to create the initial state
   explicit ExecutionState(KFunction *kf);
   // XXX total hack, just used to make a state so solver can
   // use on structure
@@ -164,6 +170,15 @@ public:
 
   bool merge(const ExecutionState &b);
   void dumpStack(llvm::raw_ostream &out) const;
+
+  std::uint32_t getID() const { return id; };
+  void setID() { id = nextID++; };
+};
+
+struct ExecutionStateIDCompare {
+  bool operator()(const ExecutionState *a, const ExecutionState *b) const {
+    return a->getID() < b->getID();
+  }
 };
 }
 
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 83409983..03deeda7 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -3178,11 +3178,12 @@ void Executor::terminateStateOnError(ExecutionState &state,
 
     std::string MsgString;
     llvm::raw_string_ostream msg(MsgString);
-    msg << "Error: " << message << "\n";
+    msg << "Error: " << message << '\n';
     if (ii.file != "") {
-      msg << "File: " << ii.file << "\n";
-      msg << "Line: " << ii.line << "\n";
-      msg << "assembly.ll line: " << ii.assemblyLine << "\n";
+      msg << "File: " << ii.file << '\n'
+          << "Line: " << ii.line << '\n'
+          << "assembly.ll line: " << ii.assemblyLine << '\n'
+          << "State: " << state.getID() << '\n';
     }
     msg << "Stack: \n";
     state.dumpStack(msg);
@@ -3813,7 +3814,7 @@ void Executor::runFunctionAsMain(Function *f,
   }
 
   ExecutionState *state = new ExecutionState(kmodule->functionMap[f]);
-  
+
   if (pathWriter) 
     state->pathOS = pathWriter->open();
   if (symPathWriter) 
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 2cb97d66..4ddbc98e 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -120,7 +120,7 @@ private:
   ExternalDispatcher *externalDispatcher;
   TimingSolver *solver;
   MemoryManager *memory;
-  std::set<ExecutionState*> states;
+  std::set<ExecutionState*, ExecutionStateIDCompare> states;
   StatsTracker *statsTracker;
   TreeStreamWriter *pathWriter, *symPathWriter;
   SpecialFunctionHandler *specialFunctionHandler;