Abstract
Symbolic execution can be problematic when applied to real applications. This paper addresses two of these problems: (1) the constraints generated during symbolic execution may be of a type not handled by the underlying decision procedure, and (2) some parts of the application may be unsuitable for symbolic execution (e.g.,third-party libraries). The paper presents type-dependence analysis, which performs a context- and field-sensitive interprocedural static analysis to identify program entities that may store symbolic values at run-time. This information is used to identify the above two problematic cases and assist the user in addressing them. The paper also presents a technique to transform real applications for efficient symbolic execution. Instead of transforming the entire application, which can be inefficient and infeasible (mostly for pragmatic reasons), our technique leverages the results of type-dependence analysis to transform only parts of the program that may interact with symbolic values. Finally, the paper discusses the implementation of our analysis and transformation technique in a tool, stinger, and an empirical evaluation performed on two real applications. The results of the evaluation show the effectiveness of our approach.
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
Berndl, M., et al.: Points-to analysis using BDDs. In: PLDI, pp. 103–114 (2003)
Cadar, C., et al.: EXE: Automatically generating inputs of death. In: CCS, pp. 322–335 (2006)
Cadar, C., et al.: EXE: A system for automatically generating inputs of death using symbolic execution. Technical Report CSTR 2006-01, Stanford University (2006)
Dams, D.R., Holzmann, G.J., Hesse, W.: Abstracting C with abC. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 515–520. Springer, Heidelberg (2002)
Deng, X., Lee, J., Robby: Bogor/Kiasan: A k-bounded symbolic execution for checking strong heap properties of open systems. In: ASE, pp. 157–166 (2006)
Dutertre, B., de Moura, L.: A Fast Linear-Arithmetic Solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81–94. Springer, Heidelberg (2006)
Dwyer, M.B., et al.: Tool-supported program abstraction for finite-state verification. In: ICSE, pp. 177–187 (2001)
Flanagan, C., et al.: Extended static checking for Java. In: PLDI, pp. 234–245 (2002)
Ganesh, V., Dill, D.: System Description of STP, http://www.csl.sri.com/users/demoura/smt-comp/descriptions/stp.ps
Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: PLDI, pp. 213–223 (2005)
Grieskamp, W., Tillmann, N., Schulte, W.: XRT–exploring runtime for .NET architecture and applications. Electr. Notes Theor. Comp. Sci. 144(3), 3–26 (2006)
Horwitz, S., Reps, T.W., Sagiv, S.: Demand interprocedural dataflow analysis. In: FSE, pp. 104–115 (1995)
Java PathFinder, http://javapathfinder.sourceforge.net
Visser, W., Păsăreanu, C.S., Khurshid, S.: Generalized Symbolic Execution for Model Checking and Testing. In: Garavel, H., Hatcliff, J. (eds.) ETAPS 2003 and TACAS 2003. LNCS, vol. 2619, pp. 553–568. Springer, Heidelberg (2003)
King, J.C.: Symbolic execution and program testing. CACM 19(7), 385–394 (1976)
Lhoták, O., Hendren, L.J.: Jedd: a BDD-based relational extension of Java. In: PLDI, pp. 158–169 (2004)
Pugh, W.: The Omega test: a fast and practical integer programming algorithm for dependence analysis. In: SC, pp. 4–13 (1991)
Reps, T.W.: Program analysis via graph reachability. In: ILPS, pp. 5–19 (1997)
Sen, K., Marinov, D., Agha, G.: CUTE: a concolic unit testing engine for C. In: FSE, pp. 263–272 (2005)
Shankar, U., et al.: Detecting format-string vulnerabilities with type qualifiers. In: USENIX Security Symposium, pp. 201–218 (2001)
Shivers, O.: Control-flow analysis in Scheme. In: PLDI, pp. 164–174 (1988)
Sridharan, M., et al.: Demand-driven points-to analysis for Java. In: OOPSLA, pp. 59–76 (2005)
Tilevich, E., Smaragdakis, Y.: Transparent program transformations in the presence of opaque code. In: GPCE, pp. 89–94 (2006)
Vallée-Rai, R., et al.: Soot - a Java optimization framework. In: CASCON, pp. 125–135 (1999)
Visser, W., Pasareanu, C.S., Khurshid, S.: Test input generation with Java PathFinder. In: ISSTA, pp. 97–107 (2004)
Volpano, D.M., Irvine, C.E., Smith, G.: A sound type system for secure flow analysis. Journal of Computer Security 4(2-3), 167–188 (1996)
Whaley, J., Lam, M.S.: Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. In: PLDI, June 2004, pp. 131–144 (2004)
Notkin, D., et al.: Symstra: A Framework for Generating Object-Oriented Unit Tests Using Symbolic Execution. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 365–381. Springer, Heidelberg (2005)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Anand, S., Orso, A., Harrold, M.J. (2007). Type-Dependence Analysis and Program Transformation for Symbolic Execution. In: Grumberg, O., Huth, M. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2007. Lecture Notes in Computer Science, vol 4424. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71209-1_11
Download citation
DOI: https://doi.org/10.1007/978-3-540-71209-1_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-71208-4
Online ISBN: 978-3-540-71209-1
eBook Packages: Computer ScienceComputer Science (R0)