add pointer types, values to model

[Stephen Siegel]

Refer to how this was done for Mover. Need pointers to variables, array elements, record elements.

[Stephen Siegel]

The pointer branch has been re-integrated into the trunk and the pointer branch has been deleted.

With only a few exception, I was able to resolve all conflicts when merging, so all changes have been preserved. (Tim, you may have to change the methods in Executor from public to protected again, because it was just too challenging to correct the conflicts that created.)

Here are some of the major changes:

The value package has been replaced by a "dynamic" package. The dynamic package deals with run-time concepts of (1) dynamic types, (2) dynamic variables, and (3) values. Every value now comes with a "dynamic type", which is not the same as a (static) type. A dynamic type might contain more information, for example, the bounds on the arrays. A "dynamic variable" is a run-time variable, perhaps better thought of as a "memory cell", i.e., a place where a value can be stored. Examples: when a process is started up in the initial state, all of its process variables are "instantiated", which means one dynamic variable is created for each of the static process variables. When a function is called, a dynamic local variable is instantiated for each of the static local variables declared for that function. (Note there may be many dynamic variables corresponding to a single static local variable, thanks to recursion---the function can be on the call stack multiple times.) A call to "malloc" will create a dynamic heap variable in the heap of the process---no static variable corresponds to this dynamic variable. I think the comments in the interface files should make all of this pretty clear.

Arrays: the way that arrays are dealt with has been greatly simplified. Previously, in the (static) model, an array variable was counted as two variables: one for an array object and one for a reference to that array object. That confusing semantics is gone. Now an array variable just creates a single variable, so arrays are just like any other type in that respect. Under the hood, a non-formal array variable (which necessarily comes with dimension expressions in its declaration) is assigned an array object value, while a formal parameter array variable is assigned a reference to an array (the actual parameter used when the function is called). The "evaluate" method in the Evaluator is smart enough to distinguish between these two kinds of variables, and always returns an array value.

I have added pointers, records, pointer arithmetic, allocate, deallocate. None of this new functionality has been tested yet. I have not yet implemented the garbage collection algorithm I need to deal with allocation and deallocation properly. (To do that, I need some additional methods in the symbolic universe, which I will describe to Yi in a separate email.)

Yi, you will have to do some work now to bring your loop verification scheme up to date. Let me know if you have any questions. Tim, you can continue with the implementation of the abstract functions, accuracy, etc.

-Steve