Abstract
A recent trend in the analysis of object-oriented programs is the modeling of references as sets of guarded values, enabling multiple heap shapes to be represented in a single state. A fundamental problem with using these guarded value sets is the inability to generate test inputs in a manner similar to symbolic execution based analyses. Although several solutions have been proposed, none have been proven to be sound and complete with respect to the heap properties provable by generalized symbolic execution (GSE). This work presents a method for initializing input references in a symbolic input heap using guarded value sets that exactly preserves GSE semantics. A correctness proof for the initialization scheme is provided with a proof-of-concept implementation. Results from an empirical evaluation on a common set of GSE data structure benchmarks show an increase in the size and number of analyzed heaps over existing GSE representations. The initialization technique can be used to ensure that guarded value set based symbolic execution engines operate in a provably correct manner with regards to symbolic references as well as provide the ability to generate concrete heaps that serve as test inputs to the program.
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
Similar content being viewed by others
Notes
- 1.
Guarded value sets are variously referred to in the literature as guarded location sets, symbolic value sets, or value summaries. The term guarded value set is sometimes abbreviated in this text as value set.
- 2.
Although not treated in this presentation, the concept naturally extends to polymorphic languages.
References
Berdine, J., Calcagno, C., O’hearn, P.W.: A decidable fragment of separation logic. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 97–109. Springer, Heidelberg (2004)
Blackshear, S., Chang, B.Y.E., Sridharan, M.: Thresher: Precise refutations for heap reachability. In: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation PLDI 2013, pp. 275–286. ACM, New York (2013)
Boyapati, C., Khurshid, S., Marinov, D.: Korat: automated testing based on java predicates. In: ACM SIGSOFT Software Engineering Notes, vol. 27, pp. 123–133. ACM (2002)
Braione, P., Denaro, G., Pezzè, M.: Symbolic execution of programs with heap inputs. In: Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, pp. 602–613. ACM (2015)
Brotherston, J., Fuhs, C., Pérez, J.A.N., Gorogiannis, N.: A decision procedure for satisfiability in separation logic with inductive predicates. In: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), p. 25. ACM (2014)
Cadar, C., Dunbar, D., Engler, D.R.: Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation OSDI 2008, pp. 209–224. USENIX Association, Berkeley (2008)
Chen, T., Zhang, X.S., Guo, S.Z., Li, H.Y., Wu, Y.: State of the art: Dynamic symbolic execution for automated test generation. Future Gener. Comput. Syst. 29(7), 1758–1773 (2013)
Cook, B., Haase, C., Ouaknine, J., Parkinson, M., Worrell, J.: Tractable reasoning in a fragment of separation logic. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 235–249. Springer, Heidelberg (2011)
Deng, X., Lee, J., et al.: Bogor/kiasan: A k-bounded symbolic execution for checking strong heap properties of open systems. In: 21st IEEE/ACM International Conference on Automated Software Engineering ASE 2006, pp. 157–166. IEEE (2006)
Deng, X., Robby, Hatcliff, J.: Kiasan/KUnit: Automatic test case generation and analysis feedback for open object-oriented systems. In: TAICPART-MUTATION, pp. 3–12 (2007)
Deng, X., Robby, Hatcliff, J.: Towards a case-optimal symbolic execution algorithm for analyzing strong properties of object-oriented programs. In: Fifth IEEE International Conference on Software Engineering and Formal Methods SEFM 2007, pp. 273–282, September 2007
Dillig, I., Dillig, T., Aiken, A., Sagiv, M.: Precise and compact modular procedure summaries for heap manipulating programs. In: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation PLDI 2011, pp. 567–577. ACM, New York (2011)
Dimjašević, M., Giannakopoulou, D., Howar, F., Isberner, M., Rakamarić, Z., Raman, V.: The dart, the psyco, and the doop. In: ACM SIGSOFT Software Engineering Notes, vol. 40, pp. 1–5. ACM (2015)
Elkarablieh, B., Godefroid, P., Levin, M.Y.: Precise pointer reasoning for dynamic test generation. In: Proceedings of the Eighteenth International Symposium on Software Testing and Analysis, pp. 129–140. ACM (2009)
Felleisen, M., Hieb, R.: The revised report on the syntactic theories of sequential control and state. Theoret. Comput. Sci. 103(2), 235–271 (1992)
Ferrara, P., Müller, P., Novacek, M.: Automatic inference of heap properties exploiting value domains. In: D’Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 393–411. Springer, Heidelberg (2015)
Filieri, A., Frias, M.F., Păsăreanu, C.S., Visser, W.: Model counting for complex data structures. In: Fischer, B., Geldenhuys, J. (eds.) SPIN 2015. LNCS, vol. 9232, pp. 222–241. Springer, Heidelberg (2015)
Giannakopoulou, D., Howar, F., Isberner, M., Lauderdale, T., Rakamarić, Z., Raman, V.: Taming test inputs for separation assurance. In: Proceedings of the 29th IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 373–384. ACM (2014)
Hillery, B., Mercer, E., Rungta, N., Person, S.: Towards a lazier symbolic pathfinder. SIGSOFT Softw. Eng. Notes 39(1), 1–5 (2014)
Hillery, B., Mercer, E., Rungta, N., Person, S.: Exact heap summaries for symbolic execution. Technical report, Brigham Young University (2015). http://students.cs.byu.edu/egm/papers/SH-long.pdf
Khurshid, S., Păsăreanu, C.S., Visser, W.: Generalized symbolic execution for model checking and testing. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 553–568. Springer, Heidelberg (2003)
de Moura, L., Bjørner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
Navarro Pérez, J.A., Rybalchenko, A.: Separation logic+ superposition calculus = heap theorem prover. In: ACM SIGPLAN Notices, vol. 46, pp. 556–566. ACM (2011)
Person, S., Yang, G., Rungta, N., Khurshid, S.: Directed incremental symbolic execution. In: PLDI, pp. 504–515 (2011)
Piskac, R., Wies, T., Zufferey, D.: Automating separation logic with trees and data. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 711–728. Springer, Heidelberg (2014)
Păsăreanu, C.S., Visser, W., Bushnell, D.H., Geldenhuys, J., Mehlitz, P.C., Rungta, N.: Symbolic PathFinder: integrating symbolic execution with model checking for Java bytecode analysis. Autom. Softw. Eng. 20(3), 391–425 (2013)
Qu, X., Robinson, B.: A case study of concolic testing tools and their limitations. In: 2011 International Symposium on Empirical Software Engineering and Measurement (ESEM), pp. 117–126. IEEE (2011)
Rosner, N., Geldenhuys, J., Aguirre, N., Visser, W., Frias, M.: BLISS: Improved symbolic execution by bounded lazy initialization with sat support. Software Engineering, IEEE Transactions on PP(99), 1–1 (2015)
Sangiorgi, D.: Introduction to Bisimulation and Coinduction. Cambridge University Press, New York (2011)
Sen, K., Necula, G., Gong, L., Choi, P.W.: MultiSE: Multi-path symbolic execution using value summaries. Technical Report UCB/EECS-2014-173, University of California at Berkely Department of Electrical Engineering and Computer Sciences, October 2014
Tillmann, Nikolai, de Halleux, Jonathan: Pex–White Box Test Generation for.NET. In: Beckert, Bernhard, Hähnle, Reiner (eds.) TAP 2008. LNCS, vol. 4966, pp. 134–153. Springer, Heidelberg (2008)
Torlak, E., Bodik, R.: A lightweight symbolic virtual machine for solver-aided host languages. In: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, p. 54. ACM (2014)
Visser, W., Pǎsǎreanu, C.S., Khurshid, S.: Test input generation with Java PathFinder. ACM SIGSOFT Softw. Eng. Notes 29(4), 97–107 (2004)
Wesonga, S.O.: Javalite - An Operational Semantics for Modeling Java Programs. Master’s thesis, Brigham Young University, Provo UT (2012)
Xie, Y., Aiken, A.: Scalable error detection using boolean satisfiability. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages POPL 2005, pp. 351–363. ACM, New York (2005)
Yorsh, G., Yahav, E., Chandra, S.: Generating precise and concise procedure summaries. In: ACM SIGPLAN Notices, vol. 43, pp. 221–234. ACM (2008)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hillery, B., Mercer, E., Rungta, N., Person, S. (2016). Exact Heap Summaries for Symbolic Execution. In: Jobstmann, B., Leino, K. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2016. Lecture Notes in Computer Science(), vol 9583. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-49122-5_10
Download citation
DOI: https://doi.org/10.1007/978-3-662-49122-5_10
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-49121-8
Online ISBN: 978-3-662-49122-5
eBook Packages: Computer ScienceComputer Science (R0)