CIVL IR v2.0

Language principles

• CIVL-IR is a subset of CIVL-C. A CIVL-IR program is a CIVL-C program, and has the same semantics.
• CIVL-IR should be a small language. Whenever there is a way to express a new construct using other existing constructs, the preferred approach is to not add the new construct to the language.
• CIVL-IR is to be as close as possible to a language representation of a CIVL "Model". This is the lowest-level representation of a CIVL program, one appropriate for efficient (symbolic) execution and/or model checking.
• The basic representation of a function is as a "program graph"---a directed graph in which the nodes are locations and edges are atomic statements.
• Expressions are side-effect free.
• There are no automatic conversions. All conversions must be by explicit casts or other functions. Operations such as numeric addition (add) require that both operands have the exact same type.
• In general, symbols can be used before they are declared, as long as they are in scope. For example, a function f can call g, even if g is defined after f in the same scope. There is no need for a "prototype". Similarly, a type definition can refer to a type defined later, or can refer to itself in its own definition.
• Many of the core operations are implemented as functions in the standard library. This is similar to C. The header files for the standard library are an integral part of the language.
• Evaluation of expressions and execution of statements should always result in a value or state. There is no concept of exception or error. Hence anything that should be checked should be checked by explicit assertions.

Questions

1. Do variables have default initial values?
   • An object variable may or may not include an explicit initializer. If it does not include an initializer, the variable is initialized with an undefined value. Even in this case, the variable has some unspecified value of its type, but its "defined" bit is false.
2. How do you initialize a variable?
   • In the declaration. For example $int n=$fresh($int); will initialize n with an arbitrary integer, while $int n=$new($int); will initialize n with an undefined integer, and $int n=0 will initialize n with 0.
3. How is an array allocated?
   • An array variable a is declared with a decl such as T a[] = $new(T[n]); which assigns to a a new array value for an array of length n of elements of type T in which all entries are undefined. (Alternatively, T a[] = $fresh(T[n]) will create an array of arbitrary defined values.)
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 write something like &a[0].
5. How to you translate between sequences and arrays?
   • There are functions in the standard library to do that.
6. Can you make types values? (reification)
   • Yet, using $typeof(T) which returns a value of type $type<T>.
7. How do you monitor reads and writes?
   • There are functions in the standard library (mem.h) for this. [TODO]
8. Is there a type for $state ?
   • Coming soon. [TODO]
9. How do you model malloc when the element type is not known?
   • There will be a general$object type. [TODO]
10. How do you iterate over a domain?
    • [TODO]
11. Bitvectors?
    • [TODO]

Grammar

program: param* typedef* decl* function-definition+ ;
param: '$param' type-specifier declarator ('=' constant-expr)? ';' ;
typedef:
  type-param-list?
  ( struct ID '{' decl* '}'
  | union ID '{' decl* '}'
  | 'typedef' type-specifier declarator
  )
  ';'
  ;
decl: function-decl | object-decl ;
function-decl: type-param-list? function-kind function-qualifier*  type-specifier declarator contract-clause* ';' ;
function-kind:
    '$abstract_f'  /* abstract function; only for function decls */
  | '$system_f' '<' STRING ',' STRING '>'  /* function is defined in system code elsewhere */
  ;
function-qualifier:
    '$pure_f'  /* function is a mathematical function of its parameters */
  | '$state_f'  /* function is a mathematical function of the state */
  | '$atomic_f'  /* function invocations take place atomically */
  ;
object-decl: type-qualifier? type-specifier declarator ('=' expr)? ';' ;
function-definition: type-param-list? function-qualifier* type-specifier declarator contract-clause* block ;
block: '{' typedef* decl* function-definition* statement* '}' ;
statement: block | simpleStmt | chooseStmt ;
simpleStmt: label? dependency? guard? primitiveStmt gotoStmt? ;
chooseStmt: label? '$choose' '{' simpleStmt* '}' ;
label: ID ':' ;
guard: '$when' '(' expr ')' ;
dependency: '$depends_on' '(' expression-list? ')'
expression-list: expr (',' expr)* ;
gotoStmt: 'goto' ID ;
type-param-list: '<' type-param (',' type-param)* '>' ;
type-param: ('$typename' | '$int') ID ;
INT: ... /* integer constant */
ID: ... /* identifier */
STRING: ... /* string literal in double quotes */

