source: CIVL/notes/notes.txt@ df5c584

For implementing malloc:

Add sizeof expression in model:
  CIVLType getType();
[do we also need sizeof(expr)? -- that's different!]

For primitive types, add a method:
  NumericExpression getSizeof();

Create a symbolic constant for each primitive type, of type int,
named SIZEOF_INT, etc.  Set this in model factory.

In Evaluator: as a side-effect, if a sizeof expression is ever evaluated,
add some facts about it to the path condition: sizeof(...)>0,
maybe sizeof(char)=1 ?

Evaluator: for primitive types, get it from type.
Otherwise, compute: for arrays, multiply extent and sizeof
element type (evaluating extent).  For all others (records,
pointers) use an uninterpreted function sizeof(...) which
takes a DynamicType and returns int.

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




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