1 files changed, 45 insertions, 42 deletions

diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp
index 86b06701..f2f679ad 100644
--- a/lib/Core/Memory.cpp
+++ b/lib/Core/Memory.cpp
@@ -77,10 +77,10 @@ ObjectState::ObjectState(const MemoryObject *mo)
   : copyOnWriteOwner(0),
     object(mo),
     concreteStore(new uint8_t[mo->size]),
-    concreteMask(0),
-    flushMask(0),
-    knownSymbolics(0),
-    updates(0, 0),
+    concreteMask(nullptr),
+    knownSymbolics(nullptr),
+    unflushedMask(nullptr),
+    updates(nullptr, nullptr),
     size(mo->size),
     readOnly(false) {
   if (!UseConstantArrays) {
@@ -97,10 +97,10 @@ ObjectState::ObjectState(const MemoryObject *mo, const Array *array)
   : copyOnWriteOwner(0),
     object(mo),
     concreteStore(new uint8_t[mo->size]),
-    concreteMask(0),
-    flushMask(0),
-    knownSymbolics(0),
-    updates(array, 0),
+    concreteMask(nullptr),
+    knownSymbolics(nullptr),
+    unflushedMask(nullptr),
+    updates(array, nullptr),
     size(mo->size),
     readOnly(false) {
   makeSymbolic();
@@ -111,9 +111,9 @@ ObjectState::ObjectState(const ObjectState &os)
   : copyOnWriteOwner(0),
     object(os.object),
     concreteStore(new uint8_t[os.size]),
-    concreteMask(os.concreteMask ? new BitArray(*os.concreteMask, os.size) : 0),
-    flushMask(os.flushMask ? new BitArray(*os.flushMask, os.size) : 0),
-    knownSymbolics(0),
+    concreteMask(os.concreteMask ? new BitArray(*os.concreteMask, os.size) : nullptr),
+    knownSymbolics(nullptr),
+    unflushedMask(os.unflushedMask ? new BitArray(*os.unflushedMask, os.size) : nullptr),
     updates(os.updates),
     size(os.size),
     readOnly(false) {
@@ -129,7 +129,7 @@ ObjectState::ObjectState(const ObjectState &os)
 
 ObjectState::~ObjectState() {
   delete concreteMask;
-  delete flushMask;
+  delete unflushedMask;
   delete[] knownSymbolics;
   delete[] concreteStore;
 }
@@ -211,11 +211,11 @@ void ObjectState::flushToConcreteStore(TimingSolver *solver,
 
 void ObjectState::makeConcrete() {
   delete concreteMask;
-  delete flushMask;
+  delete unflushedMask;
   delete[] knownSymbolics;
-  concreteMask = 0;
-  flushMask = 0;
-  knownSymbolics = 0;
+  concreteMask = nullptr;
+  unflushedMask = nullptr;
+  knownSymbolics = nullptr;
 }
 
 void ObjectState::makeSymbolic() {
@@ -248,7 +248,7 @@ Cache Invariants
 --
 isByteKnownSymbolic(i) => !isByteConcrete(i)
 isByteConcrete(i) => !isByteKnownSymbolic(i)
-!isByteFlushed(i) => (isByteConcrete(i) || isByteKnownSymbolic(i))
+isByteUnflushed(i) => (isByteConcrete(i) || isByteKnownSymbolic(i))
  */
 
 void ObjectState::fastRangeCheckOffset(ref<Expr> offset,
@@ -258,44 +258,47 @@ void ObjectState::fastRangeCheckOffset(ref<Expr> offset,
   *size_r = size;
 }
 
-void ObjectState::flushRangeForRead(unsigned rangeBase, 
+void ObjectState::flushRangeForRead(unsigned rangeBase,
                                     unsigned rangeSize) const {
-  if (!flushMask) flushMask = new BitArray(size, true);
- 
-  for (unsigned offset=rangeBase; offset<rangeBase+rangeSize; offset++) {
-    if (!isByteFlushed(offset)) {
+  if (!unflushedMask)
+    unflushedMask = new BitArray(size, true);
+
+  for (unsigned offset = rangeBase; offset < rangeBase + rangeSize; offset++) {
+    if (isByteUnflushed(offset)) {
       if (isByteConcrete(offset)) {
         updates.extend(ConstantExpr::create(offset, Expr::Int32),
                        ConstantExpr::create(concreteStore[offset], Expr::Int8));
       } else {
-        assert(isByteKnownSymbolic(offset) && "invalid bit set in flushMask");
+        assert(isByteKnownSymbolic(offset) &&
+               "invalid bit set in unflushedMask");
         updates.extend(ConstantExpr::create(offset, Expr::Int32),
                        knownSymbolics[offset]);
       }
 
-      flushMask->unset(offset);
+      unflushedMask->unset(offset);
     }
-  } 
+  }
 }
 
-void ObjectState::flushRangeForWrite(unsigned rangeBase, 
-                                     unsigned rangeSize) {
-  if (!flushMask) flushMask = new BitArray(size, true);
+void ObjectState::flushRangeForWrite(unsigned rangeBase, unsigned rangeSize) {
+  if (!unflushedMask)
+    unflushedMask = new BitArray(size, true);
 
-  for (unsigned offset=rangeBase; offset<rangeBase+rangeSize; offset++) {
-    if (!isByteFlushed(offset)) {
+  for (unsigned offset = rangeBase; offset < rangeBase + rangeSize; offset++) {
+    if (isByteUnflushed(offset)) {
       if (isByteConcrete(offset)) {
         updates.extend(ConstantExpr::create(offset, Expr::Int32),
                        ConstantExpr::create(concreteStore[offset], Expr::Int8));
         markByteSymbolic(offset);
       } else {
-        assert(isByteKnownSymbolic(offset) && "invalid bit set in flushMask");
+        assert(isByteKnownSymbolic(offset) &&
+               "invalid bit set in unflushedMask");
         updates.extend(ConstantExpr::create(offset, Expr::Int32),
                        knownSymbolics[offset]);
         setKnownSymbolic(offset, 0);
       }
 
-      flushMask->unset(offset);
+      unflushedMask->unset(offset);
     } else {
       // flushed bytes that are written over still need
       // to be marked out
@@ -305,15 +308,15 @@ void ObjectState::flushRangeForWrite(unsigned rangeBase,
         setKnownSymbolic(offset, 0);
       }
     }
-  } 
+  }
 }
 
 bool ObjectState::isByteConcrete(unsigned offset) const {
   return !concreteMask || concreteMask->get(offset);
 }
 
-bool ObjectState::isByteFlushed(unsigned offset) const {
-  return flushMask && !flushMask->get(offset);
+bool ObjectState::isByteUnflushed(unsigned offset) const {
+  return !unflushedMask || unflushedMask->get(offset);
 }
 
 bool ObjectState::isByteKnownSymbolic(unsigned offset) const {
@@ -332,15 +335,15 @@ void ObjectState::markByteSymbolic(unsigned offset) {
 }
 
 void ObjectState::markByteUnflushed(unsigned offset) {
-  if (flushMask)
-    flushMask->set(offset);
+  if (unflushedMask)
+    unflushedMask->set(offset);
 }
 
 void ObjectState::markByteFlushed(unsigned offset) {
-  if (!flushMask) {
-    flushMask = new BitArray(size, false);
+  if (!unflushedMask) {
+    unflushedMask = new BitArray(size, false);
   } else {
-    flushMask->unset(offset);
+    unflushedMask->unset(offset);
   }
 }
 
@@ -364,7 +367,7 @@ ref<Expr> ObjectState::read8(unsigned offset) const {
   } else if (isByteKnownSymbolic(offset)) {
     return knownSymbolics[offset];
   } else {
-    assert(isByteFlushed(offset) && "unflushed byte without cache value");
+    assert(!isByteUnflushed(offset) && "unflushed byte without cache value");
     
     return ReadExpr::create(getUpdates(), 
                             ConstantExpr::create(offset, Expr::Int32));
@@ -568,7 +571,7 @@ void ObjectState::print() const {
     llvm::errs() << "\t\t["<<i<<"]"
                << " concrete? " << isByteConcrete(i)
                << " known-sym? " << isByteKnownSymbolic(i)
-               << " flushed? " << isByteFlushed(i) << " = ";
+               << " unflushed? " << isByteUnflushed(i) << " = ";
     ref<Expr> e = read8(i);
     llvm::errs() << e << "\n";
   }