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

CompCert

Pause

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 года.

Категории

Pause