= CIVL-C Language

== Overview of CIVL-C

===  Main Concepts

CIVL-C is an extension of a subset of Standard C. It includes the most commonly-used elements of C, including most of the syntax, types, expressions, and statements. Missing are some of the more esoteric type qualifiers, bitwise operations (at least for now), and much of the standard library. Moreover, none of the C language elements dealing with concurrency are included, as CIVL-C has its own concurrency primitives.

The keywords in CIVL-C not already in C begin with the symbol `$`. This makes them readily identifiable and also prevents any naming conflicts with identifiers in C programs. This means that most legal C programs will also be legal CIVL-C programs.

One of the most important features of CIVL-C not found in standard C is the ability to define functions in any scope. (Standard C allows function definitions only in the file scope.) This feature is also found in GNU C, the GNU extension of C.

Another central CIVL-C feature is the ability to spawn functions, i.e., run the function in a new process (thread).

Scopes and processes are the two central themes of CIVL-C. Each has a static and a dynamic aspect. The static scopes correspond to the lexical scopes in the program—typically, regions de- limited by curly braces `{`. . . `}`. At runtime, these scopes are instantiated when control in a process reaches the beginning of the scope. Processes are created dynamically by spawning functions; hence the functions are the static representation of processes.

=== Example Illustrating Scopes and Processes

To understand the static and dynamic nature of scopes and processes, and the relations between them, we consider the (artificial) example code in Fig. 1(a). The static scopes in the code are numbered from 0 to 6.

|| [[Image(scopeCodeExample.png, width=250px, valign=top, margin-left=10, margin-right=10)]] || \
[[Image(staticScopeTree.png, width=200px, valign=top, margin-left=10, margin-right=10)]] || \
[[Image(scopeStateExample.png, width=275px, valign=top, margin-left=10, margin-right=10)]] ||
  Fig. 1.  CIVL-C scopes.  (a) code skeleton to illustrate scope hierarchy.  (b) static scope tree.  (c) a state showing dynamic scopes and process call stacks

The static scopes have a tree structure: one scope is a child of another if the first is immediately contained in the second. Scope 0, which is the file scope (or root scope) is the root of this tree. The static scope tree is depicted in Fig. 1(b). Each scope is identified by its integer ID. Additionally, if the scope happens to be the scope of a function definition, the name of the function is included in this identifier. A node in this tree also shows the variables and functions declared in the scope. For brevity, we omit the proc variables.

We now look at what happens when this program executes. Fig. 1(c) illustrates a possible state of the program at one point in an execution. We now explain how this state is arrived at.

First, there is an implicit root function placed around the entire code. The body of the main function becomes the body of the root function, and the main function itself disappears. This minor transformation does not change the structure of the scope tree.

Execution begins by spawning a process p0 to execute the root function. This causes scope 0 to be instantiated. An instance of a static scope is known as a ''dynamic scope'', or ''dyscopes'' for short. The dynamic scopes are represented by the ovals with double borders in Fig. 1(c). Each dyscope specifies a value for every variable declared in the corresponding static scope. In this case, the value 3 has been assigned to variable x.

The state of process p0 is represented by a call stack (green). The entries on this stack are activation frames. Each frame contains two data: a reference to a dyscope (indicated by blue arrows) and a current location (or programmer counter vaule) in the static scope corresponding to that dyscope (not shown). The dyscope defines the environment in which the process evaluates expressions and executes statements. The currently executing function of a process, corresponding to the top frame in the call stack, can “see” only the variables in its dyscope and those of all the ancestors of its dyscope in the dyscope tree.
Returning to the example, p0 enters scope 6, instantiating that scope, and then spawns procedure `f`. This creates process p1, with a new stack with a frame pointing to a dyscope corresponding to static scope 1. The new process proceeds to run concurrently with p0. Meanwhile, p0 calls procedure `g`, which pushes a new entry onto its call stack, and instantiates scope 5. Hence p0 has two entries on its stack: the bottom one pointing to the instance of scope 6, the top one pointing to the instance of scope 5.

Meanwhile, assume x > 0, so that p1 takes the true branch of the if statement, instantiating scope 3 under the instance of scope 1. It then spawns two copies of procedure `f1`, creating processes p2 and p3 and two instances of scope 2. Then p1 spawns `f2`, creating process p4 and an instance of scope 4. Note that the instance of scope 4 is a child of the instance of scope 3, since the (static) scope 4 is a child of scope 3. Finally, p1 calls `f2`, pushing a new entry on its stack and creating another instance of scope 4. The final state arrived at is the one shown.

There are few key points to understand:

