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 ';'
  | (lvalue '=')? '$malloc' '(' expr ',' expr ',' type-name ')' ';'
  

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 $malloc-ed */

Expressions

  expr: