CIVL-C Language Manual

Types

The Boolean type

The boolean type is denoted _Bool, as in C. Its values are 0 and 1, which are also denoted by $false and $true, respectively. One may also include the standard C header stdbool.h, which defines false and true (also as 0 and 1), and defines the type bool to be an alias for _Bool.

The integer type

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. [This is expected to change.]

The real 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. [This is expected to change.]

The process 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.

The scope type $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 types: $domain and $domain(n)

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.

The range type $range

An object of this type represents an ordered set of integers. Ranges are typically used as a step in constructing domains. They can also be used in quantified expressions to specify the domain of a bound variable (see $forall and $exists).

Type qualifiers

Declaring input and output variables: $input and $output

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 (uninterpreted) functions: $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 functions: $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 functions: $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 functions: $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.

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) { r₁ , ... , r_n }

where r₁, . . . , r_n 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 (x₁,...,x_n) where x₁ ∈ r₁, ..., x_n ∈ r_n. 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 };

This scope: the $here scope expression

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

The null process reference: $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.

The root scope constant: $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.

The scope of an expression: $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 is equivalent to s2 < s1.
• s1 >= s2 is equivalent to s2 <= s1.

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

This process: $self

This expression of $proc type returns a reference to the process which is evaluating this expression. It provides a way for code to obtain the identity of the process executing the code.

Spawning a new process: $spawn

A spawn expression is an expression with side-effects. It spawns a new process and returns a reference to the new process, i.e., an object of type $proc. The syntax is the same as a procedure invocation with the keyword $spawn inserted in front:

$spawn f(expr1, ..., exprn)

Typically the returned value is assigned to a variable, e.g.,

$proc p = $spawn f(i);

If the function f returns a value, that value is simply ignored.

Statements

Atomic blocks: $atomic

An atomic block is a statement of the form

$atomic {
  stmt1;
  stmt2;
  ...
}

and indicates that the statements comprising the block should be executed without the intervention of other processes.

More precisely, there is a global atomic lock which is initially free. A process attempting to execute an atomic block will wait until the atomic lock becomes free, i.e., no other process is inside an atomic block. The process must also wait until the guard of the atomic block holds; this means that the first statement in the block is enabled. Once the atomic lock is free and the guard holds, the atomic block becomes enabled and the process may enter the atomic block. The process may not necessarily enter the atomic block as soon as these conditions hold, because some other enabled process may be scheduled first. In fact, some other process may obtain the atomic lock. But if the enabling conditions hold and this process is scheduled, it will obtain the atomic lock and begin executing the statements of the atomic block without other processes executing. Upon reaching the end of the atomic block, the process releases the atomic lock and exits the block.

There is an exception to atomicity: if the process inside the atomic block executes a $yield statement, it releases the atomic lock. This allows other processes to execute, and even obtain the lock. At any point at which the atomic lock is free and the first statement following the $yield is enabled, the original process may re-obtain the atomic lock and continue executing its block atomically.

If a statement inside an atomic block blocks, so that the process executing the atomic block has no enabled statement, execution deadlocks. The exception to this rule is that the first statement in the atomic block, and the first statement after a $yield, as described above, may block, without necessarily causing deadlock.

Atomic blocks may be nested. Hence the atomic lock is held with a certain multiplicity. Each time the process enters an atomic block, the multiplicity is incremented. Each time it leaves an atomic block, the multiplicity is decremented. When the multiplicity hits 0, the atomic lock is released. Execution of a $yield does not change the multiplicity; the process releases the lock but maintains the multiplicity, so that when the lock is re-obtained, the original multiplicity is still in place.

Nondeterministic selection statement $choose

A $choose statement has the form

$choose {
  stmt1;
  stmt2;
  ...
  default: stmt
}

The default clause is optional. The guards of the statements are evaluated and among those that are true, one is chosen nondeterministically and executed. If none are true and the default clause is present, it is chosen. The default clause will only be selected if all guards are false. If no default clause is present and all guards are false, the statement blocks. Hence the implicit guard of the $choose statement without a default clause is the disjunction of the guards of its sub-statements. The implicit guard of the $choose statement with a default clause is true.

Example: this shows how to encode a “low-level” guarded transition system:

l1:
$choose {
  $when (x>0) {x--; goto l2;}
  $when (x==0) {y=1; goto l3;}
  default: {z=1; goto l4;}
}
l2:
$choose {
  ...
}
l3:
$choose {
  ...
}

