Advertisement

A Decidable Logic for Tree Data-Structures with Measurements

  • Xiaokang QiuEmail author
  • Yanjun WangEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11388)

Abstract

We present \({\textsc {Dryad}}_\textit{dec}\), a decidable logic that allows reasoning about tree data-structures with measurements. This logic supports user-defined recursive measure functions based on Max or Sum, and recursive predicates based on these measure functions, such as AVL trees or red-black trees. We prove that the logic’s satisfiability is decidable. The crux of the decidability proof is a small model property which allows us to reduce the satisfiability of \({\textsc {Dryad}}_\textit{dec}\) to quantifier-free linear arithmetic theory which can be solved efficiently using SMT solvers. We also show that \({\textsc {Dryad}}_\textit{dec}\) can encode a variety of verification and synthesis problems, including natural proof verification conditions for functional correctness of recursive tree-manipulating programs, legality conditions for fusing tree traversals, synthesis conditions for conditional linear-integer arithmetic functions. We developed the decision procedure and successfully solved 220+ \({\textsc {Dryad}}_\textit{dec}\) formulae raised from these application scenarios, including verifying functional correctness of programs manipulating AVL trees, red-black trees and treaps, checking the fusibility of height-based mutually recursive tree traversals, and counterexample-guided synthesis from linear integer arithmetic specifications. To our knowledge, \({\textsc {Dryad}}_\textit{dec}\) is the first decidable logic that can solve such a wide variety of problems requiring flexible combination of measure-related, data-related and shape-related properties for trees.

Notes

Acknowledgments

This material is based upon work supported by the National Science Foundation under Grant No. 1837023.

