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

Grammar?

Example:

int f() {
L1 :
  $choose {
    $when (g1) stmt1; goto L2;
    $when (g2) stmt2; goto L3;
  }
L2 :
  $choose {
    $when (g3) stmt3; goto L4;
    ...
  }
...
}
// 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 (scope values)
  • $self, undefined process (proc value)

• 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)

Statements

• Assign
• Call
• Spawn
• Wait

Program Graph

Model

Libraries