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: type-qualifier? type-specifier declarator ';' ;
fundef: type-specifier declarator block ;  
block: '{' typedef* vardecl* fundef* statement* '}' ;
statement: block | simpleStmt | chooseStmt ;
simpleStmt: label? guard? primitiveStmt gotoStmt? ;
chooseStmt: label? '$choose' '{' simpleStmt* '}' ;
label: ID ':' ;
guard: '$when' '(' expr ')' ;  
gotoStmt: 'goto' ID ;
expr:
simpleStmt:
INT /* integer constant */
ID /* identifier */
conclause : '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 */
  ;
type-qualifier: '$input' | '$output' ;
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)