References

  1. 1.
  2. 2.
    Alur, R., et al.: Syntax-guided synthesis. In: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, 20–23 October 2013, pp. 1–8 (2013)Google Scholar
  3. 3.
    Bouajjani, A., Drăgoi, C., Enea, C., Sighireanu, M.: A logic-based framework for reasoning about composite data structures. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 178–195. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-04081-8_13CrossRefGoogle Scholar
  4. 4.
    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, 1006–1036 (2012)CrossRefGoogle Scholar
  5. 5.
    Chlipala, A.: Mostly-automated verification of low-level programs in computational separation logic. In: PLDI 2011, pp. 234–245 (2011)CrossRefGoogle Scholar
  6. 6.
    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).  https://doi.org/10.1007/978-3-642-23217-6_16CrossRefGoogle Scholar
  7. 7.
    Courcelle, B.: The monadic second-order logic of graphs. i. recognizable sets of finite graphs. Inf. Comput. 85(1), 12–75 (1990)MathSciNetCrossRefGoogle Scholar
  8. 8.
    Engelfriet, J., Maneth, S.: Output string languages of compositions of deterministic macro tree transducers. J. Comput. Syst. Sci. 64(2), 350–395 (2002)MathSciNetCrossRefGoogle Scholar
  9. 9.
    Goldfarb, M., Jo, Y., Kulkarni, M.: General transformations for GPU execution of tree traversals. In: Proceedings of the International Conference on High Performance Computing, Networking, Storage and Analysis (Supercomputing), SC 2013 (2013)Google Scholar
  10. 10.
    Haase, C., Ishtiaq, S., Ouaknine, J., Parkinson, M.J.: SeLoger: a tool for graph-based reasoning in separation logic. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 790–795. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-39799-8_55CrossRefGoogle Scholar
  11. 11.
    Habermehl, P., Iosif, R., Vojnar, T.: Automata-based verification of programs with tree updates. Acta Informatica 47(1), 1–31 (2010)MathSciNetCrossRefGoogle Scholar
  12. 12.
    Heinze, T.S., Møller, A., Strocco, F.: Type safety analysis for Dart. In: Proceedings of 12th Dynamic Languages Symposium (DLS), October 2016Google Scholar
  13. 13.
    Huang, K., Qiu, X., Tian, Q., Wang, Y.: Reconciling enumerative and symbolic search in syntax-guided synthesis (2018)Google Scholar
  14. 14.
    Iosif, R., Rogalewicz, A., Simacek, J.: The tree width of separation logic with recursive definitions. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 21–38. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-38574-2_2CrossRefGoogle Scholar
  15. 15.
    Itzhaky, S., Banerjee, A., Immerman, N., Nanevski, A., Sagiv, M.: Effectively-propositional reasoning about reachability in linked data structures. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 756–772. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-39799-8_53CrossRefGoogle Scholar
  16. 16.
    Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and Java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 41–55. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-20398-5_4CrossRefGoogle Scholar
  17. 17.
    Jo, Y., Kulkarni, M.: Enhancing locality for recursive traversals of recursive structures. In: Proceedings of the 2011 ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA 2011, pp. 463–482. ACM, New York (2011)Google Scholar
  18. 18.
    Jo, Y., Kulkarni, M.: Automatically enhancing locality for tree traversals with traversal splicing. In: Proceedings of the 2012 ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA 2012. ACM, New York (2012)Google Scholar
  19. 19.
    Kaki, G., Jagannathan, S.: A relational framework for higher-order shape analysis. In: Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, ICFP 2014, pp. 311–324. ACM, New York (2014)Google Scholar
  20. 20.
    Kawaguchi, M., Rondon, P., Jhala, R.: Type-based data structure verification. In: Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2009, pp. 304–315. ACM, New York (2009)Google Scholar
  21. 21.
    Klarlund, N., Schwartzbach, M.I.: Graph types. In: Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1993, pp. 196–205. ACM, New York (1993)Google Scholar
  22. 22.
    Lahiri, S., Qadeer, S.: Back to the future: revisiting precise program verification using SMT solvers. In: Principles of Programming Languages (POPL 2008), p. 16. Association for Computing Machinery, Inc., January 2008Google Scholar
  23. 23.
    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
  24. 24.
    Madhusudan, P., Parlato, G., Qiu, X.: Decidable logics combining heap structures and data. In: POPL 2011, pp. 611–622. ACM (2011)Google Scholar
  25. 25.
    Madhusudan, P., Qiu, X.: Efficient decision procedures for heaps using STRAND. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, pp. 43–59. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-23702-7_8CrossRefGoogle Scholar
  26. 26.
    Madhusudan, P., Qiu, X., Stefanescu, A.: Recursive proofs for inductive tree data-structures. In: POPL 2012, pp. 123–136. ACM (2012)Google Scholar
  27. 27.
    Maletti, A.: Compositions of extended top-down tree transducers. Inf. Comput. 206(9–10), 1187–1196 (2008)MathSciNetCrossRefGoogle Scholar
  28. 28.
    Manna, Z., Sipma, H.B., Zhang, T.: Verifying balanced trees. In: Artemov, S.N., Nerode, A. (eds.) LFCS 2007. LNCS, vol. 4514, pp. 363–378. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-72734-7_26CrossRefGoogle Scholar
  29. 29.
    McPeak, S., Necula, G.C.: Data structure specifications via local equality axioms. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 476–490. Springer, Heidelberg (2005).  https://doi.org/10.1007/11513988_47CrossRefGoogle Scholar
  30. 30.
    Meyerovich, L.A., Bodik, R.: Fast and parallel webpage layout. In: Proceedings of the 19th International Conference on World Wide Web, WWW 2010. pp. 711–720. ACM, New York (2010)Google Scholar
  31. 31.
    Meyerovich, L.A., Torok, M.E., Atkinson, E., Bodik, R.: Parallel schedule synthesis for attribute grammars. In: PPoPP 2013 (2013)Google Scholar
  32. 32.
    Møller, A., Schwartzbach, M.I.: The pointer assertion logic engine. In: PLDI 2001, pp. 221–231. ACM, June 2001Google Scholar
  33. 33.
    de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-78800-3_24CrossRefGoogle Scholar
  34. 34.
    Navarro Pérez, J.A., Rybalchenko, A.: Separation logic + superposition calculus = heap theorem prover. In: PLDI 2011, pp. 556–566 (2011)Google Scholar
  35. 35.
    O’Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 1–19. Springer, Heidelberg (2001).  https://doi.org/10.1007/3-540-44802-0_1CrossRefGoogle Scholar
  36. 36.
    Pek, E., Qiu, X., Madhusudan, P.: Natural proofs for data structure manipulation in C using separation logic. In: PLDI 2014, pp. 440–451. ACM (2014)Google Scholar
  37. 37.
    Petrashko, D., Lhoták, O., Odersky, M.: Miniphases: compilation using modular and efficient tree transformations. In: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, pp. 201–216. ACM, New York (2017)Google Scholar
  38. 38.
    Pham, T., Gacek, A., Whalen, M.W.: Reasoning about algebraic data types with abstractions. CoRR abs/1603.08769 (2016)Google Scholar
  39. 39.
    Philippaerts, P., Mühlberg, J.T., Penninckx, W., Smans, J., Jacobs, B., Piessens, F.: Software verification with VeriFast: industrial case studies. Sci. Comput. Program. 82, 77–97 (2014)CrossRefGoogle Scholar
  40. 40.
    Piskac, R., Wies, T., Zufferey, D.: Automating separation logic using SMT. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 773–789. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-39799-8_54CrossRefGoogle Scholar
  41. 41.
    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, Cham (2014).  https://doi.org/10.1007/978-3-319-08867-9_47CrossRefGoogle Scholar
  42. 42.
    Qiu, X., Garg, P., Stefanescu, A., Madhusudan, P.: Natural proofs for structure, data, and separation. In: PLDI 2013, pp. 231–242. ACM (2013)Google Scholar
  43. 43.
    Rajbhandari, S., et al.: A domain-specific compiler for a parallel multiresolution adaptive numerical simulation environment. In: Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis, SC 2016, pp. 40:1–40:12. IEEE Press, Piscataway (2016)Google Scholar
  44. 44.
    Rajbhandari, S., et al.: On fusing recursive traversals of Kd trees. In: Proceedings of the 25th International Conference on Compiler Construction, pp. 152–162. ACM (2016)Google Scholar
  45. 45.
    Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: LICS 2002, pp. 55–74. IEEE-CS (2002)Google Scholar
  46. 46.
    Rondon, P.M., Kawaguci, M., Jhala, R.: Liquid types. In: Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2008, pp. 159–169. ACM, New York (2008)Google Scholar
  47. 47.
    Saarikivi, O., Veanes, M., Mytkowicz, T., Musuvathi, M.: Fusing effectful comprehensions. SIGPLAN Not. 52(6), 17–32 (2017)CrossRefGoogle Scholar
  48. 48.
    Sakka, L., Sundararajah, K., Kulkarni, M.: Treefuser: a framework for analyzing and fusing general recursive tree traversals. Proc. ACM Program. Lang. 1(OOPSLA), 76:1–76:30 (2017)CrossRefGoogle Scholar
  49. 49.
    Suter, P., Dotta, M., Kuncak, V.: Decision procedures for algebraic data types with abstractions. In: POPL 2010, pp. 199–210 (2010)CrossRefGoogle Scholar
  50. 50.
    Suter, P., Köksal, A.S., Kuncak, V.: Satisfiability modulo recursive programs. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, pp. 298–315. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-23702-7_23CrossRefGoogle Scholar
  51. 51.
    Trakhtenbrot, B.A.: The impossibility of an algorithm for the decision problem for finite domains. Doklady Akad. Nauk SSSR (N.S.) 70, 569–572 (1950)MathSciNetzbMATHGoogle Scholar
  52. 52.
    Vazou, N., Bakst, A., Jhala, R.: Bounded refinement types. In: Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, pp. 48–61. ACM, New York (2015)Google Scholar
  53. 53.
    Vazou, N., Rondon, P.M., Jhala, R.: Abstract refinement types. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 209–228. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-37036-6_13CrossRefGoogle Scholar
  54. 54.
    Vazou, N., Seidel, E.L., Jhala, R.: LiquidHaskell: experience with refinement types in the real world. In: Haskell (2014)Google Scholar
  55. 55.
    Vazou, N., Seidel, E.L., Jhala, R., Vytiniotis, D., Peyton-Jones, S.: Refinement types for haskell. In: Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, ICFP 2014, pp. 269–282. ACM, New York (2014)Google Scholar
  56. 56.
    Vazou, N., et al.: Refinement reflection: complete verification with SMT. Proc. ACM Program. Lang. 2(2), 53 (2017)Google Scholar
  57. 57.
    Yorsh, G., Rabinovich, A., Sagiv, M., Meyer, A., Bouajjani, A.: A logic of reachable patterns in linked data-structures. In: Aceto, L., Ingólfsdóttir, A. (eds.) FoSSaCS 2006. LNCS, vol. 3921, pp. 94–110. Springer, Heidelberg (2006).  https://doi.org/10.1007/11690634_7CrossRefzbMATHGoogle Scholar
  58. 58.
    Zhang, T., Sipma, H.B., Manna, Z.: Decision procedures for term algebras with integer constraints. Inf. Comput. 204(10), 1526–1574 (2006)MathSciNetCrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Purdue UniversityWest LafayetteUSA

Personalised recommendations