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: "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)
  • 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

Set<HeapObject> reachableHeapObjectsOfState(state){
  Set <HeapObject> reachable;

  for(dyscope: state.dyscopes()){
    for(varValue: dyscope.varValues()){
      reachableHeapObjectsOfValue(varValue, reachable);
    }
  }
  return idMap;
}

//dfs
void reachableHeapObjectsOfValue(varValue, reachable){
  if(varValue NOT pointer){
    if()
    for(element: varValue.elements())
      reachableHeapObjects(varValue, reachable);
  }else if(varValue IS heap pointer){
    object = dereference(varValue);
   
    if(!reachable.contains(object))
        reachable.add(object);
  }else{//other pointer
    reachableHeapObjects(dereference(varValue), reachable){
  }
}

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);
}