CompCert Formally-Verified C Compiler

CompCert is a formally-verified C compiler for the core C language. It is distinguished by being verified using the Coq proof assistant, which provides a formal guarantee that the generated assembly code behaves exactly as prescribed by the semantics of the source C code.

Supported Architectures:

• ARM
• PowerPC
• RISC-V
• x86

CompCert is not free software. The version provided in this repository is a non-commercial release restricted to:

• Evaluation
• Research
• Educational purposes
• Personal purposes

For professional use without these restrictions, including access to professional support and additional features, a commercial version must be purchased from AbsInt.

Use clightgen to convert C source files into Coq-formatted abstract syntax files. For every input file src.c, the tool generates a corresponding src.v file containing the Clight or Csyntax representation.

These generated .v files are intended for use in Coq sessions for interactive verification, such as with the VST toolchain.

Command Syntax:

clightgen [options] <C source files>

Options:

• Run clightgen -help to see all available options.
• Many options are shared with the ccomp compiler. For a complete list of compiler-compatible options, refer to the CompCert user's manual.

The README does not contain direct installation commands or API references. For complete information regarding supported C features, installation instructions, and detailed usage guides, you must refer to the official CompCert resources:

• Official Website: https://compcert.org/
• User's Manual: https://compcert.org/man/

The clightgen tool is an experimental feature that transforms C source files into Clight or Csyntax abstract syntax, outputting them as Coq-formatted .v files. To use it, you must explicitly enable it during the CompCert configuration step.

1. Configure CompCert with the -clightgen flag:

   ./configure -clightgen

2. Build CompCert using your standard build process.

Once built, the clightgen binary will be located in the same directory as the ccomp compiler.

The CompCert runtime support library is a collection of helper functions required by code generated by the CompCert compiler. It primarily provides implementations for:

• 64-bit integer arithmetic: Essential for handling 64-bit operations on architectures where they are not natively supported or require specific handling.
• va_arg macro implementation: Provides the logic necessary to implement the va_arg macro from <stdarg.h>, enabling variadic function support.

The library is implemented in assembly language for specific architectures to ensure performance and correctness. If you need to understand the logic behind the assembly implementations, a reference C implementation is available in the c/ directory.

CompCert can execute C files using a reference interpreter instead of compiling to machine code.

Interpreter Options:

• -interp: Execute the given .c files using the reference interpreter.
• -quiet: Suppress diagnostic messages from the interpreter.
• -trace: Produce a detailed trace of reductions.
• -random: Randomize execution order.
• -all: Simulate all possible execution orders.

You can specify how CompCert should be configured using files or environment variables:

1. Via CLI flag: Use -conf <file> to read a specific configuration file. This has the highest precedence.
2. Via CLI flag: Use -target <triple> to read configuration from <triple>.ini instead of the default compcert.ini. The file is searched for in the CompCert installation's share directory.
3. Via Environment Variable: Set COMPCERT_CONFIG to the path of the configuration file. This takes precedence over default search paths and the -target option, but is overridden by -conf.

CompCert C is a formally verified compiler for the C programming language, designed for life-critical and mission-critical software. It accepts most of the ISO C 99 language and produces machine code for PowerPC (32bit), ARM (32bit), AArch64 (ARM 64bit), x86 (32bit and 64bit), and RISC-V (32bit and 64bit) architectures.

Basic Syntax:

ccomp [options] file ...

Recognized Source Files:

• .c: C source file.
• .i, .p: C source file that should not be preprocessed.
• .s: Assembly file.
• .S: Assembly file that must be preprocessed.
• .o: Object file.
• .a: Library file.

The runtime support library provides assembly implementations for the following architectures:

• arm
• powerpc
• powerpc64
• riscV
• x86_32
• x86_64

You can use -d<suffix> flags to save various stages of the compilation process to files for inspection:

• -dprepro: Save C file after preprocessing (<file>.i).
• -dparse: Save C file after parsing and elaboration (<file>.parsed.c).
• -dc: Save generated CompCert C (<file>.compcert.c).
• -dclight: Save generated Clight (<file>.light.c).
• -dcminor: Save generated Cminor (<file>.cm).
• -drtl: Save RTL at various optimization points (<file>.rtl.<n>).
• -dltl: Save LTL after register allocation (<file>.ltl).
• -dmach: Save generated Mach code (<file>.mach).
• -dasm: Save generated assembly (<file>.s).
• -dall: Save all generated intermediate files (<file>.<ext>).
• -sdump: Save abstract syntax tree of generated assembly for post-linking validation (<file>.json).