54e2dae21f
This PR adds a detailed Configuration.md document that comprehensively explains the Compiler Explorer configuration system. It covers: - Configuration file structure and hierarchical loading - Property types and automatic conversions - List separators and specialized formats - Group inheritance and compiler configuration - Variable substitution mechanisms - Advanced features like remote compilers and property debugging Additionally, it updates all related documentation to reference this central document for configuration details, reducing duplication and ensuring consistency. This document will serve as the foundation for future configuration system improvements by providing clear documentation of the current implementation.
3.4 KiB
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. For more information about the configuration system and properties files, see Configuration.md.
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:
- Error location handling in warning and error messages.
- Specifying execution flags.
- Core syntax highlighting.
- Display of AST.
- Display of other intermediate languages (Cabs, Ail).
- Tooltips/links to the ISO C document from Core annotations.