Введение 3
Глава 1. Теоретические основы трансляции программ в схемы и формулы 5
1.1. Задача выполнимости булевых формул (SAT) 5
1.2. Дискретные функции и способы их задания 5
1.3. Схемы из функциональных элементов как способ задания
дискретных функций 9
1.4. Проверка эквивалентности булевых схем 10
1.5. Проблема определения кодовых клонов 13
1.6. Проблемы символьного исполнения и трансляции в формулы для высокоуровневых языков программирования 15
Глава 2. Трансляция программ для виртуальной машины в And-
Inverter графы 17
2.1. Концепция трансляции программ в And-Inverter графы для
виртуальных машин 17
2.2. Система трансляции байткода виртуальной машины Java . . 17
2.3. Программный комплекс transbyte 18
2.4. Описание работы программного комплекса 19
2.5. Кодирование условных переходов 23
2.6. Условные переходы и циклы в байткоде JVM 25
2.7. Минимизация And-Inverter графов, генерируемых системой
трансляции 28
Глава 3. Эксперименты и результаты 31
3.1. Сумма и умножение 31
3.2. Криптографические функции: LFSR, A5/1 Generator, Wolfram
Generator 32
3.3. Функции сортировки: Bubble, Selection, Insertion, Pancake . . 34
Заключение 37
Приложения 40
Задача проверки эквивалентности программ — это задача по распознаванию частей одной или нескольких программ, задающих одну и ту же функцию. Такими частями являются кодовые клоны — дублированные фрагменты программы, возникающие вследствие копирования и дальнейшего изменения, рефакторинга, и переиспользования исходного кода.
Обнаружение и удаление таких клонов — важная задача в разработке программного обеспечения, так как они могут привести к увеличению сложности кода, ухудшению его качества, а ошибки в одной части программы также могут присутствовать и в другой, эквивалентной ей, и исправление этой ошибки в одном фрагменте кода может потребовать коррекции эквивалентной части.
Самыми сложными для распознавания являются семантические клоны. Под семантическими клонами обычно понимаются сегменты кода, схожие функционально, но реализованные через разные синтаксические конструкции. Можно считать, что в общем случае семантические клоны — это функции, написанные на каких-либо языках программирования (возможно, различных), имеющие одинаковую сигнатуру, и на общих наборах входных данных выдающие одинаковые выходы.
Одним из способов распознавания клонов является кодирование программ в булевы схемы, построение задачи проверки эквивалентности данных схем, и дальнейшее сведение этой задачи к SAT и применение SAT-решателя. Использование схем и SAT-решателя для обнаружения клонов позволяет находить не только прямые клоны, обычно возникающие при несущественном изменении исходного кода, добавлении бесполезных переменных или переименовании существующих, но и семантические клоны, которые не всегда можно распознать при исследовании только исходного кода.
В настоящей работе описывается разработанный программный комплекс transbyte для кодирования части байткода виртуальный машины Java (байткод JVM) в булевы схемы, его архитектура, функциональные возможности, а также приводятся результаты использования различных кодировок для распознавания некоторых семантических клонов с помощью SAT-решателя.
Приведем краткий обзор содержания работы. В главе 1 приводятся теоретические основы техник трансляции программ в булевы формулы, используемых в символьном исполнении и описанных в [15] и [20]. Эти результаты являются базой для последующего материала. В главе 2 приводится концепция трансляции байткода JVM, дается описание архитектуры программного комплекса transbyte, а также рассматривается вопрос минимизации генерируемых кодировок. В главе 3 приводятся результаты использования комплекса transbyte и создаваемых им кодировок для распознавания некоторых функций сортировок как семантических клонов.
В данной работе исследовалась задача проверки эквивалентности программ. Для решения данной задачи применялся подход, использующий трансляцию программ в And-Inverter графы и SAT-решатель. Для трансляции программ, компилирующихся в байткод виртуальной машины Java, был разработан программный комплекс transbyte, доступный на GitHub по адресу https://github.com/eqimd/transbyte. Описана его работа и использование сторонних инструментов для минимизации схем и создания майтеров.
Была рассмотрена трансляция некоторых операций и криптографических функций, а также установлена корректность генерируемых кодировок с помощью референтных кодировок. Также была рассмотрена трансляция некоторых функций сортировок и приведены результаты экспериментов для задачи распознавания данных функций сортировок как семантических клонов.
Результаты работы демонстрируют, что описанный метод может применяться для верификации программ, допускающих относительно компактное представление в виде схем. Такими программами могут быть, например, арифметические функции, при реализации которых на Java высоки шансы ошибки программиста. Для таких функций могут быть созданы специальные библиотеки эталонных реализаций (возможно, на специальном предметноориентированном языке). Впоследствии при некоторой очередной промышленной реализации такой функции можно верифицировать корректность этой реализации за счет проверки ее эквивалентности соответствующему эталону. Именно на этом этапе может использоваться программный комплекс, представленный в настоящей работе: для обеих функций строится их AIG- представление и решается задача проверки эквивалентности соответствующих булевых схем.
