nach oben

Erschienen in:

2016 | OriginalPaper | Buchkapitel

Exact Heap Summaries for Symbolic Execution

verfasst von : Benjamin Hillery, Eric Mercer, Neha Rungta, Suzette Person

Erschienen in: Verification, Model Checking, and Abstract Interpretation

Verlag: Springer Berlin Heidelberg

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel : Data-Driven Disjunctive Abstraction

Nächstes Kapitel Abstract Interpretation with Infinitesimals

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.

Although not treated in this presentation, the concept naturally extends to polymorphic languages.

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)CrossRef

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)CrossRef

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)CrossRef

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)

10.

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)

11.

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

12.

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)

13.

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)

14.

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)

15.

Felleisen, M., Hieb, R.: The revised report on the syntactic theories of sequential control and state. Theoret. Comput. Sci. 103(2), 235–271 (1992)MATHMathSciNetCrossRef

16.

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)

17.

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)CrossRef

18.

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)

19.

Hillery, B., Mercer, E., Rungta, N., Person, S.: Towards a lazier symbolic pathfinder. SIGSOFT Softw. Eng. Notes 39(1), 1–5 (2014)CrossRef

20.

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

21.

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)CrossRef

22.

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)CrossRef

23.

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)

24.

Person, S., Yang, G., Rungta, N., Khurshid, S.: Directed incremental symbolic execution. In: PLDI, pp. 504–515 (2011)

25.

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)

26.

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)CrossRef

27.

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)

28.

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)

29.

Sangiorgi, D.: Introduction to Bisimulation and Coinduction. Cambridge University Press, New York (2011)CrossRef

30.

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

31.

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)CrossRef

32.

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)

33.

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)CrossRef

34.

Wesonga, S.O.: Javalite - An Operational Semantics for Modeling Java Programs. Master’s thesis, Brigham Young University, Provo UT (2012)

35.

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)

36.

Yorsh, G., Yahav, E., Chandra, S.: Generating precise and concise procedure summaries. In: ACM SIGPLAN Notices, vol. 43, pp. 221–234. ACM (2008)

Titel: Exact Heap Summaries for Symbolic Execution
verfasst von: Benjamin Hillery
Eric Mercer
Neha Rungta
Suzette Person
Verlag: Springer Berlin Heidelberg
Buch: Verification, Model Checking, and Abstract Interpretation
Print ISBN: 978-3-662-49121-8

Electronic ISBN: 978-3-662-49122-5

Copyright-Jahr: 2016
DOI: https://doi.org/10.1007/978-3-662-49122-5_10

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"