= Multiple Changes to CIVL Code =

== Model Changes ==

* make sure the parameter type of a function call is never an array type.   ABC should already be doing this.
* add a method to expressions like `SymbolicExpression getConstantValue()` and a corresponding setter, to cache the value of any expression that has a constant value, such as a literal expression
* add a new `CIVLType`: `CIVLDynamicType.`
 * A CIVL Expression of that type, when evaluated, will yield a `SymbolicExpression` `x`.  A method in the `Evaluator`, `SymbolicType getSymbolicType(SymbolicExpression x);`, will take such an `x` and return a `SymbolicType` and that is basically the only operation that can be performed on `x`.  Hence this gives you a way to take a (dynamic, symbolic) type and wrap it up into a value that can be stored in a variable in your model.
* add a new kind of CIVL `Expression`: `DynamicTypeOf(t)`, where `t` is a (static) CIVL type.
 * The type of this expression is `CIVLDynamicType`.  When evaluated, it returns the dynamic type determined by the current state and the given static type.  (This assumes extent expressions are stored in array types.)  For example, if `t` is the static type `struct foo { double a[n]; }` from the source code above, then `DynamicTypeOf(t)`, evaluated in the state that arises at that point in the source code, will yield the symbolic type which is a record type with one field which is an array of doubles of length 2.  Now you can store that dynamic type in a variable if you want to save it, e.g., insert a statement like this into the model:
  * `CIVLDynamicType __struct_foo__ = DynamicTypeOf(struct foo { double a[n]; });`
* add a new kind of CIVL expression: `InitialValue[variable]`. Here, `variable` is a (static) `Variable`.  The type of this expression is the type of the variable.  When evaluated, it returns a default initial value for a variable with the dynamic type determined by the current state and the static type of the variable.  This can be used to initialize arrays and structs.
* add a new `CIVLType`: `CIVLScopeType`
* add new subtype of `Variable`: `CIVLScopeVariable` with method
 * `Scope getScope();`
* add to the CIVL pointer type a method to get the scope variable, implement appropriate constructors and modifications to the factory, etc.

== Semantics Changes ==

* use interfaces for `Executor`, `Evaluator`, etc.
* finish javadocs for all methods
* don't use `Vector`.  Use `LinkedList` if you only need to iterate; use `ArrayList` if you need constant time access
* use `switch` instead of big `if...else if…` sequence (mostly DONE)
* implement pointer subtraction
* construct and set the heap type in the constructor for `Evaluator`, just like the other special types

== Translation ==

Thoughts on processing struct definitions:

* transform the AST to factor out all struct definitions embedded in declarations.  This is really part of "side-effect-removal".
* translate a struct definition `struct foo { … } ` as follows.
 * Let `t` be the `CIVLType` resulting from translating the ABC type.
 * Create a new `Variable` of type `CIVLDynamicType` and add it to the current scope. Call the variable `__struct_foo__`.
 * Create as assignment statement at the current location: `__struct_foo__ = DynamicTypeOf(t)`
* any variable declaration with a compound type (struct, union, array) should be translated as follows:
 * add the variable `v` to the current scope with the translated type `t` as usual
 * add an assignment statement at the current location: `v=InitialValue[v]`
* define a method in the `Evaluator`, `SymbolicType getDynamicType(State s, Type t)`
 * if `t` is a primitive type, map to the corresponding symbolic type
 * if `t` is a struct type, say with tag `foo`, then the result is the result of evaluating the variable (in s) `__struct_foo__` and extracting the symbolic type from the result
 * if `t` is an array type with element type `E` and length expression `l`, the result is obtained by evaluating `getDynamicType(s, E)`, call the result `de`; evaluating `l`, call the result `dl`; and returning `completeArrayType(de,dl)` (eliding the wrapping and unwrapping of the symbolic type into a symbolic expression value)
* define a method in the `Evaluator`, `SymbolicType computeDynamicType(State s, Type t)`
 * if `t` is a struct type, return the symbolic tuple type obtained by invoking `computeDynamicType` recursively on the component types of `t`
 * if `t` is an array type or primitive type proceed analogously to `getDynamicType`
* define a method in the `Evaluator`, `SymbolicExpression computeInitialValue(State s, LHSExpression expr, SymbolicType dynamicType);`
 * if `dynamicType` is a tuple type, create the concrete tuple of that type with each component obtained by evaluating `computeInitialValue(s, dotExpression(…), componentType)`
 * if `dynamicType` is an array type, create a unique symbolic constant name based on the LHS expression and a symbolic constant with that name and type `dynamicType` (no recursion in this case)
* Evaluation of `DynamicTypeOf(t)` in a state `s` is defined by `computeDynamicType(s,t)`
* Evaluation of `InitialValue[v]` is as follows:
 * let `t` be the (static) type of `v`
 * if `t` is primitive, return appropriate symbolic value (null expression, …)
 * else let `d` be `getDynamicType(s,t)`
 * return `computeInitialValue(s, v, d)`