автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.11, диссертация на тему:Методы и средства статического анализа семантических свойств программ

^ На правах рукописи

%

ЕМЕЛЬЯНОВ Павел Геннадьевич

Методы и средства статического анализа семантических свойств программ

Специальность 05.15.11 - "р^пяммное

обеспечение вычислительных машин, комплексов, систем и сетей

Автореферат диссертации на соискание учёной степени кандидата физико-математических наук

Новосибирск 1997

Работа выполнена в Новосибирском государственном университете.

Научный руководитель: М.А.Булъонков,

кандидат физико-математических наук

Официальные оппоненты: Р.И. Подловченко,

доктор физико-математических наук В.И. Шелехов

кандидат технических наук

Ведущая организация: Санкт-Петербургский государственный

университет

Защита состоится 26 декабря 1997 г. в 14 час. 30 мин. на заседании специализированного совета К0003.93.01 в Институте систем информатики Сибирского отделения РАН по адресу:

630090, Новосибирск, пр. ак. Лаврентьева, 6.

С диссертацией можно ознакомиться в читальном зале библиотеки ВЦ СО РАН (пр. ак. Лаврентьева, 6).

Автореферат разослан 26 ноября 1997 г.

Учёный секретарь специализированного совета К0003.93.01

к.ф.-м.н.

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

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

Однако, как и для всякой достаточно общей математической модели, многие важные алгоритмические проблемы в этой области, позволяющие извлечь необходимую информацию о свойствах программ, либо являются неразрешимыми, либо решаются с помощью чрезвычайно неэффективных методов, что не даёт возможности использовать их на практике. Целью семантического анализа программ является построение другой математической модели — абстрактной семантики программ, которая корректно аппроксимирует стандартную семантику программ в следующем смысле (неформальное пояснение). Корректность: для всякой программы П, если свойство р программы П описывается абстрактной семантикой Л(П), то оно описывается и стандартной семантикой 5(П). Очевидно, что если бы предыдущее утверждение было справедливо и в обратную сторону, то абстрактная и стандартная семантики были бы эквивалентными моделями, описывающими поведение программ, а значит, и для абстрактной семантики мы бы столкнулись с теми же самыми алгоритмическими проблемами. Аппроксимационность: ключевой идеей семантического анализа программ является отказ от желания иметь полную информацию о поведении программ, некоторое "огрубление" её (получение абстрактной семантики) и за счёт этого получение возможности автоматически и эффективно извлекать какую-либо нетривиальную семантическую информацию о программах.

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

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

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

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

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

Научная новизна работы состоит в следующем:

• описан новый межпроцедурный потокочувствительный анализ значений для императивных программ, получивший название анализа отношений равенства программных термов; обоснована корректность данной аппроксимации;

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

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

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

Апробация работы и публикации. Результаты работы докладывались и обсуждались на объединённом семинаре ИСИ СО РАН и НГУ "Конструирование и оптимизация программ" (март 1995 г.), семинаре "Sémantique et interptrétation abstraite" в École Normale Supérieure (декабрь 1995, Париж, Франция), объединённом семинаре ИСИ СО РАН и НГУ "Теоретическое программирование" (март 1996 г.) и объединённом семинаре ИСИ СО РАН, НФ ИТМ и ВТ, НГУ "Системное программирование" (октябрь 1996 г.). Они также были представлены на XXXIII Международной Научной Студенческой Конференции (апрель 1995, Новосибирск), на Третьем (сентябрь 1996, Аахен,

Германия) и Четвёртом (сентябрь 1997, Париж, Франция) Международных Симпозиумах по Статическому Анализу. По теме диссертации опубликовано 6 научных работ. Работа поддерживалась грантами РФФИ 93-01-00576, 95-07-19269, 97-01-00724, а также грантом Госкомитета по высшему образованию РФ "Формальные методы анализа и преобразования программ" и грантом ISSEP А97-1521.

Структура и объём работы. Диссертационная работа состоит из введения, четырех глав, заключения, списка литературы из 138 наименований и двух приложений. Объём основной части работы — 135 страниц, объём приложений— 12 страниц. Работа включает 11 таблиц и 12 рисунков.

Содержание работы

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

