Применение формальных методов для тестирования компиляторов тема диссертации и автореферата по ВАК РФ 05.13.11, кандидат физико-математических наук Посыпкин, Михаил Анатольевич

• Посыпкин, Михаил Анатольевич
• кандидат физико-математических наук
• 2004

Оглавление диссертации кандидат физико-математических наук Посыпкин, Михаил Анатольевич

Введение

1 Обзор методов тестирования компиляторов. Постановка задачи.

1.1 Основные понятия теории компиляции

1.2 Тестирование синтаксического анализатора.

1.3 Тестирования фазы анализа статической семантики.

1.4 Тестирование оптимизирующих преобразований в компиляторе

1.5 Тесты для проверки динамической семантики

1.6 Тестовые оракулы для фаз оптимизирующих преобразований и генерации кода.

1.7 Постановка задачи.

2 Базовые алгоритмы генерации тестовых программ для языка программирования

2.1 Описание подхода.

2.2 Алгоритмы генерации тестов.

2.3 Результаты главы

3 Генерация тестов для проверки реализации динамической семантики

3.1 Генерация строго конформных программ.

3.2 Синтаксис и семантика языка CHSimpie.

3.2.1 ЯзыкСи!.

3.2.2 Язык Сиг: Chi + указатели.

3.2.3 Язык CHSimpie = Си2 + адресная арифметика, массивы и преобразования типов.

3.3 Практическая апробация методики.

3.4 Основные результаты главы.

4 Критерии покрытия спецификаций семантики языка программирования

4.1 Система "Montages" описания семантики языков программирования

4.1.1 Формализм ASM.

4.1.2 Монтажи как средство описания семантики языков программирования.

4.2 Критерии покрытия Montage-спецификаций

4.2.1 Покрытие ASM-спецификаций.

4.2.2 Комбинированный критерий покрытия

4.2.3 Критерий покрытия для семантических ограничений

4.3 Основные результаты главы.

5 Опыт практического применения предложенной методики генерации тестов

5.1 Прототипная реализация генератора тестов и системы прогона тестов.

5.2 Набор тестов для проверки реализации динамической семантики расширений, введенных стандартом Си 99 . 101 5.3 Тестирование компилятора с языка программирования шрС

5.3.1 Векторные и параллельные возможности языка трС

5.3.2 Использование формализма Montages для определения семантики выражений трС.

5.3.3 Результаты тестирования.

5.3.4 Набор негативных тестов.

5.4 Основные результаты главы.

Введение диссертации (часть автореферата) на тему «Применение формальных методов для тестирования компиляторов»

Общая характеристика работы

Языки высокого уровня давно стали основным средством разработки программного обеспечения. Это явилось причиной широкого распространения программ, обеспечивающих процесс такой разработки и, в частности, компиляторов.

Компиляторы решают задачу перевода языка высокого уровня в представление, которое может быть выполнено ЭВМ. Ошибки в компиляторах приводят к тому, что программы на исходном языке транслируются в исполняемые модули, поведение которых отличается от поведения, определяемого семантикой исходной программы. Такого рода ошибки очень сложно выявлять и исправлять, их наличие ставит под сомнение качество компонент для генерации которых использовался компилятор. Можно с уверенностью утверждать, что корректность работы компилятора с языка программирования является необходимым условием надежной работы любого программного обеспечения, реализованного с его помощью, а контроль правильности работы компиляторов - одной из важнейших мер по обеспечению надежности программного обеспечения.

Для компилятора, как и для любого другого вида программного обеспечения, одним из важнейших методов обеспечения надежности является тестирование. Процесс тестирования включает в себя три основные задачи

• Генерация (написание) тестов.

• Вынесение вердикта о прохождении теста (тестовый оракул).

• Оценка качества тестов (критерий покрытия).

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

В случае компиляторов, метод черного ящика состоит в получении тестовых наборов по описанию синтаксиса и семантики языка. Такие тестовые наборы предназначены для проверки того, что компилятор работает в соответствии с синтаксисом и семантикой поддерживаемого им языка. Метод белого ящика позволяет учитывать особенности конкретной реализации компилятора. Созданные этим методом тесты позволяют более тщательно проверять части компилятора, специфичные для тестируемой реализации компилятора.

