Advertisement

Compositional Verification of Heap-Manipulating Programs Through Property-Guided Learning

  • Long H. PhamEmail author
  • Jun Sun
  • Quang Loc Le
Conference paper
First Online:
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11893)

Abstract

Analyzing and verifying heap-manipulating programs automatically is challenging. A key for fighting the complexity is to develop compositional methods. For instance, many existing verifiers for heap-manipulating programs require user-provided specification for each function in the program in order to decompose the verification problem. The requirement, however, often hinders the users from applying such tools. To overcome the issue, we propose to automatically learn heap-related program invariants in a property-guided way for each function call. The invariants are learned based on the memory graphs observed during test execution and improved through memory graph mutation. We implemented a prototype of our approach and integrated it with two existing program verifiers. The experimental results show that our approach enhances existing verifiers effectively in automatically verifying complex heap-manipulating programs with multiple function calls.

This is a preview of subscription content, log in to check access.

Notes

Acknowledgments

This research is supported by MOE research grant MOE2016-T2-2-123.

References

  1. 1.
    Facebook Infer. https://fbinfer.com
  2. 2.
  3. 3.
  4. 4.
    Albarghouthi, A., Berdine, J., Cook, B., Kincaid, Z.: Spatial interpolants. In: Vitek, J. (ed.) ESOP 2015, pp. 634–660 (2015).  https://doi.org/10.1007/978-3-662-46669-8_26CrossRefGoogle Scholar
  5. 5.
    Berdine, J., Cox, A., Ishtiaq, S., Wintersteiger, C.M.: Diagnosing abstraction failure for separation logic-based analyses. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012, pp. 155–173 (2012).  https://doi.org/10.1007/978-3-642-31424-7_16CrossRefGoogle Scholar
  6. 6.
    Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011, pp. 184–190 (2011).  https://doi.org/10.1007/978-3-642-22110-1_16CrossRefGoogle Scholar
  7. 7.
    Brockschmidt, M., Chen, Y., Kohli, P., Krishna, S., Tarlow, D.: Learning shape analysis. In: Ranzato, F. (ed.) SAS 2017, pp. 66–87 (2017).  https://doi.org/10.1007/978-3-319-66706-5_4CrossRefGoogle Scholar
  8. 8.
    Bshouty, N.H., Goldman, S.A., Mathias, H.D., Suri, S., Tamaki, H.: Noise-tolerant distribution-free learning of general geometric concepts. J. ACM 45(5), 863–890 (1998).  https://doi.org/10.1145/290179.290184MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Calcagno, C., Distefano, D., O’Hearn, P.W., Yang, H.: Compositional Shape Analysis by Means of Bi-Abduction. J. ACM 58(6), 26:1–26:66 (2011).  https://doi.org/10.1145/2049697.2049700MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Chin, W., 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
  11. 11.
    Cleve, H., Zeller, A.: Locating causes of program failures. In: Roman, G., Griswold, W.G., Nuseibeh, B. (eds.) ICSE 2005, pp. 342–351 (2005).  https://doi.org/10.1145/1062455.1062522
  12. 12.
    Distefano, D., Parkinson, M.J.: jStar: towards practical verification for Java. In: Harris, G.E. (ed.) OOPSLA 2008, pp. 213–226 (2008).  https://doi.org/10.1145/1449764.1449782
  13. 13.
    Dudka, K., Peringer, P., Vojnar, T.: Predator: a practical tool for checking manipulation of dynamic data structures using separation logic. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011, pp. 372–378 (2011).  https://doi.org/10.1007/978-3-642-22110-1_29CrossRefGoogle Scholar
  14. 14.
    Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S., Xiao, C.: The Daikon system for dynamic detection of likely invariants. Sci. Comput. Program 69(1–3), 35–45 (2007).  https://doi.org/10.1016/j.scico.2007.01.015MathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    Flanagan, C., Leino, K.R.M.: Houdini, an annotation assistant for ESC/Java. In: Oliveira, J.N., Zave, P. (eds.) FME 2001, pp. 500–517 (2001).  https://doi.org/10.1007/3-540-45251-6_29Google Scholar
  16. 16.
    Garg, P., Löding, C., Madhusudan, P., Neider, D.: Learning universally quantified invariants of linear data structures. In: Sharygina, N., Veith, H. (eds.) CAV 2013, pp. 813–829 (2013).  https://doi.org/10.1007/978-3-642-39799-8_57CrossRefGoogle Scholar
  17. 17.
    Garg, P., Löding, C., Madhusudan, P., Neider, D.: ICE: a robust framework for learning invariants. In: Biere, A., Bloem, R. (eds.) CAV 2014, pp. 69–87 (2014).  https://doi.org/10.1007/978-3-319-08867-9_5CrossRefGoogle Scholar
  18. 18.
    Garg, P., Neider, D., Madhusudan, P., Roth, D.: Learning invariants using decision trees and implication counterexamples. In: Bodík, R., Majumdar, R. (eds.) POPL 2016, pp. 499–512 (2016).  https://doi.org/10.1145/2837614.2837664
  19. 19.
    Ginsburg, S., Spanier, E.: Semigroups, presburger formulas, and languages. Pac. J. Math. 16(2), 285–296 (1966)MathSciNetCrossRefGoogle Scholar
  20. 20.
    Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Kroening, D., Pasareanu, C.S. (eds.) CAV 2015, pp. 343–361 (2015).  https://doi.org/10.1007/978-3-319-21690-4_20CrossRefGoogle Scholar
  21. 21.
    Holík, L., Hruska, M., Lengál, O., Rogalewicz, A., Simácek, J., Vojnar, T.: Forester: from heap shapes to automata predicates - (competition contribution). In: Legay, A., Margaria, T. (eds.) TACAS 2017, pp. 365–369 (2017).  https://doi.org/10.1007/978-3-662-54580-5_24CrossRefGoogle Scholar
  22. 22.
    Holík, L., Lengál, O., Rogalewicz, A., Simácek, J., Vojnar, T.: Fully automated shape analysis based on forest automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013, pp. 740–755 (2013).  https://doi.org/10.1007/978-3-642-39799-8_52CrossRefGoogle Scholar
  23. 23.
    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 (2001)CrossRefGoogle Scholar
  24. 24.
    Itzhaky, S., Bjørner, N., Reps, T.W., Sagiv, M., Thakur, A.V.: Property-directed shape analysis. In: Biere, A., Bloem, R. (eds.) CAV 2014, pp. 35–51 (2014).  https://doi.org/10.1007/978-3-319-08867-9_3CrossRefGoogle Scholar
  25. 25.
    Kulkarni, S., Mangal, R., Zhang, X., Naik, M.: Accelerating program analyses by cross-program training. In: Visser, E., Smaragdakis, Y. (eds.) OOPSLA 2016, pp. 359–377 (2016).  https://doi.org/10.1145/2983990.2984023
  26. 26.
    Le, Q.L., Gherghina, C., Qin, S., Chin, W.: Shape analysis via second-order bi-abduction. In: Biere, A., Bloem, R. (eds.) CAV 2014, pp. 52–68 (2014).  https://doi.org/10.1007/978-3-319-08867-9_4CrossRefGoogle Scholar
  27. 27.
    Le, Q.L., Sun, J., Chin, W.: Satisfiability modulo heap-based programs. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016, pp. 382–404 (2016).  https://doi.org/10.1007/978-3-319-41528-4_21CrossRefGoogle Scholar
  28. 28.
    Le, Q.L., Sun, J., Qin, S.: Frame inference for inductive entailment proofs in separation logic. In: Beyer, D., Huisman, M. (eds.) TACAS 2018, pp. 41–60 (2018).  https://doi.org/10.1007/978-3-319-89960-2_3CrossRefGoogle Scholar
  29. 29.
    Le, Q.L., Tatsuta, M., Sun, J., Chin, W.: A decidable fragment in separation logic with inductive predicates and arithmetic. In: Majumdar, R., Kuncak, V. (eds.) CAV 2017, pp. 495–517 (2017).  https://doi.org/10.1007/978-3-319-63390-9_26CrossRefGoogle Scholar
  30. 30.
    Le, T.C., Zheng, G., Nguyen, T.: SLING: using dynamic analysis to infer program invariants in separation logic. In: McKinley, K.S., Fisher, K. (eds.) PLDI 2019, pp. 788–801 (2019).  https://doi.org/10.1145/3314221.3314634
  31. 31.
    Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010, pp. 348–370 (2010). https://doi.org/10.1007/978-3-642-17511-4_20CrossRefGoogle Scholar
  32. 32.
    Li, Y., Tarlow, D., Brockschmidt, M., Zemel, R.S.: Gated graph sequence neural networks. CoRR abs/1511.05493 (2015)Google Scholar
  33. 33.
    Malík, V., Hruska, M., Schrammel, P., Vojnar, T.: Template-based verification of heap-manipulating programs. In: Bjørner, N., Gurfinkel, A. (eds.) FMCAD 2018, pp. 1–9 (2018).  https://doi.org/10.23919/FMCAD.2018.8603009
  34. 34.
    Miné, A.: The octagon abstract domain. High. Order. Symbolic Comput. 19(1), 31–100 (2006).  https://doi.org/10.1007/s10990-006-8609-1CrossRefzbMATHGoogle Scholar
  35. 35.
    Mühlberg, J.T., White, D.H., Dodds, M., Lüttgen, G., Piessens, F.: Learning assertions to verify linked-list programs. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015, pp. 37–52 (2015).  https://doi.org/10.1007/978-3-319-22969-0_3CrossRefGoogle Scholar
  36. 36.
    O’Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001, pp. 1–19 (2001).  https://doi.org/10.1007/3-540-44802-0_1Google Scholar
  37. 37.
    Pacheco, C., Lahiri, S.K., Ernst, M.D., Ball, T.: Feedback-directed random test generation. In: ICSE, vol. 2007, pp. 75–84 (2007).  https://doi.org/10.1109/ICSE.2007.37
  38. 38.
    Padhi, S., Sharma, R., Millstein, T.D.: Data-driven precondition inference with learned features. In: Krintz, C., Berger, E. (eds.) PLDI 2016, pp. 42–56 (2016).  https://doi.org/10.1145/2908080.2908099
  39. 39.
    Pham, L.H., Le, Q.L., Phan, Q.S., Sun, J.: Concolic testing heap-manipulating programs. In: FM 2019. To appearGoogle Scholar
  40. 40.
    Pham, L.H., Le, Q.L., Phan, Q.S., Sun, J., Qin, S.: Enhancing symbolic execution of heap-based programs with separation logic for test input generation. In: ATVA 2019. To appearGoogle Scholar
  41. 41.
    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
  42. 42.
    Pham, L.H., Thi, L.T., Sun, J.: Assertion generation through active learning. In: Duan, Z., Ong, L. (eds.) ICFEM 2017, pp. 174–191 (2017).  https://doi.org/10.1007/978-3-319-68690-5_11CrossRefGoogle Scholar
  43. 43.
    Piskac, R., Wies, T., Zufferey, D.: Automating separation logic with trees and data. In: Biere, A., Bloem, R. (eds.) CAV 2014, pp. 711–728 (2014).  https://doi.org/10.1007/978-3-319-08867-9_47CrossRefGoogle Scholar
  44. 44.
    Piskac, R., Wies, T., Zufferey, D.: GRASShopper - complete heap verification with mixed specifications. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014, pp. 124–139 (2014).  https://doi.org/10.1007/978-3-642-54862-8_9CrossRefGoogle Scholar
  45. 45.
    Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS, vol. 2002, pp. 55–74 (2002).  https://doi.org/10.1109/LICS.2002.1029817
  46. 46.
    Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. In: Appel, A.W., Aiken, A. (eds.) POPL 1999, pp. 105–118 (1999).  https://doi.org/10.1145/292540.292552
  47. 47.
    Zhu, H., Petri, G., Jagannathan, S.: Automatically learning shape specifications. In: Krintz, C., Berger, E. (eds.) PLDI 2016, pp. 491–507 (2016).  https://doi.org/10.1145/2908080.2908125

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Singapore University of Technology and DesignSingaporeSingapore
  2. 2.Singapore Management UniversitySingaporeSingapore
  3. 3.School of Computing & Digital TechnologiesTeesside UniversityMiddlesbroughUK

Personalised recommendations

Cite paper

Buy options