Введение 4
1. Постановка задачи 6
2. Обзор 7
2.1. Символьное исполнение 7
2.2. Система типов 8
2.3. Существующие подходы 9
3. Архитектура подсистемы интерпретации типов 10
4. Композициональное символьное исполнение с типами 12
4.1. Частично определенные типы 12
4.2. Подстановка типов 13
5. Формализация системы типов .NET 15
6. Алгоритм решения систем ограничений на типы 19
7. Тестирование 30
Заключение 31
Список литературы 32
В области верификации есть методы, которые используют технику символьного исполнения [2, 12, 13] для сведения кода к языку логики первого порядка и решатели дизъюнктов Хорна [8, 9, 14] для их разрешения. Одна из главных задач, решаемых символьным интерпретатором — исследование веток выполнения кода на неопределенных входных данных.
Во время символьного исполнения .NET-кода появляется проблема, порождаемая неопределенностью данных, а именно неопределенность динамических типов объектов. Один из самых простых примеров, демонстрирующих эту проблему — функция Object.Equals(Object). Вне контекста конкретного вызова невозможно понять, какой именно объект будет передан в качестве параметра этого метода, в частности, неизвестно какой у объекта будет тип. Ситуация осложняется наличием обобщений (generics) с ограничениями на типовые параметры, а также вариантностью для обобщенных интерфейсов. Не стоит забывать и о сложности системы типов .NET. В частности, решение должно естественным образом масштабироваться на массивы символьных размерностей, делегаты, unsafe-указатели и т. д.
Одна из главных проблем, от которой страдают символьные интерпретаторы — проблема взрыва путей исполнения: количество путей исполнения программы в общем случае зависит экспоненциально от ее размера[1]. Один из подходов, направленных на решение этой проблемы — это композиционное символьное исполнение [6], которое позволяет переиспользовать уже проинтерпретированные участки кода во время символьного исполнения. В случае с динамическими типами объектов композиционность заключается в возможности получить корректный результат интерпретации кода, при условии того, что типы объектов могут быть конкретизированы, без повторного исполнения.
V# — это проект, направленный на создание неограничиваемого верификатора для платформы .NET. Помимо огромной важности для самого проекта V#, эта задача может представлять интерес для академического сообщества. К примеру, существует довольно большое количество работ, посвященных статическому анализу языка Java (одна из последних обзорных статей на эту тему является [16]). Существуют и работы на тему символьного исполнения в условиях неопределенности типа объектов, например, [10]. Стоит отметить также, что в наиболее известных state-of-art-интерпретаторах (таких как Java PathFinder [7] и Pex [21]), символьное исполнение кода со сложными типами поддержано в весьма ограниченном виде. В частности, не один из этих инструментов не поддерживает исполнение кода с открытыми типами в полном объёме, хотя возможность получить корректный результат символьной интерпретации кода с открытыми типами в сочетании с композициональностью позволяет сильно повысить эффективность исполнения.
В данной работе были выполнены следующие задачи.
• Спроектирована архитектура подсистемы, отвечающей за интерпретацию типов.
• Реализовано символьное исполнение функций с учетом открытых типов и полиморфизма. Неопределенность динамических типов выражена в символьных типах, на которые накладываются ограничения в виде символьных булевых термов. Поддержка исполнения кода с неопределенными типами реализована с учетом композициональности исполнения.
• Предложен и реализован алгоритм, который решает ситемы ограничений на открытые .NET типы. В частности, разработан и реализован алгоритм, который сводит задачу определения выполнимости набора ограничений на открытые типы платформы .NET к разрешимому фрагменту логики первого порядка.
• Подана статья на конференцию SEIM 2018, c последующей публикацией в CEUR (индексируется в базе данных SCOPUS).
• Проведено тестирование функциональности реализованной подсистемы.
