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.
Supplemental Material
- Aws Albarghouthi, Sumit Gulwani, and Zachary Kincaid. 2013. Recursive Program Synthesis. In CAV (Part II) (LNCS), Vol. 9780. Springer, 934–950.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- Andrew W. Appel. 2011. Verified Software Toolchain - (Invited Talk). In ESOP (LNCS), Vol. 6602. Springer, 1–17. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Josh Berdine, Cristiano Calcagno, and Peter W. O’Hearn. 2005. Symbolic Execution with Separation Logic. In APLAS (LNCS), Vol. 3780. Springer, 52–68. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Josh Berdine, Byron Cook, and Samin Ishtiaq. 2011. SLAyer: Memory Safety for Systems-Level Code. In CAV (LNCS), Vol. 6806. Springer, 178–183. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- James Brotherston, Richard Bornat, and Cristiano Calcagno. 2008. Cyclic proofs of program termination in separation logic. In POPL. ACM, 101–112. Google ScholarDigital Library
- 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.Google Scholar
- James Brotherston, Nikos Gorogiannis, and Rasmus Lerchedahl Petersen. 2012. A Generic Cyclic Theorem Prover. In APLAS (LNCS), Vol. 7705. Springer, 350–367.Google Scholar
- 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. Google ScholarDigital Library
- Qinxiang Cao, Santiago Cuellar, and Andrew W. Appel. 2017. Bringing Order to the Separation Logic Jungle. In APLAS (LNCS), Vol. 10695. Springer, 190–211.Google Scholar
- 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. Google ScholarDigital Library
- Arthur Charguéraud. 2010. Program verification through characteristic formulae. In ICFP. ACM, 321–332. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Wei-Ngan Chin, Cristina David, and Cristian Gherghina. 2011. A HIP and SLEEK verification system. In OOPSLA (Companion). ACM, 9–10. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Adam Chlipala. 2011. Mostly-automated verification of low-level programs in computational separation logic. In PLDI. ACM, 234–245. Google ScholarDigital Library
- Coq Development Team. 2018. The Coq Proof Assistant Reference Manual - Version 8.8. Available at http://coq.inria.fr/ .Google Scholar
- Leonardo Mendonça de Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In TACAS (LNCS), Vol. 4963. Springer, 337–340.Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Dino Distefano and Matthew J. Parkinson. 2008. jStar: Towards Practical Verification for Java. In OOPSLA. ACM, 213–226. Google ScholarDigital Library
- Shingo Eguchi, Naoki Kobayashi, and Takeshi Tsukada. 2018. Automated Synthesis of Functional Programs with Auxiliary Functions. In APLAS. To appear.Google Scholar
- 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. Google ScholarDigital Library
- John K. Feser, Swarat Chaudhuri, and Isil Dillig. 2015. Synthesizing data structure transformations from input-output examples. In PLDI. ACM, 229–239. Google ScholarDigital Library
- Jonathan Frankle, Peter-Michael Osera, David Walker, and Steve Zdancewic. 2016. Example-directed synthesis: a typetheoretic interpretation. In POPL. ACM, 802–815. Google ScholarDigital Library
- Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, and Derek Dreyer. 2011. How to make ad hoc proof automation less ad hoc. In ICFP. ACM. Google ScholarDigital Library
- Sumit Gulwani, Susmit Jha, Ashish Tiwari, and Ramarathnam Venkatesan. 2011. Synthesis of loop-free programs. In PLDI. ACM, 62–73. Google ScholarDigital Library
- Aquinas Hobor and Jules Villard. 2013. The ramifications of sharing in data structures. In POPL. ACM, 523–536. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Swen Jacobs, Viktor Kuncak, and Philippe Suter. 2013. Reductions for Synthesis Procedures. In VMCAI (LNCS), Vol. 7737. Springer, 88–107. Google ScholarDigital Library
- Thomas Kleymann. 1999. Hoare Logic and Auxiliary Variables. Formal Asp. Comput. 11, 5 (1999), 541–566. Google ScholarCross Ref
- Etienne Kneuss, Ivan Kuraj, Viktor Kuncak, and Philippe Suter. 2013. Synthesis modulo recursive functions. In OOPSLA. ACM, 407–426. Google ScholarDigital Library
- Viktor Kuncak, Mikaël Mayer, Ruzica Piskac, and Philippe Suter. 2010. Complete Functional Synthesis. In PLDI. 316–329. Google ScholarDigital Library
- 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.Google Scholar
- Vu Le and Sumit Gulwani. 2014. FlashExtract: a framework for data extraction by examples. In PLDI. ACM, 542–553. Google ScholarDigital Library
- Xuan Bach Le and Aquinas Hobor. 2018. Logical Reasoning for Disjoint Permissions. In ESOP (LNCS), Vol. 10801. Springer, 385–414.Google Scholar
- Chin Soon Lee, Neil D. Jones, and Amir M. Ben-Amram. 2001. The size-change principle for program termination. In POPL. ACM, 81–92. Google ScholarDigital Library
- K. Rustan M. Leino. 2013. Developing verified programs with Dafny. In ICSE. ACM, 1488–1490. Google ScholarDigital Library
- K. Rustan M. Leino and Aleksandar Milicevic. 2012. Program Extrapolation with Jennisys. In OOPSLA. ACM, 411–430. Google ScholarDigital Library
- Chuck Liang and Dale Miller. 2009. Focusing and polarization in linear, intuitionistic, and classical logics. Theor. Comput. Sci. 410, 46 (2009), 4747–4768. Google ScholarDigital Library
- Parthasarathy Madhusudan, Xiaokang Qiu, and Andrei Stefanescu. 2012. Recursive proofs for inductive tree data-structures. In POPL. ACM, 123–136. Google ScholarDigital Library
- Zohar Manna and Richard J. Waldinger. 1980. A Deductive Approach to Program Synthesis. ACM Trans. Program. Lang. Syst. 2, 1 (1980), 90–121. Google ScholarDigital Library
- Per Martin-Löf. 1984. Intuitionistic Type Theory. Bibliopolis.Google Scholar
- Andrew McCreight. 2009. Practical Tactics for Separation Logic. In TPHOLs (LNCS), Vol. 5674. Springer, 343–358. Google ScholarDigital Library
- Chris Mellish and Steve Hardy. 1984. Integrating Prolog in the POPLOG Environment. In Implementations of Prolog. 147–162.Google Scholar
- Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, and Steve Zdancewic. 2018. Synthesizing bijective lenses. PACMPL 2, POPL (2018), 1:1–1:30. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Vijayaraghavan Murali, Letao Qi, Swarat Chaudhuri, and Chris Jermaine. 2018. Neural Sketch Learning for Conditional Program Generation. In ICLR. To appear.Google Scholar
- 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 .Google Scholar
- Aleksandar Nanevski, Viktor Vafeiadis, and Josh Berdine. 2010. Structuring the verification of heap-manipulating programs. In POPL. 261–274. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Peter-Michael Osera and Steve Zdancewic. 2015. Type-and-example-directed program synthesis. In PLDI. ACM, 619–630. Google ScholarDigital Library
- 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 .Google Scholar
- Ruzica Piskac, Thomas Wies, and Damien Zufferey. 2014a. Automating Separation Logic with Trees and Data. In CAV (LNCS), Vol. 8559. Springer, 711–728. Google ScholarDigital Library
- Ruzica Piskac, Thomas Wies, and Damien Zufferey. 2014b. GRASShopper - Complete Heap Verification with Mixed Specifications. In TACAS (LNCS), Vol. 8413. Springer, 124–139.Google Scholar
- Nadia Polikarpova, Ivan Kuraj, and Armando Solar-Lezama. 2016. Program synthesis from polymorphic refinement types. In PLDI. ACM, 522–538. Google ScholarDigital Library
- 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 Google ScholarDigital Library
- Oleksandr Polozov and Sumit Gulwani. 2015. FlashMeta: a framework for inductive program synthesis. In OOPSLA. ACM, 107–126. Google ScholarDigital Library
- Xiaokang Qiu, Pranav Garg, Andrei Stefanescu, and Parthasarathy Madhusudan. 2013. Natural proofs for structure, data, and separation. In PLDI. ACM, 231–242. Google ScholarDigital Library
- Xiaokang Qiu and Armando Solar-Lezama. 2017. Natural synthesis of provably-correct data-structure manipulations. PACMPL 1, OOPSLA (2017), 65:1–65:28. Google ScholarDigital Library
- 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.Google Scholar
- John C. Reynolds. 2002. Separation Logic: A Logic for Shared Mutable Data Structures. In LICS. IEEE Computer Society, 55–74. Google ScholarDigital Library
- Reuben N. S. Rowe and James Brotherston. 2017. Automatic cyclic termination proofs for recursive procedures in separation logic. In CPP. ACM, 53–65. Google ScholarDigital Library
- Gabriel Scherer. 2017. Search for Program Structure. In SNAPL (LIPIcs), Vol. 71. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 15:1–15:14.Google Scholar
- 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. Google ScholarDigital Library
- Calvin Smith and Aws Albarghouthi. 2016. MapReduce program synthesis. In PLDI. ACM, 326–340. Google ScholarDigital Library
- Sunbeom So and Hakjoo Oh. 2017. Synthesizing Imperative Programs from Examples Guided by Static Analysis. In SAS (LNCS), Vol. 10422. Springer, 364–381.Google Scholar
- Armando Solar-Lezama. 2013. Program sketching. STTT 15, 5-6 (2013), 475–495. Google ScholarDigital Library
- Saurabh Srivastava, Sumit Gulwani, and Jeffrey S. Foster. 2010. From program verification to program synthesis. In POPL. ACM, 313–326. Google ScholarDigital Library
- Emina Torlak and Rastislav Bodík. 2014. A lightweight symbolic virtual machine for solver-aided host languages. In PLDI. ACM, 530–541. Google ScholarDigital Library
- Rijnard van Tonder and Claire Le Goues. 2018. Static automated program repair for heap properties. In ICSE. ACM, 151–162. Google ScholarDigital Library
- Navid Yaghmazadeh, Yuepeng Wang, Isil Dillig, and Thomas Dillig. 2017. SQLizer: query synthesis from natural language. PACMPL 1, OOPSLA (2017), 63:1–63:26. Google ScholarDigital Library
Index Terms
- Structuring the synthesis of heap-manipulating programs
Recommendations
Cyclic program synthesis
PLDI 2021: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and ImplementationWe describe the first approach to automatically synthesizing heap-manipulating programs with auxiliary recursive procedures. Such procedures occur routinely in data structure transformations (e.g., flattening a tree into a list) or traversals of ...
Certifying the synthesis of heap-manipulating programs
Automated deductive program synthesis promises to generate executable programs from concise specifications, along with proofs of correctness that can be independently verified using third-party tools. However, an attempt to exercise this promise using ...
Structuring the verification of heap-manipulating programs
POPL '10Most systems based on separation logic consider only restricted forms of implication or non-separating conjunction, as full support for these connectives requires a non-trivial notion of variable context, inherited from the logic of bunched implications ...
Comments