* In any state, there is a mapping from the dyscope tree to the static scope tree which maps a dyscope to the static scope of which it is an instance. This mapping is a tree homomorphism, i.e., if dyscope u is a child of dyscope v, then the static scope corresponding to u is a child of the static scope corresponding to v.
* A static scope may have any number of instances, including 0.
* Dynamic scopes are created when control enters the corresponding static scope; they disappear from the state when they become unreachable. A dyscope v is “reachable” if some process has a frame pointing to a dyscope u and there is a path from u up to v that follows the parent edges in the dyscope tree.
* Processes are created when functions are spawned; they disappear from the state when their stack becomes empty (either because the process terminates normally or invokes the exit system function).

=== Structure of a CIVL-C program

A CIVL-C program is structured very much like a standard C program. In particular, a CIVL- C program may use the preprocessor directives specified in the C Standard, and with the same meaning. A source program is preprocessed, then parsed, resulting in a translation unit, just as with standard C. The main differences are the nesting of function definitions and the new primitives beginning with `$`, which are described in detail in the remainder of this part of the manual.

If the suffix of the filename of the program is not `.cvl`, then the program must include the line
{{{
#include <civlc.cvh>
}}}
somewhere near the beginning (before any CIVL-C primitives are used).  This includes the main CIVL-C header file, which declares all the types and other CIVL primitives.

As usual, a translation unit consists of a sequence of variable declarations, function prototypes, and function definitions in file scope. In addition, assume statements may occur in the file scope.  These are used to state assumptions on the input values to a program.


== Qualifiers

=== The `$input` and  `$output` type qualifiers

The declaration of a variable in the root scope may include the type qualifier `$input`, e.g.,
{{{
$input int N;
}}}
This declares the variable to be an input variable, i.e., one which is considered to be an input to the program.
Such a variable is initialized with an arbitrary (unconstrained) value of its type.
When using symbolic execution to verify a program, such a variable will be assigned a unique symbolic constant of its type.
In contrast, variables in the root scope which are not input variables will instead be initialized with the “undefined” value.
Reading an undefined value is erroneous. [Note: the model checker attempts to catch such errors but currently
does not do so for arrays, which are always initialized with unconstrained values.]
In addition, input variables may only be read, never written to; an attempt to write to an input variable is also flagged as an error.

Alternatively, it is possible to specify a particular concrete value for an input variable, either on the command line, e.g.,
{{{
civl verify -inputN=8 ...
}}}
or by including an initializer in the declaration, e.g.
{{{
$input int N=8;
}}}
The protocol for initializing an input variable is the following: if a command line value is specified, it is used.
Otherwise, if an initializer is present, it is used.   Otherwise, the variable is assigned an arbitrary value of its type.

A variable in the root scope may be declared with `$output` to declare it to be an output variable.
Output variables may only be written to, never read.
They are used primarily in functional equivalence checking.

Input and output variables play a key role when determining whether two programs are functionally equivalent.
Two programs are considered functionally equivalent if, whenever they are given the same inputs (i.e., corresponding $input
variables are initialized with the same values) they will produce the same outputs (i.e., corresponding $output variables will 
end up with the same values at termination).

=== `$abstract`

An abstract function declares a function without a body.  An abstract function is declared using a standard function prototype with the function qualifier `$abstract`, e.g.,
{{{
  $abstract int f(int x);
}}}
An abstract function must have a non-void return type and take at least one parameter.   An invocation of an abstract function is an expression and can be used anywhere an expression is allowed.  The interpretation is an "uninterpreted function".    A unique symbolic constant of function type will be created, corresponding to the abstract function, and invocations are represented as applications of the uninterpreted function to the arguments.  

=== `$atomic_f`

A function is declared atomic using the function qualifier `$atomic_f`, e.g.,
{{{
$atomic_f int f(int x) {
  ...
}
}}}
A call to such a function executes as a single atomic step, i.e., without interleaving from other processes.   Hence, this is only relevant for concurrent programs.  Declaring a function to be atomic is almost equivalent to placing `$atomic{ ... }` around the function body.   The difference is that in the latter case, the call to the function and the execution of the body are executed in two atomic steps, i.e., after activation frame is pushed onto the call stack, another process could execute before the first process obtains the atomic lock and executes its body.   For an atomic function, the entire sequence of events happens in one atomic step.

An atomic function must have a definition; in particular, neither a system function nor an abstract function may be declared using `$atomic_f`.

=== `$system`

A system function is one in which the definition of the function is not provided in CIVL-C code, but is implemented instead in a certain Java class.  A system function is declared by adding the function qualifier `$system` to a function prototype.  Invocation of a system function always takes place in a single atomic step.

A system function may have a guard, which is specified in the function contract using a `$executes_when` clause.  Unless constrained by its contract or other qualifiers, a system function may modify the stay in an arbitrary way.

=== `$pure`

