Метод резюме для разработки универсального многоцелевого анализатора кодов программ с возможностью обнаружения различных классов дефектов в программах, созданных с использованием языков С и С++

Приведено подробное описание разработанного метода межпроцедурного анализа с использованием резюме для метода символьного выполнения. Этот метод реализован на модели анализатора Clang Static Analyzer, что позволило использовать метод резюме для разработки универсального многоцелевого анализатора с возможностью поиска различных классов дефектов в программах, разработанных с использованием языков C и C++. Описаны методы сбора и применения резюме для метода символьного выполнения, перевода символьных значений из контекста вызывающей функции в контекст вызываемой и обратно. Разработан и описан метод построения отчета о дефекте с использованием метода резюме для межпроцедурного анализа. Исследование проведено в целях построения анализатора, способного осуществлять межпроцедурный анализ крупных программных комплексов масштаба операционной системы Android за приемлемое время. Приведены данные измерений времени анализа и выполнено сравнение результатов методов резюме и метода встраивания.

Литература

[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.

[4] Cha Sang Kil, Avgerinos Th., Rebert A., Brumley D. Unleashing Mayhem on Binary Code // In Proceedings of the 33rd IEEE Symposium on Security and Privacy. 2012.

[5] Using Symbolic Evaluation to Understand Behavior in Configurable Software Systems / E. Reisner, Ch. Song, Kin-Keung Ma, Jeffrey S. Foster, A. Porter // In Proceedings of the 32nd International Conference on Software Engineering (ICSE). Cape Town, South Africa. 2010. P. 445-454.

[6] Xu Zh., Zhang J., Xu Zh. Melton: a practical and precise memory leak detection tool for C programs // Frontiers of Computer Science in China. 2015. Vol. 9. No. 1. P. 34-54.

[7] Qadeer S., Rajamani S., Rehof J. Summarizing procedures in concurrent programs // 31st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2004. Vol. 39. P. 245-255.

[8] Braberman V., Garbervetsky D., Hym S., Yovine S. Summary-based inference of quantitative bounds of live heap objects // Science of Computer Programming. 2013. Vol. 92. P. 56-84.

[9] Clang Static Analyzer. URL: http://clang-analyzer.llvm.org (дата обращения: 15.04.2015).

[10] Clang: a C language family frontend for LLVM. URL: http://clang.llvm.org (дата обращения: 15.04.2015).

[11] The LLVM compiler infrastructure. URL: http://llvm.org (дата обращения: 14.04.2015).

[12] 12. Игнатьев В.Н. Использование легковесного статического анализа для проверки настраиваемых семантических ограничений языка программирования // Труды Института системного программирования РАН. 2012. Т. 22. С. 169-188.

[13] 13. Масштабируемый инструмент поиска клонов кода на основе семантического анализа программ / С. Саргсян, Ш. Курмангалеев, А. Белеванцев, А. Асланян, А. Балоян // Труды Института системного программирования РАН. 2015. Т. 27. С. 39-50.

[14] 14. Reps T., Horwitz S., Sagiv M. Precise interprocedural dataflow analysis via graph reachability // In POPL ’95 Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 1995. Р. 49-61.

[15] 15. Xu Z., Kremenek T., Zhang J. A memory model for static analysis of C programs // In ISoLA’10 Proceedings of the 4th international conference on Leveraging applications of formal methods, verification, and validation. 2010. Р. 535-548.