Для тестирования компиляторов важны как методы "черного ящика", так и методы "белого ящика". Эти методы взаимно дополняют друг друга и могут использоваться совместно. Диссертационная работа посвящена тестированию компиляторов на основе формальных спецификаций синтаксиса и семантики языка программирования, т.е. методам "черного ящика".

Язык программирования определяется синтаксисом, статической семантикой и динамической семантикой. Спецификация каждого из этих аспектов языка может быть основой для создания тестов.

Синтаксис языка задается контекстно-свободной грамматикой. Цепочки терминальных символов, выводимые из стартового символа грамматики, называются синтаксически корректными программами. Множество синтаксически корректных программ является подмножеством множества всех цепочек терминальных символов. Они используются для тестирования того, что фаза синтаксического анализа распознает тест как корректный и генерирует внутреннее представление. Цепочки, не выводимые из стартового символа, используются для проверки способности компилятора распознавать синтаксическую ошибку.

Статическая семантика, определяемая только для синтаксически корректных программ, задает правила вычисления свойств программы, не требующих для своего вычисления ее выполнения. К таким свойствам относятся, в частности, типы переменных и выражений. Помимо правил вычисления задаются также правила проверки статической корректности программы, или контекстные условия, которые накладывают ограничения на возможные комбинации значений статических свойств программы.

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

Динамическая семантика определяет смысл выполнения статически корректных программ языка. Для тестирования ее реализации в компиляторе используются статически корректные программы, которые компилируются тестируемым компилятором, полученные в результате загрузочные модули выполняются, после чего их наблюдаемое поведение сравнивается с эталонным, определяемым динамической семантикой языка. Очевидно, что такое сравнение осмысленно только, если программы обладают однозначно определенным наблюдаемым поведением. Такие программы составляют подмножество во множестве всех статически корректных программ и далее в статье называются позитивными тестами.

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

Синтаксис Статическая семантика Динамическая семантика

Генерация тестов Предложены алгоритмы генерации синтакс. корректных и некорректных тестов. Предложены алгоритмы генерации статически корректных тестов. Нет алгоритмов генерации тестов, содержащих ошибки. Решена для ряда частных случаев. Отсутствуют алгоритмы генерации программ с однозначным наблюдаемым поведением.

Тестовый оракул Проверяет способность компилятора воспринимать корректные тесты и обнаруживать ошибки в некорректных тестах. Подходы, основанные на сравнении наблюдаемого поведения.

Критерий покрытия Предложен ряд критериев для синтаксически корректных и некорректных тестов. Предложен ряд критериев для статически корректных тестов. Нет критериев для тестов, содержащих ошибку. Отсутствуют какие-либо критерии покрытия.

Таблица 1: Степень решенности

На основании проведенного анализа состояния проблемы были сформулированы цель и задачи работы. Целью работы являлась разработка и реализация методов автоматизированной генерации тестов проверки статической и динамической семантики в компиляторах. Для достижения этой цели предполагалось решить следующие основные задачи:

• Разработка и реализация алгоритмов генерации тестов, нарушающих контекстные условия (негативные тесты).

• Разработка и реализация алгоритмов генерации тестов, предназначенных для проверки реализации динамической семантики в компиляторе1, которые представляют собой статически корректные программы с однозначно определенным поведением (позитивные тесты).

• Разработка и реализация критериев покрытия для негативных и позитивных тестов.

На различных этапах решения поставленной задачи применялись различные методы исследования. Для формализации динамической семантики и доказательства ее свойств использовалась структурная операционная семантика (SOS) [53]. Для реализации контекстного анализатора и интерпретатора динамической семантики использовался инструмент Gem-Mex [9], основанный на формализмах Montages [44] и ASM [33] описания операционной семантики программ. Инструменты для генерации тестов и измерения тестового покрытия были реализованы с использованием языков Perl и Shell.

Научная новизна

В диссертационной работе предлагаются новые алгоритмы автоматизированной генерации тестов для проверки реализации статической (негативные тесты) и динамической семантики (позитивные тесты) в компиляторе.

