Моделирование поведения функций стандартной библиотеки в задачах анализа программ

Аннотация

Введение: статический анализ программных проектов, использующих внешние библиотеки, сопряжен с экспоненциальным ростом числа анализируемых трасс программы. Это приводит к необходимости искусственно ограничивать время анализа или использовать какие-либо упрощения, в результате чего ухудшаются полнота и точность анализа, снижается тестовое покрытие. Цель: разработать подход к моделированию поведения внешних библиотек на основе формальных спецификаций, аппроксимирующих поведение исходных функций, позволяющий упростить анализируемые проекты и снизить время анализа. Методы: моделирование функций стандартной библиотеки с помощью формальных спецификаций на языке LibSL и последующий автоматический синтез простых эквивалентов библиотечных функций на основе формальных описаний. Результаты: предложен подход к спецификации функций стандартной библиотеки языка Java на языке LibSL, заменяющий наиболее часто используемые библиотеки и их функции на формальные спецификации, повторяющие видимое извне поведение функций. Полученные аппроксимирующие описания транслируются в эффективные для анализа замены функций стандартной библиотеки и подставляются анализатору вместо исходных библиотечных функций. Предложенный подход реализован в виде набора спецификаций части стандартной библиотеки Java и транслирующих утилит. Проведенные эксперименты на части стандартной библиотеки языка Java показали применимость подхода: время анализа промышленных проектов сократилось в среднем на треть. Практическая значимость: разработанный подход позволяет значительно расширить область применения статического анализа в задачах обнаружения дефектов и генерации тестов, так как ввиду сокращения пространства состояний увеличивается точность и полнота обнаружения дефектов и в большинстве случаев обеспечивается более высокое покрытие программы сгенерированными тестами.