CompCert

Last updated
CompCert
Original author(s) Xavier Leroy
Developer(s) AbsInt
Initial release2005;19 years ago (2005)
Stable release
3.12 / 25 November 2022; 4 July 2023 [1] [2]
Repository
Type Compiler
License free for noncommercial use [3]
Website compcert.org/compcert-C.html OOjs UI icon edit-ltr-progressive.svg

CompCert is a formally verified optimizing compiler for a large subset of the C99 programming language (known as Clight) which currently targets PowerPC, ARM, RISC-V, x86 and x86-64 [4] architectures. [5] This project, led by Xavier Leroy, started officially in 2005, funded by the French institutes ANR and INRIA. The compiler is specified, programmed and proven in Coq. It aims to be used for programming embedded systems requiring reliability. The performance of its generated code is often close to that of GCC (version 3) at optimization level -O1, and always better than that of GCC without optimizations. [6]

Since 2015, AbsInt offers commercial licenses, [7] provides support and maintenance, and contributes to the advancement of the tool. CompCert is released under a noncommercial license, and is therefore not free software, although some of its source files are dual-licensed with the GNU Lesser General Public License version 2.1 or later or are available under the terms of other licenses. [3]

For the development of CompCert, the first practically useful optimizing compiler targeting multiple commercial architectures that has a complete, mechanically checked proof of its correctness, Xavier Leroy and the development team of CompCert received the 2021 ACM Software System Award.

Related Research Articles

In computing, a compiler is a computer program that translates computer code written in one programming language into another language. The name "compiler" is primarily used for programs that translate source code from a high-level programming language to a low-level programming language to create an executable program.

<span class="mw-page-title-main">GNU Compiler Collection</span> Free and open-source compiler for various programming languages

The GNU Compiler Collection (GCC) is an optimizing compiler produced by the GNU Project supporting various programming languages, hardware architectures and operating systems. The Free Software Foundation (FSF) distributes GCC as free software under the GNU General Public License. GCC is a key component of the GNU toolchain and the standard compiler for most projects related to GNU and the Linux kernel. With roughly 15 million lines of code in 2019, GCC is one of the biggest free programs in existence. It has played an important role in the growth of free software, as both a tool and an example.

OCaml is a general-purpose, high-level, multi-paradigm programming language which extends the Caml dialect of ML with object-oriented features. OCaml was created in 1996 by Xavier Leroy, Jérôme Vouillon, Damien Doligez, Didier Rémy, Ascánder Suárez, and others.

L4 is a family of second-generation microkernels, used to implement a variety of types of operating systems (OS), though mostly for Unix-like, Portable Operating System Interface (POSIX) compliant types.

<span class="mw-page-title-main">GNAT</span> Free-software compiler for the Ada programming language

GNAT is a free-software compiler for the Ada programming language which forms part of the GNU Compiler Collection (GCC). It supports all versions of the language, i.e. Ada 2012, Ada 2005, Ada 95 and Ada 83. Originally its name was an acronym that stood for GNU NYU Ada Translator, but that name no longer applies. The front-end and run-time are written in Ada.

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of a system with respect to a certain formal specification or property, using formal methods of mathematics. Formal verification is a key incentive for formal specification of systems, and is at the core of formal methods. It represents an important dimension of analysis and verification in electronic design automation and is one approach to software verification. The use of formal verification enables the highest Evaluation Assurance Level (EAL7) in the framework of common criteria for computer security certification.

A cross compiler is a compiler capable of creating executable code for a platform other than the one on which the compiler is running. For example, a compiler that runs on a PC but generates code that runs on an Android smartphone is a cross compiler.

<span class="mw-page-title-main">LLVM</span> Compiler backend for multiple programming languages

LLVM is a set of compiler and toolchain technologies that can be used to develop a frontend for any programming language and a backend for any instruction set architecture. LLVM is designed around a language-independent intermediate representation (IR) that serves as a portable, high-level assembly language that can be optimized with a variety of transformations over multiple passes. The name LLVM originally stood for Low Level Virtual Machine, though the project has expanded and the name is no longer officially an initialism.

