Changes between Version 2 and Version 3 of HeapCanonicalization

Timestamp:

08/05/14 14:43:28 (12 years ago)

Author:

zmanchun

Comment:

--

HeapCanonicalization

@@ -23 +23 @@
   - Otherwise, initialize each leaf-node element of the heap object with the symbolic NULL expression (not Java NULL).
 
-* Naming rule: `"Hp" + pid + "s" + dyscopeId + "i" + mallocId + "l" + calledId`
+* Naming rule: `"Ho" + "p" + pid + "s" + dyscopeId + "i" + mallocId + "l" + calledId`
 
 * Deallocation: a heap object is removed from the heap when a `$free` is called with the corresponding pointer. (Semantics of `$free` follows C11 standards)
@@ -32 +32 @@
 
 {{{
-Map<HeapObject, Integer> reachableHeapObjectsOfState(state){
-  Map<HeapObject, Integer> idMap;
+Set<HeapObject> reachableHeapObjectsOfState(state){
+  Set <HeapObject> reachable;
 
   for(dyscope: state.dyscopes()){
     for(varValue: dyscope.varValues()){
-      reachableHeapObjectsOfValue(varValue, idMap);
+      reachableHeapObjectsOfValue(varValue, reachable);
     }
   }
@@ -44 +44 @@
 
 //dfs
-void reachableHeapObjectsOfValue(varValue, idMap){
+void reachableHeapObjectsOfValue(varValue, reachable){
   if(varValue NOT pointer){
-    for(element: varValue.elements()){
-      reachableHeapObjects(varValue, idMap);
-    }
+    if()
+    for(element: varValue.elements())
+      reachableHeapObjects(varValue, reachable);
   }else if(varValue IS heap pointer){
     object = dereference(varValue);
    
-    if(! dMap.containsKey(object))
-      if(object is SymbolicConstant)
-        idMap.put(object, idMap.size());
-      else
-         idMap.put(object, -1);
+    if(!reachable.contains(object))
+        reachable.add(object);
   }else{//other pointer
-    reachableHeapObjects(dereference(varValue), idMap){
+    reachableHeapObjects(dereference(varValue), reachable){
   }
 }
 }}}
 
-TBC
+==== Heap Canonicalization ====
+
+{{{
+State collectHeaps(state, reachable){
+  int id = 0;
+  Map<Object, Object> oldToNew;
+
+  for(dyscope: state.dyscopes()){
+    heap = dyscope.heap();
+    for(object: heap.objects()){
+      if(reachable.contains(object))
+        oldToNewNames.put(object, object.rename("Ho"+id));
+        id++;
+    }else{
+       heap.remove(object);
+       newHeapObjectPointers(heap, oldToNew);
+    }
+  }
+  return state.substitute(oldToNew);
+}
+}}}
+