Verifying a program

The file is the one source file of the run. It is this function:

The command takes these options and no others. An option that is not in this table is refused with exit status 2, even if the front end would accept it: verification must not depend on a diagnostic that was switched off or a dialect that was changed behind its back.

The tools the verifier runs (the Java runtime, Silicon, Z3 and the system include directories) are fixed when cerastes is built. Environment variables such as SILICON_JAR or Z3_EXE do not change a result.

cerastes verifies the primary file and every user header it includes: each function body in them. A header is verified again in every run that includes it.

A system file is not verified. It is a file under one of the system include directories the tool was built with (the SDK, the C++ library, the compiler’s own headers), or exactly the include/cerastes.h of the cerastes checkout. The test is made on the file’s real path (symbolic links and .. are resolved), never on a flag in the source, so a #pragma or a #line in your code cannot turn the checks off. A #line directive in a verified file is rejected for the same reason. A function declared in a system file is used only through a contract; its body is never read.

A directory you give with -I is a user directory, even if it holds library code.

The bodies of functions marked CERASTES_PREDICATE and CERASTES_PURE are specification and are not verified. In this version a call of one of them in executable code is rejected, and in a contract only cerastes::old may be called.

A verification error is one line on standard output, followed by notes that say which clause is involved:

The file is written as you gave it on the command line (or as the include resolved, for a header), the line is the line of the C or C++ source, and the category is one of eleven names that Error messages explains. Errors are sorted by file, then line, then category, and each is printed once. A program with errors exits with status 1.

A program that cerastes does not accept, because EDG finds a compile error or because it uses a construct that cerastes does not verify, is reported on standard error in EDG’s format, with the diagnostic’s name, and the exit status is 2. Standard output is then empty:

Nothing else is printed. In particular a warning from the front end in a verified file is shown on standard error like any diagnostic, so a program that is meant to verify cleanly should compile without warnings.

A loop needs an invariant to be verified (the verifier does not unroll it) and a measure, CERASTES_DECREASES(…​), to show that it ends. The invariant must hold when the loop is first reached and after every iteration, and what follows the loop is proved from the invariant and the negation of the condition. The measure is one or more integer expressions that get smaller with every iteration and never go below zero: in n - i, the loop condition i < n makes it positive, and i += 1 makes it smaller. The arithmetic in the loop is checked on every iteration, and so is the condition each time it is evaluated, and so is the arithmetic of the measure.

Here the invariant s == 2 * i and the bound i ⇐ n give s == 2 * n when the loop ends, and the measure n - i shows that it ends. A loop with no CERASTES_INVARIANT is verified with only the facts the verifier derives automatically (that each variable the loop assigns stays in the range of its type), which is rarely enough to prove anything about the result.

A recursive function needs a measure too, written after its parameter list. It is compared from the entry of the function to every call of a function in the same recursion cycle, over the arguments of the call:

A measure with several expressions is compared lexicographically: at the first one that changes, the new value must be smaller than the old one, which must not be negative, and the later ones may be anything. A function that is not in a recursion cycle needs no measure. A loop, or a function in a cycle (direct recursion, or mutual recursion through other functions of the file), without one is rejected, because a program whose termination is not shown cannot be called verified:

The errors a wrong invariant or measure can cause are invariant-entry, invariant-preserved and termination, described in Error messages.

break leaves a loop, or a switch, at once, without evaluating the loop’s condition, so the invariant is not checked there. What follows the loop is proved from the way it was left: the invariant and the negated condition, or the state at one of the break statements. continue ends the iteration: in a for loop the increment runs, then the condition is evaluated again, so the invariant and the measure are checked there as at the end of the body.

In smallest_divisor the loop ends either at the break, where n % d == 0, or when d < n is false, where the invariant gives d == n; both give the postcondition.

A do loop runs its body before its first test, so its invariant holds at the start of every iteration (on entry, and each time the test is true), and the arithmetic of its condition is checked after the body, where the condition is evaluated. CERASTES_INVARIANT and CERASTES_DECREASES are written before do. A do { …​ } while (0), whose body runs once, needs no measure; a condition that names a variable, even a constant equal to zero, makes it an ordinary loop that needs one.

A switch evaluates its controlling expression once, with the usual checks, and goes to the matching case label, to default, or past the switch. Execution falls through from one label’s statements to the next until a break; [[fallthrough]]; (or [[gnu::fallthrough]];) marks an intended fallthrough for compilers that warn about it. Each case value is checked as it is written, like any constant: case 1 << 40: is a shift error at the label, even where the compiler only warns. The case values are checked at the start of the function, whether or not the switch is reached, and in C++ they may name constants (Named constants). A switch on an enumeration must also pass the compilers' -Wswitch rules (Enumerations). A label may jump past a declaration without an initializer: the variable has no value there until it is assigned (Locals without an initializer). cerastes rejects a case or default label that is not directly inside the braces of its switch (as in Duff’s device), a GNU case range (case 1 …​ 3:), a statement other than a declaration without an initializer before the first label, a declaration with an initializer that a later label jumps over, and a switch with an init-statement or a declaration in its condition.

