Abstract
This paper presents a parallel symbolic execution engine as a plug-in extension to Eclipse CDT/Codan. It uses the CDT parser and the control flow graph builder from CDT’s code analysis framework (Codan). Path satisfiability and bug conditions are checked with an SMT solver in the logic of arrays, uninterpreted functions and nonlinear integer and real arithmetic (AUFNIRA). Each worker of the parallel engine keeps the symbolic program states along its current program path in memory, to allow for quick backtracking. Dynamic redistribution of work between workers is enabled by splitting a worker’s partition of the execution tree at the partition’s top decision node, where a partition is defined by the start path leading to its root control flow decision node. The runtime behaviour of the parallel symbolic execution engine is evaluated by running it on buffer overflow test programs from the NSA’s Juliet test suite for static analyzers. Both the speedup of backtracking the symbolic program state over a previous single-threaded implementation with path replay and the speedup with an increasing number of workers are investigated.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
King, J.: Symbolic execution and program testing. Communications of the ACM 19(7), 385–394 (1976)
Dechter, R.: Constraint Processing. Morgan Kaufmann Publishers (2003)
Harrison, J.: Handbook of Practical Logic and Automated Reasoning. Cambridge University Press (2009)
Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB Standard Version 2.0 (December 2010), http://goedel.cs.uiowa.edu/smtlib/papers/smt-lib-reference-v2.0-r10.12.21.pdf
Cadar, C., Sen, K., Godefroid, P., Tillmann, N., Khurshid, S., Visser, W., Pasareanu, C.: Symbolic execution for software testing in practice – preliminary assessment. In: Int. Conf. Software Eng. (2011)
Pasareanu, C., Visser, W.: A survey of new trends in symbolic execution for software testing and analysis. Int. J. Software Tools Technology Transfer 11, 339–353 (2009)
Cadar, C., Dunbar, D., Engler, D.: KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: USENIX Symp. Operating Systems Design and Implementation (2008)
Lattner, C., Adve, V.: LLVM: A compilation framework for lifelong program analysis and transformation. In: Int. Symp. Code Generation and Optimization (2004)
Correnson, L., et al.: FRAMA-C User Manual, release oxygen-20120901. CEA LIST (2012), http://frama-c.com/download/frama-c-user-manual.pdf
Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: CIL: Intermediate language and tools for analysis and transformation of C programs. In: Nigel Horspool, R. (ed.) CC 2002. LNCS, vol. 2304, pp. 213–228. Springer, Heidelberg (2002), http://dl.acm.org/citation.cfm?id=647478.727796
Visser, W., Pasareanu, C., Khurshid, S.: Test input generation with Java Pathfinder. In: Int. Symp. Software Testing and Analysis (2004)
Staats, M., Pasareanu, C.: Parallel symbolic execution for structural test generation. In: Int. Symp. Software Testing and Analysis, pp. 183–193 (2010)
Bucur, S., Ureche, V., Candea, G.: Parallel symbolic execution for automated real-world software testing. In: EuroSys (2011)
Kremenek, T.: Finding software bugs with the Clang static analyzer. LLVM Developers’ Meeting (August 2008), http://llvm.org/devmtg/2008-08/Kremenek_StaticAnalyzer.pdf
Archer, S., VanderLei, P., McAffer, J.: OSGi and Equinox: Creating Highly Modular Java Systems. Addison Wesley (2010)
Laskavaia, A.: Codan- C/C++ static analysis framework for CDT. In: EclipseCon (2011)
Ibing, A.: SMT-constrained symbolic execution for Eclipse CDT/Codan. In: Workshop on Formal Methods in the Development of Software (2013)
United States National Security Agency, Center for Assured Software: Juliet Test Suite v1.1 for C/C++ (December 2011), http://samate.nist.gov/SRD/testCases/suites/Juliet_Test_Suite_v1.1_for_C_Cpp.zip
Nielson, F., Nielson, H., Hankin, C.: Principles of Program Analysis. Springer (2010)
Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. In: Muchnik, S., Jones, N. (eds.) Program Flow Analysis: Theory and Applications, pp. 189–233. Prentice-Hall (1981)
Parr, T.: Language Implementation Patterns. Pragmatic Bookshelf (2010)
Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The mathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 93–107. Springer, Heidelberg (2013)
Madadhain, J., Fisher, D., Smyth, P., White, S., Boey, Y.: Analysis and visualization of network data using JUNG. J. Statistical Software (2005)
Apache: Batik Java svg toolkit, http://xmlgraphics.apache.org/batik/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 IFIP International Federation for Information Processing
About this paper
Cite this paper
Ibing, A. (2013). Parallel SMT-Constrained Symbolic Execution for Eclipse CDT/Codan. In: Yenigün, H., Yilmaz, C., Ulrich, A. (eds) Testing Software and Systems. ICTSS 2013. Lecture Notes in Computer Science, vol 8254. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-41707-8_13
Download citation
DOI: https://doi.org/10.1007/978-3-642-41707-8_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-41706-1
Online ISBN: 978-3-642-41707-8
eBook Packages: Computer ScienceComputer Science (R0)