Систематический подход к верификации функций компилятора
Функции компилятора тесно связаны, поэтому при верификации компилятора необходимо проверять корректность каждой из них. В предлагаемом подходе задача верификации компилятора декомпозируется на основе декомпозиции функциональности компилятора. Мы выделяем следующие задачи:
- Верификация синтаксического анализатора компилятора.
- Верификация семантического анализатора компилятора.
- Верификация оптимизаций и генерации кода.
- Верификация библиотек поддержки времени исполнения (runtime).
Некорректное функционирование подсистемы поддержки исполнения делает почти бесполезным весь компилятор - результат компиляции будет работать неверно из-за ошибок в этой подсистеме и, следовательно, станет непригодным для нужд пользователя. Тесная связь компилятора и подсистемы поддержки исполнения служит обоснованием того, чтобы включить верификацию подсистемы поддержки исполнения в общую задачу верификации компилятора.
Корректность оптимизаций и генерации кода определяет корректность создаваемых транслятором выходных данных. Поэтому верификация этой функциональности является основной задачей верификации компилятора.
От корректности синтаксического анализа и анализа контекстных условий зависит корректность основной функциональности транслятора - оптимизирующих преобразований, генерации кода. Поэтому решение задачи верификации анализа синтаксиса и контекстных условий является базой для решения задач верификации остальных функций компилятора.
В литературе выделяют два вида верификации - статическая верификация средствами анализа кода и аналитической верификации и динамическая верификация посредством тестирования. Компилятор любого практически полезного языка представляет собой настолько сложную систему, что статической верификации поддаются только отдельные небольшие подсистемы, например, отдельные блоки оптимизации. Для решения задач верификации, поставленных выше, на практике используются методы динамической верификации.
В связи с этим при проведении верификации компилятора и его функций необходимо решить следующий набор задач:
- автоматизация построения тестов:
- автоматизация генерации тестовых данных;
- автоматизация проверки корректности обработки тестовых данных (проблема построения оракула);
- определение критерия завершения верификации.
В данной работе мы предлагаем решать эти задачи на систематической основе.
Во всех задачах верификации методы верификации строятся по единой схеме (рис. 1).