A goto is verified when it jumps outward and forward: its label is a later statement of a block that encloses the goto, and no declaration of that block lies between them. That covers the usual uses: an early exit to a common label at the end of a function, a cleanup label, and leaving nested loops or a switch at once. As with break, the loop’s condition is not evaluated on the way out, so its invariant is not checked there; after the label, what follows is proved from each way of getting there.

After done:, the postcondition is proved for each way of getting there: from either goto, where result is still -1, and from the subtraction, which cannot overflow because 0 ⇐ y ⇐ x holds there.

A goto may jump past a declaration without an initializer; the variable has no value at the label until it is assigned (Locals without an initializer). cerastes rejects a goto that jumps backward (write the loop as while, for or do), one that jumps into a block, an if branch, a loop or the body of a switch, one that jumps past a declaration with an initializer that is still in scope at the label (the initialization would be skipped), and the GNU computed goto.

A local may be declared without an initializer and given its value later. Until it is assigned it has no value: reading it is undefined behaviour in C and in C++ (erroneous behaviour in C++26), and the first rule of the C++ initialization profile (P4222) forbids it. cerastes checks every read. A read that may come before the variable has a value is an uninitialized error at the read (Error messages). The check follows the paths of the program, so a variable assigned on every path that reaches the read verifies, even when the assignment is in another branch than the read:

In pick, x is read only when c is non-zero, and then it was assigned.

A read is any use of the value: in an expression, a condition, a return, an argument, the old value in x += 1 or x++, and an annotation such as CERASTES_CHECK or a loop invariant. Each time its declaration is reached, in the next iteration of a loop for example, the variable has no value again. A goto or a case label may jump past a declaration without an initializer, as C and C++ allow; the variable then has no value at the label until it is assigned. A const local without an initializer is rejected, since it can never be given a value. cerastes is stricter than C++ in two cases: copying an indeterminate unsigned char is allowed there and an error here, and an expression statement that only names the variable (x; or (void)x;) does not read it in C++, while cerastes counts it as a read, as C does. An operand of sizeof is never a read.

An assignment, a compound assignment and ++ or -- may be used as a value, and the comma operator may join expressions, in both modes:

The value of x = e is the value stored in x: e converted to the type of x, which is checked like every conversion (Integer semantics). The value of x += e and of ++x is the new value of x, the value of x++ the old one. In a, b the left operand is evaluated completely, then the right one, whose value is the value of the whole expression. A side effect in the right operand of && or ||, or in an arm of ?:, happens only when that operand is evaluated, and one in a loop condition happens each time the condition is evaluated: the loop invariant holds before each evaluation. A variable assigned inside an expression has its value from that point on (Locals without an initializer).

The last evaluation of a loop condition counts too. In count_up the condition’s i++ runs once more than the body, so after the loop i is n + 1; returning total + i - 1 instead gives 3 * n, and the postcondition fails at the return:

C leaves the order in which most operands are evaluated unspecified, and an expression that modifies a variable and also reads or modifies it in an operand that is not sequenced with the modification is undefined behaviour. cerastes rejects such an expression at the modification, by C’s rules in both modes, even where C++17 defines it (x = x++):

The operators that sequence their operands are &&, ||, , and the condition of ?:; both arms of ?: count as modifying what either arm modifies. The operands of the other operators, and the arguments of a call, are not sequenced. As with -Wswitch, a few shapes that the compilers' -Wall warns about are rejected too: an assignment used as a condition without extra parentheses (write if x = e) != 0) or if ((x = e, not if (x = e)), a comma operator one of whose operands has no effect, a discarded value computed around a side effect (x++ + 1;), and a side effect inside sizeof, which is never evaluated.

A function declared [[noreturn]] (or _Noreturn in C, or with the GNU attribute noreturn) must never return: cerastes checks that no return and no closing brace of its body can be reached, and reports one that can as a noreturn error. A call of such a function ends the path of its caller, so what would follow it is not checked.

abort, exit and _Exit from <stdlib.h> are known not to return. They are the only functions of the C library that cerastes knows so far; quick_exit, __builtin_trap, __builtin_unreachable (and C23’s unreachable()) and std::terminate are rejected.

Without the call of fail, a / b would be a division-by-zero and an overflow error. A function declared not to return cannot have CERASTES_ENSURES (it would never be checked), and main cannot be declared not to return. A function that never returns by looping forever is rejected, since every loop needs a measure.