Open64 is a free, open-source, optimizing compiler for the Itanium and x86-64 microprocessor architectures. It derives from the SGI compilers for the MIPS R10000 processor, called MIPSPro. It was initially released in 2000 as GNU GPL software under the name Pro64. The following year, University of Delaware adopted the project and renamed the compiler to Open64. It now mostly serves as a research platform for compiler and computer architecture research groups. Open64 supports Fortran 77/95 and C/C++, as well as the shared memory programming model OpenMP. It can conduct high-quality interprocedural analysis, data-flow analysis, data dependence analysis, and array region analysis. Development has ceased, although other projects can use the project's source.

SIGPLAN is the Association for Computing Machinery's Special Interest Group on programming languages.

<span class="mw-page-title-main">Xavier Leroy</span> French computer scientist and programmer (born 1968)

Xavier Leroy is a French computer scientist and programmer. He is best known for his role as a primary developer of the OCaml system. He is Professor of software science at Collège de France. Before his appointment at Collège de France in 2018, he was senior scientist at the French government research institution Inria.

The Portable C Compiler is an early compiler for the C programming language written by Stephen C. Johnson of Bell Labs in the mid-1970s, based in part on ideas proposed by Alan Snyder in 1973, and "distributed as the C compiler by Bell Labs... with the blessing of Dennis Ritchie."

Oracle Developer Studio, formerly named Oracle Solaris Studio, Sun Studio, Sun WorkShop, Forte Developer, and SunPro Compilers, is the Oracle Corporation's flagship software development product for the Solaris and Linux operating systems. It includes optimizing C, C++, and Fortran compilers, libraries, and performance analysis and debugging tools, for Solaris on SPARC and x86 platforms, and Linux on x86/x64 platforms, including multi-core systems.

<span class="mw-page-title-main">Ikarus (Scheme implementation)</span> R6RS Scheme compiler

Ikarus Scheme is a free software optimizing incremental compiler for R6RS Scheme that compiles directly to the x86 IA-32 architecture. Ikarus is the first public implementation of a large part of the R6RS Scheme standard. Version 0.0.3 has 94% of the total R6RS forms and procedures. Development stopped in 2008.

In computing, compiler correctness is the branch of computer science that deals with trying to show that a compiler behaves according to its language specification. Techniques include developing the compiler using formal methods and using rigorous testing on an existing compiler.

DDC-I, Inc. is a privately held company providing software development of real-time operating systems, software development tools, and software services for safety-critical embedded applications, headquartered in Phoenix, Arizona. It was first created in 1985 as the Danish firm DDC International A/S, a commercial outgrowth of Dansk Datamatik Center, a Danish software research and development organization of the 1980s. The American subsidiary was created in 1986. For many years, the firm specialized in language compilers for the programming language Ada.

<span class="mw-page-title-main">Thierry Coquand</span> French computer scientist and mathematician

Thierry Coquand is a French computer scientist and mathematician who is currently a professor of computer science at the University of Gothenburg, having previously worked at INRIA. He is known for his work in constructive mathematics, especially the calculus of constructions.

AbsInt is a software-development tools vendor based in Saarbrücken, Germany. The company was founded in 1998 as a technology spin-off from the Department of Programming Languages and Compiler Construction of Prof. Reinhard Wilhelm at Saarland University. AbsInt specializes in software-verification tools based on abstract interpretation. Its tools are used worldwide by Fortune 500 companies, educational institutions, government agencies and startups.

References

  1. "Release 3.12". 25 November 2022. Retrieved 8 December 2022.
  2. "Release 3.13". 4 July 2023. Retrieved 2 November 2023.
  3. 1 2 "CompCert License".
  4. v3.0 Release Notes
  5. CompCert Website
  6. CompCert Performance
  7. "CompCert - Partners". compcert.inria.fr. Retrieved 2019-03-21.