7 / 16
Разработка и исследование синтетического метода верификации программы…
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. Приборостроение. 2016. № 4
55
позволяет отказаться от бинарного представления состояний программы;
выполняет построение и верификацию инварианта программы;
осуществляет поиск синтаксических и семантических ошибок (ошибки
компоновки, ошибки выполнения, логические и динамические ошибки);
осуществляет покрытие условий, путей и функций программы;
формирует контрпримеры, тем самым выполняя поиск модели данных, на
которых отдельная функция или программа становятся невыполнимыми.
Лексический транслятор.
Лексический транслятор (рис. 4) представляет
собой средство, объединяющее транс-
ляцию во внутреннее представление
компилятора и программу, которая
осуществляет построение суммы преди-
катов по всем состояниям программы.
LLVMPass позволяет построить бо-
лее упрощенное представление про-
граммы, разбивая сложные условия или
состояния программы на их более про-
стые составляющие, тем самым упрощая построение предикатов состояний си-
стемы и формирование проверяемого инварианта программы.
Построение инварианта по внутреннему представлению программы.
Преобразование внутреннего представления кода в формулы логики перво-
го порядка.
Инвариантом программы является сумма предикатов состояний
программы. Предикат задает множество переходов программы при произволь-
ных значениях переменных. Состояние программы — это мгновенный снимок,
задающий множество значений всех переменных программы и значения счет-
чика команд
.
pc
Состояние программы выражается следующим образом:
4 1
2
3
( , ),
;
1;
4;
2;
s PC V s pc m v
v
v
здесь
PC
множество переменных счетчика команд;
1 2 3
{ ,
, }
V v v v
— множе-
ство переменных программы, придающих значения в
,
i
i
i
D v D
;
n
m
— метка
состояния программы.
Также его можно представить следующим предикатом:
4
1
2
3
(
)
1 (
4) (
2).
pc m v
v
v
Предикатом называется функция из некоторого множества (значений век-
торов программных переменных) во множестве
{ ,
}.
true false
Другими словами, состояние программы — это предикат, истинный на том
конкретном программном состоянии, на котором выполняются заданные соот-
ношения. Предикатом можно задать множество состояний программы:
1 2
3
(
) (
5)
P v v
v
— данный предикат определят множество состоя-
ний, на котором переменные
1 2 3
, ,
v v v
удовлетворяют соотношению
;
P
Рис. 4.
Лексический транслятор