Abstract
Symbolic execution is a well established method for test input generation. Despite of having achieved tremendous success over numerical domains, existing symbolic execution techniques for heap-based programs are limited due to the lack of a succinct and precise description for symbolic values over unbounded heaps. In this work, we present a new symbolic execution method for heap-based programs based on separation logic. The essence of our proposal is context-sensitive lazy initialization, a novel approach for efficient test input generation. Our approach differs from existing approaches in two ways. Firstly, our approach is based on separation logic, which allows us to precisely capture preconditions of heap-based programs so that we avoid generating invalid test inputs. Secondly, we generate only fully initialized test inputs, which are more useful in practice compared to those partially initialized test inputs generated by the state-of-the-art tools. We have implemented our approach as a tool, called Java StarFinder, and evaluated it on a set of programs with complex heap inputs. The results show that our approach significantly reduces the number of invalid test inputs and improves the test coverage.
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
Notes
- 1.
- 2.
In all path conditions in this example we only show the constraints over those variables which are relevant to the inputs \({ \mathtt{x}}\) and \({ \mathtt{y}}\); the constraints over local variables \({ \mathtt{z}}\) and \({ \mathtt{dummyHead}}\) are separated from \({ \mathtt{x}}\), \({ \mathtt{y}}\) and thus are omitted for simplicity.
- 3.
We use the same symbol \(s\) as in concrete setting. From the context, it should be clear as to whether we are referring to symbolic stack or concrete stack.
References
Facebook Infer. https://fbinfer.com/
JaCoCo. https://www.eclemma.org/jacoco/
SUSHI Experiments. https://github.com/pietrobraione/sushi-experiments
Berdine, J., Calcagno, C., O’Hearn, P.W.: Symbolic execution with separation logic. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 52–68. Springer, Heidelberg (2005). https://doi.org/10.1007/11575467_5
Braione, P., Denaro, G., Mattavelli, A., Pezzè, M.: Combining symbolic execution and search-based testing for programs with complex heap inputs. In: Bultan, T., Sen, K. (eds.) ISSTA 2017, pp. 90–101. ACM (2017). https://doi.org/10.1145/3092703.3092715
Braione, P., Denaro, G., Pezzè, M.: Symbolic execution of programs with heap inputs. In: Nitto, E.D., Harman, M., Heymans, P. (eds.) FSE 2015, pp. 602–613. ACM (2015). https://doi.org/10.1145/2786805.2786842
Braione, P., Denaro, G., Pezzè, M.: JBSE: a symbolic executor for Java programs with complex heap inputs. In: Zimmermann, T., Cleland-Huang, J., Su, Z. (eds.) FSE 2016, pp. 1018–1022. ACM (2016). https://doi.org/10.1145/2950290.2983940
Cadar, C., et al.: Symbolic execution for software testing in practice: preliminary assessment. In: Taylor, R.N., Gall, H.C., Medvidovic, N. (eds.) ICSE 2011, pp. 1066–1071. ACM (2011). https://doi.org/10.1145/1985793.1985995
Calcagno, C., Distefano, D., O’Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. JACM 58(6), 26:1–26:66 (2011). https://doi.org/10.1145/2049697.2049700
Chin, W.N., David, C., Nguyen, H.H., Qin, S.: Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Sci. Comput. Program. 77(9), 1006–1036 (2012). https://doi.org/10.1016/j.scico.2010.07.004
Deng, X., Lee, J., Robby: Bogor/Kiasan: a K-bounded symbolic execution for checking strong heap properties of open systems. In: ASE 2006, pp. 157–166. IEEE Computer Society (2006). https://doi.org/10.1109/ASE.2006.26
Deng, X., Robby, Hatcliff, J.: Towards a case-optimal symbolic execution algorithm for analyzing strong properties of object-oriented programs. In: SEFM 2007. IEEE Computer Society (2007). https://doi.org/10.1109/SEFM.2007.43
Enderton, H.B.: A Mathematical Introduction to Logic, 2nd Edn. pp. 67–181. Academic Press (2001). https://doi.org/10.1016/B978-0-08-049646-7.50008-4
Galeotti, J.P., Rosner, N., López Pombo, C.G., Frias, M.F.: Analysis of invariants for efficient bounded verification. In: Tonella, P., Orso, A. (eds.) ISSTA 2010, pp. 25–36. ACM (2010). https://doi.org/10.1145/1831708.1831712
Geldenhuys, J., Aguirre, N., Frias, M.F., Visser, W.: Bounded lazy initialization. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 229–243. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38088-4_16
Hillery, B., Mercer, E., Rungta, N., Person, S.: Exact heap summaries for symbolic execution. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 206–225. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49122-5_10
Ishtiaq, S.S., O’Hearn, P.W.: BI as an assertion language for mutable data structures. In: Hankin, C., Schmidt, D. (eds.) POPL 2001, pp. 14–26. ACM (2001). https://doi.org/10.1145/360204.375719
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). https://doi.org/10.1007/3-540-36577-X_40
King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976). https://doi.org/10.1145/360248.360252
Le, Q.L., Gherghina, C., Qin, S., Chin, W.-N.: Shape analysis via second-order bi-abduction. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 52–68. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_4
Le, Q.L., Sun, J., Chin, W.-N.: Satisfiability modulo heap-based programs. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 382–404. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41528-4_21
Le, Q.L., Sun, J., Qin, S.: Frame inference for inductive entailment proofs in separation logic. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 41–60. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89960-2_3
Le, Q.L., Tatsuta, M., Sun, J., Chin, W.-N.: A decidable fragment in separation logic with inductive predicates and arithmetic. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 495–517. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63390-9_26
Leavens, G.T., Baker, A.L., Ruby, C.: JML: a notation for detailed design. In: Kilov, H., Rumpe, B., Simmonds, I. (eds.) Behavioral Specifications of Businesses and Systems, vol. 523, pp. 175–188. Springer, Heidelberg (1999). https://doi.org/10.1007/978-1-4615-5229-1_12
Müller, P., Schwerhoff, M., Summers, A.J.: Automatic verification of iterated separating conjunctions using symbolic execution. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 405–425. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41528-4_22
Pham, L.H., Le, Q.L., Phan, Q.S., Sun, J.: Concolic testing heap-manipulating programs. In: FM 2019 (2019, to appear)
Pham, L.H., Le, Q.L., Phan, Q.S., Sun, J., Qin, S.: Testing heap-based programs with Java StarFinder. In: Chaudron, M., Crnkovic, I., Chechik, M., Harman, M. (eds.) ICSE 2018, pp. 268–269. ACM (2018). https://doi.org/10.1145/3183440.3194964
Păsăreanu, C.S., Visser, W., Bushnell, D., Geldenhuys, J., Mehlitz, P., Rungta, N.: Symbolic PathFinder: integrating symbolic execution with model checking for Java bytecode analysis. Autom. Softw. Eng. 20(3), 391–425 (2013). https://doi.org/10.1007/s10515-013-0122-2
Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: LICS 2002, pp. 55–74. IEEE Computer Society (2002). https://doi.org/10.1109/LICS.2002.1029817
Rosner, N., Geldenhuys, J., Aguirre, N., Visser, W., Frias, M.F.: BLISS: improved symbolic execution by bounded lazy initialization with SAT support. IEEE Trans. Softw. Eng. 41(7), 639–660 (2015). https://doi.org/10.1109/TSE.2015.2389225
Schwartz, E.J., Avgerinos, T., Brumley, D.: All you ever wanted to know about dynamic taint analysis and forward symbolic execution (but Might Have Been Afraid to Ask). In: S&P 2010, pp. 317–331. IEEE Computer Society (2010). https://doi.org/10.1109/SP.2010.26
Tatsuta, M., Le, Q.L., Chin, W.-N.: Decision procedure for separation logic with inductive definitions and presburger arithmetic. In: Igarashi, A. (ed.) APLAS 2016. LNCS, vol. 10017, pp. 423–443. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47958-3_22
Visser, W., Pǎsǎreanu, C.S., Khurshid, S.: Test input generation with Java PathFinder. In: Avrunin, G.S., Rothermel, G. (eds.) ISSTA 2004, pp. 97–107. ACM (2004). https://doi.org/10.1145/1007512.1007526
Zheng, G., Le, Q.L., Nguyen, T., Phan, Q.S.: Automatic data structure repair using separation logic. In: JPF 2018 (2018)
Acknowledgments
This research is supported by the project 19-C220-SMU-001. The first author is also partially supported by the Google Summer of Code 2017 program.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Pham, L.H., Le, Q.L., Phan, QS., Sun, J., Qin, S. (2019). Enhancing Symbolic Execution of Heap-Based Programs with Separation Logic for Test Input Generation. In: Chen, YF., Cheng, CH., Esparza, J. (eds) Automated Technology for Verification and Analysis. ATVA 2019. Lecture Notes in Computer Science(), vol 11781. Springer, Cham. https://doi.org/10.1007/978-3-030-31784-3_12
Download citation
DOI: https://doi.org/10.1007/978-3-030-31784-3_12
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-31783-6
Online ISBN: 978-3-030-31784-3
eBook Packages: Computer ScienceComputer Science (R0)