Алгоритмы антиунификации и их применение для вычисления инвариантов программ

Задача антиунификации (англ. anti-unification, generalization) была впервые рассмотрена в работах [18] и [20]. В общем виде она состоит в том, чтобы для двух заданных выражений Е и Е2 отыскать наиболее специальное выражение Е0, примерами которого являются оба выражения и Е2, то есть существуют подстановки и д2. для которых выполняются равенства Е = Е0д и Е2 = Ео$ 2- Такое выражение Е0 называется наименее общим шаблоном выражений Е и Е2.

Задача антиунификации двойственна гораздо более широко исследованной задаче унификации. Последняя состоит в том, чтобы для двух заданных выражении Е и Е2 отыскать наиболее общее выражение Е0, которое является примером обоих выражений Е и Е2, то есть удовлетворяет равенствам Е0 = Ещ и Е0 — Е2ц2 для некоторых подстановок щ и г/2. Такое выражение Eq называется наиболее общим примером выражений и Е2. Задача унификации была впервые исследована Дж. Робинсоном [21] в 1965 году в связи с созданием метода резолюций для автоматического доказательства теорем. В дальнейшем метод резолюций послужил отправной точкой для разработки концепции логического программирования, и алгоритмы унификации фактически стали основным средством вычисления логических программ. За прошедшие годы задача унификации была детально исследована. В частности, был разработан широкий спектр эффективных алгоритмов унификации [2, 12, 17, 27, 28], имеющих почти линейную сложность, а также были найдены подходящие структуры данных для практической реализации этих алгоритмов. Одной из таких структур для представления подстановок являются ациклические ориентирование графы, получаемые из деревьев «склеиванием» изоморфных поддеревьев. Важным частным случаем задачи унификации является задача метчипга (от англ. matching — приведение в соответствие). Она состоит в том, чтобы для двух заданных выражений Е0 и Ei отыскать подстановку ?/, удовлетворяющую равенству Ех = Е0г).

Задача антиунификации (построения наименее общих шаблонов) рассматривалась в ряде работ [5, 10, 11, 14, 15, 18, 20, 22, 24, 25, 36]. В этих работах были предложены различные алгоритмы антиунификации, и в некоторых случаях была исследована сложность этой задачи. Так, например, в статье [10] было установлено, что задача антиунификации для термов, представленных в виде деревьев, являтся JVC-полной (в отличие от задачи унификации, которая относится к числу Р-полных задач). В статье [5] были предложены параллельные алгоритмы антиунификации для термов, представленных в виде деревьев. Было показано, что антиунификацию термов, представленных деревьями размера N, можно провести за время О (log2 А'") с использованием TV/log2 N процессоров в модели параллельных вычислений EREW PRAM, не допускающей одновременное считывание и запись данных несколькими процессорами в одну и ту же ячейку памяти. В этой же работе было показано, что в том случае, когда нескольким процессорам разрешается одновременно проводить операции считывания и записи, относящиеся к одной и той же ячейке общей памяти (модель параллельных вычислений CRCW PRAM), антиунификацию древесных термов можно провести за время О (log N) с использованием N/ log Аг процессоров. Однако сложность задачи антиунификации для термов, для представления которых используются структуры данных, отличные от деревьев, ранее не исследовалась.

Цель главы 1 этой работы — выяснить, какова сложность задачи антиунификации в том случае, когда рассматриваемые термы представлены ациклическими ориентированными графами. Задача антиунификации термов эквивалентна задаче антиунификации подстановок. Под подстановкой в данном случае понимается отображение из одного множества переменных в множество термов, построенное над конечным множеством функциональных символов и другим множеством переменных. В параграфе 1.2.2 представлен последовательный алгоритм антиунификации подстановок, сложность которого линейно зависит от размера вычисляемого им наименее общего шаблона. Таким образом, устанавливается, что при измерении сложности алгоритмов относительно размеров исходных данных и вычисляемого результата задача антиунификации имеет почти такую же сложность, что и задача унификации, независимо от формы представления термов. В параграфе 1.2.3 дается нижняя оценка сложности задачи антиунификации для подстановок, представленных ациклическими ориентированными графами. Для этого представлен пример последовательности пар подстановок, размер наименее общих шаблонов которых квадратично зависит от размеров исходных подстановок. Полученный результат подчеркивает существенное комбинаторное отличие задачи антиунификации от задачи унификации. Известно, что размер наиболее общего примера двух выражений может экспоненциально зависеть от размеров самих выражений, если эти выражения представлены в виде деревьев. Однако в том случае, если для представления выражений использовать ациклические ориентированные графы, то размер наиболее общего примера будет ограничен величиной, линейно зависящей от размеров исходных выражений. Для задачи антиунификации все происходит наоборот: если выражения представлены в виде деревьев, то размер наименее общего шаблона двух выражений не превосходит размеров самих исходных выражений, а если для представления выражений использовать ациклические ориентированные графы (более «компактную» структуру данных), то размер наименее общего шаблона может квадратично зависеть от размеров исходных выражений. Таким образом, сложность алгоритмов антиунификации существенно зависит от способа представления исходных данных.

В разделе 1.3 рассмотрены параллельные алгоритмы антиунификации подстановок, представленных ациклическими ориентированными графами. Первый из них — предложенный в параграфе 1.3.1 алгоритм распознавания точного антиунификатора — проверяет, является ли заданная подстановка г] точной нижней гранью двух других заданных подстановок и Затем на основании этого алгоритма показывается, что задача распознавания точного антиунификатора для подстановок, представленных в виде ациклических ориентированных графов, принадлежит классу сложности N0. Однако применять этот алгоритм для вычисления точной нижней грани подстановок невозможно. В параграфе 1.3.2 рассмотрен второй из алгоритмов — параллельный алгоритм построения ациклического ориентированного графа, представляющего точную нижнюю грань двух подстановок, — и оценена его сложность.

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

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