Теоретические основы семантического анализа, близкие к современным, были заложены в начале 70-х в работах G. Kildall и В. Wegbreit, хотя элементы этого могут быть найдены в работах А.П. Ершова, A.A. Летичевского, F. Allen и других, а их корни глубоко уходят в теорию схем программ, теорию областей и формальные методы описания семантики языков программирования. Окончательно вариант теории семантического анализа, получивший название потоковый анализ, сформировался в работах J. Каш и J. Ullman, S. Graham и М. Wegman и других. При этом подходе, в процессе анализа с использованием некоторого правила и разработанных семантических преобразователей по управляющему графу программы "просачивалась" семантическая информация, представленная абстрактными семантическими свойствами. Прй условии, что абстрактная семантическая область удовлетворяем условию обрыва цепей и заданные на ней се-

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

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

Некоторое решение этих проблем было предложено в подходе, получившем название абстрактной интерпретации, изложению основных принципов которого посвящена Первая глава данной диссертации. Укажем, что впервые это подход был представлен Р. и R. Cousot в работе для POPL'77. В их последующих работах он неоднократно расширялся и переизлагался в различных вариантах. Большой вклад в теорию абстрактной интерпретации также внесли F. Nielson, N. Jones, К. Marriott и другие, в основном европейские, исследователи. Абстрактная интерпретация полностью включает в себя теорию потокового анализа и значительно обобщает её.

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

программ. Эта теория опирается на две фундаментальные теоремы:

ТЕОРЕМА 1 (Тарский, Клини и др.) Если <р — отображение на полной решётке ±,Т,и, П), удовлетворяющее условиям Ух, у б£:гС у 1р{у) (монотонность) иЗигед-г ¡р(и1бхж) = 1-1хех<р(х) (непре-

рывность), то наименьшая неподвижная точка (р (т.е. наименьшая в смысле отношения порядка С точка х такая, что ¡¿з(х) = х) вычисляется как КрО?) = = ип>оуп(±), где </(х) = 1иу"- Ч*) = ¥>(¥>"(*))•

говорит о том, как можно вычислить неподвижную точку оператора, а ТЕОРЕМА 2 Пусть для полных решёток Ь(С) и Ь'(С') и монотонных отображений а : X ¿' и 7 : —ь Ь выполнено Ух £ Ь, V?/ € : а(х) С' у' <=> х С у(у'). Тогда если <р — монотонное отображение на Ь, то а(1Гр(у>)) С' Цр(а о ц> о 7).

говорит о об условиях гарантирующих корректность аппроксимации при переходе от одной семантической области, представляющей конкретные семантические свойства и в которой итеративная процедура вычисления неподвижной точки не является эффективной, к другой, представляющей абстрактные (аппроксимирующие) семантические свойства и для которой такая эффективная процедура имеется. Это соотношение между решётками называется связью Галуа и обозначается I!. В теории семантического анализа а получила название функции абстракции, а 7 — функции конкретизации.

Ввиду того, что процесс вычисления неподвижной точки является итерационным, следующим вопросом, возникающим при конструировании нового семантического анализа, является вопрос обеспечения приемлемой скорости сходимости этого процесса. Обсуждению этого вопроса посвящен раздел 1.3. В случае, когда абстрактная семантическая область удовлетворяет условию обрыва цепей и длины цепей ограничены небольшой величиной Н, то верхней оценкой количества шагов алгоритма семантического анализа является 0(пК), где п — размер программы. Однако, если величина, ограничивающая длины цепей, очень большая, а также если абстрактная семантическая область не удовлетворяет условию обрыва цепей, для обеспечения как сходимости вообще, так и сходимости за подходящее количество шагов процесса абстрактной интерпретации Р. и Я. Cousot был предложен метод экстраполяциопных операторов. Использование оператора расширения у Ь х Ь Ь, удовлетворяющего условиям а) V х,у £ С =>■ (х С х у у) Л (у С х V У) и б) для всех возрастающих цепей а:0 С г1 С ..., цепь вида = я0,..., г1+х = г1 у х'+1,... не является строго возрастающей, при итеративном вычислении неподвижной

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

Далее в этом разделе обсуждается проблема выбора оптимальных стратегий процесса абстрактной интерпретации и применения оператора расширения, с целью сохранения точности анализа. В общем случае отыскание оптимальной стратегии применения оператора расширения сводится к задаче отыскания минимального множества вершин обратной связи, которая является Л^Р-полной. Однако для рассматриваемых в работе структурированных программ эта задача имеет эффективное решение. Справедлива следующая теорема (Г. Воигс1оп-с1е):

