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:
  • a sequence of type definitions
  • 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.

Can we specify that elements must appear in the order above? Or would that create a problem in something like

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

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.

Types

Do you need dependent types? I.e., can parameters to some of the types be arbitrary expressions, or do they have to be constants?

Do you need typedefs?

Question about types. In the following, where in the state is the length of the array field stored?

#include <stdio.h>
int n=10;
int main() {
  struct S {int a[n];};
  struct S x1;
  n=20;
  struct S x2;
  printf("%ld, %ld\n", sizeof(x1), sizeof(x2));
  x2.a[10]=1; // error caught by CIVL
  fflush(stdout);
}

• $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.
  • Do we want to allow lo and hi to be any values of type $integer, which means they are dynamic types, like complete array types?
• $hint : Herbrand integers. Values are unsimplified symbolic expressions.
• $real : the mathematical real numbers
• $float(e,f), e, f are integers, each at least 1. Same question for e and f as for lo and hi.
  • 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
• do we need the complete array type T[e], which is a dependent type?
• 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?

Type names

Do we need another syntactic category for code that specifies a dynamic type, for example

• int[n*m+3].

This can be used in sizeof, ...

Do we need to clearly distinguish dynamic type names and static type names?

Declarations

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

Example of declaration of a function:

$integer f($real x, $bool y);

Additional modifiers that may be placed on any of above:

• $pure : the function has no side effects, but may be nondeterministic
• $abstract: function is a pure, mathematical function: deterministic function of inputs

System functions:

• A function declaration which is not abstract and for which no definition is provided is a system function.
• 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 any memory it can reach. This includes allocating new data on heaps it can reach.
• A system function may have an implicit guard. This is specified how?
• A system function may have an explicit guard. This is specified how?

Example of a declaration of a system function with guard. Fix me:

$bool g($real x, $bool y) { ... }
$integer f($real x, $bool y) $guard g;

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 lengths e1,...,en
  • do we need this for more types? E.g., structs of arrays of structs of arrays of ...?
• $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
• MemoryUnitExpressions?: are these literal values of type $mem?
  • could we use Frama-C notation p+(e1..e2) for example?
  • are there conversions between pointers and mems?

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