Абстрактная интерпретация в статическом анализе программ

Введение

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

Интуиция

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

This section illustrates abstract interpretation by means of real world, non computing examples. Consider the people in a conference room. Assume a unique identifier for each person in the room, like a social security number in the United States. To prove that someone is not present, all one needs to do is see if their social security number is not on the list. Since two different people cannot have the same number, it is possible to prove or disprove the presence of a participant simply by looking up their number. However it is possible that only the names of attendees were registered. If the name of a person is not found in the list, we may safely conclude that that person was not present; but if it is, we cannot conclude definitely without further inquiries, due to the possibility of homonyms (for example, two people named John Smith). Note that this imprecise information will still be adequate for most purposes, because homonyms are rare in practice. However, in all rigor, we cannot say for sure that somebody was present in the room; all we can say is that they were possibly here. If the person we are looking up is a criminal, we will issue an alarm; but there is of course the possibility of issuing a false alarm. Similar phenomena will occur in the analysis of programs. If we are only interested in some specific information, say, "was there a person of age in the room? ", keeping a list of all names and dates of births is unnecessary. We may safely and without loss of precision restrict ourselves to keeping a list of the participants' ages. If this is already too much to handle, we might keep only the age of the youngest, and oldest person, If the question is about an age strictly lower than or strictly higher than , then we may safely respond that no such participant was present. Otherwise, we may only be able to say that we do not know. In the case of computing, concrete, precise information is in general not computable within finite time and memory (see Rice's theorem and the halting problem). Abstraction is used to allow for generalized answers to questions (for example, answering "maybe" to a yes/no question, meaning "yes or no", when we (an algorithm of abstract interpretation) cannot compute the precise answer with certainty); this simplifies the problems, making them amenable to automatic solutions. One crucial requirement is to add enough vagueness so as to make problems manageable while still retaining enough precision for answering the important questions (such as "might the program crash? ").

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

При наличии языка программирования или спецификации, абстрактная интерпретация состоит в определении нескольких семантик, связанных отношениями абстракции. Семантика – это математическая характеристика возможного поведения программы. Наиболее точная семантика, очень близко описывающая фактическое выполнение программы, называется конкретной семантикой. Например, конкретная семантика императивного языка программирования может сопоставлять каждой программе множество возможных трасс выполнения – трасса выполнения является последовательностью возможных последовательных состояний выполнения программы; состояние обычно состоит из значения счётчика программы и расположений памяти (глобальные переменные, стек и куча). Затем выводятся более абстрактные семантики; например, можно рассматривать только множество достижимых состояний в трассах выполнения (что эквивалентно рассмотрению последних состояний в конечных трассах). Цель статического анализа – получить вычислимую семантическую интерпретацию в определённый момент. Например, можно выбрать представление состояния программы, работающей с целочисленными переменными, путём игнорирования фактических значений переменных и сохранения только их знаков (+, − или 0). Для некоторых элементарных операций, таких как умножение, такая абстракция не приводит к потере точности: для определения знака произведения достаточно знать знаки операндов. Для других операций абстракция может терять точность: например, невозможно определить знак суммы, операнды которой имеют соответственно положительный и отрицательный знаки. Иногда потеря точности необходима для обеспечения разрешимости семантики (см. теорему Райса и проблему останова). В общем случае, необходимо искать компромисс между точностью анализа и его разрешимостью (вычислимостью) или практической применимостью (вычислительной сложностью). На практике определяемые абстракции адаптируются как к свойствам программы, которые требуется анализировать, так и к набору целевых программ. Первый крупномасштабный автоматизированный анализ компьютерных программ с использованием абстрактной интерпретации был вызван аварией, приведшей к разрушению первого полёта ракеты Ariane 5 в 1996 году.

Given a programming or specification language, abstract interpretation consists of giving several semantics linked by relations of abstraction. A semantics is a mathematical characterization of a possible behavior of the program. The most precise semantics, describing very closely the actual execution of the program, are called the concrete semantics. For instance, the concrete semantics of an imperative programming language may associate to each program the set of execution traces it may produce – an execution trace being a sequence of possible consecutive states of the execution of the program; a state typically consists of the value of the program counter and the memory locations (globals, stack and heap). More abstract semantics are then derived; for instance, one may consider only the set of reachable states in the executions (which amounts to considering the last states in finite traces). The goal of static analysis is to derive a computable semantic interpretation at some point. For instance, one may choose to represent the state of a program manipulating integer variables by forgetting the actual values of the variables and only keeping their signs (+, − or 0). For some elementary operations, such as multiplication, such an abstraction does not lose any precision: to get the sign of a product, it is sufficient to know the sign of the operands. For some other operations, the abstraction may lose precision: for instance, it is impossible to know the sign of a sum whose operands are respectively positive and negative. Sometimes a loss of precision is necessary to make the semantics decidable (see Rice's theorem and the halting problem). In general, there is a compromise to be made between the precision of the analysis and its decidability (computability), or tractability (computational cost). In practice the abstractions that are defined are tailored to both the program properties one desires to analyze, and to the set of target programs. The first large scale automated analysis of computer programs with abstract interpretation was motivated by the accident that resulted in the destruction of the first flight of the Ariane 5 rocket in 1996.