Background Image
Previous Page  2 / 22 Next Page
Information
Show Menu
Previous Page 2 / 22 Next Page
Page Background

analysis of large software projects, such as Android, in reasonable time. The results

of measuring the analysis time are given. The summary-based and inlining methods

are compared.

Keywords

:

summary-based method, interprocedural analysis, symbolic execution,

Clang Static Analyzer, search for defects, report building, C/C++.

Введение.

Метод символьного выполнения, впервые описанный в

1976 г. Дж. Кингом [1], по-прежнему активно используется в различ-

ных инструментах анализа кода. Суть метода символьного выполне-

ния заключается в разбиении множества входных данных на классы

эквивалентности, что позволяет оперировать при анализе не отдель-

ными входными значениями (их число может быть очень большим

и экспоненциально возрастает в зависимости от числа входных аргу-

ментов) и их перебором, а целыми классами эквивалентности, число

которых также может оказаться большим, но не превышает общее чи-

сло комбинаций отдельных входных значений. Однако, как правило,

число классов эквивалентности комбинаций входных данных оказы-

вается значительно ниже числа всех возможных комбинаций входных

данных, что резко увеличивает возможности анализатора по обработке

путей выполнения.

Основное преимущество метода символьного выполнения — про-

стота и очевидность концепции, на которой он основан: метод ис-

пользует идею “симуляции” выполнения программы так, как это де-

лает программист. Метод символьного выполнения получил распро-

странение не только в инструментах статического, но и смешанного

анализа: хорошо зарекомендовали себя инструменты, использующие

подход concolic testing (символьно-конкретное — concrete+symbolic).

При использовании этого подхода на основе символьного выполнения

генерируются тестовые данные, при применении которых программа

проявляет некорректное поведение.

Наряду с преимуществами, метод имеет ряд недостатков. Так, су-

ществует проблема экспоненциального роста числа проходимых путей

(path explosion), приводящая к проблемам с масштабируемостью ме-

тода [2]. Возникают также проблемы при моделировании циклов, по-

скольку зачастую число итераций цикла точно неизвестно — оно также

является символьной величиной. Тем не менее метод символьного вы-

полнения активно используется, в том числе, многими популярными

инструментами анализа программ. Таким образом, разработка подхо-

дов для улучшения указанного метода — актуальная и практически

важная задача.

Одна из основных проблем с масштабируемостью метода —

трудности, возникающие при реализации межпроцедурного анализа.

В случае выполнения контекстно-чувствительного межпроцедурно-

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

разрастается. Это резко замедляет анализ и увеличивает потребление

76 ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2015. № 5