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

• Boolean
• Integer types
  • Integer : the mathematical integers
  • Int<Integer lo, Integer hi, Boolean wrap>
    • 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<Integer e, Integer f> : IEEE754 floating point numbers
• Struct
  • list of name-type pairs
  • bit-widths?
• Array<T>
  • Array<Integer n,T>
• Function<S1,...,Sn;T>
• Pointer<T>

When are two types equal?

What are two types compatible?

Values

Expressions

• 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
• (T)e : cast expression
  • cast of integer to array-of-boolean, and vice-versa?

Statements

• Assign
• Call
• Spawn
• Wait

Program Graph

Model

Libraries