Введение 4
Постановка задачи 6
1. Обзор предметной области 7
1.1. SMT-решатели 7
1.2. Символьное исполнение 9
1.3. Общее устройство символьной машины 11
1.4. Общие проблемы в символьном исполнении 12
1.5. Существующие символьные машины 15
2. Описание символьной виртуальной машины 17
2.1. Основные решения 17
2.2. Архитектура 18
2.3. Представление выражений 21
2.3.1 Библиотека KSMT 21
2.3.2 Представление примитивных значений 22
2.3.3 Представление ссылочных значений 23
2.3.4 Представление массивов 24
2.3.5 Представление символьных выражений программы ... 24
2.4. Символьное состояние 27
2.5. Символьная память 28
2.5.1 Регистровый стек 31
2.5.2 Хранилище типов 32
2.6. Символьная куча 32
2.6.1 URegionHeap и регионы памяти 34
2.6.2 Дерево регионов 38
2.6.3 Разделение символьных и конкретных адресов 44
2.7. Модель 48
2.7.1 Композиция 49
2.8. Решатель ограничений 53
2.8.1 Транслятор и декодер 53
2.8.2 Решатель типовых ограничений 54
2.9. Интерпретатор 56
2.10. Очередь состояний 57
2.11. Дополнительные детали 58
2.11.1 Список типов для объекта 58
2.11.2 Операции группового копирования 58
2.11.3 Моделирование библиотеки 59
2.11.4 Регионы типов 59
3. Полученные результаты 60
3.1. Практическое применение 60
3.1.1 Тестовый язык программирования 60
3.1.2 Java 61
3.2. Замеры производительности 62
3.2.1 Скорость работы кучи 62
3.2.2 Сравнение с UTBotJava 64
3.3. Дальнейший планы 66
Заключение 67
Благодарность 68
Список литературы 69
Количество инструментов для анализа кода, помогающих в цикле разработки и поддержки программного обеспечения, постоянно растёт. Область их применения действительно широка: поиск ошибок в процессе написания кода; валидация кода на соответствие стилю, принятому в команде; автоматическая генерация регрессионных тестов; автоматическое нахождение ошибок и уязвимостей; автоматическая проверка инвариантов программ; помощь в написании программ с заданными свойствами; поиск деградаций производительности; генерация описаний функции и многое другое.
Одним из наиболее эффективных и точных подходов в анализе программ является так называемое символьное исполнение. Анализаторы, основанные на символьном исполнении, используются в системах непрерывной сборки в крупных компаниях, таких как Microsoft. Например, инструмент SAGE, использующий символьное исполнение, помог найти критическую ошибку в исходном коде операционной системы Windows [1]. Символьное исполнение активно используется для генерации модульных тестов, позволяя существенно повысить качество кода и сэкономить время разработчиков и тестировщиков.
Идея, лежащая в основе символьного исполнения, заключается в исследовании программы путём перебора различных путей исполнении и проверке предикатов, определяющих очередной путь. При этом конкретные входные значения программы заменяются на символьные, таким образом получается исчерпывающее описание условия ошибки, выраженное с помощью предикатов на входные значения.
Одним из преимуществ символьного исполнения по сравнению с другими техниками является теоретическая доказуемость. Иначе говоря, с помощью символьного исполнения можно проверять некоторые свойства анализируемой программы. К основным недостаткам символьного исполнения можно отнести высокую вычислительную сложность, связанную с необходимостью исследования большого количества состояний программы. К тому же задача проверки выполнимости формулы в теории SMT, на которой основан любой алгоритм символьного исполнения, является NP-трудной, и её решение может занимать длительное время...
В результате данной работы были успешно выполнены следующие задачи:
• Был проведён анализ существующих машин и наиболее часто встречающихся подходов в символьном исполнении.
• Реализовано ядро универсальной символьной виртуальной машины.
• С использованием данного ядра был разработан анализатор для искусственного языка программирования, а также для языка, компилирующегося в байт-код JVM.
• Были проведены замеры производительности на синтетических данных, а также проведено сравнение полученных результатов с машиной символьного исполнения UTBotJava.
Таким образом, была подтверждена возможность использования универсального символьного ядра для написания анализов для разных языков. Полученное ядро ^SVM может существенно сократить время, потраченное на разработку символьного анализатора для произвольного языка с автоматическим управлением памятью. Отдельно стоит отметить, что часть полученных решений до этого не применялась ни в одной известной автору символьной машине и представляет собой перспективный задел для дальнейших исследований.
Всю реализацию универсальной символьной виртуальной машины и анализатора для языка Java можно найти по ссылке: https://github.com/UnitTestBot/usvm.