Domain iteration statement: $for

A domain statement has the form

$for (int i₁, ..., i_n : dom) S

where i₁, . . . , i_n are n identifiers, dom is an expression of type $domain(n), and S is a statement. The identifiers declare n variables of integer type. Control iterates over the values of the domain, assigning the integer variables the components of the current tuple in the domain at the start of each iteration. The scope of the variables extends to the end of S. The iterations takes place in the order specified by the domain, e.g., dictionary order for a Caretesian domain. Note that if a range expression can be used as dom here, it will be automatically converted to a one-dimensional domain. For example,

$for (int i: 0..10) S

is equivalent to

$for (int i: ($domain(1)){0..10}) S

There is a also a parallel version of this construct, $parfor.

Parallel for loop: $parfor

A parallel for loop statement has the form

$parfor (int i₁, ..., i_n : dom) S

The syntax is exactly the same as that for the sequential domain iteration loop $for, only with $parfor replacing $for.

The semantics are as follows: when control reaches the loop, one process is spawned for each element of the domain. That process has local variables corresponding to the iteration variables, and those local variables are initialized with the components of the tuple for the element of the domain that process is assigned. Each process executes the statement S in this context. Finally, each of these processes is waited on at the end. In particular, there is an effective barrier at the end of the loop, and all the spawned processes disappear after this point.

Guarded commands: $when

A guarded command is encoded in CIVL-C using a $when statement:

$when (expr) stmt;

All statements have a guard, either implicit or explicit. For most statements, the guard is true. The $when statement allows one to attach an explicit guard to a statement.

When expr is true, the statement is enabled, otherwise it is disabled. A disabled statement is blocked—it will not be scheduled for execution. When it is enabled, it may execute by moving control to the stmt and executing the first atomic action in the stmt. If stmt itself has a non-trivial guard, the guard of the $when statement is the conjunction of the expr and the guard of stmt.

The evaluation of expr and the first atomic action of stmt occur as a single atomic action. There is no guarantee that execution of stmt will continue atomically if it contains more than one atomic action, i.e., other processes may be scheduled.

Example

$when (s>0) s--;

This will block until s is positive and then decrement s. The execution of s-- is guaranteed to take place in an environment in which s is positive.

Example

$when (s>0) { s--; t++; }

The execution of s-- must happen when s>0, but between s-- and t++, other processes may execute. The curly braces in the code above do not accomplish anything---the code is equivalent to

$when (s>0) s--; t++;

To make the entire statement atomic, one must use an $atomic statement; see the following example.

Example

The following statements are all equivalent:

$when (s>0) $atomic{ s--; t++; }
$atomic{ $when(s>0); s--; t++; }
$atomic{ $when(s>0) { s--; t++; } }

Each of these waits until s is positive, then from such a state, decrements s and increments t without the intervention of other processes.

Example

$when (s>0) $when (t>0) x=y*t;

This blocks until both x and t are positive then executes the assignment in that state. It is equivalent to

$when (s>0 && t>0) x=y*t;

Functions

Assertions: $assert

The system function $assert has the signature

void $assert(_Bool expr, ...);

It consumes a boolean expression and any number of optional expressions which are used to construct an error message. Note that CIVL-C boolean expressions have a richer syntax than C expressions, and may include universal or existential quantifiers. During verification, the assertion is checked. If it cannot be proved that it must hold, a violation is reported, and, if additional arguments are present, a specific message is printed. These additional arguments are similar in form to those used in C’s printf statement: a format string, followed by some number of arguments which are evaluated and substituted for successive codes in the format string. For example,

$assert(x<=B, "x-coordinate %f exceeds bound %f", x, B);

If x=3 and B=2, the assertion is violated and CIVL prints the error message “x-coordinate 3 exceeds bound 2”.

Assumptions: $assume

The system function $assume has signature

void $assume(_Bool expr);

During verification, the given expression is assumed to hold. If this leads to a contradiction on some execution, that execution is simply ignored. It never reports a violation, it only restricts the set of possible executions that will be explored by the verification algorithm. Like an assertion call, an assume call can be used any place a statement is expected. In addition, an assume call can be used in file scope to place restrictions on the global variables of the programs. For example,

$input int B, N;
$assume(1<=N && N<=B);

declares N and B to be integer inputs and restricts consideration to inputs satisfying 1 ≤ N ≤ B.

$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