3у13у2 ¦ • • 3ук (ъх = ?1 Л г>2 = ?2 А • ¦ • Л Ут = ¿-т), где ?1, /2,., ~ некоторые термы. Основное внимание уделено построению для произвольной точки программы наиболее специального сильного инварианта в классе инвариантов равенства, то есть такой формулы, из которой в свободных эрбрановских) интерпретациях логически следуют все инварианты равенства в этой точке.

Методы вычисления инвариантов равенства существенно зависят от модели исследуемой программы. В разделе 1.4 разработан метод вычисления инвариантов равенства одномодульных программ, то есть программ, множество операторов которых не содержит вызовов процедур. В этом случае вычисление инварианта равенства естественным образом сводится к исследованной в разделах 1.2 и 1.3 задаче антиунификации подстановок, то есть к задаче вычисления точной нижней грани в решетке подстановок. Важным свойством подстановок, позволяющим использовать антиунификацию для вычисления инвариантов равенства, является выполнимость закона левой дистрибутивности композиции подстановок относительно операции антиунификации. Это свойство позволяет применять быстрые итеративные алгоритмы вычисления неподвижных точек, широко используемые при решении задач статического анализа и верификации моделей программ (см., например, [13]).

Помимо задачи вычисления инвариантов, проблема антиунификации подстановок возникает и при решении некоторых других задач анализа программ. Так, например, полиномиальный алгоритм проверки логико-термальной эквивалентности программ, предложенный В. К. Сабельфельдом [35], фактически проводит вычисление и сравнение наименее общих шаблонов термов, которые сопоставляются в качестве значений переменным анализируемых программ. В работе [3] антиунификация термов использовалась для поиска «клонов» в тексте программы, то есть фрагментов, которые могут быть получены друг из друга заменой некоторых подфрагментов. В помощью антиунификации все операторы исследуемой программы делятся па кластеры, в результате чего программу можно рассматривать как последовательность идентификаторов таких кластеров. После этого снова при помощи антиунификации в этой последовательности выделяются «похожие» подпоследовательности. В работе [14] антиунификация использовалась для выявления широкораспространенных шаблонов формул, используемых в научных статьях. В работе [22] предложен метод суперкомпиляции функциональных программ, в котором также используется антиунификация подстановок.

