README.md 2.76 KB
Newer Older
Guillaume Claret's avatar
Guillaume Claret committed
1
# CompCert
Xavier Leroy's avatar
Xavier Leroy committed
2
The formally-verified C compiler.
3

Guillaume Claret's avatar
Guillaume Claret committed
4
## Overview
xleroy's avatar
xleroy committed
5
The CompCert C verified compiler is a compiler for a large subset of the
Xavier Leroy's avatar
Xavier Leroy committed
6
7
C programming language that generates code for the PowerPC, ARM, x86 and
RISC-V processors.
xleroy's avatar
Updates    
xleroy committed
8

xleroy's avatar
xleroy committed
9
The distinguishing feature of CompCert is that it has been formally
10
11
12
13
verified using the Coq proof assistant: the generated assembly code is
formally guaranteed to behave as prescribed by the semantics of the
source C code.

xleroy's avatar
xleroy committed
14
15
For more information on CompCert (supported platforms, supported C
features, installation instructions, using the compiler, etc), please
Xavier Leroy's avatar
Xavier Leroy committed
16
17
refer to the [Web site](https://compcert.org/) and especially
the [user's manual](https://compcert.org/man/).
Xavier Leroy's avatar
Xavier Leroy committed
18

Sylvain Boulmé's avatar
m    
Sylvain Boulmé committed
19
20
## Verimag version for IntrinSec target

Sylvain Boulmé's avatar
Sylvain Boulmé committed
21
This is an experimental version of CompCert for the IntrinSec target.
Sylvain Boulmé's avatar
Sylvain Boulmé committed
22
See also explanations in our [PriSC paper](https://popl22.sigplan.org/details/prisc-2022-papers/8/A-CompCert-backend-with-symbolic-encryption). The two experimental extensions of our backend described in this paper are in branch `intrinsec_reset` and in branch `abstract_cfi`.
Sylvain Boulmé's avatar
Sylvain Boulmé committed
23

Sylvain Boulmé's avatar
m    
Sylvain Boulmé committed
24
25
26
27
28
29
30
31
32
       
The people responsible for this version are

* Sylvain Boulmé (Grenoble-INP, Verimag)
* Paolo Torrini (Grenoble-INP, Verimag)

For inquiries on this very specific version, contact: 
 Sylvain.Boulme@univ-grenoble-alpes.fr

33
34
35
36
37
38
39
40
41
42
43
44
45
46
## Testing the IntrinSec target of CompCert

First, compile CompCert for `intrinsec`:

1. you need a GCC compiler for RISC-V 32 (e.g. `riscv32-unknown-elf-gcc` installed from `sudo apt-get -y install gcc-riscv64-linux-gnu`).
2. you need to configure CompCert compilation for `intrinsec` (e.g. use [`config_intrinsec.sh`](config_intrinsec.sh)).
3. then, run `make -j`.

Then, you may compile a C file into the IntrinSec assembly. For example, this produce a `nsieve.s` assembly file:

   ```./ccomp -S test/c/nsieve.c -o nsieve.s```

In order to run it, you need an IntrinSec assembler and an IntrinSec emulator, which we are not authorized to provide. If you are interested in, please directly contact Olivier Savry (`olivier.savry@cea.fr`).

Xavier Leroy's avatar
Xavier Leroy committed
47
48
49
50
## License
CompCert is not free software.  This non-commercial release can only
be used for evaluation, research, educational and personal purposes.
A commercial version of CompCert, without this restriction and with
Xavier Leroy's avatar
Xavier Leroy committed
51
professional support and extra features, can be purchased from
Michael Schmidt's avatar
Michael Schmidt committed
52
[AbsInt](https://www.absint.com).  See the file `LICENSE` for more
Xavier Leroy's avatar
Xavier Leroy committed
53
information.
54

Guillaume Claret's avatar
Guillaume Claret committed
55
## Copyright
Xavier Leroy's avatar
Xavier Leroy committed
56
57
58
59
The CompCert verified compiler is Copyright Institut National de
Recherche en Informatique et en Automatique (INRIA) and 
AbsInt Angewandte Informatik GmbH.

60

Guillaume Claret's avatar
Guillaume Claret committed
61
## Contact
Xavier Leroy's avatar
Xavier Leroy committed
62
63
64
65
66
67
General discussions on CompCert take place on the
[compcert-users@inria.fr](https://sympa.inria.fr/sympa/info/compcert-users)
mailing list.

For inquiries on the commercial version of CompCert, please contact
info@absint.com