Абстрактная интерпретация - Abstract interpretation

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

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

Абстрактная интерпретация была формализована рабочей парой французских компьютерных ученых. Патрик Кузо и Радия Кузо в конце 1970-х гг.[1][2]

Интуиция

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

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

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

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

В случае вычислений конкретная точная информация, как правило, не может быть вычислена за конечное время и память (см. Теорема Райса и проблема остановки ). Абстракция используется для получения обобщенных ответов на вопросы (например, ответ «может быть» на вопрос «да / нет», что означает «да или нет», когда мы (алгоритм абстрактной интерпретации) не можем вычислить точный ответ с уверенностью); это упрощает проблемы, делая их доступными для автоматических решений. Одно из важнейших требований - добавить достаточно неопределенности, чтобы проблемы можно было решить, сохраняя при этом достаточную точность для ответов на важные вопросы (например, «может произойти сбой программы?»).

Абстрактная интерпретация компьютерных программ

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

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

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

На практике определяемые абстракции приспособлены как к свойствам программы, которые необходимо анализировать, так и к набору целевых программ. Первый крупномасштабный автоматизированный анализ компьютерных программ с абстрактной интерпретацией можно отнести к аварии, в результате которой был разрушен компьютер. первый полет Ariane 5 ракета в 1996 году.[3]

Формализация

Пример: абстракция целочисленных наборов (красный) до наборов знаков (зеленый)

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

Функция α называется функция абстракции если он отображает элемент Икс в бетонном наборе L элементу α (Икс) в абстрактном множестве L′. То есть элемент α (Икс) в L' это абстракция из Икс в L.

Функция γ называется функция конкретизации если он отображает элемент Икс′ В абстрактном множестве L′ На элемент γ (Икс′) В конкретном множестве L. То есть элемент γ (Икс') в L это конкретизация из Икс' в L′.

Позволять L1, L2, L′1 и L′2 быть заказанными наборами. Конкретная семантика ж является монотонной функцией из L1 к L2. Функция ж' от L′1 к L′2 считается действительная абстракция из ж если для всех Икс' в L′1, (ж ∘ γ) (Икс′) ≤ (γ ∘ ж′)(Икс′).

Семантика программы обычно описывается с помощью фиксированные точки при наличии циклов или рекурсивных процедур. Предположим, что L является полной решеткой и пусть ж быть монотонной функцией из L в L. Тогда любой ИксТакие, что ж(Икс′) ≤ Икс′ - абстракция наименьшей неподвижной точки ж, который существует, согласно Теорема Кнастера – Тарского.

Теперь трудность состоит в том, чтобы получить такой Икс′. Если L'Имеет конечную высоту или, по крайней мере, подтверждает условие возрастающей цепи (все восходящие последовательности в конечном итоге стационарны), то такая Икс′ Может быть получена как стационарный предел восходящей последовательности Икс′п определяется по индукции следующим образом: Икс′0= ⊥ (наименьший элемент L') и Икс′п+1=ж′(Икс′п).

В других случаях все же возможно получить такой Икс'Через оператор расширения [4] ∇: для всех Икс и у, Икс ∇ у должно быть больше или равно обоих Икс и у, и для любой последовательности у′п, последовательность, определяемая Икс′0= ⊥ и Икс′п+1=Икс′п ∇ у′п в конечном итоге стационарен. Затем мы можем взять у′п=ж′(Икс′п).

В некоторых случаях можно определить абстракции, используя Связи Галуа (α, γ) где α из L к L′ И γ из L'К L. Это предполагает наличие лучших абстракций, что не обязательно так. Например, если мы абстрагируем наборы пар (Икс, у) из действительные числа заключив выпуклый многогранники, не существует оптимальной абстракции к диску, определяемой Икс2+у2 ≤ 1.

Примеры абстрактных доменов

Каждой переменной можно присвоить Икс доступный в данной программной точке интервал [LИкс, ЧАСИкс]. Состояние, присваивающее значение v(Икс) к переменной Икс будет конкретизацией этих интервалов, если для всех Икс, v(Икс) в [LИкс, ЧАСИкс]. Из интервалов [LИкс, ЧАСИкс] и [Lу, ЧАСу] для переменных Икс и у, легко получить интервалы для Икс+у ([LИкс+Lу, ЧАСИкс+ЧАСу]) и для Икс−у ([LИкс−ЧАСу, ЧАСИкс−Lу]); обратите внимание, что это точный абстракции, поскольку множество возможных результатов, скажем, Икс+у, в точности интервал ([LИкс+Lу, ЧАСИкс+ЧАСу]). Более сложные формулы могут быть получены для умножения, деления и т. Д., Давая так называемые интервальная арифметика.[5]

Давайте теперь рассмотрим следующую очень простую программу:

