Войти
В информатике, абстрактная интерпретация- это теория приближения звука семантики компьютерных программ, основанной на монотонных функциях над упорядоченными наборами, особенно решетками. Его можно рассматривать как частичное выполнение компьютерной программы , которая получает информацию о своей семантике (например, поток управления, поток данных ) без выполнения всех вычислений.
Его основным конкретным применением является формальный статический анализ, автоматическое извлечение информации о возможном выполнении компьютерных программ; такой анализ имеет два основных применения:
Абстрактная интерпретация была формализована рабочей парой французских компьютерных ученых Патрик Кузо и Радия Кузо в конце 1970-х.
Этот раздел иллюстрирует абстрактную интерпретацию с помощью реальных, не вычислительных примеров.
Представьте себе людей в конференц-зале. Предположите уникальный идентификатор для каждого человека в комнате, например, номер социального страхования в США. Чтобы доказать, что кого-то нет, достаточно посмотреть, нет ли его номера социального страхования в списке. Поскольку у двух разных людей не может быть одного и того же номера, можно доказать или опровергнуть присутствие участника, просто посмотрев его или ее номер.
Однако возможно, что были зарегистрированы только имена участников. Если имя человека не найдено в списке, мы можем с уверенностью сделать вывод, что этого человека не было; но если это так, мы не можем сделать окончательный вывод без дальнейших исследований из-за возможности омонимов (например, два человека по имени Джон Смит). Обратите внимание, что этой неточной информации будет достаточно для большинства целей, поскольку омонимы на практике встречаются редко. Однако со всей строгостью мы не можем сказать наверняка, что кто-то присутствовал в комнате; все, что мы можем сказать, это то, что он или она, возможно, были здесь. Если человек, которого мы ищем, является преступником, мы подадим сигнал тревоги; но, конечно, есть вероятность ложной тревоги. Подобные явления будут возникать при анализе программ.
Если нас интересует только некоторая конкретная информация, скажем, «был ли в комнате человек в возрасте n?», То вести список всех имен и дат рождений нет необходимости. Мы можем безопасно и без потери точности ограничиться ведением списка возрастов участников. Если это уже слишком, мы можем сохранить только возраст самого молодого, m и самого старшего человека, M. Если вопрос касается возраста строго ниже m или строго выше M, то мы можем смело ответить, что нет такой участник присутствовал. В противном случае мы можем сказать только то, что не знаем.
В случае вычислений конкретная точная информация, как правило, не может быть вычислена за конечное время и память (см. теорему Райса и проблему остановки ). Абстракция используется для получения обобщенных ответов на вопросы (например, ответ «возможно» на вопрос «да / нет», что означает «да или нет», когда мы (алгоритм абстрактной интерпретации) не можем вычислить точный ответ с уверенностью); это упрощает проблемы, делая их доступными для автоматических решений. Одно из важнейших требований - добавить достаточно неопределенности, чтобы проблемы можно было решить, сохраняя при этом достаточную точность для ответов на важные вопросы (например, «может произойти сбой программы?»).
Для данного языка программирования или спецификаций абстрактная интерпретация состоит из предоставления нескольких семантик, связанных отношениями абстракции. Семантика - это математическая характеристика возможного поведения программы. Наиболее точная семантика, очень точно описывающая фактическое выполнение программы, называется конкретной семантикой. Например, конкретная семантика языка императивного программирования может связывать с каждой программой набор трассировок выполнения, которые она может создавать - трасса выполнения представляет собой последовательность возможных последовательных состояний выполнения программы; состояние обычно состоит из значения счетчика программ и ячеек памяти (глобальных объектов, стека и кучи). Затем выводится более абстрактная семантика; например, можно рассматривать только набор достижимых состояний в выполнениях (что составляет рассмотрение последних состояний в конечных трассировках).
Цель статического анализа - получить вычислимую семантическую интерпретацию в какой-то момент. Например, можно выбрать представление состояния программы, управляющей целочисленными переменными, путем забвения фактических значений переменных и сохранения только их знаков (+, - или 0). Для некоторых элементарных операций, таких как умножение, такая абстракция не теряет точности: чтобы получить знак продукта, достаточно знать знак операндов. Для некоторых других операций абстракция может потерять точность: например, невозможно узнать знак суммы, операнды которой соответственно положительны и отрицательны.
Иногда потеря точности необходима, чтобы сделать семантику разрешимой (см. теорема Райса, проблема остановки ). Как правило, необходимо идти на компромисс между точностью анализа и его разрешимостью (вычислимость ) или управляемостью (вычислительные затраты ).
На практике определяемые абстракции приспособлены как к свойствам программы, которые необходимо анализировать, так и к набору целевых программ. Первый крупномасштабный автоматизированный анализ компьютерных программ с абстрактной интерпретацией можно отнести к аварии, которая привела к разрушению первого полета ракеты Ariane 5 в 1996 году.
Пусть L будет упорядоченным набором, называемым конкретным набором, и пусть L ′ будет другим упорядоченным набором, называемым абстрактный набор. Эти два набора связаны друг с другом посредством определения общих функций, которые сопоставляют элементы друг с другом.
Функция α называется функцией абстракции, если она отображает элемент x в конкретном множестве L на элемент α (x) в абстрактном множестве L '. То есть, элемент α (x) в L ′ является абстракциейx в L.
Функция γ называется функцией конкретизации, если она отображает элемент x ′ в абстрактном множестве L ′ на элемент γ (x ′) в конкретном множестве L. То есть элемент γ (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 ∘ γ) (x ′) ≤ (γ ∘ f ′) (x ′).
Семантика программы обычно описывается с помощью фиксированных точек при наличии циклов или рекурсивных процедур. Предположим, что L - полная решетка, и пусть f - монотонная функция из L в L. Тогда любой x ′ такой, что f (x ′) ≤ x ′, является абстракцией наименьшей неподвижной точки f, которая существует , согласно теореме Кнастера – Тарского.
Теперь трудность состоит в том, чтобы получить такое x ′. Если L 'имеет конечную высоту или, по крайней мере, проверяет условие восходящей цепи (все восходящие последовательности в конечном итоге стационарны), то такой x' может быть получен как стационарный предел восходящей последовательности x 'n определяется по индукции следующим образом: x ′ 0 = ⊥ (наименьший элемент L ′) и x ′ n + 1 = f ′ (x ′ n ).
В других случаях все еще возможно получить такой x ′ с помощью оператора расширения ∇: для всех x и y x ∇ y должно быть больше или равно, чем x и y, и для любой последовательности y ′ n последовательность, определенная как x ′ 0 = ⊥ и x ′ n + 1 = x ′ n ∇ y ′ n в конечном итоге стационарен. Затем мы можем взять y ′ n = f ′ (x ′ n ).
В некоторых случаях можно определить абстракции с помощью связей Галуа (α, γ), где α от L до L ', а γ от L до L. Это предполагает наличие лучших абстракций, что не обязательно так. Например, если мы абстрагируем наборы пар (x, y) вещественных чисел путем включения выпуклых многогранников, не будет оптимальной абстракции для диска, определяемого x + y ≤ 1.
Каждой переменной x, доступной в данной программной точке, можно присвоить интервал [L x , H x ]. Состояние, присваивающее значение v (x) переменной x, будет конкретизацией этих интервалов, если для всех x v (x) находится в [L x , H x ]. Из интервалов [L x , H x ] и [L y , H y ] для переменных x и y можно легко получить интервалы для x + y ([L x+Ly, H x+Hy]) и для x-y ([L x−Hy, H x−Ly]); обратите внимание, что это точные абстракции, поскольку набор возможных результатов, скажем, для x + y, в точности соответствует интервалу ([L x+Ly, H x+Hy]). Более сложные формулы могут быть получены для умножения, деления и т.д., что дает так называемую интервальную арифметику.
Давайте теперь рассмотрим следующую очень простую программу:
y = x; г = х - у;
| Комбинация интервальной арифметики (зеленый) и сравнения по модулю 2 на целых числах (голубой) в качестве абстрактных областей для анализа простого фрагмента кода C (красный: конкретные наборы возможных значений во время выполнения). Используя информацию сравнения (0 = четный, 1 = нечетный), можно исключить деление на ноль. (Поскольку задействована только одна переменная, реляционные и нереляционные домены здесь не проблема.) |
| Пример трехмерного выпуклого многогранника, описывающего возможные значения трех переменных в некоторой точке программы. Каждая из переменных может быть равна нулю, но все три не могут быть равны нулю одновременно. Последнее свойство не может быть описано в области интервальной арифметики. |
При разумных типах арифметики результат для zдолжен быть равен нулю. Но если мы выполним интервальную арифметику, начиная с xв [0, 1], мы получим zв [-1, +1]. В то время как каждая из операций, взятых по отдельности, была точно абстрактной, их состав - нет.
Проблема очевидна: мы не отслеживали отношения равенства между xи y; фактически, эта область интервалов не принимает во внимание никаких отношений между переменными и, таким образом, является нереляционной областью. Нереляционные домены обычно бывают быстрыми и простыми в реализации, но неточными.
Некоторые примеры реляционныхчисловых абстрактных областей:
и их комбинации (например, уменьшенное произведение, см. Справа картина).
Когда кто-то выбирает абстрактную область, он обычно должен найти баланс между сохранением детальных отношений и высокими вычислительными затратами.
