Kex: платформа для анализа JVM-программ
Ключевые слова:
анализ программ, платформа для анализа программ, автоматическая генерация тестов, символьное исполнениеАннотация
Введение: методы статического и динамического анализа программ все чаще используются для проверки качества программного обеспечения. Однако разные виды анализа программ требуют работы с разными моделями представления программ, методами анализа и т. д. Возросла важность платформ для создания инструментов анализа программ, так как они позволяют упростить и ускорить процесс разработки. Цель: разработать платформу для анализа JVM-программ. Результаты: разработана платформа Kex для построения инструментов анализа программ, компилирующихся в JVM-байткод. Kex предоставляет три уровня абстракции. Первый уровень — библиотека Kfg — реализует граф потока управления в форме статического однократного присваивания для анализа и трансформации JVM-байткода. Второй уровень — символьное представление программы, называемое Predicate State, которое состоит из предикатов логики первого порядка, соответствующих инструкциям программы, контрактам, дополнительным ограничениям и т. д. Третий уровень — интерфейс для создания и работы с SMT-формулами, позволяющий решать задачи выполнимости. Интерфейс в данный момент поддерживает взаимодействие с тремя SMT-решателями. Практическая значимость: платформа Kex использовалась при разработке двух инструментов: автоматической генерации тестов для языка Java, который был подан на соревнования SBST 2021, и автоматического поиска ошибок интеграции библиотек. Оба этих прототипа показали, что платформа Kex может быть использована для разработки инструментов автоматического анализа программ.
