Overview

cerastes is a deductive verifier for C and C++. It is in development. Today cerastes verify verifies functions over the integer types and bool, against contracts you write in the source; templates, pointers, classes and the rest of the languages are not verified yet. This page says what it is meant to be and what exists today.

Design

You will write contracts (preconditions, postconditions, loop invariants and assertions) as [[cerastes::...]] attributes in your C or C++ source. The EDG front end parses them as ordinary C++ expressions. cerastes translates the program and its contracts into Viper, a verification language. The Silicon verifier, which uses the Z3 solver, then checks them, and cerastes reports every failure against a line of your C or C++ source, not against generated code.

The distinguishing goal is to verify templates generically. A function template is meant to be proved once, against the properties that its template parameters are required to have, and the result is meant to hold for every instantiation that meets those requirements. None of this works yet: cerastes verify rejects function templates.

Pipeline

The pipeline is described below. The marks show what exists today.

C/C++ source + contracts
        |
        v
  EDG front end            built, in the cerastes configuration; parses
        |                  C and C++ and the cerastes annotations
        v
  Back end                 checks the rules EDG cannot check for the
        |                  annotations, then encodes functions over
        |                  integers and bool into a small internal IR
        v
  Viper text (.vpr)        written, with a map back to your source lines
        |
        v
  Silicon, Z3              run on the Viper text
        |
        v
  Errors at C/C++ lines    reported, with a category and a note

Current status

cerastes verify is the command (Verifying a program). What it verifies and what it does not:

  • Verified: functions over bool and the integer types in C23 and in C++20, with locals (with or without an initializer: a read before the first assignment is an error), arithmetic, comparisons and logical operators, assignments and ++/-- used as values and the comma operator, if/else, switch, while, do and for loops with invariants and termination measures, break and continue, forward goto, recursion with measures, return, named constants (const globals), enumerations and their constants, calls of functions that have a contract or a body in the same file, functions that do not return ([[noreturn]], abort, exit), assert and check. The integer rules (overflow is an error, unsigned arithmetic wraps, a conversion to a signed type must be exact, a value of an enumeration is one of its values) are on Integer semantics.

  • Reported: thirteen kinds of error, each at a line of your source, with what it means and how to fix it on Error messages.

  • Rejected with a diagnostic, never approximated: everything else, among it pointers, references, classes, templates, a backward goto, bitwise operators and floating point (the list).

  • Parsed and checked, not verified: the annotations beyond requires, ensures, invariant, decreases and check: fold, unfold, predicates, pure functions and the specification functions (Annotations).

  • Results are for one translation unit and mean total correctness: a verified function terminates and satisfies its contract. A contract declared for a function defined elsewhere is trusted, termination included.

What supports it:

  • A bootstrap script that builds the whole toolchain on macOS with Apple silicon (Installation).

  • A test harness that runs cerastes verify, the front end and Viper files, and checks the errors they report, including the line.

  • The annotation layer: nine annotations, written with the macros of <cerastes.h>, parsed and type-checked by the EDG front end, with the rules it cannot check made by cerastes. See Annotations, and Building annotated code with ordinary compilers for building the same source with clang or GCC.

  • scripts/cerastes-fe.sh, a developer tool that runs the front end with cerastes’s checks and prints a listing of EDG’s intermediate language.

Following progress

License

Apache License v2.0 with LLVM Exceptions. The submodules under third_party/ carry their own licenses.