Detecting Memory and Resource Leaks in the Svace Static Analyzer
Nikita Evgenyevich MALYSHEV,
Alexey Evgenevich BORODIN,
Andrey Andreevich BELEVANTSEV,
Vitaly Adolfovich SEMENOV https://doi.org/10.15514/ISPRAS-2025-37(3)-20
Abstract
The paper presents an approach to detecting memory and other resource leaks in the Svace static analyzer. We lay down a set of static analysis requirements that show the philosophy behind Svace, briefly describe the main analysis infrastructure based on an interprocedural symbolic execution with state merging, and show how this infrastructure can be applied to leak detection. We list attributes that are computed during analysis and present how this computation is performed, how allocation and release functions are modeled via specifications, how escaped memory is accounted for. We propose a way to provide external information not present in the source code to the analyzer via creating artificial functions. Experimental results on the Juliet test suite and the Binutils package show the viability of our ideas.
About the Authors
Nikita Evgenyevich MALYSHEV
Ivannikov Institute for System Programming of the Russian Academy of Sciences,
Lomonosov Moscow State University
Russian Federation
Russian Federation
Researcher at ISP RAS, assistant at Chair for System Programming of Department of Computational Mathematics and Cybernetics at MSU. Research interests: static analysis, SMT solvers, program optimization.
Alexey Evgenevich BORODIN
Ivannikov Institute for System Programming of the Russian Academy of Sciences
Russian Federation
Russian Federation
Cand. Sci. (Phys.-Math.), researcher. Research interests: static analysis for finding errors in source code.
Andrey Andreevich BELEVANTSEV
Ivannikov Institute for System Programming of the Russian Academy of Sciences,
Lomonosov Moscow State University
Russian Federation
Russian Federation
Dr. Sci. (Phys.-Math.), Prof., leading researcher at ISP RAS, Professor at MSU. Research interests: static analysis, program optimization, parallel programming.
Vitaly Adolfovich SEMENOV
Ivannikov Institute for System Programming of the Russian Academy of Sciences, Moscow Institute of Physics and Technology (National Research University)
Russian Federation
Russian Federation
Dr. Sci. (Phys.-Math.), Prof., Head of the Department of System Integration and Multi-disciplinary Applied Systems of the ISP RAS since 2015. Research interests: model-driven methodologies and CASE toolkits for creating digital platforms and advanced applied systems, visualization and computer graphics, building information modeling, project management and scheduling.
References
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/
Review
For citations:
MALYSHEV N.E., BORODIN A.E., BELEVANTSEV A.A., SEMENOV V.A. Detecting Memory and Resource Leaks in the Svace Static Analyzer. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2025;37(3):291-302. (In Russ.) https://doi.org/10.15514/ISPRAS-2025-37(3)-20
Email this article 