В диссертационной работе впервые сформулирован набор требований к позитивным тестам на основе понятия однозначно определенного наблюдаемого поведения и предложен алгоритм их автоматической генерации с использованием формального описания операционной семантики языка программирования или его подмножества.

Также разработаны критерии новые критерии покрытия для негативных и позитивных тестов. Предложены алгоритмы генерации те

1 Корректность реализации динамической семантики в компиляторе означает, что для любой программы поведение полученного в результате ее компиляции загрузочного модуля должно совпадать с поведением, определяемым динамической семантикой этой программы. стов, согласованные с этими критериями покрытия.

Все алгоритмы, описанные в диссертационной работе, реализованы и прошли практическую апробацию.

Практическая значимость

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

Разработанные критерии покрытия дают возможность автоматически измерять качество создаваемых тестовых наборов. Такая методика предпочтительнее "интуитивной" оценки качества тестов, производимой тестировщиком, т.к., во-первых, экономит его усилия, а во-вторых, является более точной.

С помощью реализованных в рамках работы над диссертацией инструментов для автоматизированной генерации тестов и измерения покрытия были получены тестовые наборы для подмножества языка Си, позволившие обнаружить две ошибки в интерпретаторе выражений отладчика Gnu Debugger (версия 3.0) и одну ошибку в промышленном компиляторе. Также эти инструменты были применены для полномасштабного тестирования компилятора с языка параллельного программирования трС, в результате которого было выявлено большое число ошибок.

Апробация работы и публикации

По материалам диссертации опубликовано пять печатных работ.

Основные положения работы докладывались на следующих конференциях и семинарах:

• на секции LDTA'2003 (Third Workshop on 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), Kopenhagen, Denmark, 2002 r.

• на семинарах Института Системного Программирования РАН, 2002 г. и 2003 г.

Структура и объем диссертации

Диссертация состоит из введения, пяти основных глав, заключения, одного приложения и списка литературы. Общий объем диссертации составляет 156 страницы. Список литературы включает 62 наименования.

Заключение диссертации по теме «Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей», Посыпкин, Михаил Анатольевич

5.4 Основные результаты главы

В этой главе описаны следующие результаты практического применения предлагаемого в работе подхода к тестированию компиляторов:

1. Реализован интерпретатор динамической и статической семантики для подмножества Си simple языка Си, описанного в третьей главе, и для подмножества языка шрС и построен интерпретатор программ из этого подмножества с помощью инструмента Gem-Mex.

2. Реализованы компоненты для генерации тестов и измерения покрытия по формальным спецификациям языка, заданным с помощью формализма Montages. С их помощью сгенерированы тестовые наборы для языков Си и трС. На полученных тестовых наборах были выявлены ошибки в компиляторах с этих языков.

Результаты этой главы опубликованы в работах [20, 19].

Список литературы диссертационного исследования кандидат физико-математических наук Посыпкин, Михаил Анатольевич, 2004 год

1. М.А. Посыпкин. Применение формальных методов для тестирования компиляторов. Препринт ИСП РАН, 12 стр., 2004.

2. Зеленов С.А., Зеленова С.В., Косачев А.С., Петренко А.К. Применение модельного подхода для автоматического тестирования оптимизирующих компиляторов, http://www.citforrnn.ru.

3. Петренко А.К. Чацкина Т.А. Борисова М.В., Морозова Т.А. Тестирование компиляторов на основе формальной модели языка. Москва. Институт Прикладной Математики им. М.В. Келдыша Российской Академии Наук, 1992.

4. Зеленова С.В. Демаков А.В., Зеленов С.А. Тестирование парсеров текстов на формальных языках. Программные системы и инструменты, 2, 2001.

5. А.Я. Калинов, A.JI. Ластовецкий, И.Н. Ледовских, М.А. Посыпкин. Пересмотренное сообщение о языке программирования С]. Программирование, б, 2002.

6. G. С. С. Гайсарян, А. Л. Ластовецкий . Расширение ANSI С для векторных и суперскалярных компьютеров. Программирование, 1, 1995.

