Lazy initialization of function arguments and variables marked as 'extern'

include/klee/KValue.h

@@ -43,6 +43,8 @@ namespace klee {
       : value(value), pointerSegment(ConstantExpr::alloc(VALUES_SEGMENT, value->getWidth())) {}
     KValue(ref<Expr> segment, ref<Expr> offset)
       : value(offset), pointerSegment(segment) {}
+    KValue(uint64_t segment, ref<Expr> offset)
+      : value(offset), pointerSegment(ConstantExpr::alloc(segment, value->getWidth())) {}
 
     KValue(SpecialSegment segment, ref<Expr> offset)
       : value(offset), pointerSegment(ConstantExpr::alloc(segment, value->getWidth())) {}

lib/Core/AddressSpace.cpp

@@ -24,13 +24,23 @@ void AddressSpace::bindObject(const MemoryObject *mo, ObjectState *os) {
   assert(os->copyOnWriteOwner==0 && "object already has owner");
   os->copyOnWriteOwner = cowKey;
   objects = objects.replace(std::make_pair(mo, os));
-  if (mo->segment != 0)
+  if (mo->segment != 0) {
     segmentMap = segmentMap.replace(std::make_pair(mo->segment, mo));
+    if (mo->isLazyInitialized) {
+      lazilyInitializedOffsets.insert({mo->getSegment(), {}});
+    }
+  }
+
 }
 
 void AddressSpace::unbindObject(const MemoryObject *mo) {
-  if (mo->segment != 0)
+  if (mo->segment != 0) {
     segmentMap = segmentMap.remove(mo->segment);
+    if (mo->isLazyInitialized) {
+      lazilyInitializedOffsets.erase(mo->segment);
+    }
+  }
+
   objects = objects.remove(mo);
   // NOTE MemoryObjects are reference counted, *mo is deleted at this point
 }

lib/Core/AddressSpace.h

@@ -40,6 +40,9 @@ 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*/ ref<Expr>> RemovedObjectsMap;
+typedef std::map</*pointer segment*/ const uint64_t, /*value segment:offset*/ std::pair<uint64_t, uint64_t>> LazyPointersSegmentMap;
+typedef std::map</*segment*/ const uint64_t, /*lazily initialized offsets*/std::vector<uint64_t>> LazilyInitializedOffsets;
+
 
 class AddressSpace {
   friend class ExecutionState;
@@ -67,12 +70,19 @@ class AddressSpace {
 
   RemovedObjectsMap removedObjectsMap;
 
+  LazilyInitializedOffsets lazilyInitializedOffsets;
+
+  LazyPointersSegmentMap lazyPointersSegmentMap;
+
   AddressSpace() : cowKey(1) {}
   AddressSpace(const AddressSpace &b)
       : cowKey(++b.cowKey),
         objects(b.objects),
         segmentMap(b.segmentMap),
-        removedObjectsMap(b.removedObjectsMap) { }
+        concreteAddressMap(b.concreteAddressMap),
+        removedObjectsMap(b.removedObjectsMap),
+        lazilyInitializedOffsets(b.lazilyInitializedOffsets),
+        lazyPointersSegmentMap(b.lazyPointersSegmentMap){ }
   ~AddressSpace() {}
 
   /// Looks up constant segment in concreteAddressMap.