АссистентНовый вопросИсторияОбласти знаний
Партнёрские проектыСпецпроектыСтать автором
Сменить язык
О РУВИКИ

CompCert

CompCert — проект по созданию формально верифицированных компиляторов.

Общие сведения
CompCert
Тип Компилятор
Разработчики Ксавье Леруа, Сандрин Блази, INRIA
Написана на OCaml, Rocq
Интерфейс командная строка (ccomp)
Операционная система мультиплатформенный
Первый выпуск 3 апреля 2008
Последняя версия
Репозиторий github.com/AbsInt/CompCe…
Лицензия INRIA Non-Commercial License Agreement
Сайт compcert.org/comp… (англ.)

Продукция

Основной продукт проекта — компилятор CompCert C для языка C (ISO C99 с небольшими ограничениями и рядом расширений, вдохновлённых стандартом ISO C2011[2]), полностью реализованный и проверенный с помощью программного обеспечения Rocq.

Раззработка

Ведущий разработчик проекта — Ксавье Леруа. В проекте также активно участвуют Сандрин Блази, Зайна Дарге, Жак-Анри Журдан, Михаэль Шмидт, Бернард Шоммер и Жан-Батист Тристан.

Для этого компилятора машинно доказано, что сгенерированный им код ведёт себя так же, как исходный исходный код. CompCert способен генерировать машинный код для процессорных архитектур PowerPC, ARM, RISC-V, x86 и x86-64.

Мотивация

Компиляторы относятся к весьма сложному программному обеспечению и часто содержат множество ошибок[3]. Например, компилятор может сгенерировать код, не соответствующий исходному. Такие ошибки могут иметь серьёзные последствия в критически важных областях. Поэтому задача CompCert состоит в создании формально верифицированного компилятора с математической гарантией корректности.

Производительность

Сгенерированный CompCert код примерно вдвое быстрее, чем код, полученный с помощью GCC без оптимизации, и немного медленнее кода, сгенерированного GCC с высокими уровнями оптимизации[4].

Награды

CompCert был отмечен наградой Ассоциации вычислительной техники — премией Software System в 2021 году[5].

Примечания

  1. ↑ Release 3.16 — 2025.
  2. ↑ The CompCert C language (англ.). compcert.org. Дата обращения: 31 марта 2022. Архивировано 29 апреля 2025 года.
  3. ↑ Xuejun Yang, Yang Chen, Eric Eide, John Regehr. Finding and Understanding Bugs in C Compilers (англ.). University of Utah, School of Computing. Архивировано 9 апреля 2011 года.
  4. ↑ CompCert — Performance of the generated code (англ.). INRIA. Архивировано 17 мая 2008 года.
  5. ↑ CompCert récompensé par l’ACM pour ses garanties d’absence de bugs (фр.). CNRS (14 июня 2022). Дата обращения: 17 апреля 2023. Архивировано 19 июня 2025 года.

Категории