Cerberus C semantics

Web interfaces, papers, and web page

See https://www.cl.cam.ac.uk/~pes20/cerberus/.

Build instructions for the CLI

To build Cerberus, you need opam (>= 2.0.0, see here to install) and OCaml (>= 4.07).

First install the dependencies (including lem and menhir) using opam:

$ opam install --deps-only .

Then build the CLI using:

$ make

The CLI can then be used either from the source directory using:

$ dune exec cerberus -- ARG1 .. ARGN

or, after doing $ make install, using the cerberus executable.

Basic usage

Executing some translation units:

$ cerberus --exec file1.c ... fileN.c

This will elaborate to Core, link, look for a main() function, and start executing the Core from there. To see a printout of the return value, and to get a machine-friendly collection of stdout and stderr, add the --batch argument.

Passing command line arguments to the C program

$ cerberus --args="arg1","arg2" file.c

Printing the intermediate representations

• The C abstract syntax (Cabs) and the Ail intermediate representation can be printed with --ast=cabs and --ast=ail.

• The Ail intermediate representation and the Core program can be pretty-printed with --pp=ail and --pp=core.

Running the elaborate-and-link pipeline without executing:

$ cerberus file1.c ... fileN.c

This will elaborate the C translation units to Core programs, and link them, before returning silently.

Include directories can be added with the usual -I, and macros can be forwarded to the preprocessor using -D (and unset with -U).

---

For more, see cerberus --help

---

Various C programs can be found in tests/.

Building Cerberus-BMC

Install the common dependencies and the following extra ones:

• z3 (4.8.6)
• angstrom (4.06.0)

$ opam install z3 angstrom

Then run:

$ make cerberus-bmc

---

To run:

$ cerberus-bmc --help

Building the web server

Install the common dependencies and the following extra ones:

• z3 (4.8.6)
• angstrom (4.06.0)
• lwt (3.3.0)
• cohttp (2.5.5)
• base64 (2.2.0)
• cohttp-lwt-unix (1.0.3)
• ezgzip (0.2.0)

presuming z3 and angstrom are already installed:

$ opam install lwt cohttp base64 cohttp-lwt-unix ezgzip

Then:

$ make web

This installs all the available web instances as webcerb.* and the web server cerberus-webserver.

To build the UI, install node package manager npm (sudo apt install nodejs npm ) and:

$ make ui

Edit the generated config.json.

Run:

$ cerberus-server --help

Building the abstract interpreter

Install the common dependencies and the APRON library (tested with 20160125).

$ opam install apron

Then:

$ make absint

All targets

You can also compile all the targets with:

$ make all

Docker image

$ make -f Makefile_docker

creates a Docker image than can be used for example with:

$ docker run --volume `PWD`:/data/ cerberus:0.1 tests/tcc/00_assignment.c --pp=core

This image contains all the source code.

People

Contributors:

• Kayvan Memarian
• Christopher Pulte
• Victor B. F. Gomes
• Stella Lau
• Kyndylan Nienhuis
• Justus Matthiesen
• James Lingard
• David Chisnall
• Robert N. M. Watson
• Peter Sewell

The main Cerberus developer is Kayvan Memarian. The experimental CN backend is by Christopher Pulte. Victor Gomes made substantial contributions across the system, and Stella Lau was the main developer of Cerberus BMC. Kyndylan Nienhuis worked on the operational semantics for C11 concurrency. Cerberus originated with Justus Matthiesen's 2010-11 Part II project dissertation and his 2011-12 MPhil dissertation. James Lingard's 2013-14 MPhil dissertation developed a certifying translation validator for simple C programs for the Clang front-end, w.r.t. the Cerberus and Vellvm semantics.

Funding

This software was developed largely within the Rigorous Engineering of Mainstream Systems (REMS) project at the University of Cambridge. It has received funding from the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation programme (grant agreement No 789108, ELVER); the EPSRC Programme Grant REMS: Rigorous Engineering of Mainstream Systems (EP/K008528/1); an EPSRC Leadership Fellowship EP/H005633 (Sewell); a Gates Cambridge Scholarship (Nienhuis); an MIT EECS Graduate Alumni Fellowship (Lau); and Google.