Введение 4
Постановка задачи 5
1. Обзор предметной области 6
1.1. SMT 6
1.2. Теория битовых векторов 6
1.3. Теория линейной целочисленной арифметики 8
1.4. Теория нелинейной целочисленной арифметики 9
2. Существующие решения 10
2.1. Подход к трансляции основных операций 10
2.1.1 Трансляция переменных и арифметических операций . 11
2.1.2 Трансляция битовых операций за исключением bvand . 12
2.1.3 Трансляция операций битового сдвига 13
2.2. Трансляция операции bvand 14
2.2.1 «Eager» подходы к трансляции 14
2.2.2 «Lazy» подходы к трансляции 15
3. Предложенный подход 18
3.1. Доработка подхода к трансляции основных выражений ... 18
3.2. «1-bit overflow» трансляция арифметики 21
3.3. «Lazy overflow» трансляция арифметики 22
3.4. Оптимизации 23
3.4.1 Битовые операции с константой 24
3.4.2 Оптимизация стратегии «1-bit overflow» 24
3.4.3 Сравнения с константой 25
3.4.4 Сохранение информации о битах 26
4. Реализация и оценка разработанных подходов 27
4.1. Подход к тестированию 27
4.2. Тестирование на SMT-COMP 28
4.2.1 SMT-COMP с операцией bvand 29
4.2.2 SMT-COMP без операции bvand 33
4.2.3 SMT-COMP все примеры 36
4.3. Тестирование на USVM-TON 37
4.3.1 USVM-TON без операции bvand 38
4.3.2 USVM-TON с операцией bvand 39
4.3.3 USVM-TON все примеры 41
4.4. Тестирование на USVM-Java 43
4.5. Вывод 44
Заключение 46
Список литературы 47
Верификация и анализ программ являются критически важными областями в сфере разработки программного обеспечения. Для некоторых задач требуется абсолютная уверенность в корректности программ, например, в медицинском оборудовании или в программном обеспечении для критической инфраструктуры, где сбои могут привести к серьезным последствиям, включая потерю жизни. В таких случаях ПО верифицируется на соответствие установленной спецификации. В то же время анализ программ снижает затраты на разработку, выявляя уязвимости и генерируя тесты, что сокращает время работы над проектом.
Значительная часть инструментов для верификации и анализа программ внутри используют SMT-решатели. Несколько примеров:
• SAGE [1]. Инструмент от Microsoft Research, предназначенный для автоматического тестирования программного обеспечения.
• Dafny [2]. Язык программирования от Microsoft Research, проверяющий соответствие кода спецификации, написанной программистом.
• SeaHorn [3]. Фрейморк для анализа LLVM языков.
Для моделирования операций над целыми числами в программах инструменты анализа зачастую используют SMT теорию битвекторов. В работе [5] было показано, что для моделирования программ, использующих числа большой размерности теория битвекторов оказывается неэффективной. Также в некоторых языках, например, в языке Java в большинстве программ используются только арифметические операции над числами, что не требует использования теории битвекторов для моделирования.
В данной работе рассматриваются альтернативные подходы для моделирования операций над целыми числами.
Постановка задачи
Целью данной работы является разработка подходов, улучшающих процедуру проверки выполнимости SMT формул в теории битовых векторов в двух сценариях:
1. Формулы, содержащие битовые вектора большой разрядности
2. Формулы, состоящие из операций линейной арифметики
В данной работе рассматриваются различные подходы проверки выполнимости SMT формул в теории битовых векторов с помощью проверки выполнимости в теории целых чисел.
Всю работу можно разделить на четыре задачи:
1. Изучение существующих подходов к проверке выполнимости SMT формул в теории битвекторов с помощью решателей теории нелинейной целочисленной арифметики.
2. Улучшение существующих и создание новых подходов проверки выполнимости формул в теории битовых векторов с помощью проверки выполнимости в теории целых чисел.
3. Реализация описанных подходов.
4. Оценка разработанных подходов к проверке выполнимости формул в теории битовых векторов с помощью проверки выполнимости в теории целых чисел. Критериями оценки являются: корректность проверки выполнимости, а также затраченное время на проверку выполнимости.
В рамках данной работы были рассмотрены и реализованы подходы проверки выполнимости SMT формул в теории битовых векторов с помощью проверки выполнимости в теории целочисленной арифметики. По результатам работы можно сделать вывод, что
1. В случае отсутствия bvand операций подходы с транслированием формул в теорию целочисленной арифметики позволяют сократить время проверки выполнимости в ситуациях битовых векторов большой размерности или же большого числа линейных арифметических операций. В остальных ситуациях преимущество транслирования неочевидно и зависит от предметной области.
2. В случае наличия bvand операций все рассмотренные подходы с транслированием формул в теорию целочисленной арифметики показывают худшее время по сравнению с использованием решателя теории битовых векторов.
Для получения преимущества от использования рассмотренных подходов в общем случае можно использовать гибридный подход, рассмотренный в разделе 4.5. Также можно использовать портфолио решателей, включающее решатели теории битовых векторов и решатели целочисленной арифметики.