ТЕОРЕМА 3 В алгоритме абстрактной интерпретации, использующем оператор расширения и стратегию "компонента стабилизируется в результате стабилизации её подкомпонент" (она называется рекурсивной стратегией процесса абстрактной интерпретации), требуется не более к шагов для нахождения решения. Здесь 1г — максимум длин цепей абстрактной области, возникающих во время алгоритма (определяется конструкцией оператора расширения), С — множество контрольных точек в программе, ¿(с) — глубина точки с в иерархии сильно связанных компонент.

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

Вторая глава диссертации посвящена обзору классификационных характеристик алгоритмов семантического анализа, а также рассмотрению конкретных алгоритмов анализа императивных программ, на примере которых демонстрируется практическая реализация общих принципов абстрактной интерпретации. К числу таких характеристик относятся: попроцедурность и межпроцедурностъ алгоритма анализа; способность анализировать сложные структуры данных или ограничение на скалярные переменные (анализ высшего или нулевого порядка соответственно); реляционностъ (учёт зависимостей между анализируемыми объектами) и нереляционность алгоритма; чувствительность и нечувствительность к контексту при анализе процедур; чувствительность к потоку управления, и масштабируемость. Отмечается, что чувствительность к потоку управления алгоритма анализа и его масштабируемость тесно связаны со степенью его интерпрета-ционности, которая показывает, насколько глубоко в процессе анализа

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

В первых четырёх разделах Второй главы дан краткий обзор следующих классов алгоритмов семантического анализа: неинтерпретационные (схемные) алгоритмы анализа, используемые в теории схем программ; теоретико-графовые алгоритмы; алгоритмы анализа, оперирующие с битовыми шкалами; алгоритмы анализа синонимов и наследования типов. Однако, поскольку особый интерес для нас представляют алгоритмы анализа значений императивных программ, они подробно рассматриваются в разделе 2.5. Этот интерес определяется в первую очередь тем, что разрабатываемый нами анализ отношений равенства программных термов также имеет дело с аппроксимацией множеств значений. Другой причиной является необходимость иметь вспомогательный анализ значений для целей повышения точности разрабатываемого нами. Здесь рассмотрены следующие алгоритмы анализа: втягивание констант; анализ интервалов и его обобщения; конгруэнтный анализ. В качестве вспомогательного анализа значений нами выбран нереляционный интервально-конгруэнтный анализ (Р. Мавёиршз), который является обобщением интервального и конгруэнтного алгоритмов анализа. В нём множество значений целочисленной переменной аппроксимируется посредством объединения конечного семейства множеств, представляющих собой распределенные на прямой с фиксированным шагом интервалы рациональных чисел. В разделе 2.5.4 приведено детальное описание данного алгоритма. В заключении Второй главы (раздел 2.6) даётся краткий обзор исследований, посвящённых, во-первых, использованию результатов анализа (системы трансформационного программирования, автоматизация отладки и тестирования программ); во-вторых, системам автоматического построения семантических анализаторов.

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

ства равенств (семантическая область не удовлетворяет условию обрыва цепей); интерпретационный анализ реального языка программирования. Следует отметить, что все алгоритмы анализа значений по существу являются алгоритмами анализа отношений равенства термов с различного рода ограничениями на их вид. Рассматриваемый в данной работе алгоритм анализа имеет дело с произвольными термами, из чего, впрочем, не следует, что он является обобщением остальных алгоритмов (за исключением анализа втягивания констант). В общем случае алгоритмы, анализирующие различные классы свойств, не сравнимы, так как специфические преобразователи, используемые в конкретном алгоритме анализа, позволяют более точно аппроксимировать конкретные свойства. Однако анализ отношений равенства предоставляет широкие возможности для учёта потока управления, которые недоступны другим алгоритмам. Наиболее близким к нему по рассам-триваемым свойствам является алгоритм Alpern-WegmaIl-Zadeck, который посредством некоторой модификации алгоритма минимизации конечных автоматов позволяет получить соотношения переменная = выражение.

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

Пусть СУ является множеством 0-местных символов, которые представляют описанные в программе переменные, имена функций и полей записей, всевозможные константы (в том числе и структурные). Множество Т'Р является множеством п-местньгх (функциональных) символов, которые представляют примитивные операции языка программирования. Множество 7~7&> является множеством регулярных термов над сигнатурой СУ и!РР, которые называются программными термами. Пусть £— это множество всех равенств термов из то есть £0,Б — = Ь> | , 6 Т71£}. Множество 5 € р(Ш5) называется вычислительным состоянием и описывает следующее свойство состояния вычислений в программе: для всех равенств ¿1 = ¿2 из в выражения, представляемые ^ и Ь^, вычислены и их значения равны.

