source: CIVL/notes/notes.txt@ 0d850b0

For implementing malloc:

Add sizeof expression in model.
Semantics: get the dynamic type and evaluate the sizeof that
using some well-known formulas.  Add things to the path condition
as a side effect, like sizes are greater than 0, or 1, or
whatever.

Add a MallocStatement to the model.  Example
(double*)malloc(&h, sizeof(double)*10).
  - int getMallocId();
  - Expression getHeapPointerExpression(); // &h 
  - Type getStaticElementType(); // double
  - SymbolicType getDynamicObjectType(); // symbolic array of double
  - Expression getSizeExpression(); // sizeof(double)*10
  - SymbolicExpression getUndefinedObject(); // symbolic constant UNDEFINED
                                             // of type array of double

During model building, count the malloc statements as they are
encountered and assign each a unique ID.

Complete the $heap type:  
  For each i, you have the static CIVL type T_i and the 
  __malloc__ function.  Compute the most general symbolic
  type t_i by translating t_i and using incomplete types
  for arrays.  Store t_i in the malloc call object.
  let $heap be the symbolic type which is the tuple type

  [array of array of t1,
   array of array of t2,
   array of array of t3, ...]

Initial value:

  [array of length 0, array of length 0, ...]
 
Semantics:
  to execute a malloc statement with malloc index i:
  let h be the result of evaluating the heap argument. *h is a tuple.
  (*h).i is a concrete array.  Let l be its concrete length.
  create a new symbolic constant whose name is a function of
  the pid, dynamic scope id, heap variable ID, index i, and
  l.  The type of this new symbolic constant is array of t_i
  of length arg/sizeof(t+i), where arg is the result of evaluating
  the size argument.  Check that it evenly divides, and log
  an error if it might not.  Now append this symbolic constant
  to the concrete array. [Really need a method in SARL to do this.]
  Anyway, since it is concrete, get its sequence and append on to that.
  Return the reference with tree:
  - ref to heap (h)
  - tuple component ref (i)
  - array element reference (l)
  - array element reference (0)
  which is a reference to the first element of the newly allocated
  array.  

free: sets the value in the heap array to some symbolic constant
UNDEFINED of type array of t_i.

Canonicalization: map
  Ref[h,i,l,0] -> Ref[h,i,l',0]
  H_p_s_v_i_l -> H_p_s_v_i_l' (symbolic constants)
Perform substitution on the state


---

   
Think about moving more stuff into model factory, like pointer value
manipulation

better printing of model

better printing of states during execution