Notes

• Parameters are named constants. They can be assigned a constant value, or can be left unconstrained. A parameter looks like a variable but can never be assigned and its address cannot be taken. A constant expression is one comprised of constants, parameters, and a few basic operations, including addition, multiplication, division, modulo, and subtraction.
• A typedef can be used to define parameterized types. The type parameters are listed between angular brackets preceding the typedef. When the identifier is later used, it must be used with angular brackets and actual type names to replace the type parameters.
• A declaration declares a variable to have either an object type or a function type. (An object type is any type that is not a function type.)
• The optional type-param-list in a declaration may be applied only to a declaration of function type. It declares a "generic" function. When the function is called (or spawned), the call must include the angular brackets with a list of type names that replace the type parameters used in the declaration or definition of the function.
• A variable of function type represents either an abstract or a system function. The declaration of such a variable must use either the qualifier $abstract_f or $system_f. Moreover, those two qualifiers can only be used in a declaration of function type.
• An abstract function represents a new uninterpreted pure function.
• A system function has no definition in the program, 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.
• $atomic_f can only be used in a function definition. It indicates that a defined function is to behave atomically, i.e., every call to such a function will be executed as if in atomic region. (An abstract or system function must necessarily be atomic.)
• $pure_f can be applied to a system function or defined function only. (An abstract function is necessarily pure.) The use of $pure_f indicates that the function has no side-effects, and the value returned in a mathematical function of the arguments. If the function is not actually pure, the behavior is undefined.
• $state_f can be applied to a system function or defined function only. It declares that the function has no side-effects, and the value returned is a mathematical function of the state in which the call occurred; i.e., the value returned may depend on the arguments in the call, the values of global variables, or any other component of the state. But, if called twice from the same state, it will always return the same value. If the function does not actually have this property, the behavior is undefined. Any $pure_f function is necessarily a $state_f, so at most one of these two qualifiers can occur in a declaration or definition.
• Contract clauses can occur only with system functions and defined functions (not with abstract functions, not with variables).
• A program must contain a function definition for a function named main. (Signature?)
• The expr in a guard must have type $bool.

Contracts

contract-clause:
    '$assigns' '(' expression-list? ')'   /* frame condition */
  | '$requires' '(' expr ')'  /* precondition */
  | '$ensures' '(' expr ')'  /* postcondition */
  | '$depends_on' '(' expression-list? ')'  /* dependency specification */
  | '$when '(' ID ')'  /* guard clause */
  ;

Notes

• A guard clause can occur only in the declaration of a system function. The identifier is the name of the function that will be used as the guard in all calls to the system function. The guard function must have the same input signature as the system function, but must return $bool. Any call to the system function will block unless the guard function returns $true on the arguments used in the call. The execution of the system function and the return of "true" from the guard function will occur atomically, i.e., no state change will occur between the return of true and the call of the system function. The guard function must be a $state_f function; in particular, it must be side-effect free. The guard function may be a system function or a defined function; it cannot be abstract. If omitted, the guard is understood to be "true", i.e., a call to the system function will never block.
• The expressions in a dependency clause must have pointer type. This declares that the following transition depends only on the objects pointed to.

Types

type-specifier:
    ID type-args?  /* type parameter or (possibly parameterized) typedef use */
  | '$int' size-spec?  /* mathematical integers */
  | '$bool' size-spec?  /* boolean type ($true and $false, unrelated to integers) */
  | '$char' size-spec?  /* character type (Unicode characters, unrelated to integers) */
  | '$real' size-spec?   /* mathematical reals */
  | '$float' size-spec?  /* IEEE floating-point numbers */
  | '$proc'  /* process type */
  | '$heap'  /* heap type, for dynamic allocation */
  | '$mem'  /* set of memory locations */
  | '$type' '<' type-name '>'  /* a value type of a named static type */
  | 'struct' ID  type-param-list?  /* structure type */
  | 'union' ID  type-param-list?  /* 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-args  /* relation: set of n-tuples with specified component types */
  ;
size-spec: '<' expr '>' ;
declarator: '*'* direct-declarator ;
direct-declarator:
    ID  /* variable being declared */
  | direct-declarator '[' ']'  /* array of ... */
  | direct-declarator  '(' parameter-type-list? ')'  /* function consuming ... and returning ... */
  | '(' declarator ')'
  ;
