0781e2b1be
# Cerberus [Cerberus](https://www.cl.cam.ac.uk/~pes20/cerberus/) offers executable semantics for a substantial fragment of 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 The easiest way to install both the Cerberus and Cerberus-CHERI compilers is by using Docker: `docker pull vzaliva/cerberus-cheri` Then, for example, you can print the _Core_ elaboration for `test.c` using ISO C semantics: `docker run -v $HOME/tmp:/mnt -it vzaliva/cerberus-cheri cerberus --pp=core --exec /mnt/test.c` ## Configuration The file `etc/config/c.defaults.properties` defines a group of two compilers: 'cerberus' for ISO C and 'cerberus-cheri' for CHERI-C. It assumes that the corresponding executables are in the path. ## Limitations and Future Improvement 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: - [Cerberus (project page)](https://www.cl.cam.ac.uk/~pes20/cerberus/) - [Cerberus (GitHub repository)](https://github.com/rems-project/cerberus) - ["Formal Mechanised Semantics of CHERI C: Capabilities, Undefined Behaviour, and Provenance" (paper, preprint)](https://zaliva.org/cheric-asplos24.pdf) - ["CHERI C semantics as an extension of the ISO C17 standard" (tech report)](https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-988.html)
How do I ?
This is a how-to guide for the user-interface presented by Compiler Explorer. This doesn't cover the details of how to set up or modify Compiler Explorer for your own needs. For that, please check the documents which already cover topics like:
- Adding a language
- Adding a compiler
- Adding a library
- Adding a tool
- and many more at compiler-explorer/docs
Fast links:
Change the assembly syntax from Intel
The option to switch assembly from Intel to AT&T syntax is present in the Output option of each compiler. If enough
space is not present, the option also presents itself as the gear symbol (⚙)
Compare the time taken by compilation and networking
This is the symbol that looks like a bar graph (📊). If your compilations are taking long, you can use this to check the time taken by:
- Networking, JavaScript, waiting for events, etc.
- Checking the cache and retrieving from it on a cache-hit
- Compilation (on force compilation or cache-miss)
- Parsing the generated assembly before presenting it
View intermediate information provided by the compilers
Though both GCC and Clang create supplementary outputs along with assembly (shown by default), and an executable (created if an executor has been added), the exact nature of the outputs and their formats differ between the compilers.
GCC allows the Tree, IPA, RTL and graph outputs, while Clang allows optimization, AST, IR and graph outputs. Some outputs (e.g. RTL or graph) also have a rich set of options in the UI to enable focussing on a particular function or compiler stage.