Termination checking

Functions and loops can be given a termination measure with an annotation of the form

_(decreases expr1, expr2, ..., exprN)

If this annotation is put on a loop, then when taking a back-edge within the loop, the tuple <expr1,...exprN> is checked to decrease under the lexicographic order. More precisely, let x[N] be the tuple of these values at the beginning of a loop iteration, and let y[N] be the tuple of these values when control goes backwards within the loop; VCC checks that
\exists unsigned i; i < N && x[i] >= 0 && y[i] < x[i] /\ \forall unsigned j; j < i ==> x[j] == y[j]

If this annotation is put on a function, then when calling a function, VCC checks that the measure of the called function (at function entry) is lexicographically smaller than the measure of the calling function (at function entry). If a function with measure x[N] calls a function with measure y[M], VCC checks that
(\exists unsigned i; i < M && (i = N || (i < N && x_i >= 0 && y_i < x_i)) /\ \forall unsigned j; j < i ==> x_j == y_j) .

There is an implicit 0-th element to each function measure, called the “level” of the function. Thus, function calls to higher levels are disallowed, function calls to lower levels are allowed with no further measure check, and function calls within the same level are subject to the measure check above. VCC computes levels based on the call graph graph visible to the verifier. Call cycles (i.e., groups of functions which are allowed to call each other recursively, subject to non-level measure decrease) need to be declared explicitly. The example syntax is:

_(def \integer f(\integer x)
  _(recursive_with g)
  if (x <= 0) return 7;
  return g(x - 1) + 1;

_(def \integer g(\integer x)
  _(recursive_with f)
  if (x <= 0) return 1;
  return f(x - 1) + 1;

VCC takes the edges introduced with _(recursive_with ...) and compute strongly connected components. Each such component will constitute a call group, where every function will get the same level.

The correctness of this inference will be checked in future with the help of “verification linker”. If VCC sees the entire call graph, it will infer correct levels. Otherwise, if the functions calling each other recursively are never seen in the same verification, the missing _(recursive_with ...) annotation will be missed.

All that means that if there are no recursive functions, no function measures need to be supplied.

Measures can currently be only integers. The \size(...) function is defined on data types and records.

The measure of a function defaults to the tuple of its arguments, with \size(...) applied where appropriate, and incomparable elements (pointers, Booleans, structs) removed. Integers used in measures are required to be positive, at the point where the measure is required to be decreased.

When the measure is explicitly specified, VCC will check termination for that function (unless –termination:0 is passed). Otherwise, -termination:1, 2 or 3 specifies if VCC should check termination of pure functions, all ghost functions, or all functions respectively.

VCC will guess decreases measures for while and for loops with the condition of the form a < b , a <= b , a > b , a >= b , a != b . In each of this cases the measure is the absolute value of a - b . So far this is the only inference pattern supported.

Last edited Nov 8, 2011 at 7:24 AM by erniecohen, version 9


No comments yet.