about summary refs log tree commit diff homepage
path: root/lib/Core
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Core')
-rw-r--r--lib/Core/AddressSpace.cpp64
-rw-r--r--lib/Core/AddressSpace.h8
-rw-r--r--lib/Core/ExecutionState.cpp6
-rw-r--r--lib/Core/Memory.cpp35
-rw-r--r--lib/Core/Memory.h6
-rw-r--r--lib/Core/ObjectHolder.h32
6 files changed, 51 insertions, 100 deletions
diff --git a/lib/Core/AddressSpace.cpp b/lib/Core/AddressSpace.cpp
index 12e74c77..e006d4d0 100644
--- a/lib/Core/AddressSpace.cpp
+++ b/lib/Core/AddressSpace.cpp
@@ -30,23 +30,23 @@ void AddressSpace::unbindObject(const MemoryObject *mo) {
 }
 
 const ObjectState *AddressSpace::findObject(const MemoryObject *mo) const {
-  const MemoryMap::value_type *res = objects.lookup(mo);
-  
-  return res ? res->second : 0;
+  const auto res = objects.lookup(mo);
+  return res ? res->second.get() : nullptr;
 }
 
 ObjectState *AddressSpace::getWriteable(const MemoryObject *mo,
                                         const ObjectState *os) {
   assert(!os->readOnly);
 
-  if (cowKey==os->copyOnWriteOwner) {
+  // If this address space owns they object, return it
+  if (cowKey == os->copyOnWriteOwner)
     return const_cast<ObjectState*>(os);
-  } else {
-    ObjectState *n = new ObjectState(*os);
-    n->copyOnWriteOwner = cowKey;
-    objects = objects.replace(std::make_pair(mo, n));
-    return n;    
-  }
+
+  // Add a copy of this object state that can be updated
+  ref<ObjectState> newObjectState(new ObjectState(*os));
+  newObjectState->copyOnWriteOwner = cowKey;
+  objects = objects.replace(std::make_pair(mo, newObjectState));
+  return newObjectState.get();
 }
 
 /// 
