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

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

Петров О.М. (ИСП РАН, Москва, Россия)

Аннотация

В рамках инструмента статической верификации программ CPAchecker рассматриваются анализ на основе символьных графов памяти (SMG) и метод мемоизации абстракций блоков (BAM), позволяющий использовать резюме процедур. SMG анализ моделирует память программы в виде графа с рёбрами между объектами в памяти и символьными значениями. С помощью этого анализа были найдены ошибки работы с памятью в драйверах операционной системы Linux. BAM позволяет, используя произвольный статический анализ, получить резюме блока (тела функции или цикла) и использовать это резюме снова, когда анализ входит в тот же блок с достаточно схожим контекстом. В этой статье представлен ряд вариантов операторов BAM, необходимых для работы этого метода с анализом SMG. Варианты различаются по точности захватываемого контекста. Использование BAM позволило анализу получить более 50 вердиктов, но привело к потере 25 вердиктов на 845 модулях драйверов.

Ключевые слова

статическая верификация программ; CPAchecker; символьные графы памяти; абстракция блоков; резюме процедур.

Издание

Труды Института системного программирования РАН, том 38, вып. 5, 2026, стр. 337-350.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2026-38(5)-19

Для цитирования

Петров О.М. Мемоизация абстракций блоков для символьных графов памяти. Труды Института системного программирования РАН, том 38, вып. 5, 2026, стр. 337-350. DOI: 10.15514/ISPRAS-2026-38(5)-19.

Полный текст статьи в формате pdf (на английском) Вернуться к содержанию тома