CompCert
CompCert — проект по созданию официально верифицированных компиляторов. В рамках проекта разработан компилятор CompCert C для языка С (стандартов ISO C90 / ANSI C с некоторыми незначительными ограничениями и отдельными расширениями, вдохновленные последующими стандартами), а также полностью написана и продемонстрирована система верификации Coq. Основной разработчик — Ксавье Лерой. У этого компилятора есть машинная проверка того, что сгенерированный код ведет себя так же, как и исходный код. Компилятор позволяет генерировать машинный код для архитектур процессора PowerPC, ARM и x86.
| CompCert | |
|---|---|
| Тип | Компилятор |
| Автор | Ксавье Лерой, INRIA |
| Написана на | Caml, Coq |
| Первый выпуск | 3 Апреля 2008 г. |
| Аппаратная платформа | Кроссплатформенное программное обеспечение |
| Последняя версия | |
| Лицензия | бесплатно для некоммерческого использования[2]; коммерческие лицензии от AbsInt |
| Сайт | compcert.inria.fr |
Мотивация
Поскольку компиляторы являются очень сложным программным обеспечением, они часто страдают от большого количества багов[3]. Например, они не могут генерировать код, соответствующий исходному коду. Эти баги могут привести к очень серьезным последствиям в критических областях. Таким образом, цель CompCert в создании формально верифицированного компилятора с математическими гарантиями.
Реализация
Код, сгенерированный CompCert, примерно вдвое быстрее, чем сгенерированный GCC без оптимизации и немного медленнее, чем сгенерированный с более высокими уровнями оптимизации.[4]