Structuring the synthesis of heap-manipulating programs

Abstract

This paper describes a deductive approach to synthesizing imperative programs with pointers from declarative specifications expressed in Separation Logic. Our synthesis algorithm takes as input a pair of assertions—a pre- and a postcondition—which describe two states of the symbolic heap, and derives a program that transforms one state into the other, guided by the shape of the heap. Our approach to program synthesis is grounded in proof theory: we introduce the novel framework of Synthetic Separation Logic (SSL), which generalises the classical notion of heap entailment P ⊢ Q to incorporate a possibility of transforming a heap satisfying an assertion P into a heap satisfying an assertion Q. A synthesized program represents a proof term for a transforming entailment statement P ↝ Q, and the synthesis procedure corresponds to a proof search. The derived programs are, thus, correct by construction, in the sense that they satisfy the ascribed pre/postconditions, and are accompanied by complete proof derivations, which can be checked independently.

We have implemented a proof search engine for SSL in a form of the program synthesizer called SuSLik. For efficiency, the engine exploits properties of SSL rules, such as invertibility and commutativity of rule applications on separate heaps, to prune the space of derivations it has to consider. We explain and showcase the use of SSL on characteristic examples, describe the design of SuSLik, and report on our experience of using it to synthesize a series of benchmark programs manipulating heap-based linked data structures.

References

