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