Таким образом, стандартная семантика программы определяется переходной системой г, 0, £25), в которой отношение перехо-

дов т соответствует стандартной семантике, приписываемой исполнению отдельных операторов программы, 0 начальное и £ОБ конечное состояние вычислений. Набор рассмотренных нами операторов покрывает основные конструкции структурированных языков программирования. Статическая семантика программы описывается наименьшей неподвижной точкой оператора F, который определяется индукцией по элементарным операторам программы, на полной решётке р(р(£2«!>))(С, б,и). Напомним, что статическая семантика по-прежнему является полной по отношению к инвариантным свойствам процесса вычислений, т.е. к таким свойствам, информация о которых имеется во всех вычислительных состояниях, соответствующих рассматриваемой программной точке. Естественным образом возникает абстракция конкретных свойств, выявляющая такие соотношения равенства.

Выберем в качестве абстрактной семантической области полурешётку АББЕ и определим аппроксимацию следующим образом. Если 7г £ р{р(£0.8)) — конкретное свойство и 7г 6 ЕО,Б — абстрактное свойство, то функциями абстракции а : р(р(£<2$)) —> и кон-

кретизации 7 : р(£О.Б) —> р{р(£0,5)) являются

¡£0.8, если 7г = 0,

р)5 иначе и у(тг) = и{ тг | а(тг) 3' тг }.

Яётг

Для описания абстрактных вычислительных состояний используются широко известные понятия теории формальных языков (раздел 3.3). Вычислительное состояние описывается КС-языком Ь = £(С), порождённым некоторой грамматикой в = (М,Т,Р, Б) специального вида: Н — конечное множество нетерминалов, обозначаемых прописными буквами, 5 £ М — инициальный символ грамматики С, Т = СУ и ТТ и {(,),=, 5} — множество терминалов и Р — множество правил грамматики, имеющих вид: УЛ € N \ {5} : й —> А = А, А а и А /(А\,.. .,Ап), где а € СУ и / € ТТ. Таким образом,

¿(С) = <1 = *2 | А&г А } = { Ч }.

В разделе 3.4 определяется преобразование, получившее название редукции грамматики, и приводится реализующий его алгоритм. Это преобразование состоит в том, что из грамматики удаляются объекты, которые не используются в выводе ни одной терминальной цепочки. Временная сложность этого преобразования оценивается как 0()С|2), где |С| — мощность множества правил. Отметим, что сложность большинства операций над грамматиками имеет такой же порядок.

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

В качестве операции пересечения для полурешётки семантических свойств используется теоретико-множественное пересечение соответствующих языков L(G) = ¿(Gri) П L(G2), для которого в разделе 3.5 представлен алгоритм со средней сложностью 0(|Gi)log IG2I), позволяющий одновременно проверить включение L(G\) С ¿(Go).

Полурешётка языков равенств термов не удовлетворяет условию обрыва цепей. Фрагмент программы, при анализе которой может возникнуть эта ситуация, приведен в разделе 3.7.8. Для обеспечения сходимости процесса абстрактной интерпретации в разделе 3.6 предлагается подход, основанный на применении (двойственного) оператора расширения. Если в процессе интерпретации размер грамматики становится больше некоторого параметра d (в нашей реализации d = 5п, где п — количество переменных программы), то грамматика преобразуется в ациклическую, а значит порождаемый ею язык будет конечным. Подполу решётка конечных языков удовлетворяет условию обрыва цепей, что гарантирует сходимость алгоритма (меняя параметр, мы можем также регулировать и её скорость).

Такое преобразование может быть выполнено нахождением функциональных элементов, удаление которых разрывает все циклические выводы в грамматике последующим их удалением. При этом желательно, чтобы потери в точности анализа были наименьшими. Эта задача оказывается не менее сложной, чем упоминавшаяся ранее задача отыскания минимального множества вершин обратной связи. В работе приведён метод построения по грамматике некоторого орграфа, описывающего циклические выводы в грамматике, и определено преобразование £(G)\ rvs- Результат этого преобразования — ациклическая грамматика, порождающая конечный язык, который является подмножеством исходного. Оператор расширения определяется следующим образом:

f £(Gi)\fvs П' L{Ga) if |Ga| > |Gi| > d, L(Gi)v£(G3) = L(G 1) П' ¿(G2)\fvs if |Gi| > |G2| > d, 1 L(Gi) П' £(G2) иначе.

