Задание 2. Анализ потоков данных
Виды анализа
В этом задании вам предлагается реализовать следующие виды анализа потоков данных:
Как нетрудно заметить, на базе полученного вами решения путем замены абстрактного домена можно потенциально реализовать и другие виды анализа, но мы для примера ограничимся только упомянутыми выше.
Общая схема алгоритма
-
Построить граф потока управления программы.
-
Составить систему уравнений относительно абстрактных состояний вершин графа, определяемую передаточными функциями.
-
Найти решение с использованием алгоритма поиска неподвижной точки.
Примеры использования
1. Распространение целочисленных констант
mulua dataflow-analysis --type=integer-constant-propagation const.luab = true
m = nil
n = input()
c = 1
if n > 0 then
c = 3 - 2
end[c → 1, n → Integer, _ → never]Здесь _ обозначает «все остальное». Обратите внимание, что в выводе опущены связки b → never и m → never.
mulua dataflow-analysis --type=integer-constant-propagation division-by-zero.luan = input()
c = 1 - 1
x = n // c[c → 0, n → Integer, _ → never]Обратите внимание, что в выводе опущена связка x → never.
2. Распространение констант с выводом примитивных типов
mulua dataflow-analysis --type=typed-constant-propagation alternative.luam = nil
x = input()
if x >= 0 then
n = x > 0
end
if x >= 42 then
n = 42
end[n → nil | Boolean | 42, x → Integer, _ → nil]Обратите внимание, что в выводе опущена связка m → nil.
mulua dataflow-analysis --type=typed-constant-propagation bool-from-int.luaa = 2 + 2
b = a > 0[a → 4, b → true, _ → nil]Формат выходных данных
-
Выводится окружение, описывающее абстрактное состояние программы на момент завершения ее выполнения.
-
Переменные {xᵢ} в окружении
[x₁ → σ(x₁), …, xₙ → σ(xₙ), _ → default]перечисляются в лексикографическом порядке. -
Для анализа распространения целочисленных констант не выводятся связки вида
xᵢ → never, поскольку значениеnil(которым обладают все переменные по умолчанию) соответствует абстрактному значениюnever(⊥) в доменеInteger. -
Для анализа распространения констант с выводом примитивных типов не выводятся связки вида
xᵢ → nil, поскольку значениеnilсоответствует абстрактному значениюnilв доменеValue.
Библиотеки
В заготовке задания по разработке интерпретатора были описаны следующие библиотеки:
-
mulua.syntax— абстрактный синтаксис. -
mulua.parser— парсер. -
mulua.semantics— семантика языка и его интерпретатор.
В процессе решения этого задания у вас должны возникнуть как минимум следующие библиотеки:
-
mulua.lattice— решетки. -
mulua.domain— абстрактные домены. -
mulua.flowgraph— построение графа потока управления (control flow graph) по абстрактному синтаксису. -
mulua.dataflow— анализатор потоков данных.
Создайте эти библиотеки по аналогии с другими библиотеками. Для этого необходимо создать соответствующие директории в lib/ и написать в каждой конфигурационный файл dune.
Решетки
Можно посмотреть примеры решеток, которые мы написали на одном из занятий. Однако, для наших целей будет достаточно сигнатуры полной решетки.
CompleteLattice
Сигнатура полной решетки:
module type S = {
[@deriving equal]
type t;
let meet: (t, t) => t;
let join: (t, t) => t;
let top: t;
let bottom: t;
};Constant
Для распространения констант нам потребуется плоская решетка:
open Base;
module Make = (Value: Equal.S): {
type t =
| Any
| Some(Value.t)
| None;
include CompleteLattice.S with type t := t;
let of_option: option(Value.t) => t;
/* ... */
} => {
/* ... */
};Map
Для представления абстрактного состояния программы нам потребуется функциональная решетка Key → Value, где Key — множество, а Value — полная решетка:
open Base;
module Make = (Key: Comparable.S, Value: CompleteLattice.S): {
include (module type of TotalMap.Make(Key, Value));
include CompleteLattice.S with type t := t;
} => {
include TotalMap.Make(Key, Value);
/* ... */
};Использовать ее для анализа программ мы будем для представления абстрактного состояния (окружения) программы. В качестве множества Key мы будем использовать множество идентификаторов переменных Identifier. Решетка Value будет моделировать абстрактные значения этих переменных.
Домены
Домен (в т.ч. абстрактный) определяется решеткой значений и семантикой операций.
open MuLua_lattice;
module type S = {
include CompleteLattice.S;
let of_value: MuLua_semantics.Value.t => t;
let to_string: t => string;
let (+): (t, t) => t;
/* ... */
};Nil
Тип Nil имеет единственное значение — nil.
open MuLua_lattice;
include (module type of Constant.Make(Base.Nothing));
include Domain.S with type t := t;Поскольку тип Base.Nothing.t является ненаселенным, конструктором Some воспользоваться нельзя.
Boolean
Тип Boolean имеет два возможных значения — false и true.
open MuLua_lattice;
include (module type of Constant.Make(Base.Bool));
include Domain.S with type t := t;Integer
Тип Integer имеет целочисленные значения в некотором допустимом диапазоне.
open MuLua_lattice;
include (module type of Constant.Make(Base.Int));
include Domain.S with type t := t;Value
В языке μLua существуют значения только следующих типов времени выполнения: Nil, Boolean и Integer. Все эти типы являются примитивными.
Нас интересует статический анализ, который позволит для каждой переменной узнать, каким примитивным типам может принадлежать ее значение. Более того, если переменная может принадлежать некоторому типу, то в таком случае также интересно, является ли эта переменная константой этого типа.
Произведение доменов, соответствующих примитивным типам, дает нам домен, который используется в решении данной задачи:
type t = {
nil: Nil.t,
boolean: Boolean.t,
integer: Integer.t,
};
include Domain.S with type t := t;Иными словами, данный анализ можно рассматривать как композицию результатов нескольких независимых анализов распространения констант для каждого примитивного типа.
Реализация модуля Value пишется тривиальным образом.
Примеры строковых представлений абстрактных значений
Данные примеры должны помочь понять, как следует написать функцию Value.to_string.
| Абстрактное значение | Строковое представление |
|---|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Таким образом, never и any являются исключениями из общего правила формирования строковых представлений.
Построение графа потока управления
Для построения графа потока управления вы можете использовать модуль Graph библиотеки ocamlgraph. Можно также писать самостоятельно или с использованием других библиотек.
|
Анализатор потоков данных
Environment
В коде анализатора окружение будет представлено с использованием функциональной решетки Map:
open Base;
open MuLua_syntax;
open MuLua_semantics;
open MuLua_lattice;
open MuLua_domain;
module Make = (Domain: Domain.S): {
include (module type of Map.Make(Identifier, Domain));
let empty: t;
let to_string: t => string;
} => {
include Map.Make(Identifier, Domain);
let empty = Value.Nil |> Domain.of_value |> const;
/* ... */
};Поиск неподвижной точки
Вы можете использовать готовый алгоритм рабочего списка для поиска неподвижной точки из модуля Graph.Fixpoint. Пример использования (если непонятен синтаксис, пропустите через refmt). Можно также писать самостоятельно или с использованием других библиотек. Можно использовать любой алгоритм поиска неподвижной точки, в том числе наивный.
|
Тестовые примеры
-
Подготовьте тесты, аналогично тому, как вы это делали в предыдущем задании.
-
Тесты должны использовать не менее 20 различных примеров программ.
-
Убедитесь на этих примерах, что реализованные виды анализа выдают ожидаемый результат.