1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
|
# CompCert
The formally-verified C compiler.
## Overview
The CompCert C verified compiler is a compiler for a large subset of the
C programming language that generates code for the PowerPC, ARM, x86 and
RISC-V processors.
The distinguishing feature of CompCert is that it has been formally
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.
For more information on CompCert (supported platforms, supported C
features, installation instructions, using the compiler, etc), please
refer to the [Web site](https://compcert.org/) and especially
the [user's manual](https://compcert.org/man/).
## Verimag-Kalray version
This is a special version with additions from Verimag and Kalray :
* A backend for the KVX processor: see [`README_Kalray.md`](README_Kalray.md) for details.
* Some general-purpose optimization phases (e.g. profiling).
* see [`PROFILING.md`](PROFILING.md) for details on the profiling system
The people responsible for this version are
* Sylvain Boulmé (Grenoble-INP, Verimag)
* David Monniaux (CNRS, Verimag)
* Cyril Six (Kalray)
## Papers, docs, etc on this CompCert version
* [a 5-minutes video](http://www-verimag.imag.fr/~boulme/videos/poster-oopsla20.mp4) by C. Six, presenting the postpass scheduling and the KVX backend
(also on [YouTube if you need subtitles](https://www.youtube.com/watch?v=RAzMDS9OVSw)).
* [Certified and Efficient Instruction Scheduling](https://hal.archives-ouvertes.fr/hal-02185883), an OOPSLA'20 paper, by Six, Boulmé and Monniaux.
* [the documentation of the KVX backend Coq sources](https://certicompil.gricad-pages.univ-grenoble-alpes.fr/compcert-kvx)
## CompCertSSA version
This development is a version of CompCert extended with an SSA
middle-end:
- construction of the SSA form, from RTL
- SSA-based optimizations
- SSA-related librairies on dominance and dominators
- SSA destruction with coalescing, on the Conventional SSA form
The following people contibuted to this extension (alphabetic order):
Sandrine Blazy, Delphine Demange, Yon Fernandez de Retana, David
Pichardie, Léo Stefanesco.
## 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
professional support and extra features, can be purchased from
[AbsInt](https://www.absint.com). See the file `LICENSE` for more
information.
## Copyright
The CompCert verified compiler is Copyright Institut National de
Recherche en Informatique et en Automatique (INRIA) and
AbsInt Angewandte Informatik GmbH.
The additions related to CSE3, LICM and the KVX backend are Copyright Grenoble-INP, CNRS and Kalray.
The additions related to the SSA middle-end are Copyright Univ Rennes,
Inria, IRISA.
## Contact
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
For inquiries on the Verimag-specific additions, contact the researchers.
For inquiries on the SSA-specific additions, please contact Delphine
Demange.
|
