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* vardecl* fundef+ ;
block: '{' typedef* vardecl* fundef* statement* '}' ;
statement: block | basicStmt ;
basicStmt:  (ID ':')? (simpleStmt | chooseStmt | gotoStmt) ;
gotoStmt: 'goto' ID ;
simpleStmt: (guardedStmt | primitiveStmt) gotoStmt? ;
guardedStmt: 'when' expr 'do' primitiveStmt ;
chooseStmt: 'begin choose' simpleStmt+ 'end choose' ;
typedef: 'type' ID '=' typeName ';' ;
vardecl: 'var' varopts? ID ':' typeName ';' ;
varopts: '[' varopt+ ']' ;
varopt: 'input' | 'output' ;
fundef:  'fun' funopts? ID '(' paramlist ')' (':' typeName)? conclause* block ;
funopts: '[' funopt+ ']' ;
conclause : 'assigns' expr ';' 
          | 'requires' expr ';'
          | 'ensures' expr ';'
          ...

Types

• $bool : boolean type ($true and $false, unrelated to integers)
• $char : character type (Unicode characters, unrelated to integers)
• $int : mathematical integers
• $real : mathematical reals
• $float<e,f> : IEEE floating-point numbers e=significand bits, f=exponent bits
• $herbrand<T> : 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 tag : enumerated type
• struct tag : structured type, can also be used for "tuples"
• union tag : union type
• T[] : array of T
• void * : pointer to anything
• T * : pointer to T
• T(T1, ..., Tn) : function (aka procedure) consuming T1, ..., Tn and returning T
• $seq<T> : sequence of T
• $set<T> : set of T
• $map<T1,T2> : map from T1 to T2
• $rel<T1, ..., Tn> : relation, set of n-tuples

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)