Свойства состояний

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

Выделяют две группы задач о нахождении свойств состояний: прямые и обратные. Свойство состояний в некоторый момент выполнения схемы в прямой задаче зависит только от свойств состояний в моменты выполнения, предшествующие данному, а в обратной — только от свойств состояний в моменты выполнения, следующие за данным. Метод решения таких задач, получивший название метод разметки, связан с их формулированием в виде уравнений, описывающих изменения свойств состояний на каждом из путей по схеме. Решение задачи анализа свойств состояний имеет вид разметки, которая сопоставляет некоторое значение с каждой вершиной уграфа; этим значением может быть множество фактов, отношение или множество утверждений, которое является пересечением соответствующих множеств, получаемых при движении по направлению дуг по всем путям до данной вершины от начальной вершины в случае прямой задачи (соответственно против направления дуг от конечной вершины до данной в случае обратной задачи). Особенно эффективно применение этого метода в случае, когда свойства состояний, различаемые в формулировке задачи, образуют конечное множество, что позволяет эффективно реализовать пометки, описывающие свойство состояний в разных точках программы, в виде шкал, и находить точное решение. Когда точное решение не может быть вычислено, обычно методы анализа свойств состояний работают с некоторой полурешеткой свойств состояний (с заданным на свойствах отношением аппроксимации) и нацелены на поиск наилучшего приближенного решения (наилучшей аппроксимации).

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

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

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

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

Использование пересечения в задачах анализа свойств состояний в некотором смысле не по существу и в силу двойственности все рассуждения могли бы быть произведены в терминах полурешеток объединения. В полурешетке объединения вместо терминов "пересечение по всем путям", "максимальная неподвижная точка", "наибольшее решение" должны использоваться термины "объединение по всем путям", "минимальная неподвижная точка", "наименьшее решение" соответственно.

Иногда схемы свойств состояний классифицируются в пространстве векторов, образующих множество (пересечение/объединение) X (прямая/обратная) X (максимальное решение/минимальное решение). Существуют алгоритмы, которые используют различные комбинации векторов на различных фазах своего выполнения.

Литература

• Касьянов В.Н., Евстигнеев В.А. Графы в программировании: обработка, визуализация и применение. — СПб.: БХВ-Петербург, 2003.

• Касьянов В.Н. Оптимизирующие преобразования программ. — М.: Наука, 1988.