abstract-declarator: '*'* abstract-direct-declarator ;
abstract-direct-declarator:
  | abstract-direct-declarator '[' expr? ']'
  | abstract-direct-declarator  '(' parameter-type-list? ')'
  | '(' abstract-declarator ')'
  ;
type-name: type-qualifier? type-specifier abstract-declarator ;
type-args: '<' type-arg (',' type-arg)* '>';
type-arg: type-name | expr ;
parameter-type-list: type-specifier declarator (',' type-specifier declarator)* ;

Notes

• Certain basic types can have a specified size---the number of bytes consumed by an object of that type. These basic types include '$bool', '$int', '$char', and '$real'. Two versions of the basic type with different sizes are in fact disjoint types. There is also a basic type without a specified size, and this type is distinct from all the sized types. Certain operations require a sized type (specify these!).
• Sequences, sets, maps, relations, and $mem objects are immutable. An assignment using objects of this type creates a new copy of the object, just as with primitive types like $int.
• Arrays are similar to sequences. The main differences are as follows:
  • An object (i.e., a variable or component of an object) of array type is initialized once, then will never be assigned to again. Hence there cannot be a statement of the form a=... where a has array type. (Except for the first one?)
  • After initialization, an object of array type can appear only as the first (left) argument to the subscript operator [] or as the argument to the $length operator.
  • Arrays are mutable. As in C, the left hand size of an assignment may have the form a[i], where a is an object of array type. Sequences are immutable.
  • 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.
  • A function may neither consume nor return an object of array type. [why?] There is no such restriction for sequences.
• The difference between the function type and map type:
  • a function cannot return a function; nor can a function consume an argument of functional type [why?]
  • a function may return a pointer to a function and may consume an argument of type pointer to function...
  • a function pointer is formed by &f, where f is the name of a function
  • there is no pointer arithmetic on function pointers
  • a map has a finite number of entries
  • a map cannot be executed in a call or spawn; nor can functions on maps have any side effects
  • a function can return a map and can consume an argument of map type
• A type name in a type-args list may be void. In this case, the type name designates the type whose domain is the union, over all types T of the type name obtained by substituting T for void. For example, the domain of $seq<void> is the union over all types T of $seq<T>. The sequence {1,2,3} is in the domain of $seq<$int> and of $seq<void>. The sequence {1,3.14} is not in $seq<void> since there is no type T containing $int and $real. Hence $seq<void> is a super type of all $seq<T>, and an expression of type $seq<T> can be used where one of type $seq<void> is required. It is similar to the relation between void* and T*.
  • A "bundle" type is not needed. A bundle is just a $seq<void>.
  • A message in an MPI communication might be represented as an element of type $seq<$seq<void>>. That is, a sequence, each element of which is a sequence of elements of the same type. An example of a message would be {{1,2,3}, {3.14,2.7},{'a','b','c'}}.
  • A general C "object" might be represented as a structure

    struct $object {
      $int size; // number of bytes
      $map<$int, $seq<void>> data; // offset (in bytes), contiguous values
    };
    

• A pure type name is one in which the optional length expression for an array type never occurs. Type arguments in angular brackets must be pure types. Declarations are pure types by the grammar.
• A complete type name is defined recursively as follows: a struct or union type is complete if and only if all the member types are complete; an array type is complete if and only if the element type is complete and the length is specified; all other types are complete.

Statements

An lvalue is an expression that represents an object, as in C. It is either a variable, an array element expression, a struct or union field expression, or dereference expression.

primitiveStmt:
    ';'  /* noop */
  | lvalue '=' expr ';'  /* assignment */
  | (lvalue '=')? expr type-args? '(' expression-list? ')' ';'  /* function call */
  | lvalue '=' '$spawn' expr type-args? '(' expression-list? ')' ';'  /* process creation */
  | '$wait' expr ';'  /* wait until p terminates */
  | 'return' expr? ';'  /* return from function call */
  | '$atomic_enter' ';'  /* enter atomic region */
  | '$atomic_exit' ';'  /* exit atomic region */
  | '$yield' ';'  /* release atomic lock */
  | '$assert' expr (',' expr)* ';'  /* assertion with optional error message */
  | '$assume' expr ';'  /* assumption */
  | '$assume_push' expr ';'  /* temporary assumption pushed on stack */
  | '$assume_pop' ';'  /* pop the temporary assumption stack */
  ;

