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)