1. Aws Albarghouthi, Sumit Gulwani, and Zachary Kincaid. 2013. Recursive Program Synthesis. In CAV (Part II) (LNCS), Vol. 9780. Springer, 934–950.
2. Rajeev Alur, Rastislav Bodík, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. 2013. Syntax-guided synthesis. In FMCAD. IEEE, 1–8.
3. Rajeev Alur, Arjun Radhakrishna, and Abhishek Udupa. 2017. Scaling Enumerative Program Synthesis via Divide and Conquer. In TACAS (Part I) (LNCS), Vol. 10205. Springer, 319–336.
4. Timos Antonopoulos, Nikos Gorogiannis, Christoph Haase, Max I. Kanovich, and Joël Ouaknine. 2014. Foundations for Decision Problems in Separation Logic with General Inductive Predicates. In FOSSACS (LNCS), Vol. 8412. Springer, 411–425.
5. Andrew W. Appel. 2011. Verified Software Toolchain - (Invited Talk). In ESOP (LNCS), Vol. 6602. Springer, 1–17.
6. Andrew W. Appel, Robert Dockins, Aquinas Hobor, Lennart Beringer, Josiah Dodds, Gordon Stewart, Sandrine Blazy, and Xavier Leroy. 2014. Program Logics for Certified Compilers. Cambridge University Press.
7. Andrew W. Appel, Paul-André Melliès, Christopher D. Richards, and Jérôme Vouillon. 2007. A very modal model of a modern, major, general type system. In POPL. ACM, 109–122.
8. Josh Berdine, Cristiano Calcagno, and Peter W. O’Hearn. 2005. Symbolic Execution with Separation Logic. In APLAS (LNCS), Vol. 3780. Springer, 52–68.
9. Josh Berdine, Cristiano Calcagno, and Peter W. O’Hearn. 2006. Smallfoot: Modular Automatic Assertion Checking with Separation Logic. In FMCO (LNCS), Vol. 4111. Springer, 115–137.
10. Josh Berdine, Byron Cook, and Samin Ishtiaq. 2011. SLAyer: Memory Safety for Systems-Level Code. In CAV (LNCS), Vol. 6806. Springer, 178–183.
11. Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, and Mihaela Sighireanu. 2012. Accurate Invariant Checking for Programs Manipulating Lists and Arrays with Infinite Data. In ATVA (LNCS), Vol. 7561. Springer, 167–182.
12. James Brotherston, Richard Bornat, and Cristiano Calcagno. 2008. Cyclic proofs of program termination in separation logic. In POPL. ACM, 101–112.
13. James Brotherston, Nikos Gorogiannis, and Max I. Kanovich. 2017. Biabduction (and Related Problems) in Array Separation Logic. In CADE (LNCS), Vol. 10395. Springer, 472–490.
14. James Brotherston, Nikos Gorogiannis, and Rasmus Lerchedahl Petersen. 2012. A Generic Cyclic Theorem Prover. In APLAS (LNCS), Vol. 7705. Springer, 350–367.
15. Cristiano Calcagno and Dino Distefano. 2011. Infer: An Automatic Program Verifier for Memory Safety of C Programs. In NASA Formal Methods (LNCS), Vol. 6617. Springer, 459–465.
16. Qinxiang Cao, Santiago Cuellar, and Andrew W. Appel. 2017. Bringing Order to the Separation Logic Jungle. In APLAS (LNCS), Vol. 10695. Springer, 190–211.
17. Franck Cassez and Anthony M. Sloane. 2017. ScalaSMT: Satisfiability Modulo Theory in Scala (Tool Paper). In Proceedings of the 8th ACM SIGPLAN International Symposium on Scala. 51–55.
18. Arthur Charguéraud. 2010. Program verification through characteristic formulae. In ICFP. ACM, 321–332.
19. Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich. 2015. Using Crash Hoare logic for certifying the FSCQ file system. In SOSP. ACM, 18–37.
20. Wei-Ngan Chin, Cristina David, and Cristian Gherghina. 2011. A HIP and SLEEK verification system. In OOPSLA (Companion). ACM, 9–10.
21. Wei-Ngan Chin, Cristina David, Huu Hai Nguyen, and Shengchao Qin. 2012. Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Sci. Comput. Program. 77, 9 (2012), 1006–1036.
22. Adam Chlipala. 2011. Mostly-automated verification of low-level programs in computational separation logic. In PLDI. ACM, 234–245.
23. Coq Development Team. 2018. The Coq Proof Assistant Reference Manual - Version 8.8. Available at http://coq.inria.fr/ .
24. Leonardo Mendonça de Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In TACAS (LNCS), Vol. 4963. Springer, 337–340.
25. Benjamin Delaware, Clément Pit-Claudel, Jason Gross, and Adam Chlipala. 2015. Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant. In POPL. ACM, 689–700.
26. Dino Distefano and Matthew J. Parkinson. 2008. jStar: Towards Practical Verification for Java. In OOPSLA. ACM, 213–226.
27. Shingo Eguchi, Naoki Kobayashi, and Takeshi Tsukada. 2018. Automated Synthesis of Functional Programs with Auxiliary Functions. In APLAS. To appear.
28. Yu Feng, Ruben Martins, Jacob Van Geffen, Isil Dillig, and Swarat Chaudhuri. 2017. Component-based synthesis of table consolidation and transformation tasks from examples. In PLDI. ACM, 422–436.
29. John K. Feser, Swarat Chaudhuri, and Isil Dillig. 2015. Synthesizing data structure transformations from input-output examples. In PLDI. ACM, 229–239.
30. Jonathan Frankle, Peter-Michael Osera, David Walker, and Steve Zdancewic. 2016. Example-directed synthesis: a typetheoretic interpretation. In POPL. ACM, 802–815.
31. Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, and Derek Dreyer. 2011. How to make ad hoc proof automation less ad hoc. In ICFP. ACM.
32. Sumit Gulwani, Susmit Jha, Ashish Tiwari, and Ramarathnam Venkatesan. 2011. Synthesis of loop-free programs. In PLDI. ACM, 62–73.
33. Aquinas Hobor and Jules Villard. 2013. The ramifications of sharing in data structures. In POPL. ACM, 523–536.
34. Shachar Itzhaky, Rohit Singh, Armando Solar-Lezama, Kuat Yessenov, Yongquan Lu, Charles E. Leiserson, and Rezaul Alam Chowdhury. 2016. Deriving divide-and-conquer dynamic programming algorithms using solver-aided transformations. In OOPSLA. ACM, 145–164.
35. Bart Jacobs, Jan Smans, Pieter Philippaerts, Frédéric Vogels, Willem Penninckx, and Frank Piessens. 2011. VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java. In NASA Formal Methods (LNCS), Vol. 6617. Springer, 41–55.
36. Swen Jacobs, Viktor Kuncak, and Philippe Suter. 2013. Reductions for Synthesis Procedures. In VMCAI (LNCS), Vol. 7737. Springer, 88–107.
37. Thomas Kleymann. 1999. Hoare Logic and Auxiliary Variables. Formal Asp. Comput. 11, 5 (1999), 541–566.
38. Etienne Kneuss, Ivan Kuraj, Viktor Kuncak, and Philippe Suter. 2013. Synthesis modulo recursive functions. In OOPSLA. ACM, 407–426.
39. Viktor Kuncak, Mikaël Mayer, Ruzica Piskac, and Philippe Suter. 2010. Complete Functional Synthesis. In PLDI. 316–329.
40. Ton Chanh Le, Cristian Gherghina, Aquinas Hobor, and Wei-Ngan Chin. 2014. A Resource-Based Logic for Termination and Non-termination Proofs. In ICFEM (LNCS), Vol. 8829. Springer, 267–283.
41. Vu Le and Sumit Gulwani. 2014. FlashExtract: a framework for data extraction by examples. In PLDI. ACM, 542–553.
42. Xuan Bach Le and Aquinas Hobor. 2018. Logical Reasoning for Disjoint Permissions. In ESOP (LNCS), Vol. 10801. Springer, 385–414.
43. Chin Soon Lee, Neil D. Jones, and Amir M. Ben-Amram. 2001. The size-change principle for program termination. In POPL. ACM, 81–92.
44. K. Rustan M. Leino. 2013. Developing verified programs with Dafny. In ICSE. ACM, 1488–1490.
45. K. Rustan M. Leino and Aleksandar Milicevic. 2012. Program Extrapolation with Jennisys. In OOPSLA. ACM, 411–430.
46. Chuck Liang and Dale Miller. 2009. Focusing and polarization in linear, intuitionistic, and classical logics. Theor. Comput. Sci. 410, 46 (2009), 4747–4768.
47. Parthasarathy Madhusudan, Xiaokang Qiu, and Andrei Stefanescu. 2012. Recursive proofs for inductive tree data-structures. In POPL. ACM, 123–136.
48. Zohar Manna and Richard J. Waldinger. 1980. A Deductive Approach to Program Synthesis. ACM Trans. Program. Lang. Syst. 2, 1 (1980), 90–121.
49. Per Martin-Löf. 1984. Intuitionistic Type Theory. Bibliopolis.
50. Andrew McCreight. 2009. Practical Tactics for Separation Logic. In TPHOLs (LNCS), Vol. 5674. Springer, 343–358.
51. Chris Mellish and Steve Hardy. 1984. Integrating Prolog in the POPLOG Environment. In Implementations of Prolog. 147–162.
52. Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, and Steve Zdancewic. 2018. Synthesizing bijective lenses. PACMPL 2, POPL (2018), 1:1–1:30.
53. Peter Müller, Malte Schwerhoff, and Alexander J. Summers. 2016. Viper: A Verification Infrastructure for Permission-Based Reasoning. In VMCAI (LNCS), Vol. 9583. Springer, 41–62.
54. Vijayaraghavan Murali, Letao Qi, Swarat Chaudhuri, and Chris Jermaine. 2018. Neural Sketch Learning for Conditional Program Generation. In ICLR. To appear.
55. Aleksandar Nanevski. 2016. Separation Logic and Concurrency. (June 2016). Lecture notes for Oregon Programming Languages Summer School (OPLSS). Available from http://software.imdea.org/~aleks/oplss16/notes.pdf .
56. Aleksandar Nanevski, Viktor Vafeiadis, and Josh Berdine. 2010. Structuring the verification of heap-manipulating programs. In POPL. 261–274.
57. Huu Hai Nguyen, Cristina David, Shengchao Qin, and Wei-Ngan Chin. 2007. Automated Verification of Shape and Size Properties Via Separation Logic. In VMCAI (LNCS), Vol. 4349. Springer, 251–266.
58. Peter W. O’Hearn, John C. Reynolds, and Hongseok Yang. 2001. Local Reasoning about Programs that Alter Data Structures. In CSL (LNCS), Vol. 2142. Springer, 1–19.
59. Peter W. O’Hearn, Hongseok Yang, and John C. Reynolds. 2009. Separation and information hiding. ACM Trans. Program. Lang. Syst. 31, 3 (2009), 11:1–11:50.
60. Peter-Michael Osera and Steve Zdancewic. 2015. Type-and-example-directed program synthesis. In PLDI. ACM, 619–630.
61. Frank Pfenning. 2010. Lecture Notes on Focusing. (June 2010). Oregon Summer School on Proof Theory Foundations (OPLSS). Available from https://www.cs.cmu.edu/~fp/courses/oregon-m10/04-focusing.pdf .
62. Ruzica Piskac, Thomas Wies, and Damien Zufferey. 2014a. Automating Separation Logic with Trees and Data. In CAV (LNCS), Vol. 8559. Springer, 711–728.
63. Ruzica Piskac, Thomas Wies, and Damien Zufferey. 2014b. GRASShopper - Complete Heap Verification with Mixed Specifications. In TACAS (LNCS), Vol. 8413. Springer, 124–139.
64. Nadia Polikarpova, Ivan Kuraj, and Armando Solar-Lezama. 2016. Program synthesis from polymorphic refinement types. In PLDI. ACM, 522–538.
65. Nadia Polikarpova and Ilya Sergey. 2018. Structuring the Synthesis of Heap-Manipulating Programs – Extended Version. CoRR abs/1807.07022 (2018). arXiv: 1807.07022 http://arxiv.org/abs/1807.07022
66. Oleksandr Polozov and Sumit Gulwani. 2015. FlashMeta: a framework for inductive program synthesis. In OOPSLA. ACM, 107–126.
67. Xiaokang Qiu, Pranav Garg, Andrei Stefanescu, and Parthasarathy Madhusudan. 2013. Natural proofs for structure, data, and separation. In PLDI. ACM, 231–242.
68. Xiaokang Qiu and Armando Solar-Lezama. 2017. Natural synthesis of provably-correct data-structure manipulations. PACMPL 1, OOPSLA (2017), 65:1–65:28.
69. Andrew Reynolds, Morgan Deters, Viktor Kuncak, Cesare Tinelli, and Clark W. Barrett. 2015. Counterexample-Guided Quantifier Instantiation for Synthesis in SMT. In CAV (Part II) (LNCS), Vol. 9207. Springer, 198–216.
70. John C. Reynolds. 2002. Separation Logic: A Logic for Shared Mutable Data Structures. In LICS. IEEE Computer Society, 55–74.
71. Reuben N. S. Rowe and James Brotherston. 2017. Automatic cyclic termination proofs for recursive procedures in separation logic. In CPP. ACM, 53–65.
72. Gabriel Scherer. 2017. Search for Program Structure. In SNAPL (LIPIcs), Vol. 71. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 15:1–15:14.
73. Xujie Si, Woosuk Lee, Richard Zhang, Aws Albarghouthi, Paris Koutris, and Mayur Naik. 2018. Syntax-Guided Synthesis of Datalog Programs. In ESEC/SIGSOFT FSE. ACM, 515–527.
74. Calvin Smith and Aws Albarghouthi. 2016. MapReduce program synthesis. In PLDI. ACM, 326–340.
75. Sunbeom So and Hakjoo Oh. 2017. Synthesizing Imperative Programs from Examples Guided by Static Analysis. In SAS (LNCS), Vol. 10422. Springer, 364–381.
76. Armando Solar-Lezama. 2013. Program sketching. STTT 15, 5-6 (2013), 475–495.
77. Saurabh Srivastava, Sumit Gulwani, and Jeffrey S. Foster. 2010. From program verification to program synthesis. In POPL. ACM, 313–326.
78. Emina Torlak and Rastislav Bodík. 2014. A lightweight symbolic virtual machine for solver-aided host languages. In PLDI. ACM, 530–541.
79. Rijnard van Tonder and Claire Le Goues. 2018. Static automated program repair for heap properties. In ICSE. ACM, 151–162.
80. Navid Yaghmazadeh, Yuepeng Wang, Isil Dillig, and Thomas Dillig. 2017. SQLizer: query synthesis from natural language. PACMPL 1, OOPSLA (2017), 63:1–63:26.

Index Terms

• Software and its engineering

  • Software creation and management

    • Software development techniques

      • Automatic programming

• Theory of computation

  • Logic

    • Logic and verification