19 / 22
Заключение.
1. Разработан и подробно описан метод межпро-
цедурного анализа с помощью резюме для модели анализатора, ис-
пользуемой в статическом анализаторе CSA. В результате получена
новая модификация метода межпроцедурного анализа с помощью ре-
зюме для метода символьного выполнения, применимая для анализа
программ в целях выявления различных классов потенциальных де-
фектов.
2. Полученный метод реализован в виде опциональной возможно-
сти статического анализатора CSA. Это позволяет как непосредствен-
но проводить анализ программ, разработанных с использованием язы-
ков C и C++, для поиска дефектов с помощью разработанного метода,
так и сравнивать производительность при применении разработанной
модификации метода резюме с методом встраивания.
3. Для разработанного метода предложен новый метод отображе-
ния результатов анализа в целях получения возможности оценки каче-
ства анализатора, его отладки и доработки, а также в качестве потен-
циального решения для отображения результатов анализа конечному
пользователю, чтобы сократить время, затрачиваемое на поиск и ис-
правление найденных дефектов. Такой метод также реализован для
анализатора CSA.
4. Проведено предварительное сравнение двух методов межпроце-
дурного анализа: метода встраивания, реализованного непосредствен-
но в анализаторе; метода резюме, реализованного и описанного в на-
стоящей работе. Результаты предварительных измерений показывают
увеличение общей скорости анализа в однофайловом режиме прибли-
зительно на 20%: с 1,5 до 1,2 ч для анализа исходных файлов на
языках C и C++ в составе операционной системы Android с использо-
ванием двухпроцессорного сервера Intel Xeon E5-2650 (2,6 ГГц, всего
16 физических и 32 виртуальных ядра).
В дальнейшем планируется провести подробное сравнение произ-
водительности как в однофайловом, так и в межмодульном режиме
при различных опциях анализатора в целях получения достоверных
результатов. Кроме того, поскольку разработанный метод показал хо-
рошую применимость для различных задач, планируется расширить
список проверяющих модулей, поддерживающих использование ре-
зюме.
ЛИТЕРАТУРА
1.
James C. King.
Symbolic execution and program testing // Communications of the
ACM, 1976. Vol. 19. No. 7. P. 385–394.
2.
Ахо А.
,
Лам М.
,
Сети Р.
,
Ульман Д.
Компиляторы: принципы, технологии и
инструментарий. М.: Вильямс, 2008.
3.
Cadar C.
,
Dunbar D.
,
Engler D
. KLEE: Unassisted and automatic generation of
high-coverage tests for complex systems programs // In Proceedings of the USENIX
Symposium on Operating System Design and Implementation. 2008.
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2015. № 5 93