Automated testing of LLVM programs with complex input data structures
Alexander Vladimirovich MISONIZHNIK,
Alexey Alexandrovich BABUSHKIN,
Sergey Antonovich MOROZOV,
Yurii Olegovich KOSTYUKOV,
Dmitry Alexandrovich MORDVINOV,
Dmitry Vladimirovich KOZNOV https://doi.org/10.15514/ISPRAS-2022-34(4)-4
Abstract
Symbolic execution is a widely used approach for automatic regression test generation and bug and vulnerability finding. The main goal of this paper is to present a practical symbolic execution-based approach for LLVM programs with complex input data structures. The approach is based on the well-known idea of lazy initialization, which frees the user from providing constraints on input data structures manually. Thus, it provides us with a fully automatic symbolic execution of even complex program. Two lazy initialization improvements are proposed for segmented memory models: one based on timestamps and one based on type information. The approach is implemented in the KLEE symbolic virtual machine for the LLVM platform and tested on real C data structures — lists, binomial heaps, AVL trees, red-black trees, binary trees, and tries.
Keywords
Supporting agencies: The work is supported by the grant of RNF № 22-21-00697
About the Authors
Alexander Vladimirovich MISONIZHNIK
St. Petersburg State University
Russian Federation
Russian Federation
Received his master's degree in computer science at St. Petersburg State University in 2021
Alexey Alexandrovich BABUSHKIN
St. Petersburg State University
Russian Federation
Russian Federation
Received his bachelor's degree in mathematics and computer science at St. Petersburg State University in 2022
Sergey Antonovich MOROZOV
HSE University
Russian Federation
Russian Federation
A 3rd-year undergraduate student in Applied Mathematics and Computer Science
Yurii Olegovich KOSTYUKOV
St. Petersburg State University
Russian Federation
Russian Federation
PhD student of the Department of System Programming
Dmitry Alexandrovich MORDVINOV
St. Petersburg State University
Russian Federation
Russian Federation
PhD in Physics and Mathematics, Associate Professor at the Department of System Programming
Dmitry Vladimirovich KOZNOV
St. Petersburg State University
Russian Federation
Russian Federation
Doctor of Technical Sciences, Professor of the System Programming Department
References
1. Korel B., Al-Yami A.M. Automated Regression Test Generation. ACM SIGSOFT Software Engineering Notes, vol. 23, issue 2, 1998, pp. 143-152.
2. Cadar C., Sen K. Symbolic execution for software testing: three decades later. Communications of the ACM, vol. 56, issue 2, 2013, pp. 82-90.
3. Baldoni R., Coppa E. et al. A survey of symbolic execution techniques. ACM Computing Surveys (CSUR), vol. 51, issue 3, 2018, pp. 1-39.
4. Barrett C., Tinelli C. Satisfiability Modulo Theories. In Handbook of Model Checking, Springer, 2018, pp. 305-343.
5. Volanschi N., Lawall J. The impact of generic data structures: decoding the role of lists in the linux kernel. In Proc. of the 35th IEEE/ACM International Conference on Automated Software Engineering (ASE), 2020, pp. 103-114.
6. Corbet J. Trees II: red-black trees. URL: https://lwn.net/Articles/184495/, 2006.
7. Bacthu N., Banerjee A. et al. Dynamic and compressed trie for use in route lookup. United States Patent Application 20180212876, URL: https://www.freepatentsonline.com/20180212876.pdf, 2018.
8. Braione P., Denaro G. et al. Combining symbolic execution and search-based testing for programs with complex heap inputs. In Proc. of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2017), 2017, pp. 90-101.
9. Galeotti J.P., Rosner N. et al. Analysis of invariants for efficient bounded verification. In Proc. of the 19th International Symposium on Software Testing and Analysis (ISSTA '10), 2010, pp. 25-36.
10. Khurshid S., Puasuareanu C.S., Visser W. Generalized symbolic execution for model checking and testing. In Proc. of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2003, pp. 553-568.
11. Kapus T., Cadar C.A segmented memory model for symbolic execution. In Proc. of the 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2019, pp. 774-784.
12. Cadar C., Dunbar D., Engler D. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In Proc. of the 8th USENIX Conference on Operating Systems Design and Implementation, 2008, pp. 209-224.
13. ISO/IEC 9899:201x - N1570 - Programming languages – C. URL: https://web.cs.dal.ca/~vlado/pl/C_Standard_2011-n1570.pdf.
14. Cadar C., Dunbar D. KLEE. URL: https://github.com/klee/klee/tree/v2.3, 2022.
15. de Moura L., Bjorner N. Z3: An Efficient SMT Solver. Lecture Notes in Computer Science, vol. 4963, 2008, pp. 337-340.
16. Gough B., Stallman R. M. An Introduction to GCC for the GNU Compilers gcc and g++. Network Theory Ltd, 2004, 144 p.
17. Geldenhuys J., Aguirre N. et al. Bounded Lazy Initialization. Lecture Notes in Computer Science, vol. 7871, 2013, pp. 229-243.
18. Puasuareanu C. S., Rungta N. Symbolic PathFinder: symbolic execution of Java bytecode. In Proc. of the IEEE/ACM International Conference on Automated Software Engineering, 2010, pp. 179-180.
19. Rosner N., Geldenhuys J. et al. BLISS: improved symbolic execution by bounded lazy initialization with SAT support. IEEE Transactions on Software Engineering, vol. 41, issue 7, 2015, pp. 639-660.
20. Braione P., Denaro G., Pezze M. Symbolic Execution of Programs with Heap Inputs. In Proc. of the 10th Joint Meeting on Foundations of Software Engineering, 2015, pp. 602-613.
21. Ramos D. A., Engler D. Under-Constrained Symbolic Execution: Correctness Checking for Real Code. In Proc. of the 24th USENIX Security Symposium (USENIX Security 15), 2015, pp. 49-64.
22. Rutledge R., Orso A. PG-KLEE: Trading Soundness for Coverage. In Proc. of the IEEE/ACM 42nd International Conference on Software Engineering: Companion Proceedings (ICSE-Companion), 2020, pp. 65-68.
Review
For citations:
MISONIZHNIK A.V., BABUSHKIN A.A., MOROZOV S.A., KOSTYUKOV Yu.O., MORDVINOV D.A., KOZNOV D.V. Automated testing of LLVM programs with complex input data structures. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2022;34(4):49-62. (In Russ.) https://doi.org/10.15514/ISPRAS-2022-34(4)-4
Email this article 