Comment the code dealing with un/flushed bytes, and resolve old naming issue by renaming flushMask to unflushedMask

2 files changed, 62 insertions, 50 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";
   }
diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h
index d5189df5..7e1f097a 100644
--- a/lib/Core/Memory.h
+++ b/lib/Core/Memory.h
@@ -172,16 +172,20 @@ private:
 
   ref<const MemoryObject> object;
 
+  /// @brief Holds all known concrete bytes
   uint8_t *concreteStore;
 
-  // XXX cleanup name of flushMask (its backwards or something)
+  /// @brief concreteMask[byte] is set if byte is known to be concrete
   BitArray *concreteMask;
 
-  // mutable because may need flushed during read of const
-  mutable BitArray *flushMask;
-
+  /// knownSymbolics[byte] holds the symbolic expression for byte,
+  /// if byte is known to be symbolic
   ref<Expr> *knownSymbolics;
 
+  /// unflushedMask[byte] is set if byte is unflushed
+  /// mutable because may need flushed during read of const
+  mutable BitArray *unflushedMask;
+
   // mutable because we may need flush during read of const
   mutable UpdateList updates;
 
@@ -207,16 +211,16 @@ public:
 
   void setReadOnly(bool ro) { readOnly = ro; }
 
-  // make contents all concrete and zero
+  /// Make contents all concrete and zero
   void initializeToZero();
-  // make contents all concrete and random
+
+  /// Make contents all concrete and random
   void initializeToRandom();
 
   ref<Expr> read(ref<Expr> offset, Expr::Width width) const;
   ref<Expr> read(unsigned offset, Expr::Width width) const;
   ref<Expr> read8(unsigned offset) const;
 
-  // return bytes written.
   void write(unsigned offset, ref<Expr> value);
   void write(ref<Expr> offset, ref<Expr> value);
 
@@ -249,10 +253,15 @@ private:
   void flushRangeForRead(unsigned rangeBase, unsigned rangeSize) const;
   void flushRangeForWrite(unsigned rangeBase, unsigned rangeSize);
 
+  /// isByteConcrete ==> !isByteKnownSymbolic
   bool isByteConcrete(unsigned offset) const;
-  bool isByteFlushed(unsigned offset) const;
+
+  /// isByteKnownSymbolic ==> !isByteConcrete
   bool isByteKnownSymbolic(unsigned offset) const;
 
+  /// isByteUnflushed(i) => (isByteConcrete(i) || isByteKnownSymbolic(i))
+  bool isByteUnflushed(unsigned offset) const;
+
   void markByteConcrete(unsigned offset);
   void markByteSymbolic(unsigned offset);
   void markByteFlushed(unsigned offset);