Из Википедии, свободной энциклопедии
Перейти к навигации Перейти к поиску

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

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

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

Интуиция [ править ]

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

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

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

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

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

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

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

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

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

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

Формализация [ править ]

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

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

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

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

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

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

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

В других случаях, это все еще можно получить такой х 'через расширяющуюся оператора [4] ∇: для всех х и у , х ∇ у должно быть больше или равно , чем как х и у , и для любой последовательности у ' п , последовательность, определяемая формулами x ′ 0 = ⊥ и x ′ n +1 = x ′ n ∇ y ′ n, в конечном итоге стационарна. Тогда мы можем взять y ′ n = f′ ( X ′ n ).

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

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

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

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

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

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

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

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

  • отношения сравнения на целых числах [6] [7]
  • выпуклые многогранники [8] (см. рисунок слева) - с некоторыми высокими вычислительными затратами
  • матрицы с разностной границей [9]
  • «восьмиугольники» [10] [11] [12]
  • линейные равенства [13]

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

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

См. Также [ править ]

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

Ссылки [ править ]

  1. ^ Кузо, Патрик; Cousot, Radhia (1977). "Абстрактная интерпретация: модель единой решетки для статического анализа программ путем построения или аппроксимации фиксированных точек" (PDF) . Конференция Запись четвертого симпозиума ACM по принципам языков программирования, Лос - Анджелес, Калифорния, США, январь 1977 года . ACM Press. С. 238–252. DOI : 10.1145 / 512950.512973 .
  2. ^ a b Кузо, Патрик; Cousot, Radhia (1979). «Систематическое проектирование рамок анализа программ» (PDF) . Конференция Запись ежегодного симпозиума Шестой ACM по принципам языков программирования, Сан - Антонио, штат Техас, США, январь 1979 . ACM Press. С. 269–282. DOI : 10.1145 / 567752.567778 .
  3. ^ Фор, Christèle. «История технологий PolySpace» . Проверено 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. DOI : 10.1080 / 00207168908803778 .
  7. ^ Филипп Грейнджер (1991). "Статический анализ равенств линейной конгруэнтности между переменными программы". По Абрамскому, С .; Майбаум, TSE (ред.). Proc. Int. J. Conf. по теории и практике разработки программного обеспечения (TAPSOFT) . Конспект лекций по информатике. 493 . Springer. С. 169–192.
  8. ^ Кузо, Патрик; Halbwachs, Николас (январь 1978 г.). «Автоматическое обнаружение линейных ограничений среди переменных программы» (PDF) . Конф. Рек. 5-й симпозиум ACM. по принципам языков программирования (POPL) . С. 84–97.
  9. ^ Mine, Антуан (2001). «Новая числовая абстрактная область, основанная на разностных матрицах». В Данви, Оливье; Филински, Анджей (ред.). Программы как объекты данных, Второй симпозиум (PADO) . Конспект лекций по информатике. 2053 . Springer. С. 155–172. arXiv : cs / 0703073 .
  10. ^ Mine, Антуан (декабрь 2004). Слабо реляционные числовые абстрактные области (PDF) (кандидатская диссертация). Laboratoire d'Informatique de l'École Normale Supérieure.
  11. ^ Antoine Mine (2006). "Абстрактная область восьмиугольника". Символ высшего порядка. Comput . 19 (1): 31–100. arXiv : cs / 0703084 . DOI : 10.1007 / s10990-006-8609-1 .
  12. ^ Кларисо, Роберт; Кортаделла, Хорди (2007). «Абстрактная область октаэдра». Наука компьютерного программирования . 64 : 115–139. DOI : 10.1016 / j.scico.2006.03.009 . hdl : 10609/109823 .
  13. ^ Майкл Карр (1976). «Аффинные отношения между переменными программы». Acta Informatica . 6 (2): 133–151. DOI : 10.1007 / BF00268497 .

Внешние ссылки [ править ]

  • Веб-страница по абстрактной интерпретации, поддерживаемая Патриком Кузо
  • Статья Роберто Багнары, показывающая, как можно реализовать статический анализатор на основе абстрактной интерпретации для C-подобного языка программирования.
  • Статический анализ симпозиумы , производство , появляющиеся в Springer LNCS серии
  • Конференция по вопросам проверки, проверки моделей и абстрактной интерпретации (VMCAI), аффилированная на POPL конференции , производство , появляющаяся в Springer LNCS серии
Конспект лекций
  • Абстрактная интерпретация . Патрик Кузо. Массачусетский технологический институт.
  • Конспект Дэвида Шмидта по абстрактной интерпретации
  • Конспект лекций Мёллера и Шварцбаха по статическому анализу программ
  • Конспект лекций Агостино Кортези по анализу и проверке программ
  • Слайды Грегуара Сютра, демонстрирующие каждый этап абстрактной интерпретации, с множеством примеров, а также знакомство с связями Галуа