Содержание к диссертации
Введение
1 Обзор методов тестирования компиляторов. Постановка задачи . 22
1.1 Основные понятия теории компиляции 23
1.2 Тестирование синтаксического анализатора 26
1.3 Тестирования фазы анализа статической семантики 31
1.4 Тестирование оптимизирующих преобразований в компиляторе 34
1.5 Тесты для проверки динамической семантики 36
1.6 Тестовые оракулы для фаз оптимизирующих преобразований и генерации кода 40
1.7 Постановка задачи 41
2 Базовые алгоритмы генерации тестовых программ для языка программирования 43
2.1 Описание подхода 44
2.2 Алгоритмы генерации тестов 48
2.3 Результаты главы 57
3 Генерация тестов для проверки реализации динамиче ской семантики 59
3.1 Генерация строго конформных программ 64
3.2 Синтаксис и семантика языка Си5ітріе 67
3.2.1 Язык Сиі 67
3.2.2 Язык Си2: Сиі + указатели 76
3.2.3 Язык Сивіше — Си2 + адресная арифметика, массивы и преобразования типов 78
3.3 Практическая апробация методики 83
3.4 Основные результаты главы 84
4 Критерии покрытия спецификаций семантики языка про граммирования 85
4.1 Система "Montages" описания семантики языков програм мирования 86
4.1.1 Формализм ASM 86
4.1.2 Моитажи как средство описания семантики языков программирования 88
4.2 Критерии покрытия Montage-спецификаций 91
4.2.1 Покрытие ASM-спецификаций 93
4.2.2 Комбинированный критерий покрытия 94
4.2.3 Критерий покрытия для семантических ограничений 95
4.3 Основные результаты главы 97
5 Опыт практического применения предложенной методи ки генерации тестов 98
5.1 Прототипная реализация генератора тестов и системы прогона тестов 99
5.2 Набор тестов для проверки реализации динамической семантики расширений, введенных стандартом Си 99 101
5.3 Тестирование компилятора с языка программирования трС 103
5.3.1 Векторные и параллельные возможности языка трС 105
5.3.2 Использование формализма Montages для определения семантики выражений трС 109
5.3.3 Результаты тестирования 117
5.3.4 Набор негативных тестов 119
5.4 Основные результаты главы 119
Заключение 121
- Тестирование оптимизирующих преобразований в компиляторе
- Алгоритмы генерации тестов
- Язык Сивіше — Си2 + адресная арифметика, массивы и преобразования типов
- Моитажи как средство описания семантики языков программирования
Введение к работе
Общая характеристика работы
Языки высокого уровня давно стали основным средством разработки программного обеспечения. Это явилось причиной широкого распространения программ, обеспечивающих процесс такой разработки и, в частности, компиляторов.
Компиляторы решают задачу перевода языка высокого уровня в представление, которое может быть выполнено ЭВМ. Ошибки в компиляторах приводят к тому, что программы на исходном языке транслируются в исполняемые модули, поведение которых отличается от поведения, определяемого семантикой исходной программы. Такого рода ошибки очень сложно выявлять и исправлять, их наличие ставит под сомнение качество компонент для генерации которых использовался компилятор. Можно с уверенностью утверждать, что корректность работы компилятора с языка программирования является необходимым условием надежной работы любого программного обеспечения, реализованного с его помощью, а контроль правильности работы компиляторов - одной из важнейших мер по обеспечению надежности программного обеспечения.
Для компилятора, как и для любого другого вида программного обеспечения, одним из важнейших методов обеспечения надежности является тестирование. Процесс тестирования включает в себя три основные задачи
Генерация (написание) тестов.
Вынесение вердикта о прохождении теста (тестовый оракул).
Оценка качества тестов (критерий покрытия).
Для решения этих задач применяются различные методы, которые можно разделить на две группы - методы "черного" и "белого" ящика. В первом случае, единственным источником информации для создания тестов является описание функциональности тестируемого продукта, также называемое спецификацией. Во втором, для создания тестов также используется информация о реализации, исходный код тестируемого продукта.
В случае компиляторов, метод черного ящика состоит в получении тестовых наборов по описанию синтаксиса и семантики языка. Такие тестовые наборы предназначены для проверки того, что компилятор работает в соответствии с синтаксисом и семантикой поддерживаемого им языка. Метод белого ящика позволяет учитывать особенности конкретной реализации компилятора. Созданные этим методом тесты позволяют более тщательно проверять части компилятора, специфичные для тестируемой реализации компилятора.
Для тестирования компиляторов важны как методы "черного ящика", так и методы "белого ящика". Эти методы взаимно дополняют друг друга и могут использоваться совместно. Диссертационная работа посвящена тестированию компиляторов на основе формальных спецификаций синтаксиса и семантики языка программирования, т.е. методам "черного ящика".
Язык программирования определяется синтаксисом, статической семантикой и динамической семантикой. Спецификация каждого из этих аспектов языка может быть основой для создания тестов.
Синтаксис языка задается контекстно-свободной грамматикой. Цепочки терминальных символов, выводимые из стартового символа грамматики, называются синтаксически корректными программами. Множество синтаксически корректных программ является подмножеством множества всех цепочек терминальных символов. Они используются для тестирования того, что фаза, синтаксического анализа распознает
тест как корректный и генерирует внутреннее представление. Цепочки, не выводимые из стартового символа, используются для проверки способности компилятора распознавать синтаксическую ошибку.
Статическая семантика, определяемая только для синтаксически корректных программ, задает правила вычисления свойств программы, не требующих для своего вычисления ее выполнения. К таким свойствам относятся, в частности, типы переменных и выражений. Помимо правил вычисления задаются также правила проверки статической корректности программы, или контекстные условия, которые накладывают ограничения на возможные комбинации значений статических свойств программы.
Интерес с точки зрения тестирования представляют как программы, удовлетворяющие контекстным условиям, так и программы, нарушающие их. Программы, удовлетворяющие контекстным условиям, называются статически корректными. Статически корректные программы являются подмножеством множества синтаксически корректных программ. Они используются для тестирования того, что фаза статического анализа в компиляторе правильно распознает корректные программы. Синтаксически корректные программы, нарушающие контекстные условия, используются для проверки способности компилятора распознавать статические ошибки. Такие фразы в дальнейшем также будем называть негативными тестами.
Динамическая семантика определяет смысл выполнения статически корректных программ языка. Для тестирования ее реализации в компиляторе используются статически корректные программы, которые компилируются тестируемым компилятором, полученные в результате загрузочные модули выполняются, после чего их наблюдаемое поведение сравнивается с эталонным, определяемым динамической семантикой языка. Очевидно, что такое сравнение осмысленно только, если программы обладают однозначно определенным наблюдаемым поведением. Такие программы составляют подмножество во множестве всех статически корректных программ и далее в статье называются позитивными тестами.
Подробный обзор исследований, посвященных задаче тестирования на основе описания синтаксиса и семантики языка программирования, приводится в главе 1. На основании этого обзора можно сделать выводы о степени решенности основных задач тестирования, приведенные в таблице 1. Строки таблицы соответствуют задачам тестирования, а столбцы - составляющим описания языка программирования. Жирным шрифтом выделены нерешенные проблемы.
Таблица 1: Степень решенности
На основании проведенного анализа состояния проблемы были сформулированы цель и задачи работы. Целью работы являлась разработка и реализация методов автоматизированной генерации тестов проверки статической и динамической семантики в компиляторах. Для достижения этой цели предполагалось решить следующие основные задачи:
Разработка и реализация алгоритмов генерации тестов, нарушающих контекстные условия (негативные тесты).
Разработка и реализация алгоритмов генерации тестов, предназначенных для проверки реализации динамической семантики в компиляторе1, которые представляют собой статически корректные программы с однозначно определенным поведением (позитивные тесты).
Разработка и реализация критериев покрытия для негативных и позитивных тестов.
На различных этапах решения поставленной задачи применялись различные методы исследования. Для формализации динамической семантики и доказательства ее свойств использовалась структурная операционная семантика (SOS) [53]. Для реализации контекстного анализатора и интерпретатора динамической семантики использовался инструмент Gem-Mex [9], основанный на формализмах Montages [44] и ASM [33] описания операционной семантики программ. Инструменты для генерации тестов и измерения тестового покрытия были реализованы с использованием языков Perl и Shell.
Научная новизна
В диссертационной работе предлагаются новые алгоритмы автоматизированной генерации тестов для проверки реализации статической (негативные тесты) и динамической семантики (позитивные тесты) в компиляторе.
В диссертационной работе впервые сформулирован набор требований к позитивным тестам на основе понятия однозначно определенного наблюдаемого поведения и предложен алгоритм их автоматической генерации с использованием формального описания операционной семантики языка программирования или его подмножества.
Также разработаны критерии новые критерии покрытия для негативных и позитивных тестов. Предложены алгоритмы генерации те-
корректность реализации динамической семантики в компиляторе означает, что для любой программы поведение полученного в результате се компиляции загрузочного модуля должно совпадать с поведением, определяемым динамической семантикой этой программы.
стов, согласованные с этими критериями покрытия.
Все алгоритмы, описанные в диссертационной работе, реализованы и прошли практическую апробацию.
Практическая значимость
Предлагаемая методика автоматизированной генерации тестов для компилятора позволяет существенно облегчить работу по созданию тестовых наборов, заменяя трудоемкий и кропотливый процесс написания программ вручную автоматическим синтезом. Предлагаемый в работе подход к генерации программ с использованием формального описания динамической семантики языка исключает возможность получения некорректного теста (с точностью до ошибок в формализации семантики), в то время как при написании тестовых программ вручную нельзя гарантировать отсутствие ошибок в них.
Разработанные критерии покрытия дают возможность автоматически измерять качество создаваемых тестовых наборов. Такая методика предпочтительнее "интуитивной1' оценки качества тестов, производимой тестировщиком, т.к., во-первых, экономит его усилия, а во-вторых, является более точной.
С помощью реализованных в рамках работы над диссертацией инструментов для автоматизированной генерации тестов и измерения покрытия были получены тестовые наборы для подмножества языка Си, позволившие обнаружить две ошибки в интерпретаторе выражений отладчика Gnu Debugger (версия 3.0) и одну ошибку в промышленном компиляторе. Также эти инструменты были применены для полномасштабного тестирования компилятора с языка параллельного программирования трС, в результате которого было выявлено большое число ошибок.
Апробация работы и публикации
По материалам диссертации опубликовано пять печатных работ.
Основные положения работы докладывались на следующих конференциях и семинарах:
на секции LDTA'2003 (Third Workshop он Language Descriptions, Tools and Applications) международной конференции ETAPS'03 (European Joint Conferences on Theory and Practice of Software), Warsaw, Poland, 2003 r.
на международной конференции ASM'03 (Abstract State Machines), Taormina, Italy, 2003 r.
на секции AS'02 (Action Semantics Workshop) международной конференции FME'02 (Formal Methods Europe), ^Copenhagen, Denmark, 2002 r.
на семинарах Института Системного Программирования РАН, 2002 г. и 2003 г.
Структура и объем диссертации
Диссертация состоит из введения, пяти основных глав, заключения, одного приложения и списка литературы. Общий объем диссертации составляет 156 страницы. Список литературы включает 62 наименования.
Краткое содержание работы
Во введении обосновываются цели и задачи данной работы, ее актуальность, научная новизна и практическая значимость. Приводится краткий обзор работы.
В первой главе производится обзор текущего состояния исследований, связанных с тестированием компиляторов, и формулируется основная задача диссертационной работы.
Во второй главе рассматриваются разработанные автором базовые алгоритмы генерации тестовых программ для компилятора по описанию синтаксиса и семантики языка программирования.
Нередко требуется создавать наборы программ, направленные на тестирование конструкций из некоторого ограниченного подмножества языка. Грамматика такого подмножества содержит меньше правил, чем грамматика всего языка, что позволяет при тех же ограничениях на ресурсы генерировать тестовые наборы, содержащие больше различных комбинаций конструкций этого подмножества. С помощью таких наборов можно провести более тщательное тестирование правильности работы компилятора па выбранных конструкциях.
В этой главе предлагаются способ описания таких подмножеств языка и алгоритмы автоматической генерации тестовых наборов по этому описанию.
Предлагаемый базовый алгоритм генерации синтаксически корректных программ состоит в последовательном построении "снизу-вверх" фраз, выводимых из нетерминальных символов грамматики. Множество фраз, выводимых из нетерминального символа грамматики, называется его синтаксической категорией. Работа алгоритма состоит в последовательном построении фраз из различных категорий, начиная с некоторого множества предопределенных фраз (содержимого предопределенных синтаксических категорий), например, набора идентификаторов и констант. Новые фразы генерируются с помощью применения продукционных правил к ранее сгенерированным фразам. Применение правила состоит в подстановке в вместо нетерминалов из его правой части ранее сгенерированных фраз из соответствующих синтаксических категорий.
Таким образом, процесс генерации управляется описанием некоторого подмножества языка, состоящим из множества правил вывода и множества предопределенных категорий. Содержимое предопределенных категорий и правила вывода определяются тестировщиком и не меняются в процессе генерации тестов. Меняя набор правил вывода и предопределенных категорий, тестировщик может управлять структурой генерируемых тестовых программ.
На основе базового алгоритма генерации синтаксически корректных программ строится алгоритм для построения программ, удовлетворяю-
щих требованиям семантики. Алгоритм основан на фильтрации в соответствии с требованиями семантики множества синтаксически корректных программ, сгенерированных базовым алгоритмом. Рассматриваются возможные оптимизации этого алгоритма для различных частных случаев.
В конце раздела формулируется и доказывается теорема, показывающая возможность построения тестового набора, удовлетворяющего произвольному достижимому критерию покрытия, за конечное число шагов предлагаемым алгоритмом генерации тестов.
В последнем разделе подводится итог и перечисляются результаты главы, которые состоят в следующем:
Предложен новый метод автоматической генерации тестов для компиляторов по индуктивному заданию языка, состоящий в последовательном применении правил вывода к фразам из заданного набора предопределенных синтаксических категорий.
Показано, каким образом предложенный метод может быть использован для генерации семантически корректных программ языка. Для случая, когда семантика языка может быть полностью или частично задана с помощью атрибутной грамматики, приводится оптимизирующее преобразование, позволяющее существенно сократить время генерации тестов.
Доказана теорема, показывающая возможность построения тестового набора, удовлетворяющего произвольному достижимому критерию покрытия, за конечное число шагов предлагаемым алгоритмом генерации семантически корректных тестов.
Третья глава посвящена генерации позитивных тестов. Позитивные тесты представляют собой программы, которые могут быть откомпилированы тестируемым компилятором и выполнены для последующего сравнения наблюдаемого поведения с эталонным (определяемым семантикой программы) и вынесения вердикта о корректности работы
кодогенератора па них. Важнейшим требованием, предъявляемым к позитивным тестам, является то, что их наблюдаемое поведение должно быть определено однозначно, либо допускать конечное (и желательно небольшое) число вариантов. В противном случае, задача сравнения наблюдаемого поведения с эталонным становится очень трудной.
Для таких языков, как Си, предоставляющих гибкие средства для непосредственной работы с памятью, далеко не каждая статически корректная программа обладает однозначно определенным поведением. Рассмотрим в качестве примера следующую программу на Си:
int *р = NULL;
main () -С
printf("'/.d\n"f *(р + 1)); >
Эта программа является статически корректной. В то же время, поведение этой программы не определено, т.к. она включает в себя вычисления с указателем на память, не принадлежащую адресному пространству процесса программы. Неопределенное поведение означает, что возможны любые варианты реакции тестируемой системы на такую программу, например:
компилятор выдаст диагностику об ошибке;
во время выполнения будет выдана диагностика об ошибке;
будет напечатано некоторое значение;
Таким образом, любое поведение компилятора на таком тесте можно считать правильным и проверка правильности этого поведения является очень сложной задачей.
Можно сформулировать ряд требований, которым должны удовлетворять позитивные тесты:
В процессе выполнения теста не должны производиться действия, поведение для которых не определяется в стандарте языка. Действия, для которых поведение не определено, иногда называют ошибками времени выполнения. Примерами такого рода действий могут быть деление на ноль или попытка обращения к памяти, находящейся за пределами адресного пространства процесса, выполняющего программу. Тесты, выполнение которых вызывает неопределенное поведение, очевидно не пригодны для тестирования, т.к. для таких тестов любой вариант наблюдаемого поведения будет правильным и вынесение вердикта о корректности теряет смысл. Программы, удовлетворяющие сформулированному условию, будем называть динамически корректными.
Наблюдаемое поведение теста не должно зависеть от неспецифи-цированиых параметров семантики. Действительно, если выполнение теста зависит от таких параметров, то наблюдаемое поведение может варьироваться в зависимости от реализации, что делает затруднительным тестирование различных компиляторов с помощью одного набора тестов. Программы, удовлетворяющие этому свойству, назовем переносимыми.
Тесты должны быть детерминированы: наблюдаемое поведение теста должно однозначно определяться входными данными. Если это свойство не выполнено, то реализация тестового оракула является нетривиальной задачей, т.к. необходимо выявить все источники неоднозначности поведения и перебрать все возможные варианты поведения программы.
Программы, удовлетворяющие всем трем условиям, называются строго конформными.2.
Способы автоматической генерации строго конформных и просто динамически корректных программ сложнее и изучены в гораздо меньшей
'Термин строго конформный (strictly-conforming) заимствован из стандарта языка Си
степени, чем способы генерации синтаксически и статически корректных программ. Можно сказать, что работы, в которых затрагиваются вопросы автоматической генерации тестов для генератора кода, не предлагают целостного подхода к проверке того, что генерируемые программы обладают детерминированным поведением, выполняются без ошибок и не зависят от определяемых реализацией особенностей семантики.
Подход, предлагаемый в данной работе, позволяет генерировать строго конформные тесты. Для этого выделяется подмножество языка, семантика которого формально задается таким образом, чтобы любая статически корректная программа, выполнение которой в этой семантике не приводит к специально выделенному ошибочному состоянию, являлась строго конформной программой по отношению к исходному языку. Далее это формальное определение используется для создания интерпретатора семантики, позволяющего автоматически выносить вердикт о корректности и вычислять результат работы программы, который используется в тестовом оракуле.
В первом разделе формулируются требования к семантике подмножества языка, позволяющие использовать ее для генерации строго конформных программ в этом языке: семантика, которую можно использовать для генерации строго конформных программ, должна, во-первых, не зависеть от параметров реализации, и, во-вторых, динамически корректная программа в этой семантике должна быть детерминирована и ее выполнение не должно приводить к ситуациям, поведение в которых не определено или не специфицировано в семантике исходного языка.
Второй раздел иллюстрирует применение предложенной в первом разделе методики па примере генерации тестов для языка Си. Для этого формально задается операционная семантика подмножества Си3ітріе языка Си, для которой показывается выполнимость свойств, которым должна удовлетворять семантика, подходящая для генерации строго конформных программ.
Сначала последовательно строятся три вложенных подмножества языка Си: Сиі С Си2 С Си5ітріе. Язык Си3ігаріс достаточно сложен и
включает в себя арифметические операции, операции адресной арифметики и преобразования типов. Для этих подмножеств определяется формальная семантика, для которой выполняются свойства сохранения типов и состояния памяти, которые формулируется в виде двух теорем.
Утверждение первой теоремы состоит в том, что при корректном начальном состоянии памяти любое корректно типизированное выражение либо единственным образом сводится к значению, лежащему в диапазоне значений типа выражения, либо к специально выделенному значению fail, означающему ошибку.
Во второй теореме утверждается, что при корректном начальном состоянии памяти, корректно типизированная программа единственным образом сводится либо к специально выделенному ошибочному состоянию abort, либо к некоторому корректному состоянию памяти.
Неформально, эти теоремы означают, что динамически корректная программа из СиЯігаріе не приводит к ошибочным ситуациям с точки зрения семантики Си, т.к. отсутствие возможных источников ошибок - выхода за границы целого типа и использование в вычислениях некорректных адресов гарантируется свойством сохранения типов. Это означает, что любая динамически корректная программа из Си^шр\е является динамически корректной Си программой. Также показывается выполнение свойств детерминизма и независимости от неспецифицированных параметров динамической семантики для программ из СийітРіе-
Апробация предлагаемого подхода к автоматической генерации тестов рассматривается в третьем разделе главы. Было сгенерировано два набора программ, направленных на тестирования двух новых возможностей языка Си, введенных последним стандартом: арифметики с комплексными числами и адресной арифметики для случая динамических массивов. Сгенерированные наборы строго конформных программ позволили найти ошибки в отладчике Gnu Debugger (GDB) и в промышленном компиляторе.
В третьей главе получены следующие результаты:
1. Предложена методика генерации тестовых программ для языка
программирования, основанная на использовании формальных спецификаций динамической семантики языка. Сгенерированные таким образом программы без ошибок выполняются любой конформной реализацией языка, при этом результат их работы не зависит от неопределенных или определяемых реализацией параметров семантики и однозначно определяется входными данными.
2. Формально описаны абстрактный синтаксис и семантика подмножества языка Си для которого доказаны теоремы сохранения типов и состояния памяти, с помощью которых обоснован тот факт, что любая корректная программа из этого подмножества является строго конформной. Для этого подмножества сгенерирован набор тестов.
Четвертая глава диссертации посвящена измерению тестового покрытия. Информация о покрытии необходима для оценки качества тестового набора и управления генерацией тестов.
В первом разделе главы приводится краткое описание формализма Montages. Каждой конструкции языка программирования соответствует отдельный элемент в спецификации, называемый монтажем. Этот элемент представляет собой диаграмму состояний с приписанными к ее элементам действиями, соответствующими правилам вычисления статической и динамической семантики. Для описания этих действий используется формализм Машин Абстрактных Состояний (ASM). С помощью инструмента Gem-Мех спецификация может быть откомпилирована в исполняемый файл, реализующий интерпретатор с описанного языка.
Для измерения покрытия тестов были разработаны ряд новых критериев покрытия для спецификаций семантики языка программирования в формализме Montages. Для позитивных тестов информация о покрытии строится на основе анализа путей выполнения в интерпретаторе динамической семантики. Тестовый набор, удовлетворяющий критерию покрытия, должен проходить все достижимые пути заданной длины в
интерпретаторе. Этот критерий называется критерием покрытия по п-путям.
Для негативных тестов применяется критерий покрытия ограничений, основанный на анализе причины нарушения контекстного условия. В большинстве случаев контекстное условие может быть сформулировано как одновременное выполнение нескольких семантических условий, называемых базовыми условиями. При этом, причиной нарушения контекстного условия может быть нарушение любого из его базовых условий. Покрытие ограничений достигается па наборе негативных тестов, если для каждой такой причины найдется тест, нарушающий семантику в соответствии с ней.
Для этого критерия доказывается теорема, в соответствии с которой введенный критерий покрытия всегда достижим, если спецификация не содержит избыточных ограничений. На практике, эта теорема применяется следующим образом. При генерации негативных тестов, тесты не увеличивающие покрытие, не добавляются к набору. После окончания процесса генерации производится анализ информации о покрытии ограничений. Если остались непокрытые случаи, то соответствующее ограничение исследуется на предмет наличия избыточных базовых условий. Если таковых не найдено, то модифицируются множество продукционных правил и предопределенных синтаксических категорий так, чтобы при новом запуске генератора были созданы тесты, покрывающие пропущенный случай.
В четвертой главе получены следующие результаты:
Разработан критерий покрытия ограничений статической семантики, позволяющий оценивать качество тестовых наборов, предназначенных для проверки способности компилятора обнаруживать ошибки статической семантики. Доказана теорема о том, что введенный критерий покрытия всегда достижим, если спецификация не содержит избыточных ограничений.
Разработан критерий покрытия динамической семантики Montage-спецификаций, являющийся комбинацией критерия покрытия для
ASM-спецификаций и спецификаций, основанных на конечных автоматах.
В пятой главе рассматривается опыт практического применения методики, предложенной в предыдущих главах.
Первый пример посвящен генерации тестов для языка Си. Основной задачей этого эксперимента была проверка теоретических результатов, изложенных в главе 3. Было сгенерировано два набора программ, направленных на тестирования двух новых возможностей языка Си, введенных последним стандартом (С99): арифметики с комплексными числами и адресной арифметики для случая динамических массивов. С помощью этих наборов удалось выявить 2 ошибки в текущей реализации отладчика Gnu Debugger (GDB): в первом случае неверно вычислялось значение разности между указателями на соседние элементы двумерного динамического массива, а во втором отладчик зависал при вычислении разности двух указателей на один и тот же динамический массив. Также была обнаружена ошибка в реализации адресной арифметики в промышленном компиляторе.
Второй пример - это применение предложенной методики для тестирования генератора кода в компиляторе с языка программирования mpC. Эта работа была выполнена в рамках промышленного проекта но созданию интегрированной среды разработки mpC-приложений трС Workshop. В результате этой работы удалось существенно повысить надежность компилятора, что подтверждает высокую практическую ценность предлагаемой технологии генерации тестов и целесообразность ее применения в процессе промышленной разработки компилятора.
В первом разделе главы рассматривается общая структура генератора тестов. Во втором и третьем разделах описывается опыт генерации тестовых наборов и тестирования компиляторов для языков Си и mpC соответственно.
Результаты пятой главы состоят в следующем:
1. Реализован интерпретатор динамической и статической семантики для строго конформного подмножества Сизітріе языка Си, описан-
ного в третьей главе, и для подмножества языка трС и построен интерпретатор для этого подмножества языка с помощью инструмента Gem-Mex.
2. Реализованы компоненты для генерации тестов и измерения покрытия по формальным спецификациям языка, заданным с помощью формализма Montages. С их помощью сгенерированы тестовые наборы для языков Си и трС. На полученных тестовых наборах были выявлены ошибки в компиляторах с этих языков.
В результате работы над спецификацией семантики языка трС были устранены противоречия и неточности в описании языка, в результате чего была создано новое описание семантики параллельных и векторных выражений трС, приведенное в приложении к диссертации.
Тестирование оптимизирующих преобразований в компиляторе
Для тестирования оптимизирующих преобразований тесты генерируются таким способом, чтобы конструкции, к которым применяются оптимизирующие преобразования, встречались в разных комбинациях. Для этой цели не подходят алгоритмы, предназначенные для генерации тестов общего вида, ориентированные па синтаксис и семантику языка в целом, т.к. с их помощью необходимые тесты могут быть вообще не сгенерированы или сгенерированы в недостаточном количестве.
В работе Burgess и др. [27] описан генератор тестов для тестирования оптимизирующих преобразований в компиляторах с языка Фортран. Входные данные генератора состоят из атрибутной грамматики и настроек генератора, дающих тестировщику возможность управлять генерацией тестов. Настройки включают в себя: 1. Количественные ограничения: максимальная степень вложенности циклов и конструкций ветвления, максимальное число операторов в теле цикла и т.д. 2. Типы данных и переменные, используемые в тестовых программах. 3. Относительные вероятности применения правил грамматики.
Алгоритм генерации состоит в последовательном раскрытии нетерминалов, начиная со стартового символа. Правила для раскрытия выбираются случайно на основе вероятностей, заданных пользователем. Наследуемые атрибуты позволяю! выбирать правило грамматики только в том случае, когда семантическое ограничение истинно, тем самым ограничивая количество сгенерированных тестов, нарушающих семантику.
Для сгенерированных программ производится полное вычисление атрибутов и выносится вердикт о ее статической корректности. Некорректные программы отбрасываются- Проверка динамической корректности программ сводится к проверке отсутствия переполнения и деления на 0 в выражениях и осуществляется на этапе генерации. Другими словами, на подмножество языка для которого генерируются тесты, наложены ограничения, допускающие алго.жтм генерации, порождающий только корректные программы, результат работы которых может быть вычислен статически. К числу таких ограничений относится, например то, что все циклы производят ровно одну итерацию.
Авторы не предлагают каких-либо критериев покрытия для отбора тестов, мотивируя это тем, что метрики, основанные на покрытии правил не обязательно являются адекватным критерием для оценки качества тестового набора. В статье также приведены результаты практических экспериментов, подтверждающие эффективность предлагаемого подхода.
В работах Зеленова и др. 58, 2, 41] рассматривается вопрос автоматической генерации программ для тестирования оптимизирующих преобразований в компиляторах. Для каждого из типов оптимизирующих преобразовании строится модельный язык, который определяет подмножество языка, содержащее только конструкции, к которым может быть применен данный тип преобразований.
Использование модельного языка позволяет абстрагироваться от несущественных с точки зрения данного оптимизирующего преобразования возможностей и генерировать только тесты, предназначенные для тестирования именно этого преобразования- В терминах модельного языка определяется подходящий для тестируемого оптимизирующего преобразования критерий покрытия.
Генератор тестов состоит из двух компонентов: итератора, который последовательно генерирует программы модельного языка исходя из критерии покрытия, и меппера} отображающего программы модельного языка в программы целевого языка.
Проверка правильности работа компилятора па конкретном тесте заключается в сравнении наблюдаемого поведения при выполнении программы с включенной оптимизацией и без нее.
Тесты, построенные па основе динамической семантики языка, используются для проверки корректности кода, генерируемого компилятором или правильности работы интерпретатора. Для типичного языка программирования множество программ, корректных с точки зрения динамической семантики, существенно уже множества статически корректных программ. Таким образом, для целенаправленного тестирования динамической семантики нужны способы генерации динамически корректных программ языка.
Генерация динамически корректных программ является более сложной задачей по сравнению с задачей генерации статически корректных программ. Причина этого заключается прежде всего в сложностях, связанных с формализацией динамической семантики языка программирования. В отличие от синтаксиса и статической семантики, для описа пин которых успешно применяются формальные грамматики, для динамической семантики до сих пор нет общепринятого способа описания. Существующие формальные описания динамической семантики реальных языков программирования редко используются в полном объеме на практике как разработчиками компиляторов, так и специалистами по стандартизации языков.
Начнем с работ, посвященных подходам, не предполагающим автоматическую генерацию тестой В работах Кауфмана [12], Сухомлина [15] и Баскакова [16] рассматриваются методы построения тестов на основе таблиц или диаграмм ситуаций, построенных по текстовому описанию языка. Каждая ситуация содержит описание входных данных (программы па языке программирования) и эффекта, в качестве которого может быть взята ситуация корректного завершения компиляции или диагностики ошибок в случае тестов для статической семантики, либо результат работы программы для тестов, ориентированных на динамическую семантику.
Тесты делятся на три категории - корректные тесты, которые представляют собой правильные программы на Си ++, статически корректные тесты, предназначенные для проверки возможностей транслятора по распознаванию сложных языковых конструкций и тестовые программы, содержащие одну или более семантических ошибок. Последняя категория предназначена для тестирования возможностей компилятора по обнаружению ошибок статической семантики.
Работа R, Guilrnette [31] посвящена системе TGGSy которая позволяет генерировать программы по грамматике, в которой с каждым правилом можно связать ограничение (guard) и семантическое действие (actions). При выборе очередного правила, выполняется семантическое действие и вычисляется ограничение. Если ограничение принимает значение "ложь", то выбирается другое правило.
Алгоритмы генерации тестов
Индуктивное определение языка Индуктивный подход к заданию языка программирования, описаннвій ниже, основан на идеях из работ 57, 38], адаптированных для целей генерации тестов. Пусть G = (Лг3 X, s, Р) - контекстно-свободная грамматика, где TV, Т, Р - множества нетерминальных символов, терминальных символов и про дукционных правил соответственно, а через s обозначен стартовый сим вол грамматики. Синтаксическая категория, соответствующая нетерми нальному символу А7 обозначается через {А}. Каждому продукционно му правилу вида где A\j..., Ап - все нетерминалы в правой части правила, a s\,..., sn+\ - возможно пустые строки терминальных символов, ставится в соответ ствие правило вывода Синтаксическими категориями называются множества фраз, удовлетворяющих правилам вывода- Язык, определяемый грамматикой является синтаксической категорией его стартового символа.
Каждая синтаксическая категория может быть представлена в виде объединения иГС Ь где (А)г определяется следующим образом: For і = 0 :
Алгоритм генерации фраз, основанный па этом определении представлен на Рис. 2.2. Алгоритм принимает четыре входных параметра: множество правил вывода Р, множество РЛГ предопределенных синтаксических категорий, множество их содержимых PN = {{тс)тс Є PN} и число г шагов вывода индукции. В результате работы алгоритма генерируется множество {s)i. Предопределенные синтаксические категории не меняются в процессе генерации алгоритма и их содержимое задается в форме перечисления. Содержимое других категорий строится индуктивно начиная с пустого множества следующим образом: для каждого нетерминала (Л) г-й шаг итерации порождает множество {А)І с помощью применения правил вывода к фразам, сгенерированным на предыдущих итерациях.
Тестировщик имеет возможность управлять работой алгоритма, меняя предопределенные синтаксические категории и множество правил вывода. Минимизация числа предопределенных синтаксических категорий позволяет охватить максимально широкий спектр конструкций языка. При этом ограничения по имеющимся ресурсам компьютеров могут быть препятствием к генерации выражений языка достаточной глубины. В этих случаях количество предопределенных категорий следует увеличивать. Часто тестирование нацелено на какую-то одну или несколько конструкций языка, например циклы или вызовы функций. В этих случаях целесообразно сделать все прочие синтаксические категории предопределенными, тж. это позволит алгоритму максимально полно протестировать конструкции, являющиеся объектом тестирования.
Семантически корректные тесты Программа р, удовлетворяющая всем семантическим ограничениям называется семантически корректной. Этот факт будем обозначать через S Ь р. В противном случае, обозначаемом через В У- р, программу будем называть семантически некорректной. : Целью генерации семантически корректных тестов является построение множества rt- = {р Є {s}{ \ S Ь р} для заданного і.
Алгоритм GenerateSyntaxTestSj рассмотренный выше, предназначен для генерации синтаксически корректных программ. Наиболее очевидный лодході (алгоритм GentrattSemanticsTests на Рис. 2.2) к конструированию семантически корректных программ состоит в том, чтобы сначала сгенерировать множество {s)i и затем отбросить тесты, нарушающие семантические ограничения. Этот подход требует быстродействия и больших объемов памяти, т-К- для реальных языков программирования существенная часть синтаксически корректных программ являются семантически некорректными.
Более экономный и эффективный подход состоит в том, что семантика проверяется для всех генерируемых фраз. Фразы, которые не могут быть частью семантически корректных выражений, отбрасываются и не участвуют в дальнейшей генерации.
В общем случае, семантика вычисляется для полных программ, т.е. элементов категории (s). Однако, в некоторых случаях, семантика может быть частично вычислена для элементов других синтаксических категорий. В результате такого вычисления может быть выявлено, что некоторая фраза не может быть частью семантически корректной программы и, таким образом, может быть исключена из процесса генерации тестов. Такие фразы будем называть строго некорректными. Например, выражения 5 = г и а/0 являются строго некорректными в языке Си.
Алгоритм GcneraieSemanticsTestsFast на Рис. 2.3 является реализацией этого подхода. Он основан па функции z/, определенной таким образом, что v(p) = false влечет то, что р - строго некорректная программа. Выгода от использования v зависит от того, какая часть строго некорректных программ распознается этой функцией. Чем больше эта часть, тем меньше ненужных семантически некорректных тестов будет генерироваться.
Конкретный способ реализации функции v зависит от формализма, выбранного для определения семантики. Функция и должна опираться на свойства семантики, не требующие всей программы для того, чтобы их вычислить: например совместимость типов или проверка lvalue для программ на Си. Эксперименты с генерацией выражений трС [20] показали, что проверка типов и lvalue позволяет выявить основную часть нарушений статической семантики.
Язык Сивіше — Си2 + адресная арифметика, массивы и преобразования типов
Массивы В языке Си8ітріе объявление typedef t id [є] вводит тип массива с именем id, длиной равной значению выражения е и типом элементов t. Абстрактное представление типа, объявленного таким образом, получается с помощью конструктора array(f, JV), где N - значение выражения е.
Массивы состоят из множества объектов одного типа, расположенных н памяти подряд. Объявление массива приводит к созданию дерева объектов данных, корнем которого является объект, соответствующий массиву целиком, а ребра соединяют объект, соответствующий массиву с объектами, соответствующими его элементам. Каждый объект данных получает тип, равный типу соответствующего элемента массива. Согласно идеологии Си многомерный массив рассматривается как "массив массивов и в результате объявления переменной такого типа создается дерево объектов, глубина которого совпадает с числом размерностей массива. Пример такого объявления представлен на рис, 3.6,
Объявление массива int а[3] [2] ; вызывает создание 10 объектов данных (элементов множества Loc). Все эти объекты являются корректными значениями для з казателей на соответствующие типы и также являются корректными адресными значениями. Согласно семантике Си только значения объектов нижнего уровня, обозначенные закрашен-иыми окружностями на рисунке, могут быть изменены. Другие объекты, обозначенные прозрачными окружностями, являются не модифицируемыми адресными значениями, т.е. могут быть операндами операции взятия адреса, но не могут выступать в качестве левого операнда
Выражение типа "массив" в Си преобразуется к типу "указатель на тип элемента массива" всегда, кроме случаев, когда оно является операндом операций sizeof или &. Во всех контекстах, предполагающих такое преобразование типа для выражения е, заменим это выражение на выражение е. 1 Правила вычисления типов и динамическая семантика для этой операции приведены на Рис. 3.7,
Эго преобразование также используется в модели последовательной точки в стандарте С99 [40]
Преобразования типов Операция преобразование типов имеет следующий синтаксис: (type) expr а ее семантика заключается в преобразовании значения выражении txpr к тину type. Допускаются преобразования к арифметическому типу или к типу указателя, В рассматриваемом языке Симетріє имеется всего лишь один арифметический тип - тип гп, и поэтому мы не рассматриваем семантику преобразования выражения одного арифметического типа к другому арифметическому типу. Преобразования указателей к целомзг типу и обратно являются операцией, корректность которой не гарантирована стандартом, поэтому мы тоже ее не рассматриваем. Рассмотрим оставшийся случай: преобразование значения выражения типа указатель к другому типу указателя.
Преобразование значения р указателя к типу t возможно если объект типа t расположен по адресу р. Поскольку первый элемент массива всегда имеет тот же адрес, что и сам массив, то преобразование от указателя на массив к указателю на его первый элемент (и обратно) всегда возможно. Это позволяет ввести отношение эквивалентности как транзитивное и рефлексивное замыкание отношения "быть первым элементом":
Тогда если существует эквивалентный р объект данных типа і, то преобразование значения р указателя к типу і возможно (правило (CAST) на Рис. 3.7). При таком определении, результат операции приведения типа всегда является объектом базового типа указателя, являющегося типом результата.
Адресная арифметика Адресные операции языка CuSimpic включают в себя три арифметических операции: сложение указателя с целым числом, вычитание целого числа из указателя и вычитание двух указателей.
Результат сложение указателя р и целого числа п определен только если р указывает на г-й элемент массива 0 (г + п) JV, где N - число (AREAD) элементов массш а/ При этом, результатом операции является (г + п)-й элемент этого массива. Вычитание числа п из указателя р эквивалентно вычислению выражения р+ {—п). Разность двух указателей определена только, если они указывают на элементы одного и того же массива и результатом операции является целое число, равное разности соответствующих индексов массива. Соответствующее ирапило перехода и вспомогательная функция apply приведены на рис. 3.8.
Моитажи как средство описания семантики языков программирования
Описание языка программирования представляется в виде набора так называемых Мантажей, в состав каждого из которых входит пять элементов: Синтаксическое правило. Записывается в виде формы Бекуса Наура. Граф потока данных и управления. Представляется в графическом виде на языке MVL (Montage Visual Language). MVL-диаграмма представляет собой ориентированный граф, вершинами которого могут быть фигуры двух типов: овалы и прямоугольники. Овалы соответствуют состояниям, связанным с данным монтажем, а прямоугольники соответствуют частям продукционного правила. Вершины соединены с помощью стрелок двух видов: сплошных и пунктирных. Сплошные стрелки предназначены для отображения потока данных, а пунктирные - потока управления. Специально выделенные вершины "Г и "Т"обозначают начальное и конечное состояния соответственно. Правила статической семантики. Правило перехода, выполняемое на проходе вычисления статической семантики. Правило проверки корректности. Представляет собой булевское XASM-выражение, которое должно принимать значение true для семантически корректных программ для данного продукционного правила.
Правила динамической семантики. С каждым состоянием связано свое правило перехода, выполняемое при переходе системы в соответствующее состояние. Рис. 4.1 демонстрирует пример монтажа для операции присваивания в некотором языке программирования. Выполнение полученной спецификации распадается на следующие фазы: Синтаксический анализ. Программа на входном языке разбирается и проверяется на синтаксическую корректность. Конструируется дерево абстрактного синтаксиса (AST). Вычисление статической семантики. На этом шаге происходит вычисление правил статической семантики. тшшенш динамической семантики. Нантом этапе, ОСУІПЄ-етнаястг обход у:шоп Л Т-дореші данной программы if ІЮСЛРДО-вательпвій обход состояний, связанных с каждым узлом и ооотнет-ітнпм о навравлпвпьши ребрами потока управления. При переходе в никоторое состояние выполняется связанное с ним правило динамической семантики. Подробнее рассмотрим последний пункт Для определения динамической семантики используется концепции кош &паёо автомата иа дс-реьс (TFSM) 55- Идея TF3\ l заключается в определении динамиче ской ссмавхшш через конечный автомат, состояниями которого явля кпеи нары, состоящие мл упла AST и состояния локальной машины, заданной MYL. Для каждого ил уллов АВТ-дерсва, рассматриваются только состоянии MVL-машины и с(ютжлч:твующем ему Мса-п&ш\ Переходы в ТК5М представляют собой кораежм вндн: (яге node, тс state, с. irg node, irg siaJe] Переход от (&гс_по(1п. ,4Tc_stale.) к (trg__ node, try state) осуществляется если условие с ИСТИННО. Таким образом, локальные переходы в MVL-машинах отображаются в TFSM-псреходы, в которых исходный и конечный узлы определяются на основе прямоугольных и овальных узлов, являющихся исходным и целевым узлами MVL-псрсходов. Выполнение программы определяется следующим образом.
Пусть пара (GNode, CState) обозначает текущий узел. выполнение начинается с TFSM-состояния, созданного с помощью корневого узла AST и начального состояния MVL-машипы, соот ветствз клцей этому узлу, т.е. CNodc - корневой узел, a CState — L на каждом шаге выполнения: - XASM-правило, ассоциированное с CState, выполняется в контексте, определяемым узлом CNodc. - TFSM-переход с началом в (GNode, CState) произвольно выбирается из тех переходов, чьи условия истинны. - текущий узел CNodc меняется на целевой узел выбранного TFSM-перехода, а текущее состояние CState заменяется па целевое состояние выбранного TFSM-перехода. Пример 4,1.1 Для пллюстраг ш рассмотрим простой язык, опредс-ляелхий двулія монтаоїсами: (рис. 4- )- Н& Рис- 4-3 представлено оы-paoiceuuc языка 1 + 2? его AST-представлсиие и визуальное представление выполнения соответствующей TFSM-модели. Формальная семантика Montage-спецификаций основана на концепциях TFSM и ASM {раздел 4.1). Формализм TFSM близок формализму конечных автоматов и для него естественным является ионятие покрытия, основанное на состояниях конечного автомата и переходах. Формализм ASM во мношм похож т программу на обычном ялы ко программирования, лотшму критерии покрытии ;иш него также похожи пакриторрш, прижлшемие для программ (раздел 4.2.1). мичоекой ггеманг ки Montago-оиоцификїщнй, учитывающий оба формализма TFSM и AS У (раздел 4.2.2) и новый критерий покрытия ограничений, предназначенный для фильтрации негативных тестов (раздел 4.2.Л). Рассмотрим Моаіа і чтшцифмкациіо 6.
Пусть !Ш = \М . ..., hin] множество всех Мон/ажей. входящих в Єн а і! - ялык. ладшіаешлй продукцией л ъш и правилами моїттажей ил Ж Оболи& шм черен Mt;$f состояние st конечного автомата для монтажа М, а через 5Т(9Л) -множество всех таких состояний для всех монтажей из 9Л. В работе Gargantini и Riccobcnc [17] вводятся несколько понятий покрытия для ASM-спецификаций, Рассмотрим понятие сильного покрытия правил (strong parallel rule coverage), которое является одним из наиболее общих критериев покрытия для ASM-спецификаций: Определение 4.2.1 Пусть {г,}, 1 г т - лтоэюсство ASM-npa-вил. Тогда кортеж Т из п правил, взятых из мпооісества {г{}, называется невыполнимым, если все п правил из Т не могут быть одновременно выполнены.
Похожие диссертации на Применение формальных методов для тестирования компиляторов