assert(e) from <assert.h> (or <cassert>) is verified as a check of e: a failure is a check error at the assert. Unlike CERASTES_CHECK, it is code: e is evaluated at run time, so its arithmetic is checked like any expression’s, and it may call functions. When NDEBUG is defined, assert does nothing, and cerastes checks nothing, as the program will run. A result holds for the configuration that was verified: with asserts on, the code after assert(e) may rely on e, which a build with NDEBUG no longer checks, so verify the configuration you ship.

Here the requires keeps sum small, the assert states a bound that the requires guarantees, and the contract pins the result exactly: r == (a + b) / 2.

A const variable at file scope (in C++ also constexpr, and at namespace scope) whose initializer is a constant can be used anywhere: in code, in CERASTES_REQUIRES, CERASTES_ENSURES, CERASTES_CHECK, invariants and measures. In C++ it can also be named in the initializer of another constant and be a case value, and so can a local const or constexpr variable initialized with a constant (case LIMIT:, case LIMIT + 1:, case k:).

A constant’s initializer is checked as you wrote it, like any constant (Integer semantics), at the start of every function in the file, whether or not the function uses it, so the error is reported at the constant even when nothing reads it:

Until it is fixed, such an error hides the other errors of the file. The case values of a function are checked the same way, at its start, so a bad case value is reported even where the switch is never reached.

Rejected: a global variable that is not const; a const declared extern and not defined in the file; in C, const int z; without an initializer (another file may define z, and the linker would use its value: write = 0, or make it static); a weak constant (__attribute__((weak)), #pragma weak), whose value another file may replace; a constant initialized by running code (in C++, an initializer that is not a constant expression, such as const int n = f();); volatile and thread_local constants; a global declared in a system header. In C, a constant cannot be named where the language requires a constant expression (a case value, _Static_assert, the initializer of another file-scope constant): a const object is not a constant expression in C, although some compilers accept it, so the front end refuses it. C23’s constexpr objects are not accepted by the front end yet.

cerastes translates the program to Viper, the verification language of the Silicon prover, and Silicon asks Z3. --keep-vpr writes the Viper text and the position map that links each checked line of it to your source:

This writes midpoint.vpr and midpoint.vpr.map into the current directory. --keep-vpr=<path> writes <path> and <path>.map. The files are written for every run that reaches the prover (exit status 0, 1 or 3), whatever the verdict. They are for people who want to see what was checked; the reports already point at your source, never at the Viper file.

A result is for one translation unit. A contract you declare for a function that is defined elsewhere, in another source file or in a library, is trusted: the callers in this unit are verified against it, and nothing here checks that the definition satisfies it. The success line says so. The definition is checked when the file that contains it is verified; a library function that is never verified is trusted for good.

Here two_ids is verified assuming next_id meets its contract. A function that has neither a contract nor a body in a verified file cannot be called from verified code: the call is rejected, because there is nothing to verify it against.

The same holds for constants: a constant’s value is the one in this file. In C++ a namespace-scope const has internal linkage, so the file that defines a function whose contract you trust may give a constant of the same name another value; keep such constants in one header that both files include.

And for enumerations: a value of an enumeration is assumed to be one of its values (Enumerations) when it comes from outside the verified code, as a parameter or as the result of a function whose contract you trust. Every conversion into an enumeration in verified code is checked, but C lets code in another file store any value of the integer type the compiler picks for the enumeration, and such a value is outside what the result covers.

A verified function terminates on every input that satisfies its requires, has no undefined behaviour on the way, and returns a value that satisfies its ensures, or ends the program by calling a function that does not return (such as abort or exit): the result is total correctness. A call of exit in main ends the program without checking the CERASTES_ENSURES of main. (In these programs, which have no input or output, a loop or recursion that never ends is undefined behaviour in C++ anyway, which is why cerastes does not leave it unchecked.)

What a result rests on is the single-unit assumption above, and it includes termination. A contract you declare for a function that is defined elsewhere is trusted to hold and to terminate. This is most visible with a contract that cannot be met:

absurd verifies, because its only path calls a function that, by its contract, never returns. If never_returns can in fact return, the verification says nothing about absurd. A contract you declare for code you have not verified is something you promise, not something the tool checks.

The termination assumption has a limit that the check cannot see. If a function of this file calls a function that is defined in another file, which in turn calls back a function of this file, the cycle goes through code that was verified in another run: each file verifies, and the program does not terminate. A recursion cycle that passes through a function defined in another translation unit is not detected.

A parameter in a postcondition denotes the value it had on entry, as the Annotations page describes. CERASTES_CHECK and a loop invariant see its current value.

The same source means the same in C23 and in C++20. Where the two standards differ (conversions to a signed type, left shift of a negative value), cerastes uses the stricter rule in both, so a .c file verifies, or fails, identically in either mode:

cerastes rejects what it cannot verify, with a diagnostic at the line, and never approximates it:

The constructs that are rejected in this version are:

A function with a body but no contract is verified against the default contract: its parameters and its result are in the range of their types.