Create new ObjectState constructor for explicitly creating symbolic objects.

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

4 files changed, 53 insertions, 27 deletions

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 63d21c6e..30c30928 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -2627,9 +2627,11 @@ ref<Expr> Executor::replaceReadWithSymbolic(ExecutionState &state,
   return res;
 }
 
-ObjectState *Executor::bindObjectInState(ExecutionState &state, const MemoryObject *mo,
-                                         bool isLocal) {
-  ObjectState *os = new ObjectState(mo, mo->size);
+ObjectState *Executor::bindObjectInState(ExecutionState &state, 
+                                         const MemoryObject *mo,
+                                         bool isLocal,
+                                         const Array *array) {
+  ObjectState *os = array ? new ObjectState(mo, array) : new ObjectState(mo);
   state.addressSpace.bindObject(mo, os);
 
   // Its possible that multiple bindings of the same mo in the state
@@ -2945,15 +2947,14 @@ void Executor::executeMemoryOperation(ExecutionState &state,
 
 void Executor::executeMakeSymbolic(ExecutionState &state, 
                                    const MemoryObject *mo) {
-  // make a new one and rebind, we use bind here because we want to
-  // create a flat out new state, not a copy. although I'm not really
-  // sure it matters.
-  ObjectState *os = bindObjectInState(state, mo, false);
+  // Create a new object state for the memory object (instead of a copy).
   if (!replayOut) {
-    os->makeSymbolic();
+    static unsigned id = 0;
+    const Array *array = new Array("arr" + llvm::utostr(++id),
+                                   mo->size);
+    ObjectState *os = bindObjectInState(state, mo, false, array);
     state.addSymbolic(mo, os->updates.root);
     
-    const Array *array = os->updates.root;
     std::map< ExecutionState*, std::vector<SeedInfo> >::iterator it = 
       seedMap.find(&state);
     if (it!=seedMap.end()) { // In seed mode we need to add this as a
@@ -2961,8 +2962,7 @@ void Executor::executeMakeSymbolic(ExecutionState &state,
       for (std::vector<SeedInfo>::iterator siit = it->second.begin(), 
              siie = it->second.end(); siit != siie; ++siit) {
         SeedInfo &si = *siit;
-        KTestObject *obj = si.getNextInput(mo,
-                                          NamedSeedMatching);
+        KTestObject *obj = si.getNextInput(mo, NamedSeedMatching);
 
         if (!obj) {
           if (ZeroSeedExtension) {
@@ -3002,6 +3002,7 @@ void Executor::executeMakeSymbolic(ExecutionState &state,
       }
     }
   } else {
+    ObjectState *os = bindObjectInState(state, mo, false);
     if (replayPosition >= replayOut->numObjects) {
       terminateStateOnError(state, "replay count mismatch", "user.err");
     } else {
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 013d3bb8..4dd89f2a 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -42,6 +42,7 @@ namespace llvm {
 }
 
 namespace klee {  
+  class Array;
   class Cell;
   class ExecutionState;
   class ExternalDispatcher;
@@ -198,7 +199,7 @@ private:
                             std::vector< ref<Expr> > &arguments);
 
   ObjectState *bindObjectInState(ExecutionState &state, const MemoryObject *mo,
-                                 bool isLocal);
+                                 bool isLocal, const Array *array = 0);
 
   /// Resolve a pointer to the memory objects it could point to the
   /// start of, forking execution when necessary and generating errors
diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp
index 513c2177..04f68737 100644
--- a/lib/Core/Memory.cpp
+++ b/lib/Core/Memory.cpp
@@ -83,18 +83,37 @@ void MemoryObject::getAllocInfo(std::string &result) const {
 
 /***/
 
-ObjectState::ObjectState(const MemoryObject *mo, unsigned _size)
+ObjectState::ObjectState(const MemoryObject *mo)
   : copyOnWriteOwner(0),
     refCount(0),
     object(mo),
-    concreteStore(new uint8_t[_size]),
+    concreteStore(new uint8_t[mo->size]),
     concreteMask(0),
     flushMask(0),
     knownSymbolics(0),
-    size(_size),
-    // FIXME: Leaked!
-    updates(new Array("arr" + llvm::utostr(mo->id), _size), 0),
+    size(mo->size),
+    updates(0, 0),
     readOnly(false) {
+  // FIXME: Leaked.
+  static unsigned id = 0;
+  const Array *array = new Array("tmp_arr" + llvm::utostr(++id), 
+                                 size);
+  updates = UpdateList(array, 0);
+}
+
+
+ObjectState::ObjectState(const MemoryObject *mo, const Array *array)
+  : copyOnWriteOwner(0),
+    refCount(0),
+    object(mo),
+    concreteStore(new uint8_t[mo->size]),
+    concreteMask(0),
+    flushMask(0),
+    knownSymbolics(0),
+    size(mo->size),
+    updates(array, 0),
+    readOnly(false) {
+  makeSymbolic();
 }
 
 ObjectState::ObjectState(const ObjectState &os) 
diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h
index 565572be..85f83ee1 100644
--- a/lib/Core/Memory.h
+++ b/lib/Core/Memory.h
@@ -160,9 +160,15 @@ public:
   bool readOnly;
 
 public:
-  // initial contents are undefined but concrete, it is the creators
-  // responsibility to initialize the object contents appropriate
-  ObjectState(const MemoryObject *mo, unsigned size);
+  /// Create a new object state for the given memory object with concrete
+  /// contents. The initial contents are undefined, it is the callers
+  /// responsibility to initialize the object contents appropriately.
+  ObjectState(const MemoryObject *mo);
+
+  /// Create a new object state for the given memory object with symbolic
+  /// contents.
+  ObjectState(const MemoryObject *mo, const Array *array);
+
   ObjectState(const ObjectState &os);
   ~ObjectState();
 
@@ -170,11 +176,6 @@ public:
 
   void setReadOnly(bool ro) { readOnly = ro; }
 
-  // make all bytes are concrete with undefined values
-  void makeConcrete();
-
-  void makeSymbolic();
-
   // make contents all concrete and zero
   void initializeToZero();
   // make contents all concrete and random
@@ -198,6 +199,10 @@ public:
   void write64(unsigned offset, uint64_t value);
 
 private:
+  void makeConcrete();
+
+  void makeSymbolic();
+
   ref<Expr> read1(ref<Expr> offset) const;
   ref<Expr> read8(ref<Expr> offset) const;
   ref<Expr> read16(ref<Expr> offset) const;
@@ -215,8 +220,8 @@ private:
   void write64(unsigned offset, ref<Expr> value);
   void write64(ref<Expr> offset, ref<Expr> value);
 
-  
-  void fastRangeCheckOffset(ref<Expr> offset, unsigned *base_r, unsigned *size_r) const;
+  void fastRangeCheckOffset(ref<Expr> offset, unsigned *base_r, 
+                            unsigned *size_r) const;
   void flushRangeForRead(unsigned rangeBase, unsigned rangeSize) const;
   void flushRangeForWrite(unsigned rangeBase, unsigned rangeSize);