Advertisement

Enhancing Symbolic Execution of Heap-Based Programs with Separation Logic for Test Input Generation

  • Long H. PhamEmail author
  • Quang Loc Le
  • Quoc-Sang Phan
  • Jun Sun
  • Shengchao Qin
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11781)

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.

Notes

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.

References

  1. 1.
    Facebook Infer. https://fbinfer.com/
  2. 2.
  3. 3.
  4. 4.
  5. 5.
  6. 6.
  7. 7.
    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_5CrossRefGoogle Scholar
  8. 8.
    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
  9. 9.
    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
  10. 10.
    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
  11. 11.
    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
  12. 12.
    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.2049700MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    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.004CrossRefzbMATHGoogle Scholar
  14. 14.
    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
  15. 15.
    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
  16. 16.
    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-4CrossRefGoogle Scholar
  17. 17.
    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
  18. 18.
    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_16CrossRefGoogle Scholar
  19. 19.
    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_10CrossRefGoogle Scholar
  20. 20.
    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
  21. 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).  https://doi.org/10.1007/3-540-36577-X_40CrossRefzbMATHGoogle Scholar
  22. 22.
    King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976).  https://doi.org/10.1145/360248.360252MathSciNetCrossRefzbMATHGoogle Scholar
  23. 23.
    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_4CrossRefGoogle Scholar
  24. 24.
    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_21CrossRefGoogle Scholar
  25. 25.
    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_3CrossRefGoogle Scholar
  26. 26.
    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_26CrossRefGoogle Scholar
  27. 27.
    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_12CrossRefGoogle Scholar
  28. 28.
    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_22CrossRefzbMATHGoogle Scholar
  29. 29.
    Pham, L.H., Le, Q.L., Phan, Q.S., Sun, J.: Concolic testing heap-manipulating programs. In: FM 2019 (2019, to appear)Google Scholar
  30. 30.
    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
  31. 31.
    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-2CrossRefGoogle Scholar
  32. 32.
    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
  33. 33.
    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.2389225CrossRefGoogle Scholar
  34. 34.
    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
  35. 35.
    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_22CrossRefzbMATHGoogle Scholar
  36. 36.
    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
  37. 37.
    Zheng, G., Le, Q.L., Nguyen, T., Phan, Q.S.: Automatic data structure repair using separation logic. In: JPF 2018 (2018)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Long H. Pham
    • 1
    Email author
  • Quang Loc Le
    • 2
  • Quoc-Sang Phan
    • 3
  • Jun Sun
    • 4
  • Shengchao Qin
    • 2
  1. 1.Singapore University of Technology and DesignSingaporeSingapore
  2. 2.School of Computing & Digital TechnologiesTeesside UniversityMiddlesbroughUK
  3. 3.Synopsys, Inc.Mountain ViewUSA
  4. 4.Singapore Management UniversitySingaporeSingapore

Personalised recommendations