📄Работа №126722
Тема: Проектирование и разработка универсальной символьной виртуальной машины
Тип работы
Бакалаврская работа
Предмет
программирование
Объем:
72 листов
Год:
2023
Просмотров:
128
4650
руб.
🛒 Купить работу
Не подходит эта работа?
Закажите новую по вашим требованиям
Узнать цену на написание
Закажите новую по вашим требованиям
Представленный материал является образцом учебного исследования, примером структуры и содержания учебного исследования по заявленной теме. Размещён исключительно в информационных и ознакомительных целях.
Workspay.ru оказывает информационные услуги по сбору, обработке и структурированию материалов в соответствии с требованиями заказчика.
Размещение материала не означает публикацию произведения впервые и не предполагает передачу исключительных авторских прав третьим лицам.
Материал не предназначен для дословной сдачи в образовательные организации и требует самостоятельной переработки с соблюдением законодательства Российской Федерации об авторском праве и принципов академической добросовестности.
Авторские права на исходные материалы принадлежат их законным правообладателям. В случае возникновения вопросов, связанных с размещённым материалом, просим направить обращение через форму обратной связи.
Настоящий учебно-методический информационный материал размещён в ознакомительных и исследовательских целях и представляет собой пример учебного исследования. Не является готовым научным трудом и требует самостоятельной переработки.
📋 Содержание
Введение 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
Постановка задачи 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]. Символьное исполнение активно используется для генерации модульных тестов, позволяя существенно повысить качество кода и сэкономить время разработчиков и тестировщиков.
Идея, лежащая в основе символьного исполнения, заключается в исследовании программы путём перебора различных путей исполнении и проверке предикатов, определяющих очередной путь. При этом конкретные входные значения программы заменяются на символьные, таким образом получается исчерпывающее описание условия ошибки, выраженное с помощью предикатов на входные значения.
Одним из преимуществ символьного исполнения по сравнению с другими техниками является теоретическая доказуемость. Иначе говоря, с помощью символьного исполнения можно проверять некоторые свойства анализируемой программы. К основным недостаткам символьного исполнения можно отнести высокую вычислительную сложность, связанную с необходимостью исследования большого количества состояний программы. К тому же задача проверки выполнимости формулы в теории SMT1, на которой основан любой алгоритм символьного исполнения, является NP-трудной2, и её решение может занимать длительное время.
Впервые идея символьного исполнения была представлена в статье 1976 года [2], однако наиболее активно развиваться и применяться символьные машины начали только в конце XX-начале XXI века. Например, для языков, компилирующихся в LLVM [3], появилась символьная машина KLEE [4], широко распространённая в индустрии и объединяющая большое количество исследователей из академической среды. С другой стороны, для многих языков всё ещё не существует решения, удовлетворяющего ограничениям по точности и прежде всего масштабируемости.
Дополнительно стоит отметить, что многие символьные машины реализуют похожие сущности, имеют общую архитектуру и решают одинаковые проблемы, независимо от анализируемого языка. Таким образом, возникает потребность в эффективной реализации ядра символьной машины, подходящего для различных целей. Идея данной работы заключается в выделении, проектировании и реализации некоторого набора компонентов, позволяющего реализовать эффективный символьную машину для любого целевого языка с автоматическим управлением памятью, такого как Java, Go, Python и т.д. Данное ограничение является довольно существенным, однако оно позволяет существенно оптимизировать представление памяти будущего ядра, к тому же согласно индексам популярности языков программирования TIOBE [5] и PYPL [6], языки с автоматическим управлением памятью составляют большую часть на рынке.
Постановка задачи
Целью данной работы является создание ядра универсальной символьной виртуальной машины, подходящей для анализа языков программирования с автоматическим управлением памятью.
Для достижения поставленной цели были выделены следующие задачи:
• Анализ существующих символьных машин и различных техник в символьном исполнении.
• Проектирование и разработка основных компонентов универсальной символьной виртуальной машины, подходящей для анализа языков с автоматическим управлением памятью.
• Реализация с использованием полученной машины анализатора для языков, компилирующихся в JVM байт-код, поддерживающего основной набор инструкций.
• Замеры производительности полученного анализатора и сравнение с одним из существующих анализаторов для языка Java.
Одним из наиболее эффективных и точных подходов в анализе программ является так называемое символьное исполнение. Анализаторы, основанные на символьном исполнении, используются в системах непрерывной сборки в крупных компаниях, таких как Microsoft. Например, инструмент SAGE, использующий символьное исполнение, помог найти критическую ошибку в исходном коде операционной системы Windows [1]. Символьное исполнение активно используется для генерации модульных тестов, позволяя существенно повысить качество кода и сэкономить время разработчиков и тестировщиков.
Идея, лежащая в основе символьного исполнения, заключается в исследовании программы путём перебора различных путей исполнении и проверке предикатов, определяющих очередной путь. При этом конкретные входные значения программы заменяются на символьные, таким образом получается исчерпывающее описание условия ошибки, выраженное с помощью предикатов на входные значения.
Одним из преимуществ символьного исполнения по сравнению с другими техниками является теоретическая доказуемость. Иначе говоря, с помощью символьного исполнения можно проверять некоторые свойства анализируемой программы. К основным недостаткам символьного исполнения можно отнести высокую вычислительную сложность, связанную с необходимостью исследования большого количества состояний программы. К тому же задача проверки выполнимости формулы в теории SMT1, на которой основан любой алгоритм символьного исполнения, является NP-трудной2, и её решение может занимать длительное время.
Впервые идея символьного исполнения была представлена в статье 1976 года [2], однако наиболее активно развиваться и применяться символьные машины начали только в конце XX-начале XXI века. Например, для языков, компилирующихся в LLVM [3], появилась символьная машина KLEE [4], широко распространённая в индустрии и объединяющая большое количество исследователей из академической среды. С другой стороны, для многих языков всё ещё не существует решения, удовлетворяющего ограничениям по точности и прежде всего масштабируемости.
Дополнительно стоит отметить, что многие символьные машины реализуют похожие сущности, имеют общую архитектуру и решают одинаковые проблемы, независимо от анализируемого языка. Таким образом, возникает потребность в эффективной реализации ядра символьной машины, подходящего для различных целей. Идея данной работы заключается в выделении, проектировании и реализации некоторого набора компонентов, позволяющего реализовать эффективный символьную машину для любого целевого языка с автоматическим управлением памятью, такого как Java, Go, Python и т.д. Данное ограничение является довольно существенным, однако оно позволяет существенно оптимизировать представление памяти будущего ядра, к тому же согласно индексам популярности языков программирования TIOBE [5] и PYPL [6], языки с автоматическим управлением памятью составляют большую часть на рынке.
Постановка задачи
Целью данной работы является создание ядра универсальной символьной виртуальной машины, подходящей для анализа языков программирования с автоматическим управлением памятью.
Для достижения поставленной цели были выделены следующие задачи:
• Анализ существующих символьных машин и различных техник в символьном исполнении.
• Проектирование и разработка основных компонентов универсальной символьной виртуальной машины, подходящей для анализа языков с автоматическим управлением памятью.
• Реализация с использованием полученной машины анализатора для языков, компилирующихся в JVM байт-код, поддерживающего основной набор инструкций.
• Замеры производительности полученного анализатора и сравнение с одним из существующих анализаторов для языка Java.
✅ Заключение
В результате данной работы были успешно выполнены следующие задачи:
• Был проведён анализ существующих машин и наиболее часто встречающихся подходов в символьном исполнении.
• Реализовано ядро универсальной символьной виртуальной машины.
• С использованием данного ядра был разработан анализатор для искусственного языка программирования, а также для языка, компилирующегося в байт-код JVM.
• Были проведены замеры производительности на синтетических данных, а также проведено сравнение полученных результатов с машиной символьного исполнения UTBotJava.
Таким образом, была подтверждена возможность использования универсального символьного ядра для написания анализов для разных языков. Полученное ядро ^SVM может существенно сократить время, потраченное на разработку символьного анализатора для произвольного языка с автоматическим управлением памятью. Отдельно стоит отметить, что часть полученных решений до этого не применялась ни в одной известной автору символьной машине и представляет собой перспективный задел для дальнейших исследований.
Всю реализацию универсальной символьной виртуальной машины и анализатора для языка Java можно найти по ссылке: https://github.com/UnitTestBot/usvm.
• Был проведён анализ существующих машин и наиболее часто встречающихся подходов в символьном исполнении.
• Реализовано ядро универсальной символьной виртуальной машины.
• С использованием данного ядра был разработан анализатор для искусственного языка программирования, а также для языка, компилирующегося в байт-код JVM.
• Были проведены замеры производительности на синтетических данных, а также проведено сравнение полученных результатов с машиной символьного исполнения UTBotJava.
Таким образом, была подтверждена возможность использования универсального символьного ядра для написания анализов для разных языков. Полученное ядро ^SVM может существенно сократить время, потраченное на разработку символьного анализатора для произвольного языка с автоматическим управлением памятью. Отдельно стоит отметить, что часть полученных решений до этого не применялась ни в одной известной автору символьной машине и представляет собой перспективный задел для дальнейших исследований.
Всю реализацию универсальной символьной виртуальной машины и анализатора для языка Java можно найти по ссылке: https://github.com/UnitTestBot/usvm.
ИЛИ
Поиск аналога
📕 Список литературы
🖼 Скриншоты
🛒 Оформить заказ
⚡ Работу высылаем в течении 5 минут после оплаты.