| 8 | | * add a new `CIVLType`: `CIVLDynamicType.` |
| 9 | | * 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. |
| 10 | | * add a new kind of CIVL `Expression`: `DynamicTypeOf(t)`, where `t` is a (static) CIVL type. |
| 11 | | * 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: |
| 12 | | * `CIVLDynamicType __struct_foo__ = DynamicTypeOf(struct foo { double a[n]; });` |
| 13 | | * 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. |
| 33 | | * translate a struct definition `struct foo { … } ` as follows. |
| 34 | | * Let `t` be the `CIVLType` resulting from translating the ABC type. |
| 35 | | * Create a new `Variable` of type `CIVLDynamicType` and add it to the current scope. Call the variable `__struct_foo__`. |
| 36 | | * Create as assignment statement at the current location: `__struct_foo__ = DynamicTypeOf(t)` |
| 37 | | * any variable declaration with a compound type (struct, union, array) should be translated as follows: |
| 38 | | * add the variable `v` to the current scope with the translated type `t` as usual |
| 39 | | * add an assignment statement at the current location: `v=InitialValue[v]` |
| 40 | | * define a method in the `Evaluator`, `SymbolicType getDynamicType(State s, Type t)` |
| 41 | | * if `t` is a primitive type, map to the corresponding symbolic type |
| 42 | | * 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 |
| 43 | | * 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) |
| 44 | | * define a method in the `Evaluator`, `SymbolicType computeDynamicType(State s, Type t)` |
| 45 | | * if `t` is a struct type, return the symbolic tuple type obtained by invoking `computeDynamicType` recursively on the component types of `t` |
| 46 | | * if `t` is an array type or primitive type proceed analogously to `getDynamicType` |
| 47 | | * define a method in the `Evaluator`, `SymbolicExpression computeInitialValue(State s, LHSExpression expr, SymbolicType dynamicType);` |
| 48 | | * if `dynamicType` is a tuple type, create the concrete tuple of that type with each component obtained by evaluating `computeInitialValue(s, dotExpression(…), componentType)` |
| 49 | | * 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) |
| 50 | | * Evaluation of `DynamicTypeOf(t)` in a state `s` is defined by `computeDynamicType(s,t)` |
| 51 | | * Evaluation of `InitialValue[v]` is as follows: |
| 52 | | * let `t` be the (static) type of `v` |
| 53 | | * if `t` is primitive, return appropriate symbolic value (null expression, …) |
| 54 | | * else let `d` be `getDynamicType(s,t)` |
| 55 | | * return `computeInitialValue(s, v, d)` |
| 56 | | |
