Подход к решению задачи проверки сохранения семантики программы во время работы оптимизатора
При тестировании важной задачей является анализ правильности работы тестируемой системы. Для случая оптимизатора такой анализ состоит из двух частей:
- проверка, что семантика программы не изменилась после работы оптимизатора;
- проверка, что были произведены все оптимизирующие трансформации.
В настоящей работе мы не касаемся проверки того, что все трансформации были сделаны. Мы здесь рассматриваем лишь необходимую часть оракула, а именно проверку сохранения семантики программы после оптимизации.
Задача проверки сохранения семантики произвольной программы при обработке ее оптимизатором равносильна задаче проверки эквивалентности двух программ. Эта задача в общем случае неразрешима. Тем не менее, для некоторых видов программ такая задача может быть решена. Например, для программ, функциональная семантика которых полностью представляется их трассой.
Напомним, что мы считаем неразличимыми для оптимизатора те программы, которым соответствуют одинаковые модельные структуры. Таким образом, можно в качестве представителей классов эквивалентности выбрать программы, функциональная семантика которых полностью представляется трассой. Для таких программ задача проверки сохранения семантики во время работы оптимизатора сводится к сравнению трассы оптимизированной программы и некоторой эталонной трассы. В качестве такого эталона мы предлагаем использовать трассу, выдаваемую неоптимизированной версией той же программы.
Пример: Инструкции для трассировки в тесте для анализатора Weak-Zero SIV Subscripts. Ниже приведен пример тестового воздействия для анализатора Weak-Zero SIV Subscripts на языке программирования C: 01: void f( int i, int* a, int* b, int* c ) 02: { 03: for( i = -10; i
Строки 03-06 содержат код, построенный по модельной структуре. Строки 07-09 содержат инструкции для трассировки.
Для решения задачи проверки сохранения оптимизатором семантики необходимо иметь множество тестов и оракул.
Для построения набора тестов будем генерировать программы P, обладающие следующими свойствами:
- множество программ P является представительным для алгоритма тестируемого оптимизатора, т.е. это множество соответствует выбранному критерию тестового покрытия;
- каждая P компилируется, т.е. синтаксически и семантически корректна;
- каждая P корректно завершается за конечное время;
- каждая P содержит некоторые вычисления в тех местах, которые должны подвергаться оптимизации;
- функциональная семантика каждой P состоит в выводе информации, зависящей от всех имеющихся в программе вычислений.
Работа оракула заключается в следующем:
- каждый тест компилируется дважды - с оптимизацией и без оптимизации;
- обе откомпилированные версии запускаются на исполнение;
- полученные трассы сравниваются;
- семантика признается сохранившейся в том и только том случае, если трассы эквивалентны.
Далее в статье мы подробно рассмотрим процессы генерации и запуска тестов.
