Верификатор промежуточного представления компилятора OpenArkCompiler

Автор: Томашев Д.Д., Ефанов Н.Н.

Журнал: Труды Московского физико-технического института @trudy-mipt

Статья в выпуске: 1 (57) т.15, 2023 года.

Бесплатный доступ

Рассматривается задача верификации промежуточного представления оптимизирующего компилятора. Несмотря на обилие разработанных решений в сфере статической верификации, было решено создать собственное средство верификации, которое отвечает условиям легкой расширяемости и удобства для разработчика компилятора. Для этих целей был создан язык, на котором предполагается описывать условия корректности генерируемых инструкций. Чтобы автоматизировать процесс верификации, был реализован транслятор языка на основе контекстно-свободной грамматики и алгоритма перевода выражений в обратную польскую запись. Полученный верификатор был протестирован на прежуточном представлении MapleIR компилятора OpenArkCompiler и добавлен в него как обязательная часть компиляции.

Еще

Статическая верификация, компиляторы, промежуточные представления, контекстно-свободные грамматики, инструменты разработчика

Короткий адрес: https://sciup.org/142238145

IDR: 142238145

Список литературы Верификатор промежуточного представления компилятора OpenArkCompiler

Mogensen T.E. Introduction to compiler design. Springer, 2017.
Камкин А.С. Введение в формальные методы верификации программ. Москва: МАКС Пресс, 2018.
OpenArkCompiler gitee // Online, 2022.gitee.com/openarkcompiler/OpenArkCompiler/blob/master
Официальная страница clang // Online, 2022. clang.llvm.org
Bright W., Alexandrescu A., Parker M. Origins of the D programming language // Proceedings of the ACM on Programming Languages. 2020. V. 4, N HOPL. P. 1–38.
Ахо А., Ульман Д. Теория синтаксического анализа, перевода и компиляции. Т. 1, 2. Москва: Мир, 1978.
Grune D. [et al.]. Modern compiler design. Springer Science & Business Media, 2012.
Рубцов А.А. Заметки и задачи о регулярных языках и конечных автоматах // Online, 2018. http://www.rubtsov.su/public/books/zz-a5-online.pdf
Hamblin C.L. Translation to and from Polish Notation // The Computer Journal. 1962. V. 5, N 3. P. 210–213.
Официальная страница LLVM // Online, 2022. llvm.org
GCC тесты для float128 // Online, 2022. https://github.com/gcc-mirror/gcc/tree/16e2427f50c208dfe07d07f18009969502c25dc8/gcc/testsuite/gcc.c-torture/execute/ieee

Статья научная