[fix] Clean memory operations

Author: misonijnik

include/klee/ADT/SparseStorage.h

@@ -79,7 +79,7 @@ class SparseStorage {
   }
 
   bool operator==(const SparseStorage<ValueType> &another) const {
-    return defaultValue == another.defaultValue && compare(another) == 0;
+    return eq(defaultValue, another.defaultValue) && compare(another) == 0;
   }
 
   bool operator!=(const SparseStorage<ValueType> &another) const {
@@ -131,7 +131,7 @@ class SparseStorage {
 
   void reset(ValueType newDefault) {
     defaultValue = newDefault;
-    internalStorage.clear();
+    reset();
   }
 
   void print(llvm::raw_ostream &os, Density) const;

lib/Core/Memory.cpp

@@ -183,13 +183,6 @@ ref<Expr> ObjectState::read8(ref<Expr> offset) const {
 }
 
 void ObjectState::write8(unsigned offset, uint8_t value) {
-  auto byte = knownSymbolics.load(offset);
-  if (byte) {
-    auto ce = dyn_cast<ConstantExpr>(byte);
-    if (ce && ce->getZExtValue(8) == value) {
-      return;
-    }
-  }
   knownSymbolics.store(offset, ConstantExpr::create(value, Expr::Int8));
   unflushedMask.store(offset, true);
 }
@@ -199,10 +192,6 @@ void ObjectState::write8(unsigned offset, ref<Expr> value) {
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(value)) {
     write8(offset, (uint8_t)CE->getZExtValue(8));
   } else {
-    auto byte = knownSymbolics.load(offset);
-    if (byte && byte == value) {
-      return;
-    }
     knownSymbolics.store(offset, value);
     unflushedMask.store(offset, true);
   }

lib/Solver/Z3Builder.cpp

@@ -284,7 +284,7 @@ Z3ASTHandle Z3Builder::getInitialArray(const Array *root) {
         }
         constant_array_assertions[root] = std::move(array_assertions);
       } else {
-        for (auto [index, value] : source->constantValues.storage()) {
+        for (auto &[index, value] : source->constantValues.storage()) {
           int width_out;
           Z3ASTHandle array_value = construct(value, &width_out);
           assert(width_out == (int)root->getRange() &&