7. А.С. Косачев, Ф. Куттер, М.А. Посыпкин. Автоматическая генерация строго конформных тестов по формальной спецификации динамической семантики языка программирования. Программирование (в печати), 2004.

8. Automated syntax testing using JSynTest™. http: //software. qip. us/j syntest. htm.9. extensible Abstract State Machines, http: //www. xasm. org.10. mpC Workshop for Windows, http://mpcw.ispras.ru.

9. Б. Керниган, Д. Ритчи. Язык программирования Си. Невский Диалект, 2001.

10. Кауфман В.Ш. Стандартизация и контроль трансляторов. Различные аспекты системного программирования, pages 47-85, 1984.

11. Серебряков В.А. Лекции по конструированию компиляторов. Москва, 1993.

12. Ластовецикий A.JI. Язык и система параллельного программирования для разработки программ, эффективно переносимых в классе распределенных вычислительных систем. Диссертация на соискание ученой степени д.ф.м.н. Москва, 1997.

13. Сухомлин В.А. Система программирования тройного стандарта ЗС++. 4~я международная конференция "Развитие и применение открытых систем". Тезисы докладов., pages 37-47, 1997.

14. Баскаков Ю.В. Принципы построения тестовых комплектов для тестирования конформности компиляторов стандартам языков программирования. Теоретические и прикладные проблемы информационных технологий: Сборник трудов, под ред. проф. Сухомлина В.А., 2001.

15. A. Gargantini and Е. Riccobene. ASM-based testing: coverage criteria and automatic tests generation. In Formal Methods and Tools for Computer Science (Proceedings of Eurocast 2001), pages 262-265, February 2001.

16. A. Kalinov, A. Kossatchev, A. Petrenko, М. Posypkin, V. Shishkov. Coverage-driven automated compiler test suite generation. In Proceedings of LDTA'2003, volume 82 of ENTCS. Elsevier, 2003.

17. A. Kalinov, A. Kossatchev, A. Petrenko, M. Posypkin, V. Shishkov. Using ASM Specifications for Compiler Testing. In Abstract State Machines Advances in Theory and Applications 10th International Workshop, ASM 2003, volume 2589 of LNCS, 2003.

18. A.G. Duncan and J.S. Hutchison. Using attributed grammars to test design and implementations. In Proceedings of the 5th international conference on Software engineering , pages 170 178, 1981.

19. A.S. Boujarwah, K. Saleh, J. Al-Dallal. Testing syntax and semantics coverage of Java language compilers. Information and Software Technology, 41:15-28, 1999.

20. B. DiFranco. Specification of ISO SQL using Montages. Master's thesis, Universita di l'Aquila, 1997.

21. E. Borger and W. Schulte. Programmer friendly modular definition of the semantics of Java. In Formal Syntax and Semantics of Java, number 1523 in LNCS. Springer, 1998.

22. Brian A. Malloy and James F. Power. An interpretation of Purdom's algorithm for automatic generation of test cases. In Proceedings of1.IS'Ol, 2001.

23. C.J. Burgess, M. Saidi. The automatic generation of test cases for optimizing Fortran compilers. Information and Software Technology, 38:111-119, 1996.

24. E. Borger. Abstract state machines at the cusp of the millenium. In Y. Gurevich and P. Kutter and M. Odersky and L. Thiele, editor, Abstract State Machines: Theory and Applications, volume 1912 of LNCS, pages 1-8. Springer-Verlag, 2000.

25. E. Sirer and B. Bershad. Using production grammars in software testing. In Proceeding of Second Conference on Domain-Specific Languages, October 1999.

26. Ronald F. Guilmette. Personal communications.

27. Ronald F. Guilmette. TGGS: A flexible system for generating efficient test case generators, 1999.

28. Y. Gurevich. Evolving algebras, a tutorial introduction. Bulletin of EATCS, 43:264-284, 1991.

29. Y. Gurevich. Evolving algebras 1993: Lipari guide. In E. Borger, editor, Specification and Validation Methods, pages 9-36. Oxford University Press, 1995.

