Составители:
Рубрика:
4.3. Верификация CIL-кода
Говорят, что код программ не разрушает память, если эти программы,
будучи запущенными в одном адресном пространстве, корректно изоли-
рованы друг от друга, то есть ошибки в одной программе не могут привес-
ти к изменению структур данных другой программы.
Верификация кода – это процесс автоматического доказательства то-
го, что этот код не разрушает память.
В этой главе мы рассмотрим общие вопросы верификации кода и ал-
горитм верификации, приведенный в спецификации CLI и реализован-
ный в Microsoft .NET Framework.
4.3.1. Классификация применяемых на практике алгоритмов
верификации
Алгоритмы верификации являются метавычислительными алгорит-
мами (верификаторы кода стоят в одном ряду с такими программами, как
частичные вычислители и суперкомпиляторы). Поэтому совершенно
неудивительно, что алгоритмы верификации в общем случае имеют проб-
лемы, свойственные любым метавычислительным алгоритмам, а именно:
экспоненциальная сложность и потенциальная нетерминируемость.
Понятно, что алгоритмы, работающие неизвестно сколько времени
(а возможно, вообще никогда не завершающиеся) и потребляющие неиз-
вестно какое количество ресурсов, представляют скорее теоретический,
нежели практический интерес. Поэтому их разработчикам приходится ка-
ким-то образом ограничивать задачу, чтобы получить применимые на пра-
ктике результаты. Для алгоритмов верификации кода известно два подхо-
да, позволяющие снизить их сложность и добиться терминируемости:
1. Концентрация усилий на выявлении только таких ошибок в
программах, поиск которых не требует экспоненциальной
сложности и выполняется за конечное время.
Для этого подхода характерно то, что существуют программы, в
которых верификатор не находит ни одной ошибки и которые,
тем не менее, разрушают память.
2. Работа лишь с некоторым подмножеством программ, для кото-
рых факт неразрушения ими памяти можно доказать за конеч-
ное время с использованием алгоритма приемлемой сложности.
Этот тип верификаторов отличается тем, что существуют не раз-
рушающие память программы, которые не могут быть доказаны
алгоритмом.
Если задача некоторого метавычислительного алгоритма была как-то
ограничена, то сразу же возникает вопрос о том, какие входные данные
(программы) он сможет обработать. Для суперкомпиляторов и частичных
Анализ кода на CIL
147
блоков. Для этого нужно каждый блок, расположенный в массиве
blockNodes по индексу i, соединить дугой с узлом Nodes[i]:
blockNodes = новый массив ссылок на узлы размера N,
изначально заполненный нулевыми ссылками;
for (int i = 0; i < BN; i++)
{
Провести дугу от B[i].block к Nodes[B[i].offset];
blockNodes[B[i].offset] = B[i].block;
}
Добавление остальных дуг осуществляется путем перебора всех уз-
лов, находящихся в массиве Nodes. Давайте рассмотрим, как это происхо-
дит для некоторого узла Nodes[i].
Прежде всего мы определяем номера инструкций, на которые может
быть передано управление от инструкции, соответствующей узлу Nodes[i].
Естественно, для этого должна учитываться семантика инструкции. Полу-
ченные номера инструкций записываются в массив Flow.
Затем для каждого номера n, входящего в массив Flow, мы проводим
дугу от узла Nodes[i] к соответствующему номеру n узлу графа:
• это узел blockNodes[n] в том случае, если blockNodes[n] содержит
ссылку на блок (то есть если инструкция под номером n являет-
ся первой инструкцией некоторого блока) и Nodes[i] непосред-
ственно или транзитивно принадлежит этому блоку;
• это узел Nodes[n] в противном случае.
На псевдоязыке это выглядит следующим образом:
for (int i = 0; i < N; i++)
{
int[] Flow = новый массив, в который добавляются
номера инструкций, на которые может быть передано
управление от инструкции, соответствующей узлу
Nodes[i];
for (int j = 0; j < Flow.Length; j++)
{
int n = Flow[j];
if (blockNodes[n] != null && blockNodes[n] не является
непосредственно или транзитивно родителем узла Nodes[i])
Провести дугу от Nodes[i] к blockNodes[n];
else
Провести дугу от Nodes[i] к Nodes[n];
}
}
146
CIL и системное программирование в Microsoft .NET
146 CIL и системное программирование в Microsoft .NET Анализ кода на CIL 147
блоков. Для этого нужно каждый блок, расположенный в массиве 4.3. Верификация CIL-кода
blockNodes по индексу i, соединить дугой с узлом Nodes[i]:
blockNodes = новый массив ссылок на узлы размера N, Говорят, что код программ не разрушает память, если эти программы,
изначально заполненный нулевыми ссылками; будучи запущенными в одном адресном пространстве, корректно изоли-
for (int i = 0; i < BN; i++) рованы друг от друга, то есть ошибки в одной программе не могут привес-
{ ти к изменению структур данных другой программы.
Провести дугу от B[i].block к Nodes[B[i].offset]; Верификация кода – это процесс автоматического доказательства то-
blockNodes[B[i].offset] = B[i].block; го, что этот код не разрушает память.
} В этой главе мы рассмотрим общие вопросы верификации кода и ал-
Добавление остальных дуг осуществляется путем перебора всех уз- горитм верификации, приведенный в спецификации CLI и реализован-
лов, находящихся в массиве Nodes. Давайте рассмотрим, как это происхо- ный в Microsoft .NET Framework.
дит для некоторого узла Nodes[i].
Прежде всего мы определяем номера инструкций, на которые может 4.3.1. Классификация применяемых на практике алгоритмов
быть передано управление от инструкции, соответствующей узлу Nodes[i]. верификации
Естественно, для этого должна учитываться семантика инструкции. Полу- Алгоритмы верификации являются метавычислительными алгорит-
ченные номера инструкций записываются в массив Flow. мами (верификаторы кода стоят в одном ряду с такими программами, как
Затем для каждого номера n, входящего в массив Flow, мы проводим частичные вычислители и суперкомпиляторы). Поэтому совершенно
дугу от узла Nodes[i] к соответствующему номеру n узлу графа: неудивительно, что алгоритмы верификации в общем случае имеют проб-
• это узел blockNodes[n] в том случае, если blockNodes[n] содержит лемы, свойственные любым метавычислительным алгоритмам, а именно:
ссылку на блок (то есть если инструкция под номером n являет- экспоненциальная сложность и потенциальная нетерминируемость.
ся первой инструкцией некоторого блока) и Nodes[i] непосред- Понятно, что алгоритмы, работающие неизвестно сколько времени
ственно или транзитивно принадлежит этому блоку; (а возможно, вообще никогда не завершающиеся) и потребляющие неиз-
• это узел Nodes[n] в противном случае. вестно какое количество ресурсов, представляют скорее теоретический,
На псевдоязыке это выглядит следующим образом: нежели практический интерес. Поэтому их разработчикам приходится ка-
ким-то образом ограничивать задачу, чтобы получить применимые на пра-
for (int i = 0; i < N; i++) ктике результаты. Для алгоритмов верификации кода известно два подхо-
{ да, позволяющие снизить их сложность и добиться терминируемости:
int[] Flow = новый массив, в который добавляются 1. Концентрация усилий на выявлении только таких ошибок в
номера инструкций, на которые может быть передано программах, поиск которых не требует экспоненциальной
управление от инструкции, соответствующей узлу сложности и выполняется за конечное время.
Nodes[i]; Для этого подхода характерно то, что существуют программы, в
for (int j = 0; j < Flow.Length; j++) которых верификатор не находит ни одной ошибки и которые,
{ тем не менее, разрушают память.
int n = Flow[j]; 2. Работа лишь с некоторым подмножеством программ, для кото-
if (blockNodes[n] != null && blockNodes[n] не является рых факт неразрушения ими памяти можно доказать за конеч-
непосредственно или транзитивно родителем узла Nodes[i]) ное время с использованием алгоритма приемлемой сложности.
Провести дугу от Nodes[i] к blockNodes[n]; Этот тип верификаторов отличается тем, что существуют не раз-
else рушающие память программы, которые не могут быть доказаны
Провести дугу от Nodes[i] к Nodes[n]; алгоритмом.
} Если задача некоторого метавычислительного алгоритма была как-то
} ограничена, то сразу же возникает вопрос о том, какие входные данные
(программы) он сможет обработать. Для суперкомпиляторов и частичных
Страницы
- « первая
- ‹ предыдущая
- …
- 78
- 79
- 80
- 81
- 82
- …
- следующая ›
- последняя »