у = х; г = х - у;
Комбинация интервальная арифметика (зеленый) и сравнение по модулю 2 на целых числах (голубой) как абстрактные области для анализа простой части C код (красный: конкретные наборы возможных значений во время выполнения). Используя информацию о сравнении (0= даже, 1= нечетное), a нулевое деление можно исключить. (Поскольку задействована только одна переменная, реляционные и нереляционные домены здесь не проблема.)
Трехмерный выпуклый пример многогранника, описывающий возможные значения трех переменных в некоторой точке программы. Каждая из переменных может быть равна нулю, но все три не могут быть равны нулю одновременно. Последнее свойство не может быть описано в области интервальной арифметики.

При разумных арифметических типах результат для z должно быть равно нулю. Но если мы будем выполнять интервальную арифметику, начиная с Икс в [0, 1] получается z в [−1, +1]. В то время как каждая из операций, взятых по отдельности, была точно абстрактной, их состав - нет.

Проблема очевидна: мы не отслеживали отношения равенства между Икс и у; на самом деле эта область интервалов не принимает во внимание какие-либо отношения между переменными и, таким образом, является нереляционный домен. Нереляционные домены обычно бывают быстрыми и простыми в реализации, но неточными.

Некоторые примеры реляционный числовые абстрактные области:

и их комбинации (например, уменьшенный продукт,[2] ср. правая картинка).

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

Смотрите также

использованная литература

  1. ^ Кузо, Патрик; Cousot, Radhia (1977). «Абстрактная интерпретация: модель единой решетки для статического анализа программ путем построения или аппроксимации фиксированных точек» (PDF). Отчет о конференции четвертого симпозиума ACM по принципам языков программирования, Лос-Анджелес, Калифорния, США, январь 1977 г.. ACM Press. С. 238–252. Дои:10.1145/512950.512973.
  2. ^ а б Кузо, Патрик; Cousot, Radhia (1979). «Систематическое проектирование структур программного анализа» (PDF). Запись конференции шестого ежегодного симпозиума ACM по принципам языков программирования, Сан-Антонио, Техас, США, январь 1979 г.. ACM Press. С. 269–282. Дои:10.1145/567752.567778.
  3. ^ Фор, Кристель. «История PolySpace Technologies». Получено 3 октября 2010.
  4. ^ Cousot, P .; Cousot, R. (август 1992 г.). «Сравнение подходов Галуа и расширения / сужения к абстрактной интерпретации» (PDF). В Брюнооге, Морис; Вирсинг, Мартин (ред.). Proc. 4-й Int. Symp. по реализации языков программирования и логическому программированию (PLILP). Конспект лекций по информатике. 631. Springer. С. 269–296. ISBN  978-0-387-55844-8.
  5. ^ Кузо, Патрик; Cousot, Radhia (1976). «Статическое определение динамических свойств программ» (PDF). Материалы Второго Международного симпозиума по программированию.. Данод, Париж, Франция. С. 106–130.
  6. ^ Грейнджер, Филипп (1989). «Статический анализ арифметических сравнений». Международный журнал компьютерной математики. 30 (3–4): 165–190. Дои:10.1080/00207168908803778.
  7. ^ Филипп Грейнджер (1991). "Статический анализ равенств линейной конгруэнтности переменных программы". По Абрамскому, С .; Майбаум, Т.С.Э. (ред.). Proc. Int. J. Conf. по теории и практике разработки программного обеспечения (TAPSOFT). Конспект лекций по информатике. 493. Springer. С. 169–192.
  8. ^ Кузо, Патрик; Хальбвакс, Николас (январь 1978 г.). «Автоматическое обнаружение линейных ограничений среди переменных программы» (PDF). Конф. Рек. 5-й симпозиум ACM. по принципам языков программирования (POPL). С. 84–97.
  9. ^ Мине, Антуан (2001). «Новая числовая абстрактная область, основанная на разностных матрицах». В Данви, Оливье; Филински, Анджей (ред.). Программы как объекты данных, Второй симпозиум (PADO). Конспект лекций по информатике. 2053. Springer. С. 155–172. arXiv:cs / 0703073.
  10. ^ Мине, Антуан (декабрь 2004 г.). Слабо реляционные числовые абстрактные области (PDF) (Кандидатская диссертация). Laboratoire d'Informatique de l'École Normale Supérieure.
  11. ^ Антуан Мине (2006). "Абстрактная область восьмиугольника". Символ высшего порядка. Вычислить. 19 (1): 31–100. arXiv:cs / 0703084. Дои:10.1007 / s10990-006-8609-1.
  12. ^ Кларисо, Роберт; Кортаделла, Хорди (2007). «Абстрактная область октаэдра». Наука компьютерного программирования. 64: 115–139. Дои:10.1016 / j.scico.2006.03.009. HDL:10609/109823.
  13. ^ Майкл Карр (1976). «Аффинные отношения между переменными программы». Acta Informatica. 6 (2): 133–151. Дои:10.1007 / BF00268497.

внешние ссылки

Конспект лекций