Changes between Initial Version and Version 1 of HeapCanonicalization

Timestamp:

07/30/14 17:44:20 (12 years ago)

Author:

zmanchun

Comment:

--

HeapCanonicalization

@@ +1 @@
+== Heap & Canonicalization ==
+
+=== Heap ===
+In CIVL, each scope has one and only one heap.
+The heaps of the same CIVL model has the same type regardless of which scope it belongs to.
+
+The heap type is defined as the following:
+{{{
+struct __heap_type{
+__type1 [][];
+__type2 [][];
+...
+}
+}}}
+where `__type1`, `__type2`,... are corresponding to the object type of each `$malloc` statement.
+
+==== Heap Object ====
+
+* Allocation: a heap object is created by a `$malloc` statement, and it is added into the heap of the dyscope specified by the `$malloc` statement.
+
+* Initialization:
+  - If the size of the `$malloc` statement is not concrete or the type of the heap object has a non-concrete state (e.g, a struct containing an array field whose extent is not concrete), then the heap object has to be a symbolic constant with a unique name;
+  - 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`
+
+* Deallocation: a heap object is removed from the heap when a `$free` is called with the corresponding pointer. (Semantics of `$free` follows C11 standards)
+  - Update all pointers to the heap object to be UNDEFINED
+  - Note: the removal of the heap object only happens later when garbage collection/canonicalization is performed.
+
+==== Heap Object Reachability Analysis ====
+
+{{{
+Map<HeapObject, Integer> reachableHeapObjectsOfState(state){
+  Set<HeapObject> visited;
+  Map<HeapObject, Integer> idMap;
+
+  for(dyscope: state.dyscopes()){
+    for(varValue: dyscope.varValues()){
+      reachableHeapObjects(varValue);
+    }
+  }
+  return idMap;
+}
+
+//dfs
+void reachableHeapObjectsOfValue(varValue, visited, idMap){
+  if(varValue NOT pointer){
+    for(element: varValue.elements()){
+      reachableHeapObjects(varValue, visited, idMap);
+    }
+  }else if(varValue IS heap pointer){
+    object = dereference(varValue);
+   
+    if(!visited.contains(object)){
+      visited.add(object);
+      idMap.put(object, idMap.size());
+    }
+  }else{//other pointer
+    reachableHeapObjects(dereference(varValue), visited, idMap){
+  }
+}
+}}}
+
+TBC