Как уже говорилось выше, благодаря выполнимости закона левой дистрибутивности композиции подстановок относительно операции взятия точной нижней грани, задача вычисления наиболее специальных инвариантов равенства в произвольной точке одномодульной программы может быть решена при помощи итеративной процедуры вычисления точных нижних граней в решетке подстановок (вычисления антиунификаторов подстановок). К сожалению, подобный подход к вычислению наиболее специальных инвариантов равенства сталкивается со значительными трудностями в том случае, когда программа состоит из нескольких модулей (процедур) и содержит операторы вызова этих модулей. Это связано с тем, что в решетке подстановок не выполняется закон правой дистрибутивности композиции подстановок относительно операции взятия точной нижней грани. Поэтому формула, полученная в результате последовательной подстановки друг в друга наиболее специальных инвариантов равенства, вычисленных отдельно для каждого из модулей, будет инвариантом равенства, но этот инвариант, вообще говоря, не будет являться наиболее специальным. В главе 2 предложено обобщающее концепцию подстановки понятие регулярной метпаподстановки, для которого выполняется закон правой дистрибутивности композиции относительно операции взятия точной нижней грани (операции антиунификации метаподстановок). Выполнимость этого закона, наряду с другими свойствами, позволяет использовать алгоритмы антиунификации метаподстановок для вычисления наиболее специальных линейных инвариантов равенства многомодульных программ. Термин «мета-подстановка» был выбран для обозначения введенного нами понятия потому, что оно естественным образом обобщает понятие подстановки. Его не следует путать с понятием «тел, азчЬзпЬи (лоп», используемым в теории переписывания для обозначения подстановок высшего порядка (см. например, [6]).

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

Множество контекстов К называется линейным по некоторому заданному мно-оюеетеу переменных, если любая переменная из этого множества встречается на листьях контекстов из К не более одного раза. Как уже говорилось выше, подстановка — это отображение из одного множества переменных VI в множество термов, построенных над множеством функциональных символов и другим множеством переменных V'2. Для вычисления инвариантов равенства многомодульных программ необходимо разделить множество переменных ТЛ на два непересекающихся подмножесгва — конечное множество 2 переменных входа (формальных аргументов модуля) и бесконечное множество 3' вспомогательных переменных, соответствующих связанным переменным в инвариантах равенства. Мы будем рассматривать множества контекстов, линейные по множеству вспомогательных переменных У. С одной стороны, такое ограничение существенно сужает круг поиска инвариантов равенства. Полученный нашим методом инвариант равенства будет наиболее специальным не во всем множестве инвариантов равенства, а только в его подмножестве линейных инвариантов равенства. Однако в главе 3 показано, что отличие между ними будет только в переменных термов, встречающихся в инварианте, а не в структуре из функциональных символов этих термов. Это означает, что наиболее специальный инвариант равенства можно получить из наиболее специального линейного инварианта равенства отождествлением некоторых связанных переменных. С другой стороны, свойство линейности множества контекстов необходимо для выполнимости закона правой дистрибутивности композиции метаподстановок относительно операции взятия точной нижней грани.

Рассмотрим теперь свойство согласованности множества контекстов. При описании свойства линейности говорилось, что множество переменных Уо, над которыми строятся термы, встречающиеся в необходимых для вычисления инвариантов равенства мстаподстановках, разделяется на непересекающиеся множества переменных входа Е и вспомогательных переменных Множество функциональных символов Н, встречающихся в этих термах, также распадается на два непересекающихся подмножества — множество Т функциональных символов операций (арифметических и пр.), встречающихся в программе, и множество V процедурных символов, каждый из которых соответствует одному из модулей программы. При вычислении инвариантов равенства сначала строятся метаподстановки для каждого модуля в отдельности, а затем в метаподстановке, построенной для исследуемой точки программы, все процедурные символы итеративно заменяются на соответствующие метаподстановки. Несогласованность двух контекстов возникает в том случае, когда при наложении друг на друга соответствующих им ветвей из набора деревьев, представляющих подстановки, обнаруживается, что две соответствующие вершины этих ветвей либо помечены различными функциональными (непроцедурными) символами, либо вспомогательная переменная накладывается на любой отличный от нее символ. Множество контекстов называется согласованным, если все его элементы попарно согласованы. Выполнимость свойства согласованности позволяет использовать разработанную в разделе 3.1 главы 3 технику аппроксимирующих последовательностей для определения того момента, когда необходимая для вычисления наиболее специального линейного инварианта равенства многомодульной рекурсивной программы метаподстановка уже получена. Согласованное множество контекстов называется метаконтекстом. В параграфах 2.1.1 и 2.1.2 даны строгие определения контекста и метаконтекста, а также исследованы их основные свойства. В частности, показано, что для линейных ме-таконтекстов на основе композиции множеств контекстов определяется нижняя полурешетка. Операция вычисления точной нижней грани в этой решетке, называемая антиунификацией метаконтекстов, является основополагающей для вычисления инвариантов равенств.

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

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

Глава 3 посвящена разработке метода вычисления наиболее специальных линейных инвариантов равенства для программ с вызовами процедур. В параграфе 3.1.1 строго введена модель итеративной недетерминированной многомодульной программы. В такой программе содержатся операторы двух видов — операторы присваивания и операторы вызова процедуры. В параграфе 3.1.2 дано определение инварианта равенства многомодульной программы и рассмотрен метод сведения задачи построения наиболее специального инварианта равенства к задаче вычисления метаподстановки определенного вида. Параграф 3.1.3 посвящен исследованию свойств такой метаподстановки. В частности, показано, что ее можно получить итеративно методом аппроксимирующих последовательностей из ме-таподстановок, сопоставленных каждому модулю. В параграфе 3.2.1 говорится о том, что автоматные представления последних легко строятся непосредственно по модели программы с помощью метода поиска неподвижной точки. В параграфе 3.2.2 приведен алгоритм вычисления наиболее специальных линейных инвариантов равенства для программ с вызовами процедур.

Основные результаты этой работы таковы.

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

2. Установлена верхняя оценка сложности в классе параллельных алгоритмов для задачи антиунификации подстановок, представленных в виде ациклических ориентированных графов.

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

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

Заключение

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

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

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

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

Таким образом, в диссертационной работе

1. разработаны новые последовательные и параллельные алгоритмы антиунификации подстановок;

2. получены новые, более точные оценки сложности задачи антиунифиикации подстановок;

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

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