Введение к работе
Актуальность темы. Семантическая информация о программе, т.е. информация о поведении программы на возможных входных данных, является чрезвычайно важной и широко используется в разного рода манипуляциях. Примерами таких манипуляций, применяемых для улучшения качества и адаптируемости программ, являются: оптимизирующая кодогенерация, специализация, верификация и отладка, повторное использование программ. Формализацией поведения программ является математическая модель, получившая название стандартной семантики программ и позволяющая получить полное математическое описание поведения программ.
Однако, как и для всякой достаточно общей математической модели, многие важные алгоритмические проблемы в этой области, позволяющие извлечь необходимую информацию о свойствах программ, либо являются неразрешимыми, либо решаются с помощью чрезвычайно неэффективных методов, что не даёт возможности использовать их на практике. Целью семантического анализа программ является построение другой математической модели — абстрактной семантики программ, которая корректно аппроксимирует стандартную семантику программ в следующем смысле (неформальное пояснение). Корректность: для всякой программы П, если свойство р программы П описывается абстрактной семантикой Л(П), то оно описывается и стандартной семантикой 5(П). Очевидно, что если бы предыдущее утверждение было справедливо и в обратную сторону, то абстрактная и стандартная семантики были бы эквивалентными моделями, описывающими поведение программ, а значит, и для абстрактной семантики мы бы столкнулись с теми же самыми алгоритмическими проблемами. Аппроксимационность: ключевой идеей семантического анализа программ является отказ от желания иметь полную информацию о поведении программ, некоторое "огрубление" её (получение абстрактной семантики) и за счёт этого получение возможности автоматически и эффективно извлекать какую-либо нетривиальную семантическую информацию о программах.
Под статическим выявлением семантических свойств, используемым в семантическом анализе, подразумевается то, что они выявляются не на основе запусков анализируемой программы на всевозможных входных данных. Программные свойства, описываемые абстрактной семантикой и аппроксимирующие конкретные семантические свой-
ства, вычисляются в процессе "абстрактного" исполнения программы, при котором данные представлены в виде некоторых абстрактных объектов, а конструкции языка программирования в виде их абстрактных аналогов, манипулирующих с этими абстрактными объектами. Естественно, при разработке нового вида семантического анализа должна быть обоснована корректность рассматриваемой аппроксимации. При этом всякий конкретный алгоритм, реализующий тот или иной вид семантического анализа, должен обладать разумным сочетанием таких свойств, как точность анализа/требование к ресурсам и возможностью их варьирования в зависимости от конкретных условий его применения (масштабируемость алгоритма анализа).
В действительности можно говорить о многих абстрактных семантиках, которые корректно аппроксимируют стандартную семантику. Многообразие возможных аппроксимаций определяется многообразием свойств, которые могут представлять интерес. В частности, для императивных языков, наиболее широко используемых в современной практике создания программного обеспечения (ПО), чрезвычайно важной является информация о значениях, которые могут быть вычислены в программе. На данный момент имеется представительное семейство алгоритмов анализа значений императивных программ, позволяющих получать аппроксимации тех или иных свойств. Однако ввиду того, что конкретный алгоритм анализа нацелен на эффективное выявление конкретного класса свойств, информация о свойствах из других классов теряется. Необходим анализ, который бы использовал унифицированный подход к накоплению и использованию семантической информации. В частности, для целей дальнейшего совершенствования остаточной программы, которая получается в результате работы специализатора, важной задачей является "полномасштабное просачивание" инвариантной информации.
Многими исследователями отмечается разрыв, наметившийся в последнее время между теорией и практикой семантического анализа. В реальной практике разработки ПО используется лишь небольшая часть разработанных алгоритмов анализа, для которых сегодня имеется эффективная: реализация. Причиной их практической эффективности является ^простота" выявляемых свойств. Поэтому в настоящий момент актуальной задачей, решение которой позволило бы вовлечь методы семантического анализа в повседневную практику разработки качественного ПО, является эффективная реализация алгоритмов семантического анализа, выявляющих "сложные" свойства программ.
Целью диссертационной работы является рассмотрение алгоритма семантического анализа, позволяющего аппроксимировать новый класс семантических свойств императивных программ; обоснование его корректности; практическая реализация данного алгоритма в виде прототипа анализатора; исследование таких характеристик, как точность анализа/требование к ресурсам, а также возможность применение результатов анализа в процессе разработки ПО.
Научная новизна работы состоит в следующем:
описан новый межпроцедурный потокочувствительный анализ значений для императивных программ, получивший название анализа отношений равенства программных термов; обоснована корректность данной аппроксимации;
предложен метод, обеспечивающий сходимость алгоритма анализа и позволяющий регулировать скорость сходимости; приведены оценки сложности цля всего алгоритма и для отдельных его частей;
рассмотренные преобразователи свойств представляют практически все конструкции императивных языков программирования, что даёт возможность применять данный алгоритм для анализа широкого класса программ.
Практическая ценность работы состоит в разработке нового анализа семантических свойств, являющегося чувствительным к потоку управления, имеющего регулируемую скорость сходимости и обладающего широкими возможностями для накопления инвариантной информации о значениях программных переменных и функциональных зависимостях между ними. Выявляемые свойства могут быть эффективно использованы для оптимизирующей кодогенерации, специализации, отладки и некоторых других манипуляциях над программами, применяемых для улучшения их качества и адаптируемости.
Апробация работы и публикации. Результаты работы докладывались и обсуждались на объединённом семинаре ИСИ СО РАН и БГУ "Конструирование и оптимизация программ" (март 1995 г.), семинаре "Semantique et interpretation abstraite" в Ecole Normale Supe-rieure (декабрь 1995, Париж, Франция), объединённом семинаре ИСИ СО РАН и НГУ "Теоретическое программирование" (март 1996 г.) и объединённом семинаре ИСИ СО РАН, НФ ИТМ и ВТ, НГУ "Системное программирование" (октябрь 1996 г.). Они также были представлены на XXXIII Международной Научной Студенческой Конференции (апрель 1995, Новосибирск), на Третьем (сентябрь 1996, Аахен,
Германия) и Четвёртом (сентябрь І997, Париж, Франция) Международных Симпозиумах по Статическому Анализу. По теме диссертации опубликовано 6 научных работ. Работа поддерживалась грантами РФФИ 93-01-00576, 95-07-19269, 97-01-00724, а также грантом Госкомитета по высшему образованию РФ "Формальные методы анализа и преобразования программ" и грантом ISSEP А97-1521.
Структура и объём работы. Диссертационная работа состоит из введения, четырех глав, заключения, списка литературы из 138 наименований и двух приложений. Объём основной части работы — 135 страниц, объём приложений— 12 страниц. Работа включает 11 таблиц и 12 рисунков.
