12 / 16
И.В. Рудаков, Р.Е. Гурин
60
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. Приборостроение. 2016. № 4
Инструмент PAGAI для преобразования программы на языке Си в
SMT-формулу также использует возможности LLVM, но в отличие от LLBMC
преобразование осуществляет в байт-код, затем осуществляется апробирование
программы в виде байт-кода в программу на языке SMT–LIB.
В отличие от инструмента LLBMC, который обладает встроенными провер-
ками кода, PAGAI имеет значительно меньшие функциональные возможности.
Все проверки осуществляются с помощью пользовательских инструкций assert
и assume. Пользователь добавляет в исходный код программы инструкции вида
assert
(
x
> 10) для проверки интересующего его свойства, далее в автоматиче-
ском режиме происходит проверка заданного пользователем свойства. В ре-
зультате пользователь получает информацию о выполнимости свойства, в слу-
чае успешного выполнения
/*assertproved*/
или
/*assertnotproved*/
, в случае, если
свойство не удается доказать.
Приведенные инструменты осуществляют исключительно статический
анализ кода, в свою очередь, с помощью приведенного метода можно выпол-
нить динамический анализ кода, проверку моделей с помощью SMT-решателей,
а также осуществить анализ графа потока управления программы.
Предложенный метод построения контрпримеров можно применить не
только к самим инструкциям программного кода, но и к состояниям програм-
мы, тем самым можно осуществить проверку выполнимости и достижимости
состояний программы. Под состоянием программы следует понимать блок, ко-
торый объединяет несколько программных инструкций.
Существует большое число методов динамического анализа [14]. Одним из
методов является проверка поведения программы в зависимости от данных,
которые подаются на ее вход.
С помощью предложенного алгоритма можно накладывать проверки и огра-
ничения на генерируемый поток данных для проверки поведения программы.
Предложенный и существующие алгоритмы покрывают все классы опера-
торов языка Си.
В табл. 4. приведено сравнение синтетического метода с существующими
алгоритмами. Главным преимуществом предлагаемого метода перед существу-
ющими является возможность осуществлять не только статический анализ, но
и динамический, а также проверку моделей. Это позволяет значительно повы-
сить точность по сравнению с ныне существующими методами.
Таблица 4
Сравнение существующих методов
Заданные свойства ПО
Алгоритмы
Синтетический
метод
LLBMC
PAGAI
Использование LLVMIR
+
–
+
SMT-решатель
Boolector или STP
Microsoft Z3
Solver
Microsoft Z3 Solver
Автоматизация
+
+/–
+