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.

Grammar

program: typedef* decl* fundef+ ;
typedef:
    enum ID '{' idnetifier-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 ;
INT: ... /* integer constant */
ID: ... /* identifier */
contract-clause :
    '$assigns' expr ';' 
  | '$requires' expr ';'
  | '$ensures' expr ';'
   ...

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: '*'* ID ('[' ']' | '(' type-list? ')')* ;
type-name: type-specifier '*'* ('[' ']' | '(' type-list? ')')* ;
type-list: type-name (',' type-name)* ;
complete-type-name: type-specifier '*'* ('[' expr ']' | '(' type-list? ')')* ;

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.

Questions

• how to allocate an array
• how to initialize a variable (what are initial values?)
• how to go between sequences and arrays
• can you make types values? (reification)

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: