|
This article is cited in 1 scientific paper (total in 1 paper)
Automated testing of LLVM programs with complex input data structures
A. V. Misonizhnika, A. A. Babushkina, S. A. Morozovb, Yu. O. Kostyukova, D. A. Mordvinova, D. V. Koznova a Saint Petersburg State University
b National Research University "Higher School of Economics", St.
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:
automated testing, symbolic execution, lazy initialization, LLVM platform, KLEE, data structures
Citation:
A. V. Misonizhnik, A. A. Babushkin, S. A. Morozov, Yu. O. Kostyukov, D. A. Mordvinov, D. V. Koznov, “Automated testing of LLVM programs with complex input data structures”, Proceedings of ISP RAS, 34:4 (2022), 49–62
Linking options:
https://www.mathnet.ru/eng/tisp704 https://www.mathnet.ru/eng/tisp/v34/i4/p49
|
Statistics & downloads: |
Abstract page: | 20 | Full-text PDF : | 2 |
|