Changes between Version 98 and Version 99 of IR2

Timestamp:

05/14/21 10:35:15 (5 years ago)

Author:

siegel

Comment:

--

IR2

@@ -17 +17 @@
 
 1. **Do variables have default initial values?**
-  * Every variable holds a value of its type, always.  However the initial values of variables is unspecified.   Therefore a correct CIVL-IR program should explicitly initialize every variable before it is used.  Moreover, there is a defined bit associated to each variable, and it is initially false, indicating that the variable is "undefined".   It becomes defined when it is assigned.  Details are below.
+  * No.  Every variable must be explicitly initialized.  However, `$undef` can be used as the initializer, indicating that the variable is undefined.  Even in this case, the variable has some unspecified value of its type.   Details are below.
 1. **How do you initialize a variable?**
-  * By assigning a value to it.   For example `n=$new($int);` will assign `n` an arbitrary integer, while `n=0;` will assign the integer `0` to `n`.
+  * In the declaration.   For example `n=$new($int);` will assign `n` an arbitrary integer, while `n=0;` will assign the integer `0` to `n`.
 1. **How is an array allocated?**
-  * An array variable `a` is declared with a decl such as `T a[];`, and then a statement such as `a=$new_array(n, T);` will assign to `a` a new array value for an array of length `n` of elements of type `T` in which all entries are undefined.   (Alternatively, `a=$new(T[n])` will create an array of arbitrary defined values.)  For heap-allocation, a pointer is declared with a decl such as `T * p;`, and a heap variable is also declared somewhere with a decl such as `$heap heap;` and then a statement such as `p = $alloc(&heap, n, T);` will add a new object to the heap and return a pointer to the first element.  An `$alloc`-ed object can be deallocated with `$free(p);`.
+  * An array variable `a` is declared with a decl such as `T a[] = $new_array(n, T);` which assigns to `a` a new array value for an array of length `n` of elements of type `T` in which all entries are undefined.   (Alternatively, `T a[] = $new(T[n])` will create an array of arbitrary defined values.)  For heap-allocation, `T * p = $undef;` followed by the statement `p = $alloc(&heap, n, T);` will add a new object to the heap and return a pointer to the first element.  An `$alloc`-ed object can be deallocated with `$free(p);`.
 1. **Is there an "array-pointer pun", as in C?**
   * No, if you want a pointer to element 0 of an array, you have to explicitly write something like `&a[0]`.
@@ -51 +51 @@
   ';'
   ;
-decl: type-param-list? qualifier* type-specifier declarator contract-clause* ';' ;
-function-definition: type-param-list? qualifier* type-specifier declarator contract-clause* block ;
-qualifier:
+decl: function-decl | object-decl ;
+function-decl: type-param-list? function-qualifier*  type-specifier declarator contract-clause* ';' ;
+object-decl: type-specifier declarator '=' initializer ';' ;
+function-definition: type-param-list? function-qualifier* type-specifier declarator contract-clause* block ;
+function-qualifier:
     '$abstract_f'  /* abstract function; only for function decls */
   | '$pure_f'  /* function is a mathematical function of its parameters */
@@ -169 +171 @@
   | lvalue '=' expr ';'  /* assignment */
   | (lvalue '=')? expr type-args? '(' expression-list? ')' ';'  /* function call */
-  | (lvalue '=')? '$spawn' expr type-args? '(' expression-list? ')' ';'  /* process creation */
+  | lvalue '=' '$spawn' expr type-args? '(' expression-list? ')' ';'  /* process creation */
   | '$wait' expr ';'  /* wait until p terminates */
   | 'return' expr? ';'  /* return from function call */
-  | (lvalue '=')? '$alloc' '(' expr ',' expr ',' type-name ')' ';'  /* heap allocation */
-  | '$free' expr ';'  /* frees something that was $alloc-ed */
-  | (lvalue '=')? '$new_array' '(' expr ',' type-name ')' ';'  /* allocation of array of undefined values*/
   | '$atomic_enter' ';'  /* enter atomic region */
   | '$atomic_exit' ';'  /* exit atomic region */
@@ -227 +226 @@
   | expr type-args? '(' expression-list? ')'  /* application of abstract function (and perhaps other functions?) */
   | '$new' '(' type-name ')'  /* returns a new arbitrary value of the given type */
+  | '$new_array' '(' expr ',' type-name ')'  /* allocation of array of undefined values*/
   | '$forall' '(' decl expr? ')' expr  /* universal quantification */
   | '$exists' '(' decl expr? ')' expr  /* existential quantification */
@@ -239 +239 @@
 expr-pair-list: expr-pair (',' expr-pair)* ;
 expr-pair: '{' expr ',' expr '}' ;
-
+initializer: expr | '$undef' ;
 }}}
 
@@ -300 +300 @@
 
 {{{
-$system void $exit(void);
-$system $bool $terminated($proc p);
-$system int $choose_int($int n); // how is this different than $new($int)?
+<T> $system alloc($heap * h, $int n);  // heap allocation of n elements of type T
+$system $free($void * p);  // frees something that was $alloc-ed
+$system void $exit();  // terminate process immediately
+$system $bool $terminated($proc p);  // has the process terminated?
+$system int $choose_int($int n);  // nondeterministic choice of int in 0..n-1
 
 }}}