Notes

• For function calls and spawns, the first expression shall have a functional type. That function must be a system or defined function (not an abstract function).

Expressions

expr:
  | ID  /* variable or function identifier */
  | '$true'
  | '$false'
  | INT
  | REAL
  | FLOAT
  | CHAR
  | STRING
  | 'NULL'
  | '$proc_null'
  | '(' type-name ')' expr  /* cast */
  | '(' type-name ')' '{' expression-list? '}'  /* concrete array, struct, $seq, $set, $mem */
  | '(' type-name ')' '{' expr-pair-list? '}'  /* concrete map */
  | '(' allocator ')' '$lambda' '(' '$int' ID ')' expr  /* array literal, aka array lambda */
  | '$lambda' '(' $decl+ (';' expr)? ')' expr   /* lambda expression */
  | expr '+' expr  /* numeric or pointer addition */
  | expr '-' expr  /* numeric or pointer subtraction */
  | expr '/' expr  /* division */
  | expr '%' expr  /* modulo */
  | expr '&&' expr  /* logical and */
  | expr '||' expr  /* logical or */
  | expr '==>' expr  /* logical implication */
  | expr '==' expr  /* equality */
  | '!' expr  /* logical not */
  | expr '<' expr  /* less than */
  | expr '<=' expr  /* less than or equal to */
  | expr '[' expr ']'  /* array element access */
  | expr '.' ID  /* field access */
  | '(' expr ')'
  | '-' expr  /* negative */
  | '*' expr  /* pointer dereference */
  | '&' lvalue  /* address-of */
  | expr type-args? '(' expression-list? ')'  /* application of abstract function (and perhaps other functions?) */
  | '$typeof' '(' type-name ')'  /* value type named by the extended type name */
  | 'sizeof' '(' (type-name | expr) ')'  /* C's sizeof expression --- number of bytes */
  | '$fresh' '(' (expr | type-name) ')'  /* returns a new arbitrary value of the given type */
  | '$new' '(' (expr | type-name) ')'  /* returns a new arbitrary and undefined value of the given complete type */
  | '$forall' '(' decl expr? ')' expr  /* universal quantification */
  | '$exists' '(' decl expr? ')' expr  /* existential quantification */
  | expr '?' expr ':' expr  /* if-then-else expression */
  | '$length' '(' expr ')'  /* length of array */
  | '$summable' '(' expr ',' expr ')'  /* is pointer addition p+i defined? */
  | '$subtractable' '(' expr ',' 'expr ')'  /* is pointer subtraction p-q defined? */
  | '$castable' '(' expr ',' type-name ')'  /* can expr be cast to type T? */
  | '$defined' '(' lvalue ')'  /* has the specified memory location been assigned? */
  | '$valid '(' expr ')'  /* does a pointer point to an object of its base type? */
  ;
expr-pair-list: expr-pair (',' expr-pair)* ;
expr-pair: '{' expr ',' expr '}' ;

Notes

• For operations on float types the rounding mode used is round-to-nearest.
• Comparisons likes == and < return a $bool (not an int, like C).
• Every object holds a value of its declared type, always. There is no notion of "trap representation", as in C.
• Evaluation of an expression always results in a value of the type of that expression. There are no "exceptions".
• For some operations, the result of applying the operation on certain inputs in unspecified. We say those applications are "unsafe". The result of an unsafe operation is unspecified, but will result in some value of the appropriate type. If an application is not unsafe, it is "safe".
• For every operation, there is a way to determine if performing that operation is safe. Hence an assertion on a certain expression can be checked before performing the operation. Examples:
  • a+b, for the $int, $real, or float types: always safe, assuming a and b are defined. Will will assume all objects are defined from now on.
  • a/b: b!=0
  • p+i (pointer arithmetic): $summable(p, i)
  • a[i]: 0<=i && i<$length(a)
  • p-q (pointer subtraction): $subtractable(p,q)
  • (T)e (cast): $castable(e, T)
  • *p: $valid(p) --- this means it is safe to write to *p. (It may not be safe to read *p because the object pointed to by p may not yet have been initialized.)
