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

Подход к статическому анализу программ

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

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

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

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

Интуиция

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Можно назначить каждой переменной, доступной в данной точке программы, интервал . Состояние, назначающее значение переменной, будет конкретизацией этих интервалов, если для всех , мы имеем . Из интервалов и для переменных и , соответственно, можно легко получить интервалы для (а именно, ) и для (а именно, ); обратите внимание, что это точные абстракции, поскольку множество возможных результатов для, скажем, , как раз и есть интервал . Более сложные формулы могут быть выведены для умножения, деления и т. д., что даст так называемую интервальную арифметику . ^[5] ${\displaystyle x}$ ${\displaystyle [L_{x},H_{x}]}$ ${\displaystyle v(x)}$ ${\displaystyle x}$ ${\displaystyle x}$ ${\displaystyle v(x)\in [L_{x},H_{x}]}$ ${\displaystyle [L_{x},H_{x}]}$ ${\displaystyle [L_{y},H_{y}]}$ ${\displaystyle x}$ ${\displaystyle y}$ ${\displaystyle x+y}$ ${\displaystyle [L_{x}+L_{y},H_{x}+H_{y}]}$ ${\displaystyle x-y}$ ${\displaystyle [L_{x}-H_{y},H_{x}-L_{y}]}$ ${\displaystyle x+y}$ ${\displaystyle [L_{x}+L_{y},H_{x}+H_{y}]}$

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

у = х;z = х - у;

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

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

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

• отношения конгруэнтности целых чисел ^{[6] [7]}
• выпуклые многогранники ^[8] (см. рисунок слева) – с некоторыми высокими вычислительными затратами
• Матрицы с разностными связями ^[9]
• "восьмиугольники" ^{[10] [11] [12]}
• линейные равенства ^[13]

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

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

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

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

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

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

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

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

Ссылки

1. Cousot, Patrick; Cousot, Radhia (1977). «Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints» (PDF) . Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977 . ACM Press. pp. 238–252. doi :10.1145/512950.512973. S2CID  207614632.
2. Cousot, Patrick; Cousot, Radhia (1979). "Систематическое проектирование структур анализа программ" (PDF) . Протокол конференции шестого ежегодного симпозиума ACM по принципам языков программирования, Сан-Антонио, Техас, США, январь 1979 г. ACM Press. стр. 269–282. doi :10.1145/567752.567778. S2CID  1547466.
3. Фор, Кристель. "История технологий PolySpace" . Получено 3 октября 2010 г.
4. Cousot, P.; Cousot, R. (август 1992 г.). «Сравнение связи Галуа и подходов расширения/сужения к абстрактной интерпретации» (PDF) . В Bruynooghe, Maurice; Wirsing, Martin (ред.). Proc. 4th Int. Symp. on Programming Language Implementation and Logic Programming (PLILP) . Lecture Notes in Computer Science. Vol. 631. Springer. pp. 269–296. ISBN 978-0-387-55844-8.
5. Кусо, Патрик; Кусо, Радхия (1976). "Статическое определение динамических свойств программ" (PDF) . Труды Второго международного симпозиума по программированию . Дюно, Париж, Франция. С. 106–130.
6. Granger, Philippe (1989). «Статический анализ арифметических сравнений». International Journal of Computer Mathematics . 30 (3–4): 165–190. doi :10.1080/00207168908803778.
7. Филипп Грэнжер (1991). «Статический анализ линейных конгруэнтных равенств среди переменных программы». В Abramsky, S.; Maibaum, TSE (ред.). Proc. Int. J. Conf. on Theory and Practice of Software Development (TAPSOFT) . Lecture Notes in Computer Science. Vol. 493. Springer. pp. 169–192.
8. Кусо, Патрик; Хальбвакс, Николас (январь 1978 г.). «Автоматическое обнаружение линейных ограничений среди переменных программы» (PDF) . Конференция. Рек. 5-й симпозиум ACM по принципам языков программирования (POPL) . стр. 84–97.
9. Мине, Антуан (2001). «Новая числовая абстрактная область на основе матриц с разностными связями». В Danvy, Olivier; Filinski, Andrzej (ред.). Программы как объекты данных, Второй симпозиум, (PADO) . Lecture Notes in Computer Science. Vol. 2053. Springer. pp. 155–172. arXiv : cs/0703073 .
10. Мине, Антуан (декабрь 2004 г.). Слабо реляционные числовые абстрактные области (PDF) (кандидатская диссертация). Лаборатория информатики Высшей нормальной школы.
11. Антуан Мине (2006). «Абстрактная область восьмиугольника». Higher Order Symbol. 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. S2CID  376574.
14. Мине, Антуан (июнь 2012 г.). «Абстрактные домены для целочисленных и плавающих операций на уровне битовой машины». WING'12 — 4-й Международный семинар по генерации инвариантов . Манчестер, Соединенное Королевство: 16.
15. Регер, Джон; Дуонгсаа, Усит (июнь 2006 г.). «Вывод абстрактных функций передачи для анализа встроенного программного обеспечения». Труды конференции ACM SIGPLAN/SIGBED 2006 г. по языку, компиляторам и поддержке инструментов для встроенных систем . LCTES '06. Нью-Йорк, штат Нью-Йорк, США: Ассоциация вычислительной техники. стр. 34–43. doi :10.1145/1134650.1134657. ISBN 978-1-59593-362-1. S2CID  13221224.
16. Репс, Т.; Логинов, А.; Сагив, М. (июль 2002 г.). «Семантическая минимизация 3-значных пропозициональных формул». Труды 17-го ежегодного симпозиума IEEE по логике в информатике . стр. 40–51. doi :10.1109/LICS.2002.1029816. ISBN 0-7695-1483-9. S2CID  8451238.
17. Юн, Ёнхо; Ли, Усук; Йи, Квангын (2023-06-06). «Индуктивный синтез программ с помощью итеративной прямой-обратной абстрактной интерпретации». Труды ACM по языкам программирования . 7 (PLDI): 174:1657–174:1681. arXiv : 2304.10768 . doi : 10.1145/3591288 .

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

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

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

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