Fix comparing to freed pointers

staticafi · Nov 24, 2020 · 07fb0d4 · 07fb0d4
1 parent ed1856b
commit 07fb0d4
Show file tree

Hide file tree

Showing 4 changed files with 37 additions and 12 deletions.
diff --git a/lib/Core/AddressSpace.h b/lib/Core/AddressSpace.h
@@ -37,7 +37,7 @@ typedef ImmutableMap<const MemoryObject*, ObjectHolder, MemoryObjectLT> MemoryMa
 typedef ImmutableMap<uint64_t, const MemoryObject*> SegmentMap;
 typedef std::map</*address*/ const uint64_t, /*segment*/ const uint64_t> ConcreteAddressMap;
 typedef std::map</*segment*/ const uint64_t, /*address*/ const uint64_t> SegmentAddressMap;
-typedef std::map</*segment*/ const uint64_t, /*symbolic array*/ const Array*> RemovedObjectsMap;
+typedef std::map</*segment*/ const uint64_t, /*symbolic array*/ ref<Expr>> RemovedObjectsMap;
 
 class AddressSpace {
   friend class ExecutionState;
@@ -69,7 +69,8 @@ class AddressSpace {
   AddressSpace(const AddressSpace &b)
       : cowKey(++b.cowKey),
         objects(b.objects),
-        segmentMap(b.segmentMap) { }
+        segmentMap(b.segmentMap),
+        removedObjectsMap(b.removedObjectsMap) { }
   ~AddressSpace() {}
 
   /// Looks up constant segment in concreteAddressMap.
@@ -189,4 +190,4 @@ class AddressSpace {
 };
 } // End klee namespace
 
-#endif /* KLEE_ADDRESSSPACE_H */
+#endif /* KLEE_ADDRESSSPACE_H */
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
@@ -2324,8 +2324,17 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
         if (!leftSegment->isZero()) {
           bool success = state.addressSpace.resolveOneConstantSegment(left, lookupResult);
           if (!success) {
-            terminateStateOnExecError(state, "Failed resolving constant segment");
-            break;
+            auto& removedObjs = state.addressSpace.removedObjectsMap;
+            auto removedIt = removedObjs.find(leftSegment->getZExtValue());
+            if (removedIt == removedObjs.end()) {
+              terminateStateOnExecError(state,
+                                        "Failed resolving constant segment");
+              break;
+            }
+
+            left = KValue(ConstantExpr::alloc(VALUES_SEGMENT,
+                                              leftSegment->getWidth()),
+                          removedIt->second);
           }
           // FIXME: we should assert that the address does not overlap with any of the
           // currently allocated objects...
@@ -2335,8 +2344,18 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
         if (!rightSegment->isZero()) {
           bool success = state.addressSpace.resolveOneConstantSegment(right, lookupResult);
           if (!success) {
-            terminateStateOnExecError(state, "Failed resolving constant segment");
-            break;
+            auto& removedObjs = state.addressSpace.removedObjectsMap;
+            auto removedIt = removedObjs.find(rightSegment->getZExtValue());
+            if (removedIt == removedObjs.end()) {
+              terminateStateOnExecError(state,
+                                        "Failed resolving constant segment");
+              break;
+            }
+
+            right = KValue(ConstantExpr::alloc(VALUES_SEGMENT,
+                                               rightSegment->getWidth()),
+                          removedIt->second);
+
           }
           right = KValue(ConstantExpr::alloc(VALUES_SEGMENT, rightSegment->getWidth()),
                          const_cast<MemoryObject*>(lookupResult.first)->getSymbolicAddress(arrayCache));
@@ -4002,8 +4021,9 @@ void Executor::executeFree(ExecutionState &state,
         terminateStateOnError(*it->second, "free of global", Free, NULL,
                               getKValueInfo(*it->second, addressOptim));
       } else {
-        const_cast<MemoryObject*>(mo)->initializeSymbolicArray(arrayCache);
-        it->second->addressSpace.removedObjectsMap.insert(std::make_pair(mo->segment, mo->symbolicAddress.getValue()));
+        it->second->addressSpace.removedObjectsMap.insert(
+            std::make_pair(mo->segment,
+                           const_cast<MemoryObject*>(mo)->getSymbolicAddress(arrayCache)));
         it->second->addressSpace.unbindObject(mo);
         if (target)
           bindLocal(target, *it->second, KValue(Expr::createPointer(0)));

diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp
@@ -94,15 +94,19 @@ void MemoryObject::getAllocInfo(std::string &result) const {
 
 void MemoryObject::initializeSymbolicArray(klee::ArrayCache &array) {
   if (!symbolicAddress) {
-    symbolicAddress = array.CreateArray(std::string("mo_addr_for_seg:") + std::to_string(segment), Context::get().getPointerWidth());
+    auto tmparray = array.CreateArray(std::string("mo_addr_for_seg:") +
+                                        std::to_string(segment),
+                                      Context::get().getPointerWidth());
+    symbolicAddress = Expr::createTempRead(tmparray,
+                                           Context::get().getPointerWidth());
   }
 }
 
 ref<Expr> MemoryObject::getSymbolicAddress(klee::ArrayCache &array) {
   if (!symbolicAddress) {
     initializeSymbolicArray(array);
   }
-  return Expr::createTempRead(symbolicAddress.getValue(), Context::get().getPointerWidth());
+  return symbolicAddress.getValue();
 }
 
 /***/

diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h
@@ -74,7 +74,7 @@ class MemoryObject {
   mutable std::vector< ref<Expr> > cexPreferences;
 
   /// Symbolic address for poiner comparison
-  llvm::Optional<const Array*> symbolicAddress;
+  llvm::Optional<ref<Expr>> symbolicAddress;
 
   // DO NOT IMPLEMENT
   MemoryObject(const MemoryObject &b);