30. Y. Gurevich and J. Huggins. The semantics of the С programming language. In E. Borger, H. Kleine Btining, G. Jager, S. Martini, and M. M. Richter, editors, Computer Science Logic, volume 702 of LNCS, pages 274-309. Springer, 1993.

31. J. Harm. Automatic test program generation from formal language specifications. Rostocker Informatik-Berishte(1997), 20:33-56, 1997.

32. J. Harm and R. Lammel. Testing attribute grammars. In Proceedings of Third Workshop on Attribute Grammars and their Applications, pages 79-98, 2000.

33. J. Harm and R. Lammel. Two-dimensional approximation coverage. Informatica, 24(3), 2000.

34. Robert Harper. Programming languages: Theory and practice, http: //www-2. cs. emu. edu/~rwh/plbook/.

35. J. Huggins and W. Shen. The static and dynamic semantics of C. Technical Report CPSC-2000-4, Kettering University, Computer Science Program, 2000.

36. O & IEC. Programming Language C. WG14/N843 Committee Draft, 1998.

37. A. Kossatchev. Personal communications.

38. P. Kutter. The formal definition of Anlauff's extensible Abstract State Machines. TIK-Report 136, Swiss Federal Institute of Technology (ETH) Zurich, June 2002.

39. P. Kutter and A. Pierantonio. The formal specification of Oberon. Journal of Universal Computer Science, 3(5):443-503, 1997.

40. P. Kutter and A. Pierantonio. Montages: Specifications of realistic programming languages. Journal of Universal Computer Science, 3(5):416-442, 1997.

41. Ralf Lammel. Grammar testing. In Proc. of Fundamental Approaches to Software Engineering (FASE) 2001, volume 2029 of LNCS, pages 201-216. Springer-Verlag, 2001.

42. Alexey Lastovetsky. mpC a multi-paradigm programming language for massively parallel computers. ACM SIGPLAN Notices, 31 (5): 13 -20, 1996.

43. Maurer P.M. Generating test data with enhanced context-free grammars. IEEE Software, pages 50-55, 1990.

44. Maurer P.M. The design and implementation of a grammar-based data generator. Software Practice and Experience, 22(3):223—244, 1992.

45. George C. Necula, Scott McPeak, and Westley Weimer. CCured: type-safe retrofitting of legacy code. In Symposium on Principles of Programming Languages, pages 128-139, 2002.

46. M. Norrish. С formalised in HOL. Technical Report UCAM-CL-TR-453, University of Cambridge, Computer Laboratory.

47. Jukka Paaki. Attribute grammar paradigms. ACM Computing Surveys, 27(2):196-255, June 1995.

48. Nikolaos S. Papaspyrou. A Formal Semantics for the С Programming Language. PhD thesis, National Technical University of Athens, 1998.

49. Gordon Plotkin. A structural approach to operational semantics. Lecture Notes DAIMI FN-19, Dept. of Computer Science, Univ. of Aarhus, 1981.

50. Purdom P. A sentence generator for testing parsers. BIT, 2:336-375, April 1972.

51. P.W. Kutter. Montages Engineering of Computer Languages. PhD thesis, ETH Zurich, 2003.

52. John C. Reynolds. Theories of Programming Languages. Cambridge Universisty Press, 1998.

53. S. Zelenov, S. Zelenova, S. Kossatchev. Test generation for compilers and other text processors. Programming and Computer Software, (1), 2003.

54. H. ter Doest. Stochastic languages and stochastic grammars. In H. M. Groenbaum, H. W. Kleijn-Hesselink, and M. M. Lankhast, editors, GRONICS-94; Proceedings of the 1994 Groningen Student Conference on Computer Science, pages 51-59, 1994.

55. Jan Tretmans. Testing techniques, 2002.

56. W. McKeeman. Differential testing for software. Digital Technical Journal, 10(1):100 107, 1998.

57. C. Wallace. The semantics of the С++ programming language. In E. Borger, editor, Specification and Validation Methods, pages 131164. Oxford University Press, 1995.

58. C. Wallace. The semantics of the Java programming language: Preliminary version. Technical Report CSE-TR-355-97, EECS Dept., University of Michigan, December 1997.