В разделе 3.7 описываются семантические преобразователи, используемые в анализе отношений равенства программных термов (3.7.1, 3.7.2, 3.7.4, 3.1, 3.7.6), обсуждается интерпрегационность алгоритма анализа отношений равенства (3.7.3), рассматриваются во-

просы использования оператора расширения и общей сложности алгоритма анализа (3.7.8).

Для описания абстрактной семантики языковых конструкций был. выбран операционный стиль, в котором отображение [ J : Construct х p{EQSf p(£QS)K определяется в терминах исходного языка. Следующие семантические преобразователи являются базовыми: вычисление терма, унификация значений термов и присваивание значения терму доступа. Поясним неформально смысл этих преобразований.

Результатом вычисления терма является новое состояние, которое содержит этот терм (в конкретной семантике соответствует обычному вычислению выражения). Унификация значений термов в абстрактной семантике отражает тот факт, что если бы конкретный вычислительный процесс протекал таким образом (это может быть и не так), значения соответствующих выражений обязательно были бы равными (это тем не менее корректное предположение). Это преобразование является ключевым для регулирования информативности анализа (см. ниже замечание о интерпретационности). Термами доступа называются программные термы, адресующие память программы, т.е. термы, представляющие переменные программы. В общем случае для учёта эффекта присваивания значения переменной необходим независимый анализ синонимов, результаты которого существенно влияют на точность нашего алгоритма анализа. Однако, при следующих предположениях: а) отсутствуют указатели и б) процедуры не имеют побочных эффектов, анализ отношений равенства является "самодостаточным". Именно для программ, удовлетворяющих этим ограничениям (плюс требование нерекурсивности процедур), предполагалось использовать разрабатываемый Анализатор Свойств. Имеется представительный класс задач вычислительной математики, для которых эти требования могут быть выполнены, хотя в общем случае они являются слишком жесткими.

ЛЕММА 1 Вычисление терма, унификация значений термов, эффект присваивания являются корректными преобразованиями, которые могут быть вычислены не более чем за 0(|£| log |G|), О(IG|2), 0(|G|2) шагов соответственно.

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

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

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

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

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

ЛЕММА 2 При некоторых предположениях оценкой временной сложности алгоритма анализа отношений равенства программных термов является 0(712С?таг)> где п — размер программы и Ста — максимальный размер грамматики, возникающей в процессе анализа. Емкостная сложность алгоритма оценивается 0(п0Гг,ах )■

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

В Четвертой главе описаны классы выявляемых семантических свойств (раздел 4.1) и результаты экспериментов по реализации алгоритма и его применению к анализу программ (разделы 4.2 и 4.3).

Из инвариантных соотношений равенства, которые являются результатом работы алгоритма, могут быть выявлены следующие программные свойства: а) использование неинициализированной переменной; б) переменная (тип, константа, процедура) описана, но нигде не используется; в) константность условия условного оператора или цикла; г) недостижимая программная точка; д) бесконечное исполнение циклов и процедур; е) ошибка времени исполнения; ж) диапазон значений выражения; з) избыточность оператора присваивания; и) для заданного выражения существует другое, более эффективно (в соответствии с заданным критерием скорость/размер) вычисляющее то же самое значение (в частности, этим значением может являться константа); к) свзи между параметрами в процедурах. Результаты анализа могут быть выведены в автоматическом режиме в виде листинга, а также визуализированы с помощью некоторой гипертекстовой среды, т.к. эксперименты показали, что не все свойства поведения программы могут быть извлечены из инвариантов автоматически. Представляется нецелесообразным включение непосредственно в анализатор рассмотрения большого числа частных случаев (см. пример в Приложении В). Вместо этого пользователю предоставляется возможность с помощью "дружественного" интерфейса конкретизировать свой запрос: выбрав интересующую eró программную точку и выражение, получить те, и только те, инвариантные свойства, которые затрагивают это выражение, и затем принять на основе этой информации какое-либо решение. Следует сказать, что инварианты, по существу, представляют собой системы уравнений и неравенств общего вида, решение которых дает ценные сведения о программных свойствах.

