За этим следует оптимизационный шаг constraint elimination. Предыдущий проход, декомпозиция, создает большое количество избыточных guard-команд, что упрощает верификацию алгоритма, но снижает быстродействие получаемого кода, поэтому данный этап нацелен на их стирание. Тут используется еще одно IR - PolyLoopSimpl, куда добавлен примитив simplify, минимизирующий политоп по заданному ограничению.

Последний шаг - трансляция программы в AST Loop, состоящее из классических команд типа if и for, которое и является результатом работы кодогенератора. Основная задача на этом этапе - трансляция loop-команд.

Полученный кодогенератор (фактически, аналог CLooG) может быть экстрагирован в Окамл и позволяет получать модели императивных программ из полиэдрального представления, впрочем, работающего фронтенда у него нет, так что представления нужно расписывать вручную.

Формализация на Coq (около 8 тысяч строк) потребовала реализовать небольшую библиотеку для линейной алгебры, операции для работы над политопами, а также описать семантику промежуточных представлений и доказать соответствующие теоремы о корректности трансляции в Loop. Как правило, верификация компиляторных проходов делается либо через доказательства сохранения семантики, либо методом валидации трансляции. В статье использована их комбинация - валидация для полиэдральных операций и доказательства для семантик всех проходов кодогенератора. Здесь заметно, что статья является продолжением линии французских работ по (в том числе верифицированным) полиэдральным методам - дается ряд ссылок на предшественников.

В заключении дан обзор методов полиэдральной кодогенерации, упомянуты применения для верификации нейросетей. Также сообщается о найденной потенциальной ошибке, связанной с упорядочиванием трёх и более политопов в алгоритме генерации циклов Quillere [2000]. Авторы выражают желание в будущем заняться верификацией непосредственно оптимизаций и реализовать генерацию С кода из Loop AST, как шаг к добавлению полиэдрального оптимизатора в CompCert. Основная потенциальная проблема - переход от арифметики произвольной точности к операциям с переполнениям.

#codegen #coq #polyhedral #verification