CIVL IR

Language principles

• CIVL-IR is a subset of CIVL-C. A CIVL-IR program is a CIVL-C program, and has the same semantics.

Questions

1. Do variables have default initial values?
   • No, a declared variable must be initialized before it is used. Otherwise, the behavior is undefined.
2. 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.
3. 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(T[n]); will assign to a a new arbitrary array value for an array of length n of elements of type T. 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);.
4. 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 say something like &a[0].
5. How to you translate between sequences and arrays?
6. Can you make types values? (reification)
7. pure functions? A pure function is a mathematical function of its arguments. It cannot modify the state.
8. state functions? A state function is a function of the current state (including arguments, global variables, ...). It cannot modify the state. Every pure function is a state function.
9. $depends_on
10. read/write sets: function calls to start, stop monitoring reads/writes? All part of mem library
11. function calls for atomic enter/exit
12. a type for $state ?

Grammar

program: typedef* decl* function-definition+ ;
typedef:
    enum ID '{' identifier-list '}' ';'
  | struct ID '{' decl* '}' ';'
  | union ID '{' decl* '}' ';'
  | 'typedef' type-specifier declarator ';'
  ;
decl: qualifier? type-specifier declarator contract-clause* ';' ;
qualifier: '$input' | '$output' | '$abstract' | '$system' '<' STRING ',' STRING '>' ;
function-definition: '$atomic_f'? type-specifier declarator contract-clause* block ;
block: '{' typedef* decl* function-definition* statement* '}' ;
statement: block | simpleStmt | chooseStmt ;
simpleStmt: label? guard? primitiveStmt gotoStmt? ;
chooseStmt: label? '$choose' '{' simpleStmt* '}' ;
label: ID ':' ;
guard: '$when' '(' expr ')' ;  
gotoStmt: 'goto' ID ;
contract-clause :
    '$assigns' expr ';' 
  | '$requires' expr ';'
  | '$ensures' expr ';'
   ...
INT: ... /* integer constant */
ID: ... /* identifier */
STRING: ... /* string literal in double quotes */

Notes

• a program must contain a function definition for a function named main
• $input and $output can be used only on global variable declarations (not on function definitions, not in block scope)
• $abstract can be used only in a declaration of a variable of function type. The function becomes a new uninterpreted function.
• $atomic_f indicates that a defined function is to behave atomically, i.e., every call to such a function will behave as if the call occurred in an $atomic block.
• a $system function has no definition in CIVL-IR, but is instead defined elsewhere (for example, in C or Java code). Such a function will always be executed atomically. The first string specifies a path (e.g., Java package) to the library containing the function, the second is the name of the library. These two Strings should be enough to tell CIVL where to find the system definition of the function.
• the expr in a guard must have type $bool

  int a[];
  void main() {
    a = (int[10])$lambda(int i; $undefined);
    a = $new(int[10]); // 
    ... initialized a somehow ...
   $assume($defined(a, 0, 10)); // ?

Types

type-specifier:
    ID  /* typedef use */
  | '$int'  /* mathematical integers */
  | '$bool'  /* boolean type ($true and $false, unrelated to integers) */
  | '$char'  /* character type (Unicode characters, unrelated to integers) */
  | '$real'   /* mathematical reals */
  | '$float' '<' INT ',' INT '>'  /* IEEE floating-point numbers e=significand bits, f=exponent bits */
  | '$herbrand' '<' type-name '>'  /* Herbrand type of non-Herbrand numeric type T */
  | '$proc'  /* process type */
  | '$bundle'  /* bundle type for sequence of any type (same as seq<T>?) */
  | '$heap'  /* heap type, for dynamic allocation */
  | '$range'  /* regular sequence of integers */
  | '$domain'  /* tuple of ranges */
  | '$mem'  /* set of memory locations */
  | 'enum' ID  /* enumerated type */
  | 'struct' ID  /* structure type */
  | 'union' ID  /* union type */
  | 'void'   /* use as pointer element-type and return type of a function */
  | '$seq' '<' type-name '>'  /* sequence of T */
  | '$set' '<' type-name '>'  /* set of T */
  | '$map' '<' type-name ',' type-name '>'  /* partial function from T1 to T2 */
  | '$rel' '<' type-list '>'  /* relation: set of n-tuples with specified component types */
  ;
declarator '*'* direct-declarator ;
direct-declarator:
    ID  /* variable being declared */
  | direct-declarator '[' expr? ']'  /* array of ... */
  | direct-declarator  '(' type-list? ')'  /* function consuming ... and returning ... */
  | '(' declarator ')'
  ;
type-name: ... /* same as declarator but without the ID */
type-list: type-name (',' type-name)* ;

Notes

• Sequences, sets, maps, and relations are immutable. An assignment using objects of this type creates a new copy of the object, just as with primitive types like int.
• The main difference between the array type and the sequence type is that elements of an array are addressable, i.e., one can form a pointer such as &a[i]. This is not possible with sequences, sets, maps, or relations---there is no way to have a pointer to any component of such a type.
• The difference between the function type and map type: a function is really a procedure in the language, so it can modify the state as well as return a value. This is like the C notion of "function". A map is a logical partial function: it is defined on some subset of the domain type, it will always "return" the same value on a given input, and reading it cannot modify the state.

Statements

primitiveStmt:
    ';'  /* noop */
  | lvalue '=' expr ';'  /* assignment */
  | expr '(' arg-list? ')' ';'  /* function call */
  | (lvalue '=')? '$spawn' expr '(' arg-list? ')' ';'  /* process creation */
  | 'return' expr? ';'  /* return from function call */
  | '$parspawn' expr ',' expr ',' expr ';'  /* parallel spawn */
  | (lvalue '=')? '$alloc' '(' expr ',' expr ',' type-name ')' ';'  /* heap allocation */
arg-list: expr (',' expr)* ;  /* actual argument list */

Notes

• For function calls and spawns, the first expression shall have type pointer-to-function-.... The function pointed to will be the one called or spawned.
• The 3 expressions in a $parspawn are (1) pointer to the first element of the process array, an expression of type $proc*, (2) an expression of type $domain, and (3) an expression of type pointer-to-function-.... The function must have the type that consumes n $ints, where n is the dimension of the domain, and returns void. The function is spawned once for each element of the domain. References to the new processes are stored in the process array.
• The first expression following $alloc has type $heap*. It is a pointer to the heap that will be modified by allocating the new memory. The second expression has type $int and is the number of elements being allocated. This is followed by the element type. The function returns a pointer to the first element of an array, similar to C's malloc. It is deallocated using function$free.

Built-in functions:

void $assert( $bool asserted_expr, ... );  /* assertion with optional error message */
void $assume( $bool expr );  /* assumption */
void $wait( $proc p );  /* wait until p terminates */
void $waitall( $int nprocs, $proc * procs );  /* wait for all procs in list to terminate */
void $free( void * ptr );  /* frees something that was $alloc-ed */

Expressions

expr:
    $new(type-name)  /* returns a new arbitrary value of the given type */
  |