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

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

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

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

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

Интуиция

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

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

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

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

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

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

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

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

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

На практике определяемые абстракции адаптируются как к свойствам программы, которые необходимо анализировать, так и к набору целевых программ. Первый крупномасштабный автоматизированный анализ компьютерных программ с абстрактной интерпретацией был вызван аварией, которая привела к разрушению первого полета ракеты «Ариан-5» в 1996 году.

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

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

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

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

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

Позволять $L_{1}$, $L_{2}$, $L'_{1}$, и $L'_{2}$можно заказать комплекты. Конкретная семантика $f$ является монотонной функцией от $L_{1}$ к $L_{2}$. Функция $f'$ от $L'_{1}$ к $L'_{2}$ считается допустимой абстракцией $f$ если для всех $x'$ в $L'_{1}$, у нас есть $(f\circ \gamma )(x')\leq (\gamma \circ f')(x')$.

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

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

В остальных случаях еще можно получить такое $x'$ через (парный) расширяющий оператор , определяется как бинарный оператор $\nabla \colon L\times L\to L$ который удовлетворяет следующим условиям:

1. Для всех $x$ и $y$, у нас есть $x\leq x\mathbin {\nabla } y$ и $y\leq x\mathbin {\nabla } y$, и
2. Для любой возрастающей последовательности $(y'_{n})_{n\geq 0}$, последовательность, определяемая $x'_{0}:=\bot$ и $x'_{n+1}:=x'_{n}\mathbin {\nabla } y'_{n}$в конечном итоге является стационарным. Тогда мы сможем взять $y'_{n}=f'(x'_{n})$.

В некоторых случаях можно определить абстракции, используя связи Галуа. $(\alpha ,\gamma )$ где $\alpha$ из $L$ к $L'$ и $\gamma$ из $L'$ к $L$. Это предполагает существование лучших абстракций, что не обязательно так. Например, если мы абстрагируем множества пар $(x,y)$ действительных чисел , заключая выпуклые многогранники , не существует оптимальной абстракции для диска, определяемого формулой $x^{2}+y^{2}\leq 1$.

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

Числовые абстрактные домены

Каждой переменной можно присвоить $x$ доступен в данной программе в определенный интервал времени $[L_{x},H_{x}]$. Государство, присваивающее значение $v(x)$ в переменную $x$ будет конкретизацией этих интервалов, если для всех $x$, у нас есть $v(x)\in [L_{x},H_{x}]$. Из интервалов $[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}+H_{y}]$. Более сложные формулы могут быть выведены для умножения, деления и т. д., что дает так называемую интервальную арифметику .

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

у = х;
 г = х - у;
 

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

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

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

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

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

• отношения сравнения целых чисел
• выпуклые многогранники (см. рисунок слева) – с некоторыми высокими вычислительными затратами
• разностные матрицы
• "восьмиугольники"
• линейные равенства

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

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

Абстрактные домены машинных слов

В то время как языки высокого уровня, такие как Python или Haskell, по умолчанию используют неограниченные целые числа, языки программирования более низкого уровня, такие как C или ассемблер, конечного размера обычно работают с машинными словами , которые более удобно моделировать с использованием целых чисел по модулю. ${\textstyle 2^{n}}$(где n — разрядность машинного слова). Существует несколько абстрактных областей, подходящих для различного анализа таких переменных.

Домен битового поля обрабатывает каждый бит машинного слова отдельно, т. е. слово ширины n рассматривается как массив из n абстрактных значений. Абстрактные значения берутся из множества ${\textstyle \{0,1,\bot \}}$, а функции абстракции и конкретизации имеют вид: $\gamma (0)=\{0\}$, $\gamma (1)=\{1\}$, $\gamma (\bot )=\{0,1\}$, $\alpha (\{0\})=0$, $\alpha (\{1\})=1$, $\alpha (\{0,1\})=\bot$, $\alpha (\{\})=\bot$. Побитовые операции над этими абстрактными значениями идентичны соответствующим логическим операциям в некоторых трехзначных логиках :

НЕ(А) А ¬A 0 1 ⊥ ⊥ 1 0	И(А, Б) А ∧ Б Б 0 ⊥ 1 А 0 0 0 0 ⊥ 0 ⊥ ⊥ 1 0 ⊥ 1	ИЛИ(А, Б) А ∨ Б Б 0 ⊥ 1 А 0 0 ⊥ 1 ⊥ ⊥ ⊥ 1 1 1 1 1

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

См. также

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

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

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

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

• Абстрактная интерпретация . Патрик Кузо. Массачусетский технологический институт.
• Конспекты лекций Дэвида Шмидта по абстрактной интерпретации
• Конспекты лекций Мёллера и Шварцбаха по статическому анализу программ
• Конспекты лекций Агостино Кортези по анализу и верификации программ
• Слайды Грегуара Сютра, описывающие каждый этап абстрактной интерпретации со множеством примеров, а также представление связей Галуа.