A system or atomic function may be declared to be `$pure`, e.g.,
{{{
$pure $system double sin(double x);
$pure $atomic_f double mysin(double x) {
  return  x - x*x*x/6.;
}
}}}
This means that the function is a mathematical function of its arguments only.    I.e., an invocation of the function has no side-effects and the return value depends on the arguments only (if called twice with the same arguments, it will return the same value, regardless of any differences in the state).   The user is responsible for ensuring that a function declared pure actually is pure.    If this is not the case, the model checker may produce incorrect results.

== Types

* The boolean type is denoted `_Bool`, as in C. Its values are 0 and 1, which are also denoted by `$false` and `$true`, respectively.
* There is one integer type, corresponding to the mathematical integers. Currently, all of the C integer types `int`, `long`, `unsigned int`, `short`, etc., are mapped to the CIVL integer type.
* There is one real type, corresponding to the mathematical real numbers. Currently, all of the C real types `double`, `float`, etc., are mapped to the CIVL real type.
* `$proc`:  This is a primitive object type and functions like any other primitive C type (e.g., `int`). An object of this type refers to a process. It can be thought of as a process ID, but it is not an integer and cannot be cast to one.  Certain expressions take an argument of `$proc` type and some return something of `$proc` type. The operators `==` and `!=` may be used with two arguments of type `$proc` to determine whether the two arguments refer to the same process.  The constant `$self` has `$proc` type and refers to the process evaluating this expression;  constant `$proc_null` has `$proc` type and refers to no process.
* `$scope`:  An object of this type is a reference to a dynamic scope. Several constants, expressions, and functions dealing with the $scope type are also provided.  The $scope type is like any other object type. It may be used as the element type of an array, a field in a structure or union, and so on. Expressions of type $scope may occur on the left or right-hand sides of assignments and as arguments in function calls just like any other expression. Two different variables of type $scope may be aliased, i.e., they may refer to the same dynamic scope.
* `$domain`: A domain type is used to represent a set of tuples of integer values. Every tuple in a domain object has the same arity (i.e., number of components). The arity must be at least 1, and is called the dimension of the domain object.  For each integer constant expression n, there is a type `$domain(n)`, representing domains of dimension n. The universal domain type, denoted `$domain`, represents domains of all positive dimensions, i.e., it is the union over all n ≥ 1 of `$domain(n)`. In particular, each `$domain(n)` is a subtype of `$domain`.   There are expressions for specifying domain values.  Certain statements use domains, such as the “CIVL-for” loop `$for`
* `$range`: An object of this type represents an ordered set of integers.  Ranges are typically used as a step in constructing domains

== Expressions

=== Boolean expressions

CIVL-C provides the boolean constants`$true` and `$false`, which are simply defined as 1 and 0, respectively.
CIVL-C is, after all, an extension of C. 
A program may also include the standard C library header file `stdbool.h`, which defines `true` and `false` in the exact same way.

In addition to the standard logical operators `&&`, `||`, and `!`, CIVL-C provides `=>` (implies).
`p => q` is equivalent to `!(p) || q` (and has the same short-circuit semantics).

A universally quantified formula has the form

  `$forall` `(` ''variable-decls'' (`;` ''variable-decls'' )* (`|` ''restriction'')? `)` ''expr''

where ''variable-decls'' has one of the forms

  ''type'' ''identifier'' (`,` ''identifier'')*

  ''type'' ''identifier'' `:` ''range''

where ''type'' is a type name (e.g., `int` or `double`), ''identifier'' is the name of the bound variable,
''restriction'' is a formula (boolean expression) which expresses some restriction on the values that the bound variable can take, 
''range'' is an expression of `$range` type, and ''expr'' is a formula.
The universally quantified formula holds iff for all values assignable to the bound variable for which the restriction holds, the formula expr holds.

The syntax for existential quantification is the same, with `$exists` in place of `$forall`.  

