Automated testing of LLVM programs with complex input data structures

Autor:	Alexander Vladimirovich Misonizhnik, Alexey Alexandrovich Babushkin, Sergey Antonovich Morozov, Yurii Olegovich Kostyukov, Dmitry Alexandrovich Mordvinov, Dmitry Vladimirovich Koznov
Rok vydání:	2022
Předmět:	General Earth and Planetary Sciences General Environmental Science
Zdroj:	Proceedings of the Institute for System Programming of the RAS. 34:49-62
ISSN:	2220-6426 2079-8156
DOI:	10.15514/ispras-2022-34(4)-4
Popis:	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.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::64ead577a447cc0eb74b64c5b1b30073 https://doi.org/10.15514/ispras-2022-34(4)-4 Zobrazit plný text záznamu