Skip to content

Latest commit

 

History

History
77 lines (59 loc) · 3.26 KB

Cerberus.md

File metadata and controls

77 lines (59 loc) · 3.26 KB
Raw

Cerberus

Cerberus offers executable semantics for a substantial fragment of the C and CHERI-C languages. It is implemented via an elaboration into a simpler Core language, which is displayed as the compiler output in the Compiler Explorer. Evaluation of C programs (execution) is also supported.

Prerequisites

To build Cerberus, you need the opam package manager (>= 2.0.0, see here for installation) and OCaml (>= 4.12.0).

Then, the following commands will set up the required opam repositories and download and install the required packages:

opam repo add --yes --this-switch coq-released https://coq.inria.fr/opam/released
opam repo add --yes --this-switch iris-dev https://gitlab.mpi-sws.org/iris/opam.git
opam pin --yes -n coq-struct-tact https://github.com/uwplse/StructTact.git
opam pin --yes -n coq-sail https://github.com/rems-project/coq-sail.git
opam pin --yes -n coq-cheri-capabilities https://github.com/rems-project/coq-cheri-capabilities.git
opam pin add -n --yes cerberus-lib https://github.com/rems-project/cerberus.git
opam pin add -n --yes cerberus https://github.com/rems-project/cerberus.git
opam pin add -n --yes cerberus-cheri https://github.com/rems-project/cerberus.git
opam install --yes cerberus cerberus-cheri

Now you can execute the cerberus-cheri and cerberus commands using opam exec -- cerberus-cheri or opam exec -- cerberus respectively.

Configuration

Once you have Cerberus installed, as described in the previous section, you can enable it by modifying the file etc/config/c.defaults.properties as shown below. This change defines a group of two compilers: 'cerberus' for ISO C and 'cerberus-cheri' for CHERI-C.

compilers=&gcc:&clang:&cerberus

group.cerberus.compilers=cerberus:cerberus-cheri
group.cerberus.compilerType=cerberus
group.cerberus.instructionSet=core
group.cerberus.demangler=
group.cerberus.postProcess=
group.cerberus.options=
group.cerberus.supportsBinary=false
group.cerberus.needsMulti=false
group.cerberus.supportsExecute=true
group.cerberus.interpreted=true
group.cerberus.versionFlag=--version

compiler.cerberus.name=Cerberus
compiler.cerberus.exe=cerberus
compiler.cerberus.objdumper=cerberus

compiler.cerberus-cheri.name=Cerberus-CHERI
compiler.cerberus-cheri.exe=cerberus-cheri
compiler.cerberus-cheri.objdumper=cerberus-cheri

Limitations and Future Improvements

Presently, only simple Core output is shown. It is not syntactically highlighted nor linked to C source code locations. Some potential future improvements include:

  1. Error location handling in warning and error messages.
  2. Specifying execution flags.
  3. Core syntax highlighting.
  4. Display of AST.
  5. Display of other intermediate languages (Cabs, Ail).
  6. Tooltips/links to the ISO C document from Core annotations.

See also: