From e2abd854b8267dadd2399b70d1cda9a6acd6d737 Mon Sep 17 00:00:00 2001
From: Cristian Cadar <c.cadar@imperial.ac.uk>
Date: Mon, 20 Dec 2021 20:03:51 +0000
Subject: Comment the code dealing with un/flushed bytes, and resolve old
 naming issue by renaming flushMask to unflushedMask

---
 lib/Core/Memory.h | 25 +++++++++++++++++--------
 1 file changed, 17 insertions(+), 8 deletions(-)

(limited to 'lib/Core/Memory.h')

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);
-- 
cgit 1.4.1