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

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

Мотивация [ править ]

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

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

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

Терминология [ править ]

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

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

Анализ [ править ]

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

Имя	Домен	Описание
до	Все утверждения и выражения	Переменные, определенно назначенные перед вычислением данного утверждения или выражения.
после	Все утверждения и выражения	Переменные, определенно назначенные после вычисления данного оператора или выражения, при условии, что оно завершается нормально.
чей	Все утверждения и выражения	Все переменные, доступные в области данного оператора или выражения.
истинный	Все логические выражения	Переменные, определенно назначенные после вычисления данного выражения, при условии, что выражение имеет значение true .
ЛОЖЬ	Все логические выражения	Переменные, определенно назначенные после вычисления данного выражения, при условии, что выражение имеет значение false .

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

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

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

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

 интервал   я   =   1  ; 
   Л  : 
  перейти к   Л  ;

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

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

 интервал   я  ; 
   если   (  j   <   0  )   вернуть  ;    иначе   я   =   j  ; 
   распечатать  (  я  );

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

Ссылки [ править ]

^ Дж. Гослинг; Б. Джой; Г. Стил; Г. Браха. «Спецификация языка Java, 3-е издание» . стр. Глава 16 (стр. 527–552) . Проверено 2 декабря 2008 г.
^ «Стандарт ECMA-334, спецификация языка C#» . ЭКМА Интернешнл . стр. Раздел 12.3 (стр. 122–133) . Проверено 2 декабря 2008 г.
^ Старк, Роберт Ф.; Э. Боргер; Иоахим Шмид (2001). Java и виртуальная машина Java: определение, проверка, валидация . Секаукус, Нью-Джерси, США: Springer-Verlag New York, Inc., стр. Раздел 8.3. ISBN 3-540-42088-6 .
^ Перейти обратно: ^а ^б Фруджа, Нику Г. (октябрь 2004 г.). «Корректность анализа определенного присваивания в C#» . Журнал объектных технологий . 3 (9): 29–52. CiteSeerX 10.1.1.165.6696 . дои : 10.5381/jot.2004.3.9.a2 . Проверено 2 декабря 2008 г. На самом деле мы доказываем больше, чем просто правильность: мы показываем, что решение анализа является идеальным решением (а не только безопасным приближением).
^ «Циклон: Определенное назначение» . Руководство пользователя Циклона . Проверено 16 декабря 2008 г.
^ «Стандарт ECMA-335, инфраструктура общего языка (CLI)» . ЭКМА Интернешнл . п. п. 1.8.1.1 (раздел III, стр. 19) . Проверено 2 декабря 2008 г.

[1] Дж. Гослинг; Б. Джой; Г. Стил; Г. Браха. «Спецификация языка Java, 3-е издание» . стр. Глава 16 (стр. 527–552) . Проверено 2 декабря 2008 г.

[2] «Стандарт ECMA-334, спецификация языка C#» . ЭКМА Интернешнл . стр. Раздел 12.3 (стр. 122–133) . Проверено 2 декабря 2008 г.

[3] Старк, Роберт Ф.; Э. Боргер; Иоахим Шмид (2001). Java и виртуальная машина Java: определение, проверка, валидация . Секаукус, Нью-Джерси, США: Springer-Verlag New York, Inc., стр. Раздел 8.3. ISBN 3-540-42088-6 .

[fruja-4] Перейти обратно: ^а ^б Фруджа, Нику Г. (октябрь 2004 г.). «Корректность анализа определенного присваивания в C#» . Журнал объектных технологий . 3 (9): 29–52. CiteSeerX 10.1.1.165.6696 . дои : 10.5381/jot.2004.3.9.a2 . Проверено 2 декабря 2008 г. На самом деле мы доказываем больше, чем просто правильность: мы показываем, что решение анализа является идеальным решением (а не только безопасным приближением).

[5] «Циклон: Определенное назначение» . Руководство пользователя Циклона . Проверено 16 декабря 2008 г.

[6] «Стандарт ECMA-335, инфраструктура общего языка (CLI)» . ЭКМА Интернешнл . п. п. 1.8.1.1 (раздел III, стр. 19) . Проверено 2 декабря 2008 г.

[1]

[2]

[3]

[4]

[5]

[6]