Большинство программ, которые были использованы для тестирования Анализатора Свойств, являются реализацией каких-либо вычислительных методов, активно использующих массивы. Было обнаружено, что помимо свойств, которые могут быть использованы для оптимизирующей кодогенерации, особенно автоматически порожденных, например специализатором, программ, Анализатор также способен выявлять свойства, говорящие о "недобротности" программ, что может служить сигналом о наличии семантических ошибок в них. Это, в частности, подтверждает пример, приведённый в Приложении В. Отметим также, что для программ, в которых индексные выражение ведут себя достаточно неоднородно, использование интервально-кон-груэнтного анализа в качестве вспомогательного повышало результативность анализа (увеличивался размер грамматики) на 10-20%.

Имеется три реализации Анализатора Свойств. Первая из них была выполнена в составе проекта СОКРАТ (система MS-DOS, компилятор TopSpeed Modula-2) и в основном была посвящена исследованию эффективного представления абстрактных свойств и эффективной (в основном по памяти) реализации алгоритмов, составляющих анализ отношений равенства. Вторая (система UNIX, компилятор GCC+4-, инструментальные средства LEX и YACC) ставила своей целью проведение экспериментов по объектно-ориетированному подходу к реализации алгоритма анализа отношений равенства. Версия Анализатора, разрабатываемая в данный момент (система WINDOWS NT/95, компилятор XDS М2/02), вобрала в себя наилучшие черты своих предшественниц, а также получила развитие по следующим направлениям: увеличение скорости анализа, реализация интервально-конгруэнтного анализа как вспомогательного, реализация оператора расширения, расширение возможностей по автоматическому выявления свойств, средства конфигурирования, интеграция с другими средствами разработки программ на базе общего интерфейса.

Приложение А посвящено обсуждению алгоритмов решения задачи отыскания множества вершин обратной связи оргафа. Показано, как эта задача сводится к задаче отыскания множества дуг обратной связи (и обратно) и приведена соответствующая библиография. Описан используемый в Анализаторе Свойств алгоритм Шпекенмей-ера, имеющий сложность 0(\V\ + \Е\ 4- YlveFnv)> гДе nv — количество вершин в строго связанных компонентах, которые вычисляются в процессе работы алгоритма и из которых выбираются вершины и, составляющие аппроксимирующее множество вершин обратной связи F.

В Приложении В представлены результаты применения алгоритма анализа соотношений равенства программных термов к программе, реализующей поиск образца в строке, специализированной специализа-тором M2Mix относительно некоторого фиксированного образца. Использование семантической информации, выявленной Анализатором Свойств, (принадлежность индексных выражений заданному диапазону, избыточность оператора присваивания, константность условий некоторых условных выражений), позволяет получить новую программу, функционально эквивалентную исходной, длина которой сократилась на 20.35%, а размер объектного кода на 26.40%.

В Заключении перечисляются основные результаты работы.

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

1. Разработан и исследован новый анализ инвариантных с жств императивных программ, получивший название анализа отношений равенства программных термов.

2. Исследован вопрос сходимости алгоритма анализа, и предложен оператор расширения, который позволяет обеспечить сходимость алгоритма анализа и предоставляет возможности регулировать её скорость.

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

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

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

1. Брюханова Ю.В., Емельянов П.Г., Касьянов В.Н., Сабельфельд В.К. Методы и средства семантического анализа Модула-программ // Конструирование и оптимизация программ. -Н.: ИСИ СО РАН, 1993. -С. 7-23.

2. Емельянов П.Г. и Сабельфельд В.К. Анализатор семантических свойств Модула-программ // Интеллектуализация и качество программного обеспечения. -Н.: ИСИ СО РАН, 1994. -С. 100-107.

3. Емельянов П.Г. Нижняя аппроксимация множества соотношений равенств программных термов // Тезисы XXXIII Международной научной студенческой конференции. -Н.: НГУ, 1995.

4. Emelianov P. Analysis of the equality relation for the program terms // Proc. of the 3rd International Static Analysis Symposium / Lect. Not. in Сотр. Sc. -Vol.1145. -Germany: Springer-Verlag, 1996. -P. 174-188.

5. Емельянов П.Г. Абстрактная интерпретация императивных программ // Проблемы архитектуры, анализа и разработки программных систем / Системная Информатика, -Т. 6, -Н.: Наука, 1997. -С. 7-47.

6. Emelianov P.G. and Baburia D.E. Semantic analyzer of Modula-programs // Proc. of the 4th International Static Analysis Symposium / Lect. Not. in Сотр. Sc. -Vol.1302. -Germany: Springer-Verlag, 1997. -P. 361-363.

Публикации по теме диссертации