The CIVL-IR. Also known as "CIVL model".

Grammar:

• a subset of CIVL-C, explicit guarded-trasition systems
• functions, scopes, functions defined in any scope
• all blocks start with variable declarations; no initializers
• 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
• $scope
• $char
• $mem
• $bundle
• $heap
• $range
• $domain
  • $domain(n), n is an integer at least 1; subtype of above
• enum types.
  • different from integers or like C?
• Integer types
  • $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.
• Real types
  • $real : the mathematical real numbers
  • $float(e,f), e, f are integers, each at least 1
  • IEEE754 floating point numbers
• struct(T1,...,Tn)
  • Why do we need the field names?
  • What about bit-widths?
• union(T1,...,Tn) : similar to struct
• T[] : array-of-T
• Function<S1,...,Sn;T>
• T* : pointer-to-T

When are two types equal?

What are two types compatible?

Values

Expressions

• literals
  • $true, $false
  • 123, -123, 3.1415, etc.
  • 'a', 'b', ... UNICODE?
  • (T[]){e0, e1, ...} : array literal
  • (S){e0, ...}` : tuple (struct) literal
  • e1..e2, e1..e2#e3 : range literals
  • domain literals?
  • "abc" : string literals (array of char -- same as array literal?)
  • $root, $here (values of type $scope)
  • $self, $proc_null, $proc_undef? (values of type $proc)
• variable
• 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(e1) : some way to get initial value of something (like array)?
• $typeof(...): what is this for?
• $sizeof(T) : T is a type name?
• all the bit-wise operations

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?

Statements

• Assign
• Call
• Spawn
• Wait
• Malloc
• Noop
• Return
• Atomic_enter
• Atomic_exit
• Parfor_spawn. is there exit?
• For_dom_enter (for domains). exit?

Program Graph

Model

Libraries