@@ -56,13 +56,14 @@ bool AddressSpace::resolveOne(const ref<ConstantExpr> &addr,
   uint64_t address = addr->getZExtValue();
   MemoryObject hack(address);
 
-  if (const MemoryMap::value_type *res = objects.lookup_previous(&hack)) {
-    const MemoryObject *mo = res->first;
+  if (const auto res = objects.lookup_previous(&hack)) {
+    const auto &mo = res->first;
     // Check if the provided address is between start and end of the object
     // [mo->address, mo->address + mo->size) or the object is a 0-sized object.
     if ((mo->size==0 && address==mo->address) ||
         (address - mo->address < mo->size)) {
-      result = *res;
+      result.first = res->first;
+      result.second = res->second.get();
       return true;
     }
   }
@@ -88,12 +89,13 @@ bool AddressSpace::resolveOne(ExecutionState &state,
       return false;
     uint64_t example = cex->getZExtValue();
     MemoryObject hack(example);
-    const MemoryMap::value_type *res = objects.lookup_previous(&hack);
-    
+    const auto res = objects.lookup_previous(&hack);
+
     if (res) {
       const MemoryObject *mo = res->first;
       if (example - mo->address < mo->size) {
-        result = *res;
+        result.first = res->first;
+        result.second = res->second.get();
         success = true;
         return true;
       }
@@ -108,14 +110,15 @@ bool AddressSpace::resolveOne(ExecutionState &state,
     MemoryMap::iterator start = oi;
     while (oi!=begin) {
       --oi;
-      const MemoryObject *mo = oi->first;
-        
+      const auto &mo = oi->first;
+
       bool mayBeTrue;
       if (!solver->mayBeTrue(state, 
                              mo->getBoundsCheckPointer(address), mayBeTrue))
         return false;
       if (mayBeTrue) {
-        result = *oi;
+        result.first = oi->first;
+        result.second = oi->second.get();
         success = true;
         return true;
       } else {
@@ -131,7 +134,7 @@ bool AddressSpace::resolveOne(ExecutionState &state,
 
     // search forwards
     for (oi=start; oi!=end; ++oi) {
-      const MemoryObject *mo = oi->first;
+      const auto &mo = oi->first;
 
       bool mustBeTrue;
       if (!solver->mustBeTrue(state, 
@@ -148,7 +151,8 @@ bool AddressSpace::resolveOne(ExecutionState &state,
                                mayBeTrue))
           return false;
         if (mayBeTrue) {
-          result = *oi;
+          result.first = oi->first;
+          result.second = oi->second.get();
           success = true;
           return true;
         }
@@ -240,8 +244,10 @@ bool AddressSpace::resolve(ExecutionState &state, TimingSolver *solver,
       if (timeout && timeout < timer.delta())
         return true;
 
+      auto op = std::make_pair<>(mo, oi->second.get());
+
       int incomplete =
-          checkPointerInObject(state, solver, p, *oi, rl, maxResolutions);
+          checkPointerInObject(state, solver, p, op, rl, maxResolutions);
       if (incomplete != 2)
         return incomplete ? true : false;
 
@@ -265,9 +271,10 @@ bool AddressSpace::resolve(ExecutionState &state, TimingSolver *solver,
         return true;
       if (mustBeTrue)
         break;
+      auto op = std::make_pair<>(mo, oi->second.get());
 
       int incomplete =
-          checkPointerInObject(state, solver, p, *oi, rl, maxResolutions);
+          checkPointerInObject(state, solver, p, op, rl, maxResolutions);
       if (incomplete != 2)
         return incomplete ? true : false;
     }
@@ -288,7 +295,7 @@ void AddressSpace::copyOutConcretes() {
     const MemoryObject *mo = it->first;
 
     if (!mo->isUserSpecified) {
-      ObjectState *os = it->second;
+      const auto &os = it->second;
       auto address = reinterpret_cast<std::uint8_t*>(mo->address);
 
       if (!os->readOnly)
@@ -298,14 +305,13 @@ void AddressSpace::copyOutConcretes() {
 }
 
 bool AddressSpace::copyInConcretes() {
-  for (MemoryMap::iterator it = objects.begin(), ie = objects.end(); 
-       it != ie; ++it) {
-    const MemoryObject *mo = it->first;
+  for (auto &obj : objects) {
+    const MemoryObject *mo = obj.first;
 
     if (!mo->isUserSpecified) {
-      const ObjectState *os = it->second;
+      const auto &os = obj.second;
 
-      if (!copyInConcrete(mo, os, mo->address))
+      if (!copyInConcrete(mo, os.get(), mo->address))
         return false;
     }
   }
diff --git a/lib/Core/AddressSpace.h b/lib/Core/AddressSpace.h
index 9e7e414a..10310a1e 100644
--- a/lib/Core/AddressSpace.h
+++ b/lib/Core/AddressSpace.h
@@ -10,8 +10,7 @@
 #ifndef KLEE_ADDRESSSPACE_H
 #define KLEE_ADDRESSSPACE_H
 
-#include "ObjectHolder.h"
-
+#include "Memory.h"
 #include "klee/Expr/Expr.h"
 #include "klee/Internal/ADT/ImmutableMap.h"
 #include "klee/Internal/System/Time.h"
@@ -31,8 +30,9 @@ namespace klee {
   struct MemoryObjectLT {
     bool operator()(const MemoryObject *a, const MemoryObject *b) const;
   };
-  
-  typedef ImmutableMap<const MemoryObject*, ObjectHolder, MemoryObjectLT> MemoryMap;
+
+  typedef ImmutableMap<const MemoryObject *, ref<ObjectState>, MemoryObjectLT>
+      MemoryMap;
 
   class AddressSpace {
   private:
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index 60715b33..78aa8f67 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -166,9 +166,9 @@ llvm::raw_ostream &klee::operator<<(llvm::raw_ostream &os, const MemoryMap &mm)
   MemoryMap::iterator it = mm.begin();
   MemoryMap::iterator ie = mm.end();
   if (it!=ie) {
-    os << "MO" << it->first->id << ":" << it->second;
+    os << "MO" << it->first->id << ":" << it->second.get();
     for (++it; it!=ie; ++it)
-      os << ", MO" << it->first->id << ":" << it->second;
+      os << ", MO" << it->first->id << ":" << it->second.get();
   }
   os << "}";
   return os;
@@ -265,7 +265,7 @@ bool ExecutionState::merge(const ExecutionState &b) {
       }
       return false;
     }
-    if (ai->second != bi->second) {
+    if (ai->second.get() != bi->second.get()) {
       if (DebugLogStateMerge)
         llvm::errs() << "\t\tmutated: " << ai->first->id << "\n";
       mutated.insert(ai->first);
diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp
index c7e7a928..37e6646b 100644
--- a/lib/Core/Memory.cpp
+++ b/lib/Core/Memory.cpp
@@ -11,7 +11,6 @@
 
 #include "Context.h"
 #include "MemoryManager.h"
-#include "ObjectHolder.h"
 
 #include "klee/Expr/ArrayCache.h"
 #include "klee/Expr/Expr.h"
@@ -42,27 +41,6 @@ namespace {
 
 /***/
 
-ObjectHolder::ObjectHolder(const ObjectHolder &b) : os(b.os) { 
-  if (os) ++os->refCount; 
-}
-
-ObjectHolder::ObjectHolder(ObjectState *_os) : os(_os) { 
-  if (os) ++os->refCount; 
-}
-
-ObjectHolder::~ObjectHolder() { 
-  if (os && --os->refCount==0) delete os; 
-}
-  
-ObjectHolder &ObjectHolder::operator=(const ObjectHolder &b) {
-  if (b.os) ++b.os->refCount;
-  if (os && --os->refCount==0) delete os;
-  os = b.os;
-  return *this;
-}
-
-/***/
-
 int MemoryObject::counter = 0;
 
 MemoryObject::~MemoryObject() {
@@ -96,7 +74,6 @@ void MemoryObject::getAllocInfo(std::string &result) const {
 
 ObjectState::ObjectState(const MemoryObject *mo)
   : copyOnWriteOwner(0),
-    refCount(0),
     object(mo),
     concreteStore(new uint8_t[mo->size]),
     concreteMask(0),
@@ -118,7 +95,6 @@ ObjectState::ObjectState(const MemoryObject *mo)
 
 ObjectState::ObjectState(const MemoryObject *mo, const Array *array)
   : copyOnWriteOwner(0),
-    refCount(0),
     object(mo),
     concreteStore(new uint8_t[mo->size]),
     concreteMask(0),
@@ -134,7 +110,6 @@ ObjectState::ObjectState(const MemoryObject *mo, const Array *array)
 
 ObjectState::ObjectState(const ObjectState &os) 
   : copyOnWriteOwner(0),
-    refCount(0),
     object(os.object),
     concreteStore(new uint8_t[os.size]),
     concreteMask(os.concreteMask ? new BitArray(*os.concreteMask, os.size) : 0),
@@ -188,10 +163,10 @@ const UpdateList &ObjectState::getUpdates() const {
     // FIXME: We should be able to do this more efficiently, we just need to be
     // careful to get the interaction with the cache right. In particular we
     // should avoid creating UpdateNode instances we never use.
-    unsigned NumWrites = updates.head ? updates.head->getSize() : 0;
+    unsigned NumWrites = updates.head.isNull() ? 0 : updates.head->getSize();
     std::vector< std::pair< ref<Expr>, ref<Expr> > > Writes(NumWrites);
-    const UpdateNode *un = updates.head;
-    for (unsigned i = NumWrites; i != 0; un = un->next) {
+    const auto *un = updates.head.get();
+    for (unsigned i = NumWrites; i != 0; un = un->next.get()) {
       --i;
       Writes[i] = std::make_pair(un->index, un->value);
     }
@@ -257,7 +232,7 @@ void ObjectState::makeConcrete() {
 }
 
 void ObjectState::makeSymbolic() {
-  assert(!updates.head &&
+  assert(updates.head.isNull() &&
          "XXX makeSymbolic of objects with symbolic values is unsupported");
 
   // XXX simplify this, can just delete various arrays I guess
@@ -612,7 +587,7 @@ void ObjectState::print() const {
   }
 
   llvm::errs() << "\tUpdates:\n";
-  for (const UpdateNode *un=updates.head; un; un=un->next) {
+  for (const auto *un = updates.head.get(); un; un = un->next.get()) {
     llvm::errs() << "\t\t[" << un->index << "] = " << un->value << "\n";
   }
 }
diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h
index dfda433c..e4260c55 100644
--- a/lib/Core/Memory.h
+++ b/lib/Core/Memory.h
@@ -148,10 +148,12 @@ public:
 class ObjectState {
 private:
   friend class AddressSpace;
+  friend class ref<ObjectState>;
+
   unsigned copyOnWriteOwner; // exclusively for AddressSpace
 
-  friend class ObjectHolder;
-  unsigned refCount;
+  /// @brief Required by klee::ref-managed objects
+  class ReferenceCounter _refCount;
 
   const MemoryObject *object;
 
diff --git a/lib/Core/ObjectHolder.h b/lib/Core/ObjectHolder.h
deleted file mode 100644
index cd6c6281..00000000
--- a/lib/Core/ObjectHolder.h
+++ /dev/null
@@ -1,32 +0,0 @@
-//===-- ObjectHolder.h ------------------------------------------*- C++ -*-===//
-//
-//                     The KLEE Symbolic Virtual Machine
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-
-#ifndef KLEE_OBJECTHOLDER_H
-#define KLEE_OBJECTHOLDER_H
-
-namespace klee {
-  class ObjectState;
-
-  class ObjectHolder {
-    ObjectState *os;
-    
-  public:
-    ObjectHolder() : os(0) {}
-    ObjectHolder(ObjectState *_os);
-    ObjectHolder(const ObjectHolder &b);
-    ~ObjectHolder(); 
-    
-    ObjectHolder &operator=(const ObjectHolder &b);
-
-    operator class ObjectState *() { return os; }
-    operator class ObjectState *() const { return (ObjectState*) os; }
-  };
-}
-
-#endif /* KLEE_OBJECTHOLDER_H */