• Explanation of $defined:
  • A bit is associated to each object. We say an object is "defined" if the bit is true, else it is undefined.
  • An object is initially undefined. It becomes defined by assignment. If the right hand side of the assignment involves undefined objects, it is unspecified whether the left hand side will be defined.
  • Objects of pointer type can change from defined to undefined. This happens when the object into which they point is deallocated or goes out of scope. Likewise, an object of $proc type becomes undefined when a call to $wait on the process returns.
  • An object of array type becomes defined when assigned a $new_array. However, its elements are undefined.
  • An object of array type also becomes defined when assigned a $new value. In that case, the elements are also defined.
  • A pointer becomes defined when assigned the result of an $alloc. Each element in the newly allocated object is undefined.
  • Example: to determine whether it is safe to read *(p+i), assert $summable(p, i) && $valid(p+i) && $defined(*(p+i)). You must check (1) you can sum p and i, (2) p+i points to an object of the base type, so dereference is safe, and (3) the object is defined (has been assigned a value). If you aren't sure p and i have been defined, you can add $defined(p) && $defined(i) to the assertion. It may be more efficient to use temporary variables and break this up into multiple assertions.
  • $fresh and $new consume an argument expression of type $type<T> and return a value of type T. For $new, the argument must specify a complete type. $fresh accepts any extended type. $new(T), where T is a type-name, is syntactic sugar for $new($typeof(T)); ditto for $fresh(T).

Example: C code

typedef T mat[n][m];
mat a;

might be translated

typedef T mat[][];
$type<mat> _type_mat = $typeof(T[n][m]);
mat a = $new(_type_mat);

How to implement $defined using symbolic execution

Create a symbolic constant named UNDEF for each type T. These can be created on-the-fly, as they are needed.

A variable without initializer is initialized to the UNDEF of its type. The exception is a struct, which may be initialized to a concrete struct in which each field is UNDEF. (Either way will work, but the latter will probably be more effective.)

For a complete type T, the "undef-initializer" for T is defined as follows: if T is not an array type, the undef-initializer is defined exactly as above: either the symbolic constant UNDEF or a concrete struct of UNDEFs. If T is the complete array type S[n], the undef-initializer is the array-lambda expression with length n and defining expression the undef-initializer for S.

$new(T[n]) returns the undef-initializer for T[n].

Evaluation of $defined(expr) returns !FORALL UNDEF:T . expr == UNDEF, where T is the type of expr.

Allowed Casts

• between two types that are the same except for sizes of the basic types
• $int -> $real
• $float -> $real
• T1* -> T2*. How to check a cast is valid? What happens if it is not? If there are no exceptions, something must be returned. Perhaps undefined value.
  • this is OK if one is a pointer to element 0 of an array, and the other is a pointer to the array
  • if one is a pointer to the first member of a struct or union, and the other is a pointer to the struct or union
  • these rules can be applied recursively. This needs to be fleshed out.
• others?

Standard CIVL Library

civlc.cvh

Work in progress. Refer to existing library. All include$system<"civl.library", "civlc">.

$template <$typenameT1, $typename T2> struct $pair { T1 left; T2 right; };
$template <$typenameT1, $typename T2> typedef struct $pair<T1,T2> $pair;
$template <$typename T> $pure_f $int $sizeof($type<T> type);
$template <$typename T> T * $alloc($heap * h, T obj);  // add an object to a heap
$int $choose_int($int n);  // nondeterministic choice of int in 0..n-1
$free($void * p);  // remove an object from the heap
void $exit();  // terminate process immediately
$bool $terminated($proc p);  // has the process terminated?

Notes

A heap is an abstraction for a set of objects of possibly different types which can be referenced by pointers. $alloc adds an object to the heap and returns a pointer to that object. The object can then be read or modified using the pointer. Example: C code that mallocs 10 ints

int * p = malloc(10*sizeof(int));

could be modeled as

int * p;
int (*p1)[]; // pointer to array of int
p1 = $alloc(&heap, $new(int[10]));
p = &(*p1)[0];

More generally, if the type of objects being malloced is not known, or changes dynamically, one could define a general "object" type...

