Поиск утечек памяти и ресурсов в статическом анализаторе Svace

В статье представлен метод поиска утечек памяти и других схожих ресурсов в статическом анализаторе Svace. Формулируются требования к статическому анализатору, представляющие стоящую за Svace философию, кратко описывается основная инфраструктура анализа на основе межпроцедурного символьного выполнения с объединением состояний и показывается, как ее можно применить для поиска утечек. Описываются атрибуты, которые необходимо вычислить в ходе анализа, демонстрируется, как они вычисляются, как используются спецификации функций выделения и освобождения памяти, а также как учитываются участки памяти, выходящие из-под контроля анализатора. Предлагается способ учета отсутствующих в исходном коде ограничений на выделение и освобождение памяти с помощью создания искусственных функций. Представляются экспериментальные результаты работы метода на наборе тестов Juliet и открытом пакете Binutils, показывающие жизнеспособность предлагаемых идей.

1. J. C. Reynolds, "Separation logic: a logic for shared mutable data structures," Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, Copenhagen, Denmark, 2002, pp. 55-74, doi: 10.1109/LICS.2002.1029817.

2. Peter W. O'Hearn. Incorrectness logic. Proc. ACM Program. Lang. 4, POPL, Article 10 (January 2020), 32 pages. https://doi.org/10.1145/3371078

3. Wen Li, Haipeng Cai, Yulei Sui, and David Manz. PCA: memory leak detection using partial call-path analysis. In Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE 2020). Association for Computing Machinery, New York, NY, USA, 1621–1625. https://doi.org/10.1145/3368089.3417923

4. Yulei Sui and Jingling Xue. SVF: interprocedural static value-flow analysis in LLVM. In Proceedings of the 25th International Conference on Compiler Construction (CC '16). Association for Computing Machinery, New York, NY, USA, 265–266.

5. Yungbum Jung and Kwangkeun Yi. 2008. Practical memory leak detector based on parameterized procedural summaries. In Proceedings of the 7th international symposium on Memory management (ISMM '08). Association for Computing Machinery, New York, NY, USA, 131–140. https://doi.org/10.1145/1375634.1375653 https://doi.org/10.1145/2892208.2892235

6. G. Fan, R. Wu, Q. Shi, X. Xiao, J. Zhou and C. Zhang, "SMOKE: Scalable Path-Sensitive Memory Leak Detection for Millions of Lines of Code," 2019 IEEE/A CM 41st International Conference on Software Engineering (ICSE), Montreal, QC, Canada, 2019, pp. 72-82, doi: 10.1109/ICSE.2019.00025.

7. X. Sun et al., "A Projection-Based Approach for Memory Leak Detection," 2018 IEEE 42nd Annual Computer Software and Applications Conference (COMPSAC), Tokyo, Japan, 2018, pp. 430-435, doi: 10.1109/COMPSAC.2018.10271.

8. A. Belevantsev, A. Borodin, I. Dudina, V. Ignatiev, A. Izbyshev, S. Polyakov, D. Zhurikhin. Design and development of Svace static analyzers. In 2018 Ivannikov Memorial Workshop (IVMEM), Yerevan, Armenia, 2018, pp. 3-9, doi: 10.1109/IVMEM.2018.00008.

9. Бородин А.Е., Белеванцев А.А. Статический анализатор Svace как коллекция анализаторов разных уровней сложности. Труды Института системного программирования РАН. 2015;27(6):111-134.

10. N. Malyshev, A. Borodin and A. Belevantsev, "A Comprehensive Approach to Finding Resource Leaks via Static Analysis," 2024 Ivannikov Ispras Open Conference (ISPRAS), Moscow, Russian Federation, 2024, pp. 1-9, doi: 10.1109/ISPRAS64596.2024.10899157.

11. Benjamin Livshits, Manu Sridharan, Yannis Smaragdakis, Ondřej Lhoták, J. Nelson Amaral, Bor-Yuh Evan Chang, Samuel Z. Guyer, Uday P. Khedker, Anders Møller, and Dimitrios Vardoulakis. In defense of soundiness: a manifesto. Commun. ACM 58, 2 (February 2015), 44–46. https://doi.org/10.1145/2644805

12. Al Bessey, Ken Block, Ben Chelf, Andy Chou, Bryan Fulton, Seth Hallem, Charles Henri-Gros, Asya Kamsky, Scott McPeak, and Dawson Engler. A few billion lines of code later: using static analysis to find bugs in the real world. Commun. ACM 53, 2 (February 2010), 66–75. https://doi.org/10.1145/1646353.1646374

13. H. Aslanyan, Z. Gevorgyan, R. Mkoyan, H. Movsisyan, V. Sahakyan and S. Sargsyan, "Static Analysis Methods For Memory Leak Detection: A Survey," 2022 Ivannikov Memorial Workshop (IVMEM), Moscow, Russian Federation, 2022, pp. 1-6, doi: 10.1109/IVMEM57067.2022.9983955.

14. “Clang Static Analyzer.” [Online]. Available: https://clanganalyzer.llvm.org/

15. Calcagno, C. et al. (2015). Moving Fast with Software Verification. In: Havelund, K., Holzmann, G., Joshi, R. (eds) NASA Formal Methods. NFM 2015. Lecture Notes in Computer Science(), vol 9058. Springer, Cham. https://doi.org/10.1007/978-3-319-17524-9_1

16. C. Scherb, L. B. Heitz, H. Grieder, and O. Mattmann, “Divide, conquer and verify: Improving symbolic execution performance,” arXiv preprint arXiv:2310.03598, 2023.

17. N. Malyshev, I. Dudina, D. Kutz, A. Novikov and S. Vartanov, "SMT Solvers in Application to Static and Dynamic Symbolic Execution: A Case Study," 2019 Ivannikov Ispras Open Conference (ISPRAS), Moscow, Russia, 2019, pp. 9-15, doi: 10.1109/ISPRAS47671.2019.00008.

18. Операционная система Tizen. [Online]. Available: https://docs.tizen.org/platform/get-started/open-source-project/