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
• the language (and grammar) are subsets of CIVL-C
• 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 body) consist of the following elements, in order:
  • a sequence of variable declarations with no initializers
  • a sequence of function definitions
  • a sequence of labeled $choose statements. Each clause in the choose statement is a $when statement with some guard and a primitive statement, followed by a goto statement
• an array is declared without any length expression. When it is initialized it can specify length.

Example:

$integer f() {
  $real x;
  $real y;
  $float(16,23) z;
 
L1 :
  $choose {
    $when (g1) stmt1; goto L2;
    $when (g2) stmt2; goto L3;
  }

  { // begin new scope
    $real x;

L2 :
    $choose {
      $when (g3) stmt3; goto L4;
      ...
    }
  } // end new scope
...
}
// etc.

Static Types

• $bool : boolean type, values are $true and $false
• $proc : process type
• $scope : scope type
• $char : character type. Alternatively, get rid of this and just use an integer type.
• $mem : type representing set of memory units
• $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 above in which all tuples have arity n.
• enum types.
  • different from integers or like C?
• $integer : the mathematical integers
• $int(lo,hi,wrap)
  • lo, hi are 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.
• $hint : Herbrand integers. Values are unsimplified symbolic expressions.
• $real : the mathematical real numbers
• $float(e,f), e, f are integers, each at least 1
  • IEEE754 floating point numbers
• $hreal : Herbrand real numbers. Values are unsimplified symbolic expressions.
• struct(T1,...,Tn)
  • structure type with named fields. Names may not seem necessary but if you want a subset of CIVL-C...
  • What about bit-widths?
• union(T1,...,Tn) : similar to struct
• T[] : array-of-T
• Function<S1,...,Sn;T>
  • function consuming S1,...,Sn and returning T. T can be void. The actual notation is the horrible C notation.
• void* : all pointers
  • T* : pointer-to-T, subtype of above

When are two types equal?

What are two types compatible?

Declarations

Declarations follow the C notation. Function prototypes are considered to be declarations similar to variable declarations.

Declarations for system, abstract/pure functions?

Expressions

• literals
  • $true, $false : values of type $bool
  • 123, -123, 3.1415, etc. : values of type $integer, $int, $real, $float
    • what particular notations for floating values?
  • 'a', 'b', ... UNICODE?
  • (T[]){e0, e1, ...} : values of type T[]
  • (S){e0, ...} : values of type S (struct literal)
  • e1..e2, e1..e2#e3 : values of type $range
  • ($domain){r1,...,rn} : value of type $domain(n)
  • "abc" : string literals: value of type $char[]
  • $root, $here : values of type $scope
  • $self, $proc_null : values of type $proc
  • NULL : value of type void*
• variables
• $defined(e1)
• e1+e2 : addition
• e1-e2 : subtraction
• e1*e2 : multiplication
• e1/e2 : division
• e1%e2 : modulus
• e1[e2] : array index
• *e : pointer dereference
• &e : address-of
• !e : logical not
• -e : negative
• (T)e : cast expression
  • cast of integer to array-of-boolean, and vice-versa?
• e1==e2, e1!=e2
• e1&&e2, e1||e2
• e1?e2:e3
• e1<e2, e1<=e2
• e0(e1,...,en) : pure function call?
• $forall, $exists
• e1.i, some natural number i (tuple read)
• $initial_value(T; e1,...,en)
  • e1,...,en are expressions of integer type
  • the type of this expression is T[e1]...[en]
  • array value with base type T and length e1,...,en
• $typeof(...): what is this for?
• $sizeof(T) : T is a type name?
• e1&e2, e1|e2, e1^e2, ~e1 : bit-wise operations: arguments are arrays of booleans

The Primitive Statements

• Assign: e1=e2;
• Call: e0(e1,...,en); and e=e0(e1,...,en);
  • regular function (one with flow graph)
  • function can be system, pure, abstract?
• Spawn: $spawn e0(e1,...,en); and e=$spawn e0(e1,...,en);
• Wait: $wait(e);
• Wailtall?
• Malloc: e=(T)$malloc(e1,e2); ??
• Free: free(e);
• Noop: ;
  • Is there a need to add annotations for "true" or "false" branch, etc.?
• Return: return; and return e;
• Atomic_enter: what notation?
• Atomic_exit: what notation?
• Parfor_spawn. what notation? Is there exit?
• For_dom_enter (for domains). What notation? Is there exit?

Program Graph

Model

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