struct $object {
  $int size; // in bytes
  $map<$int,$seq<void>> data; // byte offset -> element sequence
}
typedef struct $object $object;

math.cvh

Work in progress...

Rounding modes:

• 0 = to nearest
• 1 = upward
• 2 = downward
• 3 = toward zero.

$int $round($real x); // round to nearest integer
$int $floor($real x); // greatest integer less than or equal to
$int $ceil($real x); // least integer greater than or equal to
<$int s> $float<s> $roundf($real x, $int mode);  // round to float (see modes above)
$real $abs($real x); // absolute value on reals
$int $absi($int x); // absolute value on integers
<$int s> $float<s> $absf($float<s> x); // absolute value on $float
$real $pow($real x, $int n);  // x to the n-th power.  n>=0
$int $powi($int x, $int n); //
<$int s> $float<s> $powf($float<s> x, $int n);
// trig functions? pi?

• What about Herbrand versions of above functions? Could we instead introduce an operator for power? ? Could make all of these functions part of the language instead (grammar).

mem.cvh

Work in progress...

• mem_reach(ptr), where ptr is an expression with a pointer type.
  • This represents the set of all memory units reachable from ptr, including the memory unit pointed to by ptr itself.
• mem_union(mem1,mem2), where mem1 and mem2 are expressions of type Mem.
  • This is the union of the two memory sets.
• mem_isect(mem1,mem1) : set intersection
• mem_comp(mem1) : set complement (everything not in mem1)
• mem_slice(a,dom)
  • where a is an expression of array type and dom is an expression of Domain type.
  • The dimension of the array must match the dimension of the domain. This represents all memory units which are the cells in the array indexed by a tuple in dom.

seq.cvh

The domain of $seq<T> consists of all finite sequences of values of type T.

<T> $int $seq_length( $seq<T> a ); // length of a
<T> T $seq_get( $seq<T> a, $int i ); // get element i of a
<T> $seq<T> $seq_set( $seq<T> a, $int i, T x ); // seq obtained by replacing element i of a with x
<T> $seq<T> $seq_subseq( $seq<T> a, $int start, $int stop ); // subsequence from start to stop-1
<T> $seq<T> $seq_add( $seq<T> a, T x ); // sequence obtained by adding element x to the end of a
<T> $seq<T> $seq_append( $seq<T> a1, $seq<T> a2 ); //  sequence obtained by concatenating a1 and a2
<T> $seq<T> $seq_remove( $seq<T> a, $int i ); // sequence obtained by removing element at position i from a
<T> $seq<T> $seq_insert( $seq<T> a, $int i, T x ); // sequence obtained by inserting element x at position i in a
<T> void $seq_write( $int n, T * ptr, $seq<T> a );  // write the first n elements of a to ptr, ptr+1, ..., ptr+n-1
<T> $seq<T> $seq_read( $int n, T * ptr ); // form a sequence by reading ptr, ptr+1, ..., ptr+n-1

set.cvh

The domain of $set<T> consists of all finite sets of values of type T.

<T> $int $set_size( $set<T> s ); // number of elements in s
<T> $seq<T> $set_seq( $set<T> s ); // elements of s arranged in a sequence
<T> $bool $set_contains( $set<T> s, T x ); // does s contain x as member?
<T> $bool $set_containsAll( $set<T> s1, $set<T> s2 ); // is s2 a subset of s1?
<T> $set<T> $set_add( $set<T> s, T x ); // result of adding x to s
<T> $set<T> $set_union( $set<T> s1, $set<T> s2 ); // union of s1 and s2
<T> $set<T> $set_intersection( $set<T> s1, $set<T> s2 ); // intersection of s1 and s2
<T> $set<T> $set_difference( $set<T> s1, $set<T> s2 ); // elements of s1 not in s2

map.cvh

The domain of $map<K,V> consists of all finite sets M of ordered pairs (k,v), where k is in K and v is in V, and satisfying: for all k in K there is at most one v in V such that (k,v) is in M.