Examples:
{{{
int a[3], b[3][2];
int main() {
  int n=3, m=2;
  $assert($forall (int i | 0<=i && i<n) a[i]==0); // all elements of a are 0
  $assert($forall (int i: 0..n-1) a[i]==0); // same as above
  $assert($forall (int i: 0..n-1 | i%2==0) a[i]==0); // even elements are 0
  $assert($forall (int i: 0..n-1#2) a[i]==0); // same as above
  $assert($forall (int i: 0..n-1; int j: 0..m-1) b[i][j]==0); // all elements of b are 0
  $assert($forall (int i: 0..n-1; int j | 0<=j && j<m) b[i][j]==0); // same
  $assert($forall (int i: 0..n-1; int j: 0..m-1 | i<j ) b[i][j]==0); // lower triangle is 0
  $assert($forall (int i,j | 0<=i && i<n && 0<=j && j<m) b[i][j]==0); // all elements of b are 0
  $assert($exists (int i | 0<=i && i<n) a[i]==0); // existential: some element of a is 0
  $assert($forall (int i: 0..n-1) $exists (int j: 0..i) a[j]<=a[i]); // nested quantification
}
}}}

=== Domain literals

An expression of the form

  `(``$domain``)`  `{` ''r1'' `,` ... `,` ''rn'' `}`

where ''r1'', . . . , ''rn'' are ''n'' expressions of type `$range`, is a ''Cartesian domain expression''.
It represents the domain of dimension ''n'' which is the Cartesian product of the ''n'' ranges,
i.e., it consists of all ''n''-tuples (''x1'',...,''xn'') where ''x1'' ∈ ''r1'', ..., ''xn'' ∈ ''rn''.
The order on the domain is the dictionary order on tuples.
The type of this expression is `$domain(n)`.
When a Cartesian domain expression is used to initialize an object of domain type, the `($domain)` may be omitted. For example: 
{{{
$domain(3) dom = { 0 .. 3, r2, 10 .. 2 # -2 };
}}}


=== `$here`
Expression of type `$scope`, evaluating to the dynamic scope in which the evaluation takes place.

=== `$proc_null`
The null process constant.  Similar to the NULL pointer, this gives an object of `$proc` type a defined value, and can be used in `==` and `!=` expressions.  It cannot be used as the argument to `$wait` or `$waitall`.

=== `$root`
Constant of type `$scope`, the root dynamic scope.

=== Range literals

An expression of the form `lo .. hi` where `lo` and `hi` are integer expressions, represents the range consisting of the integers `lo`, `lo` + 1, ..., `hi` (in that order).
An expression of the form `lo .. hi # step`, where `lo`, `hi`, and `step` are integer expressions is interpreted as follows.
If `step` is positive, it represents the range consisting of `lo`, `lo` + `step`, `lo` + 2 ∗ `step`, …, up to and possibly including `hi`.
To be precise, the infinite sequence is intersected with the set of integers less than or equal to `hi`.
If `step` is negative, the expression represents the range consisting of `hi`, `hi` + `step`, `hi` + 2 ∗ `step`, . . ., down to and possibly including `lo`.
Precisely, the infinite sequence is intersected with the set of integers greater than or equal to `lo`.

=== `$scopeof`

Given any left-hand-side expression ''expr'', the expression `$scopeof(`''expr''`)` evaluates to the dynamic scope containing the object specified by ''expr''.
The following example illustrates the semantics of the `$scopeof` operator. All of the assertions hold:
{{{
{
  $scope s1 = $here;
  int x;
  double a[10];
  {
    $scope s2 = $here;
    int *p = &x;
    double *q = &a[4];
    assert($scopeof(x)==s1);
    assert($scopeof(p)==s2);
    assert($scopeof(*p)==s1);
    assert($scopeof(a)==s1);
    assert($scopeof(a[5])==s1);
    assert($scopeof(q)==s2);
    assert($scopeof(*q)==s1);
  }
}
}}}

=== Scope relational expressions

Let `s1` and `s2` be expressions of type `$scope`. The following are all CIVL-C expressions of boolean type:

* `s1 == s2`. Holds iff `s1` and `s2` refer to the same dynamic scope.
* `s1 != s2`. Holds iff `s1` and `s2` refer to different dynamic scopes.
* `s1 <= s2`. Holds iff `s1` is equal to or a descendant of `s2`, i.e., `s1` is equal to or contained in `s2`.
* `s1 < s2`. Holds iff `s1` is a strict descendant of `s2`, i.e., `s1` is contained in `s2` and is not equal to `s2`.
* `s1 > s2`. Equivalent to `s2 < s1`.
* `s1 >= s2`. Equivalent to `s2 <= s1`.

Each of these expressions is erroneous if `s1` or `s2` is undefined.  This error is reported by the model checker.


== Statements


=== `$atomic`

=== `$choose`

=== `$for`

=== `$parfor`

=== `$spawn`

=== `$when`


== Functions

=== `$assert`

=== `$assume`

=== `$assume_push`

=== `$assume_pop`

=== `$choose_int`

=== `$default_value`

=== `$elaborate_domain`

=== `$exit`

=== `$free`

=== `$havoc`

=== `$hidden`

=== `$hide`

=== `$is_derefable`

=== `$is_terminated`

=== `$local_end`

=== `$local_start`

=== `$malloc`

=== `$pathCondition`

=== `$pow` 

`$pow(double, double)` 

=== `$reveal`

=== `$wait` and `$waitall`

=== `$yield`


== Macros


=== `$elaborate`




== Contract Annotations

clauses

=== The `depends_on` clause

`\nothing`

=== The `executes_when` clause