The CIVL-IR language. A program in this language is also known as a "CIVL model".

Properties of the language:

• the language is not intended to be written by humans; it is an intermediate form constructed by CIVL. However it should be readable to help debug things
• a CIVL-IR program represents a guarded-transition system explicitly
• as in CIVL-C, there are functions, scopes, and functions can be defined in any scope
• all blocks (including a function definition) consist of the following elements, in this order:
  • a sequence of contract clauses (for function definitions only)
  • a sequence of type definitions
  • a sequence of variable declarations (with no initializers)
  • a sequence of function definitions
  • a body, which encodes a program graph.
• an array is declared without any length expression. When it is initialized it can specify length.
• curly braces are used only to indicate scopes, as in { // new scope ... }
• parentheses are used to indicate function invocations, as in add(x,y)
• angular brackets are used to delimit tuples or sequences
• square brackets are used to delimit parameters in types
• unlike C, there is no "array-pointer pun". If an array a needs to be converted to a pointer, you must use addr(asub(a, 0)).
• 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 defined, 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.

Grammar

This is not the complete grammar, but the high-level overview.

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 ';'
          ...
          ;

Notes:

• If goto is missing, default is the next location.
• If guard missing, default is true.

Example:

fun f(u:Integer, a:Array[Real]): Integer {
  var x: Real;
  var y: Real;
  var z: Float[16,23];
 
L1 :
  begin choose
    when g1 do stmt1; goto L2;
    when g2 do stmt2; goto L3;
  end choose

  { // begin new scope
    x: Real;
L2 :
    stmt3; goto L4;
    ...
  } // end new scope
...
}

Example: the C code

{
  int x=3*y;
  int a[x+1];
}

could be represented as

{
  var x: Integer;
  var a: Array[Integer];

  ASSIGN "x", mul(3,"y");
  ASSIGN "a", new(dytype(Array[Integer, add("x",1)]));
}

Types

The types (and their type names) are:

• Bool : boolean type, values are true and false
• Proc : process type
• Scope : scope type
• Char : character type
• Bundle : type representing some un-typed chunk of data
• Heap : heap type
• Range : ordered set of integers
• Domain : ordered set of tuples of integers
• Domain[n], n is an integer at least 1; subtype of Domain in which all tuples have arity n.
• Enum types.
  • different from integers or like C
• The numeric types
  • The integral types
    • Integer : the mathematical integers
    • Int[lo,hi,wrap]
      • lo, hi are concrete integers, wrap is boolean
      • finite interval of integers [lo,hi]. If wrap is true then all operations "wrap", otherwise, any operation resulting in a value outside of the interval results in an exception being thrown.
      • lo and hi can be any values of type Integer, so they are dynamic types, like complete array types
  • The real types
    • Real : the mathematical real numbers
    • Float[e,f], e, f are concrete integers, each at least 1.
      • IEEE754 floating point numbers. This type includes NaNs, negative 0s, infinities, etc.
  • Herbrand[T], for a non-Herbrand numeric type T
    • the values of this type are (unsimplified) symbolic expressions. Each numeric operator is treated as an uninterpreted function. The leaf nodes in an expression are values of type T. Two values are equal iff the two symbolic expressions are identical (using equality in T on the leaf nodes). A value of Herbrand type may therefore be thought of as representing an expression in T but where all the numerical operations have been "delayed".
• Tuple[<T0, T1, ...>]: a tuple type, the Cartesian product of T0, T1, ...
  • What about bit-widths?
• Union[<T0, T1, ...>]: union type, the disjoint union of T0, T1, ...
• Array[T] : arrays of any length whose elements belong to T
  • Note: there is also a dynamic type Array[T,n], signifying arrays of length n. That is a subtype of the dynamic type of Array[T].
• Function[<T0,T1,...>,T] : functions consuming T0,T1,... and returning T.
  • T can be absent. Function[<T0,T1,...>] means the function returns nothing.
• Mem : type representing a memory set. May be thought of as a set of pointers.
• Pointer : all pointers, a subtype of Mem
• Pointer[T] : pointer-to-T, subtype of Pointer
• Dytype : the set of all dynamic types
• Dytype[T]: dynamic types refining T, for a static type T.
  • Values of this type represent dynamic types that refine T. For example dytype(Array[Integer,24]) has static type Dytype[Array[Integer]]

Type facts:

Static types are the types assigned to variables in a program statically. A static type contains no values anywhere in the type tree. That is, there is no array length expression in the type. These are the types that are used in declarations. Each variable is declared to have some static type.

Value types (aka dynamic types) are the types associated to values. They include all the static types plus possible array lengths. A value type refines a static type if when you delete the values from the value type you get the static type.

A type name is a syntactic element that names a (static or value) type. Examples of type names include Array[Integer] and Array[Integer,24].

The expression new(t) takes a Dytype and returns an unconstrained value of that type.

Example: the C code

int n = 10;
struct S { int a[n]; };
struct S x1;
n=20;
struct S x2;

may be translated as

type S=Tuple[<Array[Integer]>];

var n: Integer;
var S_d: Dytype[S];
var x1: S;
var x2: S;

ASSIGN "n", 10;
ASSIGN "S_d", dytype(Tuple[<Array[Integer, "n"]]>);
ASSIGN "x1", new("S_d");
ASSIGN "n", 20;
ASSIGN "x2", new("S_d");

Example of self-referential data definition, a linked list:

type Node=Tuple[<Integer,Pointer[Node]>];

Expressions

In the following list of expressions, e, e0, e1, etc., are expressions. T is a type name. t is an expression of type Dytype.

Logical

• true, false : literal values of type Bool
• not(e) : logical not
• and(e1,e2), or(e1,e2): logical and/or operation.
  • These operators are short-circuiting, which matters because of exception side-effects.
• implies(e1,e2): logical implication. Short-circuiting.
• eq(e1,e2), neq(e1,e2): equality/inequality test
• forall(<i1:T1,i2:T2,...>,e) : universal quantification. For all i1 in type T1, i2 in type T2, ..., e2 holds.
• exists(<i1:T1,i2:T2,...>,e): existential quantification. There is some i1 in type T1, i2 in type T2, ..., such that e holds.

Numeric

• -? digit+: values of types Integer and Int: [+|-]? digit+, e.g., 123, -123
• -? digit+ . digit+: values of types Real and Float, e.g., 3.1415, -0.9875
• add(e1,e2) : numeric addition.
  • e1 and e2 have the same numeric type. Note that there are no "automatic conversions" as there are in C. If the original expressions have different types, explicit conversions must be inserted.
• sub(e1,e2) : subtraction
• mul(e1,e2) : multiplication
• div(e1,e2) : division
  • If both are integral types, the result is integer division. Otherwise it is real division. Need to define what happens for negative integers.
• mod(e1,e2) : integer modulus. Arguments may be Integer or any Int type. They must have the same type, which is also the type of the result.
• neg(e) : negative. Argument may have any numeric type; result has same type.
• lt(e1,e2), lte(e1,e2): less than/less than or equal to. Arguments must have same numeric type.
• round(e,t): returns value in numerical type t that is "closest" to the given value e
  • add argument for rounding mode?
  • exception if out of range?
• floor(e) : given a real or floating number, returns the greatest Integer less than or equal to it.
• ceil(e) : given a real or floating number, returns the least Integer greater than or equal to it.
• abs(e): given any numeric expression e, returns the absolute value; result is same type as e.
• pow(e,n): power operator
  • given any numeric expression e and expression n of any integral type, returns e to the n-th power.
  • n must evaluate to a nonnegative integer.
• herbrand(e): "Herbrandize" a numeric value.
  • given a numeric value of type T, returns the value as type Herbrand[T], a trivial symbolic expression consisting of a single node.
• eval(e) : evaluate a Herbrand expression
  • given a value of type Herbrand[T], returns the value of type T obtained by evaluating all the delayed operations
  • exceptions may be thrown if evaluating any of the delayed operations results in an exception

Characters and Strings

• 'a', 'b', ... : Char values.
  • \u00ea, \u00f1, ...: Unicodes
• string("abc") : string literals
  • value of type Array[Char, n+1], where n is the length of the string (the last element is the character \0)

Ranges and Domains

• range(e1,e2,e3) : value of type Range.
  • If e3 is positive, the integers e1, e1+e3, e1+2*e3, ... that are less than or equal to e2. If e3 is negative, the integers e1, e1+e3, e1+2*e3, ... that are greater than or equal to e2. Exception if e3 is 0.
• domain(<r1,...,rn>) : value of type Domain[n], the Cartesian product of the n ranges, with dictionary order

Arrays (which are also Sequences)

• array(T,<e0,...,en-1>): value of type Array[T, n], a literal array
• array(T,n,e): value of type Array[T,n] in which each of the n elements is e
• asub(e1,e2) : array subscript expression.
  • Note that e1 must have array type, not pointer type. (This is different from C.) If e1 has pointer type, use deref(padd(e1, e2)) instead.
• seq_add(a,e) : array obtained by adding element e to the end of the array. Original array a is not modified.
• seq_append(a1,a2) : array obtained by concatenating two arrays. Original array not modified.
• seq_remove(a,i) : array obtained by removing element at position i from a. Original array a not modified.
• seq_insert(a,i,x) : array obtained by inserting an element x at position i in a.
• seq_length(a) : returns length of array a (an Integer)
• bitv_and(e1, e2), bitv_or(e1, e2), bitv_xor(e1, e2), bitv_comp(e1) : bit-wise operations
  • arguments are arrays of booleans of the same length
• bitv_shiftl(a,n) : left shift of a bit vector
  • a is a bit vector, i.e., array of boolean
  • n has integral type and is nonnegative
  • exception if n is greater than the length of a
  • new spaces created are filled in with false
• bitv_shiftr(a,n) : right shift of a bit vector
• int_to_bitv(len, val) : returns a bit-vector (array of boolean) of length len from val
  • val must be a non-negative integer value from an integral type
  • len must be large enough to contain the base-2 expansion of val
• bitv_to_int(a,t) : converts a bit vector to an integer
  • a is a bit vector, i.e., an array of boolean
  • t has type Dytype and evaluates to an integral type large enough to hold the result of converting a to a non-negative integer

Tuples

• tuple(S,<e0,e1,...>) : value of tuple type S (tuple literal)
• tsel(e1,i) : tuple selection of component i of e1. i must be a literal natural number.

Unions

• union_inj(U,i,x) : x is in Ti, result is in the union type U
• union_sel(U,i,y) : y is in U, result is in Ti (or exception if y is not in image of injection from Ti)
• union_test(U,i,y) : y is in U; determines if y is in the image under injection of Ti. Returns a Bool.

Pointers and Memory

• null : value of type Pointer
• deref(e) : pointer dereference
• addr(e) : address-of operator
• padd(e1,e2): pointer addition.
  • e1 has pointer type and e2 has an integer type or range type.
  • If e2 has integer type the result has pointer type. Otherwise, the result has Mem type. (BETTER TO USE A DIFFERENT FUNCTION?)
• psub(e1,e2): pointer subtraction
  • Both args must have same type Pointer[T] for some T.
  • Result has type Integer
• 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.

Scopes and Processes

• root, here, scope_null : values of type Scope
• self, proc_null : values of type Proc
• scopeof(e): scope of left-hand-side expression e
• scope_eq(e1,e2) : equality of two dyscopes
• scope_lt(e1,e2) : is first scope a proper subscope of second?
• scope_lte(e1,e2): is first scope a subscope or equal to second?

Types

• new(t) : new unconstrained value of Dytype t. If t has type Dytype[T], then this expression has static type T.
• typeof(e) : returns the value of type Dytype representing the value type of e.
  • If e has static type T then this expression has static type Dytype[T].
• subtype(t1,t2): is t1 a subtype of t2? Both args have type Dytype. Returns a Bool
• sizeof_type(t) : the size of the dynamic type t; return an Integer
• cast(e,t) : casts e to a value of dytype t.
  • If t has type Dytype[T], this expression has static type T and the value will have dynamic type t.
  • A cast can only take place when there is no change to the underlying value in the concrete semantics. It is only for changing the type.
  • One can cast from any integral type to another (as the values in all cases are integers), but there might be an exception if the value is not in the range of the targeted type.
  • One can cast any Float value to a Real value, but not the other way. (To convert from a Real to a Float, use, e.g., round.)
  • One cannot cast from one Float type to another Float type (unless the float parameters are exactly the same). To do this, one could instead use round.
  • If t1 is a subtype of t2, one can always cast from t1 to t2 (though this is rarely necessary, since an expression of type t1 can be used wherever one of type t2 is expected). One can also cast from t2 to t1, but a runtime exception will be thrown if the value being cast does not already belong to t1. For example, one might cast from Domain to Domain[n], or from Array[Real] to Array[Real, n].
  • One cannot cast between a Herbrand type and any other type. Instead, use functions eval and herbrand.

Other expressions

• "x" : x is an identifier, naming either a type, variable, or function
• sizeof_expr(e) : the size of the value of expression e; return an Integer
• ite(e1,e2,e3): if-then-else (conditional) expression, like e1?e2:e3 in C.
  • e1 must have Bool type. e2 and e3 must have the same static types, which is the static type of the result.
• invoke(e0,<e1,...,en>) : function call
  • a function invocation where e0 must evaluate to either an abstract or pure system function

The Primitive Statements

• ASSERT e, "msg", ...; : assertion with message
• ASSUME e;
• ASSIGN e1,e2;
• CALL f, <e1,...,en>; and CALL e, f, <e1,...,en>;
  • call to a function which is not abstract and is not a pure system function. The first form has no left-hand-side. The second form assigns the result returned by the call to e.
• SPAWN f, <e1,...,en>; and SPAWN e, f, <e1,...,en>;
• WAIT e;
• WAITALL e, n; : wait on all procs in a list
  • e has type Pointer[Proc] and n has an integral type, the number of procs in the list
• ALLOCATE e, s, t, e0;
  • e has static type Pointer[T], for some static type T
  • s has type Scope
  • t has type Dytype[T], for the same static type T
  • e0 has an integral type.
  • Allocates e0 objects of type t on the heap of s, returning pointer to first element in e.
  • To translate the C malloc you first need to figure out the type of the elements being malloced. If the argument to malloc is n, then you first need to insert an assertion eq(mod(n, sizeof_type(t)), 0), and then ALLOCATE e, h, t, div(n, sizeof_type(t)).
• FREE p;
• EVAL e; : evaluates an expression e
  • useful only because e might contain exceptions (e.g., array index out of bound, division by zero)
• NOOP; or NOOP LABEL;
  • a no-op can take an optional label, which is one of the following:
    • TRUE_BRANCH_IF: to enter the true branch of a CIVL-C if-else statement;
    • FALSE_BRANCH_IF: to enter the false branch of a CIVL-C if-else statement;
    • LOOP_BODY_ENTER: to enter the body of a loop;
    • LOOP_BODY_EXIT: to exit from the body of a loop.
• RETURN; and RETURN e;
• ATOMIC_ENTER;
• ATOMIC_EXIT;
• PARSPAWN p, d, f; : spawn a sequence of procs, one for each element in a domain
  • p has type Pointer[Proc], d has Domain type and f has Function type.
  • the new procs are entered into p[0], p[1], ..., p[d-1], where d is the size of the domain. Hence p must point into an array of Proc big enough to hold d elements.
  • the function f must have the following signature: it consumes n Integers, where n is the dimension of the Domain d. It returns nothing.
• NEXT <i,j,...>, dom, flag; : move to next element in domain
  • i,j,... have integral types
  • dom has type Domain[n], where n is the number of variables in the sequence i,j,...
  • flag has type Bool
  • if flag is false in the pre-state, this indicates you want the first element of the domain
  • if flag is true in pre-state, this indicates you want the next element after current <i,j,...>
  • flag=false in post-state indicates there is no next element
  • flag=true in post-state indicates the next element is in <i,j,...>

Notes on translation:

The CIVL-C code $parfor(int i,j: dom) S; is translated into the following:

  var p:Array[Proc];

  fun f(i: Integer, j: Integer)
  {
    S;
  }

  PARSPAWN addr(asub(p,0)), dom, f;
  WAITALL addr(asub(p,0)), domsize(dom);

The CIVL-C code $for(int i,j: dom) S; is translated into the following:

{
  var i:Integer;
  var j:Integer;
  var flag:Bool;

  flag=false;
L0:
  NEXT <i,j>, dom, flag;
  when not(flag) do NOOP; goto L1;
  S;
  goto L0;
}
L1:

Function Definitions

The general form of a function definition:

fun[options] foo(x:Integer, ...) : Real
  // contract clauses (optional):
  Requires expr;
  Ensures expr ;
  MPI_requires expr ;
  MPI_ensures expr ;
  Behavior name:
    Assigns expr ;
    Reads expr ;
    Depends actions ;
{
  // all of the following are missing for a system function...

  // types defns:
  type T=tuple[<blah, blay>];
  type U=blah;

  // variable decls:
  var x : T;
  var y : U;

  // body:
  ASSIGN x, 0;
  ...
}

To specify a function returning nothing, simply leave out the return type part. For example: fun foo(x:Intger, ...) {...}.

Example of declaration of a system function defined in library Concurrency:

fun[package="edu.udel.cis.vsl.civl.lib", lib="Concurrency"] f(x: Real, b: Bool): Float[32,33] {}

Function modifiers that may be placed in the brackets after fun:

• state_f : the value returned by the function is a deterministic function of the inputs (so cannot depend on the state in any way), and furthermore the function has no side-effects. So this is just like a mathematical function. (This is intended to be used for system functions, but can it also be used for non-system functions?)
• abstract: an uninterpreted pure function. The result of a function call on such a function is a symbolic expression "f(arg1, ...)". There is no definition for such a function, not even a system definition.
• atomic: function definition is atomic, and it never blocks. A function call to such a function occurs in a single atomic transition. It is slightly different than a function in which the entire body is atomic, because in the latter case the call and return happen as two separate transitions.
  • Since every system function is atomic, this option is only useful for non-system functions.
• package="...": the package where a system function is implemented
• lib="...": function is a system function defined in specified library
• guard="...": the name of the guard function
• main : this is the program entry point (global scope only)

System functions:

• A function declaration which contains an option lib=... is a system function
• A system function will have no body. It may have any number (including 0) of contract clauses.
• If the system function is called anywhere in the program, it must be defined by providing Java code in an Enabler and Executor. Failure to do so will result in an exception.
• A system function may modify only memory it can reach. This includes allocating new data on heaps it can reach. This modifiable memory can be further limited by the contract.
• A system function may have a guard, which is another function taking the same types of inputs, but returning Bool.

Example of a declaration of a system function with guard.

fun g(x:Real):Bool { ... }
fun[lib="Blah",guard="g"] f(x:Real):Integer {}

Function Contracts:

• Function_Contracts

Program

A program consists of a sequence of type definitions, followed by a sequence of variable declarations, followed by a sequence of function definitions. This is called the "global scope."

The variable declarations in the global scope may use the options

• input
• output

There must be exactly one global function definition with option main. This function must consume no inputs and return an Integer (check this).

Semantics

Semantics issues

• define every possible cast
• define every possible +, etc.
• define every kind of pointer value and casts between pointer types
• casts between pointer and integer types?

Values

Transitions

Libraries

Library_IR

Which libraries require system functions? pointer, ... Should these be called part of the language, or not?

Questions

• fix notation for contracts
• quotes around variables in declarations? Could be awkward but might simplify parsing.
• quotes around function names in definitions, prototypes? Could be awkward.
• is there ever a need for a function prototype? Could variable decl notation be used instead? NO, variable decls are different, those are state variables.
• should we leave our parameter names in abstract and system functions? They are not needed for anything. THEY ARE NEEDED FOR CONTRACTS, sometimes, and maybe for documentation. Consider making them optional.