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, dynamicType]. Here, variable is a (static) Variable, and dynamicType is an expression of type CIVLDynamicType. The type of this expression is the type of the variable. When evaluated, it returns a default initial value for a variable with the given dynamic type. 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, CIVLDynamicType(t)]
• Evaluation of CIVLDynamicType(t) in a state s is defined as follows:
  • if t is a struct type, say with tag foo, then the result is the result of evaluating the variable (in s) __struct_foo__
  • if t is an array type with element type E and length expression l, the result is obtained by evaluating CIVLDynamicType(E), call the result de; evaluating l, call the result dl; and return completeArrayType(de,dl) (eliding the wrapping and unwrapping of the symbolic type into a symbolic expression value)
• Evaluation of InitialValue[v,d] is as follows:
  • for a primitive dynamic type, some undefined value (null expression)?
  • if d is a tuple, create the concrete tuple of type d with each component obtained by evaluating InitialValue[component, componentType]
    • XXX problem: maybe take address argument instead of variable, or LHS expression???. Or just Initialize(LHSExpression, DynamicType) statement.
  • if d is an array type, create a unique symbolic constant name based on the LHS expression and a symbolic constant with that name and type d (no recursion in this case)