Анализ определенного назначения

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

• 1 Мотивация
• 2 Терминология
• 3 Анализ
• 4 Ссылки

В C и C ++ программ, источником особенно трудно диагностируемых ошибок является недетерминированное поведение, возникающее в результате чтения неинициализированных переменных ; это поведение может различаться для разных платформ, сборок и даже от запуска к запуску.

Есть два распространенных способа решения этой проблемы. Один из них - убедиться, что все местоположения записаны до их чтения. Теорема Райса устанавливает, что эта проблема не может быть решена в целом для всех программ; однако можно создать консервативный (неточный) анализ, который будет принимать только программы, удовлетворяющие этому ограничению, и отвергать некоторые правильные программы, и анализ определенного назначения является таким анализом. Спецификации языков программирования Java и C # требуют, чтобы компилятор сообщал об ошибке времени компиляции, если анализ не удался. Оба языка требуют особой формы анализа, детально описанного. В Java этот анализ был формализован Stärk et al., И некоторые правильные программы отклоняются и должны быть изменены, чтобы ввести явные ненужные назначения. В C # этот анализ был формализован Fruja и является точным и обоснованным в том смысле, что все переменные, назначенные на всех путях потока управления, будут считаться определенно назначенными. Язык Cyclone также требует, чтобы программы проходили анализ определенного присваивания, но только для переменных с указательными типами, чтобы упростить перенос программ на C.

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

Можно сказать, что переменная или местоположение находятся в одном из трех состояний в любой заданной точке программы:

• Определенно присвоено: переменная точно известно, что она будет назначена.
• Определенно не назначена: переменная точно известно, что она не назначена.
• Неизвестно: переменная может быть присвоена или не назначена ; анализ недостаточно точен, чтобы определить, какие.

Нижеследующее основано на формализации Fruja внутрипроцедурного (единый метод) анализа определенного присваивания C #, который отвечает за обеспечение того, чтобы все локальные переменные были назначаются до их использования. Он одновременно выполняет анализ определенного присваивания и постоянное распространение логических значений. Мы определяем пять статических функций:

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

• Любое выражение или инструкция e, которые не влияют на набор переменных, определенно присвоенных: after (e) = before (e)
• Пусть e будет выражением присваивания loc = v. Тогда before (v) = before (e), а after (e) = after (v) U {loc}.
• Пусть e будет выражением true . Тогда true (e) = before (e) и false (e) = vars (e). Другими словами, если e оценивается как false, все переменные (пусто ) определенно назначаются, потому что e не оценивается как false.
• Поскольку оцениваются аргументы метода слева направо, до (arg i + 1) = after (arg i). После завершения метода параметры out однозначно назначаются.
• Пусть s будет условным оператором if (e) s 1else s2. Тогда before (e) = before (s), before (s 1) = true (e), before (s 2) = false (e) и after (s) = after (s 1) пересекаются после (s 2).
• Пусть s будет оператором цикла while while (e) s 1. Затем before (e) = before (s), before (s 1) = true (e) и after (s) = false (e).
• И так далее.

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

Алгоритм усложняется введением переходов потока управления, таких как goto, break, continue, return и обработка исключений. Любой оператор, который может быть целью одного из этих переходов, должен пересекать его перед установленным набором определенно назначенных переменных в источнике перехода. Wh en они представлены, результирующий поток данных может иметь несколько фиксированных точек, как в этом примере:

1 int i = 1; 2 л: 3 л.

Поскольку метка L может быть достигнута из двух мест, уравнение потока управления для goto диктует, что before (2) = after (1) пересекаются до (3). Но before (3) = before (2), поэтому before (2) = after (1) пересекаются до (2). У этого есть две фиксированные точки для before (2), {i} и пустое множество. Однако можно показать, что из-за монотонной формы уравнений потока данных существует уникальная максимальная фиксированная точка (фиксированная точка наибольшего размера), которая обеспечивает наиболее возможную информацию об определенно присвоенных переменных. Такую максимальную (или максимальную) фиксированную точку можно вычислить стандартными методами; см. анализ потока данных.

Дополнительная проблема заключается в том, что скачок потока управления может сделать некоторые потоки управления невозможными; например, в этом фрагменте кода переменная i определенно присваивается перед ее использованием:

1 int i; 2 if (j < 0) return; else i = j; 3 print(i);

Уравнение потока данных для if говорит, что after (2) = after (return ) пересекаются после (i = j). Чтобы это работало правильно, мы определяем after ( e) = vars (e) для всех скачков потока управления; это пусто справедливо в том же смысле, что и уравнение false (true ) = vars (e), потому что это невозможно для управления чтобы достичь точки сразу после перехода потока управления.

1. ^Дж. Гослинг; Б. Джой; Г. Стил; Г. Браха. «Спецификация языка Java, 3-е издание». Стр. Глава 16 (стр. 527–552). Проверено 2 декабря 2008 г.
2. ^«Standard ECMA-334, C # Language Specification». ECMA International. Pp. Раздел 12.3 (стр.122 –133). Проверено 2 декабря 2008 г.
3. ^Stärk, Robert F.; E. Borger; Joachim Schmid (2001). Java и виртуальная машина Java: определение, проверка, проверка. Secaucus, NJ, USA: Springer- Verlag New York, Inc., стр. Раздел 8.3. ISBN 3-540-42088-6.
4. ^ Фруха, Нику Г. (октябрь 2004 г.) «Правильность определения Анализ присвоения ите в C # ". Журнал объектных технологий. 3 (9): 29–52. CiteSeerX 10.1.1.165.6696. doi : 10.5381 / jot.2004.3.9.a2. Проверено 2 декабря 2008. На самом деле мы доказываем больше, чем правильность: мы показываем, что решение анализа является идеальным решением (а не только безопасным приближением).
5. ^«Циклон: определенное назначение». Руководство пользователя Cyclone. Проверено 16 декабря 2008 г.
6. ^«Стандартный ECMA-335, Common Language Infrastructure (CLI)». ECMA International. стр. Раздел 1.8.1.1 (Раздел III, стр. 19). Получено 2 декабря 2008 г.