<K,V> $set<K> $map_domain( $map<K,V> m ); // returns the domain of the map (the set of keys)
<K,V> $set<V> $map_range( $map<K,V> m ); // returns the range of the map (the set of values)
<K,V> $set<$pair<K,V>> $map_entries( $map<K,V> m ); // key value pairs of m arranged in a sequence
<K,V> $map<K,V> $map_put( $map<K,V> m, K k, V v ); // result of (re)defining k to map to v.
<K,V> $map<K,V> $map_putAll( $map<K,V> m1, $map<K,V> m2 ); // result of (re)defining k to map to v for every pair (k,v) in m2
<K,V> $map<K,V> $map_remove( $map<K,V> m, K k ); // result of declaring k undefined
<K,V> $map<K,V> $map_removeAll( $map<K,V> m, $set<K> ks ); // result of declaring k undefined for every k in ks
<K,V> $bool $map_contains( $map<K,V> m, K k ); // is k defined in the map?
<K,V> V $map_get( $map<K,V> m, K k ); // get the value defined at k (returns something if no k in domain)
? <K,V> $bool $map_injective( $map<K,V> m ); // does m form an injection?
? <K,V> $map<V,K> $map_inverse( $map<K,V> m ); // returns the inverse map of m. Should check $map_injective first (what do we do when m is not injective?)
? <K,I,V> $map<K,V> $map_compose( $map<I,V> m2, $map<K,I> m1 ); // returns the composition m2.m1

rel.cvh

$rel<X,Y> is an alias for $set<$pair<X,Y>>. Therefore, in addition to the functions defined specifically for $rel<X,Y> below, the $set API may also be used with $rel.

$template<$typename X, $typename Y> using $rel = $set<$pair<X,Y>>;
<X,Y> $set<X> $rel_domain( $rel<X,Y> r ); // Returns the set of x in X such that (x,y) in r for at least one y in Y.
<X,Y> $set<Y> $rel_range( $rel<X,Y> r ); // Returns the set of y in Y such that (x,y) in r for at least one x in X.
<X,Y> $set<Y> $rel_joinLeft( $rel<X,Y> r, X x); // Returns a $set<Y> B such that y in B iff (x,y) in r.
<X,Y> $set<X> $rel_joinRight( $rel<X,Y> r, Y y); // Returns a $set<X> A such that x in A iff (x,y) in r.
<X,Y> $rel<Y,X> $rel_inverse( $rel<X,Y> r ); // Returns the relation r' such that (y,x) in r' iff (x,y) in r.
<X> $rel<X,X> $rel_identity( $set<X> s ); // Returns the relation r such that (x,x) in r for every x in s.
<X,Y,Z> $rel<X,Z> $rel_join( $rel<X,Y> r1, $rel<Y,Z> r2 ); // Returns the relation r3 such that (x,z) in r3 iff (x,y) in r1 and (y,z) in r2 for some element y of Y.
<X> $rel<X,X> $rel_transitiveClosure( $rel<X,X> r ); // Returns the transitive closure of r.

concurrency.cvh

void $parspawn($proc * proc_array, $domain d, void (*f)($int, ...));  /* parallel spawn returns immediately*/
void $waitall( $int nprocs, $proc * procs );  /* wait for all procs in list to terminate */

• In$parspawn *f must have the function type that consumes n $ints, where n is the dimension of the domain. The function is spawned once for each element of the domain. References to the new processes are stored in the process array. The call to $parspawn returns immediately.

state.cvh

• $state: a first-class type in the language representing a program state

• $state $state_get(): returns a program state containing ONLY the current process state of the calling process. Equivalent to taking a snapshot of the calling process at the current state.

• $bool $state_eval_local($state s, void *buf, int size, void *out): reads the data of size from buf at state s and writes the data to out at the current state. Returns true iff the data being read is defined.

• $state $state_merge($state s, $state mono, int * place): merges the snapshot mono to the state s and returns the merged state. The process in mono is assigned a new place in the merged state. The new place is returned to the output argument place. Note that the mono state is not necessarily a state containing a single process. This function treats it as if it only contains a single process, i.e., this function only reads the process state of place 0 in mono.

• Remark 1: There is no way to let a process p to read data of a different process q in a $state through a pointer. So we still need a language construct like $state_eval(state, place, expr).

• Remark 2: To make the $state_eval_local function above more useful, we need functions to iterate elements in $mem objects. An element in a $mem object can be represented by a pair: a pointer and a size. The loop invariant transformer currently needs to write values from a $state to memory locations in a $mem object.