Abstract
Dynamic symbolic execution (or concolic execution) is a powerful method for program analysis and software testing by attaching symbolic execution to the concrete running of a program. This paper proposes an approach to handle aggregate types (e.g., pointers, arrays, structures) and their complex combinations for the dynamic symbolic execution of C programs. The main idea of the approach is splitting a complex type program variable into a series of primitive type variables. During the concrete execution of a program, a concolic execution engine is provided to observe the operations on every program variable at the level of primitive types, and then the symbolic state of the program is updated. The path constraints which must be satisfied to drive the program running along the current execution path are collected to generate new test data for other paths. Our approach guarantees that only primitive type variables can appear in the symbolic states and path constraints. Based on LLVM byte code instrumentation, we present a new tool, called PathWalker, which implements this approach. Experimental results reveal that PathWalker is effective to deal with complex types in C codes.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Godefroid, P., Levin, M., Molnar, D.: Automated whitebox fuzz testing. In: 16th Annual Network & Distributed System Security Symposium, pp. 6–79. THE INTERNET SOCIETY, San Diego, California, USA (2008)
Sen, Koushik, Agha, Gul: CUTE and jCUTE: Concolic unit testing and explicit path model-checking tools. In: Ball, Thomas, Jones, Robert B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 419–423. Springer, Heidelberg (2006)
Clarke, L.A.: A system to generate test data and symbolically execute programs. J. IEEE Trans on Software Engineering. 2(3), 215–222 (1976)
Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: 26th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 213–223. ACM Press, Chicago, Illinois, USA (2005)
Cadar, C., Godefroid, P., Tillmann, N., Visser, W.: Symbolic execution for software testing in practice preliminary assessment. In: 33th International Conference on Software Engineering, pp. 1066–1071. ACM Press, Waikiki, Honolulu, HI, USA (2011)
Cadar, C., Dunbar, D., Engler, D.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: 8th USENIX Symposium on Operating Systems Design and Implementation, pp. 209–224. IEEE Press, San Diego, California, USA. (2008)
Avgerinos, T., Rebert, T., Cha, S.K., Brumley, D.: Enhancing symbolic execution with veritesting. In: 36th International Conference on Software Engineering, pp. 1083–1094. IEEE Press, New York, USA (2014)
Lattner, C., Adve, V.: LLVM: a compilation framework for lifelong program analysis and transformation. In: 2nd International Symposium on Code Generation and Optimization, pp. 75–88. IEEE Press, San Jose, CA, USA (2004)
Lattner, C.: LLVM: an Infrastructure for Multi-Stage Optimization. Masters Thesis, Computer Science Dept., University of Illinois at Urbana-Champaign (2002)
Clang: a C language family frontend for LLVM. http://clang.llvm.org/
Lattner, C., Adve, V.: The LLVM Instruction Set and Compilation Strategy. Technical report, University of Illinois at Urbana-Champaign (2002)
de Moura, Leonardo, Bjørner, Nikolaj S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, Jakob (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
Cadar, Cristian, Engler, Dawson: Execution generated test cases: how to make systems code crash itself. In: Godefroid, Patrice (ed.) SPIN 2005. LNCS, vol. 3639, pp. 2–23. Springer, Heidelberg (2005)
Burnim, J., Sen, K.: Heuristics for scalable dynamic test generation. In: 23rd IEEE/ACM International Conference on Automated Software Engineering, pp. 443–446. IEEE Press, L’Aquila, Italy (2008)
Fraser, G., Arcuri, A.: Sound empirical evidence in software testing. In: 34th International Conference on Software Engineering, pp. 178–188. IEEE Press, Zurich, Switzerland (2012)
Kratkiewicz, K.: Evaluating Static Analysis Tools for Detecting Buffer Overflows in C Code. Harvard University, USA (2005)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Jun-xian, Z., Zhou-jun, L., Xian-chen, Z. (2015). PathWalker: A Dynamic Symbolic Execution Tool Based on LLVM Byte Code Instrumentation. In: Li, X., Liu, Z., Yi, W. (eds) Dependable Software Engineering: Theories, Tools, and Applications. SETTA 2015. Lecture Notes in Computer Science(), vol 9409. Springer, Cham. https://doi.org/10.1007/978-3-319-25942-0_15
Download citation
DOI: https://doi.org/10.1007/978-3-319-25942-0_15
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-25941-3
Online ISBN: 978-3-319-25942-0
eBook Packages: Computer ScienceComputer Science (R0)