Автоматическое тестирование LLVM-программ со сложными входными структурами данных

Символьное исполнение является известным подходом для автоматической генерации регрессионных тестов и поиска ошибок/уязвимостей в программах. Данная работа посвящена созданию практичного метода к символьному исполнению LLVM-программ, пригодного для работы со сложными входными структурами данных. Метод основан на известной идее ленивой инициализации, позволяющей избавить пользователя от необходимости вручную создавать ограничения на входные структуры данных и полностью автоматизировать процесс символьного исполнения программы. Предлагается два улучшения ленивой инициализации для сегментированной символьной моделей памяти – использование временных меток и информации о типах. Предложенный метод реализован в символьной виртуальной машине KLEE для платформы LLVM и протестирован на реальных C-структурах данных — списках, биномиальных кучах, AVL-деревьях, красно-чёрных деревьях, двоичных деревьях и борах (префиксных деревьях).