Change ExecutionState::symbolics to include both the MemoryObject and the

symbolic Array.


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73161 91177308-0d34-0410-b5e6-96231b3b80d8

2 files changed, 10 insertions, 16 deletions

diff --git a/include/klee/ExecutionState.h b/include/klee/ExecutionState.h
index 09ce2a4b..1d2df49a 100644
--- a/include/klee/ExecutionState.h
+++ b/include/klee/ExecutionState.h
@@ -23,6 +23,7 @@
 #include <vector>
 
 namespace klee {
+  class Array;
   class CallPathNode;
   class Cell;
   class KFunction;
@@ -126,7 +127,7 @@ public:
   /// ordered list of symbolics: used to generate test cases. 
   //
   // FIXME: Move to a shared list structure (not critical).
-  std::vector<const MemoryObject*> symbolics;
+  std::vector< std::pair<const MemoryObject*, const Array*> > symbolics;
 
   // Used by the checkpoint/rollback methods for fake objects.
   // FIXME: not freeing things on branch deletion.
@@ -155,8 +156,8 @@ public:
   void pushFrame(KInstIterator caller, KFunction *kf);
   void popFrame();
 
-  void addSymbolic(const MemoryObject *mo) { 
-    symbolics.push_back(mo);
+  void addSymbolic(const MemoryObject *mo, const Array *array) { 
+    symbolics.push_back(std::make_pair(mo, array));
   }
   void addConstraint(ref<Expr> e) { 
     constraints.addConstraint(e); 
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 4c5f9511..28e7111c 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -2941,7 +2941,7 @@ void Executor::executeMakeSymbolic(ExecutionState &state,
   ObjectState *os = bindObjectInState(state, mo, false);
   if (!replayOut) {
     os->makeSymbolic();
-    state.addSymbolic(mo);
+    state.addSymbolic(mo, os->updates.root);
     
     const Array *array = os->updates.root;
     std::map< ExecutionState*, std::vector<SeedInfo> >::iterator it = 
@@ -3149,10 +3149,8 @@ bool Executor::getSymbolicSolution(const ExecutionState &state,
 
   ExecutionState tmp(state);
   if (!NoPreferCex) {
-    for (std::vector<const MemoryObject*>::const_iterator 
-           it = state.symbolics.begin(), ie = state.symbolics.end(); 
-         it != ie; ++it) {
-      const MemoryObject *mo = *it;
+    for (unsigned i = 0; i != state.symbolics.size(); ++i) {
+      const MemoryObject *mo = state.symbolics[i].first;
       std::vector< ref<Expr> >::const_iterator pi = 
         mo->cexPreferences.begin(), pie = mo->cexPreferences.end();
       for (; pi != pie; ++pi) {
@@ -3169,7 +3167,7 @@ bool Executor::getSymbolicSolution(const ExecutionState &state,
   std::vector< std::vector<unsigned char> > values;
   std::vector<const Array*> objects;
   for (unsigned i = 0; i != state.symbolics.size(); ++i)
-    objects.push_back(state.symbolics[i]->array);
+    objects.push_back(state.symbolics[i].second);
   bool success = solver->getInitialValues(tmp, objects, values);
   solver->setTimeout(0);
   if (!success) {
@@ -3180,13 +3178,8 @@ bool Executor::getSymbolicSolution(const ExecutionState &state,
     return false;
   }
   
-  unsigned i = 0;
-  for (std::vector<const MemoryObject*>::const_iterator 
-         it = state.symbolics.begin(), ie = state.symbolics.end(); 
-       it != ie; ++it) {
-    res.push_back(std::make_pair((*it)->name, values[i]));
-    ++i;
-  }
+  for (unsigned i = 0; i != state.symbolics.size(); ++i)
+    res.push_back(std::make_pair(state.symbolics[i].first->name, values[i]));
   return true;
 }