Yu Feng
Thomas W. Reps
ABSTRACT
Component-based approaches to program synthesis assemble programs from a database of existing components, such as methods provided by an API. In this paper, we present a novel type-directed algorithm for component-based synthesis. The key novelty of our approach is the use of a compact Petri-net representation to model relationships between methods in an API. Given a target method signature S, our approach performs reachability analysis on the underlying Petri-net model to identify sequences of method calls that could be used to synthesize an implementation of S. The programs synthesized by our algorithm are guaranteed to type check and pass all test cases provided by the user.
We have implemented this approach in a tool called SyPet, and used it to successfully synthesize real-world programming tasks extracted from on-line forums and existing code repositories. We also compare SyPet with two state-of-the-art synthesis tools, namely InSynth and CodeHint, and demonstrate that SyPet can synthesize more programs in less time. Finally, we compare our approach with an alternative solution based on hypergraphs and demonstrate its advantages.
- SyPet. http://fredfeng.github.io/sypet/.Google Scholar
- A. Albarghouthi, S. Gulwani, and Z. Kincaid. Recursive program synthesis. In CAV, pages 934–950. Springer-Verlag, 2013.Google Scholar
- R. Alur, R. K. Brayton, T. A. Henzinger, S. Qadeer, and S. K. Rajamani. Partial-order reduction in symbolic state space exploration. In CAV, pages 340–351. Springer, 1997. Google ScholarDigital Library
- B. Avent, A. Ritz, and T. Murali. halp: Hypergraph Algorithms Package. http://murali-group.github.io/halp/.Google Scholar
- D. L. Berre and A. Parrain. The Sat4j library, release 2.2. Journal on Satisfiability, Boolean Modeling and Computation, pages 59–6, 2010.Google Scholar
- Y. Feng, R. Martins, Y. Wang, I. Dillig, and T. W. Reps. Component-Based Synthesis for Complex APIs. Technical report, University of Texas at Austin, 2016.Google Scholar
- J. K. Feser, S. Chaudhuri, and I. Dillig. Synthesizing data structure transformations from input-output examples. In PLDI, pages 229– 239. ACM, 2015. Google ScholarDigital Library
- A. Finkel. The minimal coverability graph for Petri nets. Springer, 1993.Google ScholarCross Ref
- J. Galenson, P. Reames, R. Bodik, B. Hartmann, and K. Sen. Codehint: Dynamic and interactive synthesis of code snippets. In ICSE, pages 653–663. ACM, 2014. Google ScholarDigital Library
- G. Gallo, G. Longo, and S. Pallottino. Directed hypergraphs and applications. Discrete Applied Mathematics, 42(2):177–201, 1993. Google ScholarDigital Library
- S. Gulwani. Automating string processing in spreadsheets using inputoutput examples. In POPL, pages 317–330. ACM, 2011. Google ScholarDigital Library
- S. Gulwani, S. Jha, A. Tiwari, and R. Venkatesan. Synthesis of loopfree programs. In PLDI, pages 62–73. ACM, 2011. Google ScholarDigital Library
- S. Gulwani, V. A. Korthikanti, and A. Tiwari. Synthesizing geometry constructions. In PLDI, pages 50–61. ACM, 2011. Google ScholarDigital Library
- S. Gulwani, W. R. Harris, and R. Singh. Spreadsheet data manipulation using examples. Communications of the ACM, 55(8):97–105, 2012. Google ScholarDigital Library
- T. Gvero and V. Kuncak. Synthesizing Java expressions from freeform queries. In OOPSLA, pages 416–432, 2015. Google ScholarDigital Library
- T. Gvero, V. Kuncak, and R. Piskac. Interactive synthesis of code snippets. In CAV, pages 418–423, 2011. Google ScholarDigital Library
- T. Gvero, V. Kuncak, I. Kuraj, and R. Piskac. Complete completion using types and weights. In PLDI, pages 27–38, 2013. Google ScholarDigital Library
- W. R. Harris and S. Gulwani. Spreadsheet table transformations from examples. In PLDI, pages 317–328. ACM, 2011. Google ScholarDigital Library
- K. Heljanko. Using logic programs with stable model semantics to solve deadlock and reachability problems for 1-safe petri nets. Fundamenta Informaticae, pages 247–268, 1999. Google ScholarDigital Library
- R. Holmes and G. C. Murphy. Using structural context to recommend source code examples. In ICSE, pages 117–125. ACM, 2005. Google ScholarDigital Library
- J. Jeon, X. Qiu, J. S. Foster, and A. Solar-Lezama. Jsketch: Sketching for Java. In ESEC/FSE, pages 934–937. ACM, 2015. Google ScholarDigital Library
- S. Jha, S. Gulwani, S. Seshia, and A. Tiwari. Oracle-guided component-based program synthesis. In ICSE, pages 215–224. IEEE, 2010. Google ScholarDigital Library
- R. Joshi, G. Nelson, and K. H. Randall. Denali: A goal-directed superoptimizer. In PLDI, pages 304–314. ACM, 2002. Google ScholarDigital Library
- R. M. Karp and R. E. Miller. Parallel program schemata. Journal of Computer and System Sciences, pages 147–195, 1969. Google ScholarDigital Library
- D. E. Knuth. A generalization of dijkstra’s algorithm. Inf. Process. Lett., 6(1):1–5, 1977.Google ScholarCross Ref
- D. Mandelin, L. Xu, R. Bod´ık, and D. Kimelman. Jungloid mining: helping to navigate the API jungle. In PLDI, pages 48–61. ACM, 2005. Google ScholarDigital Library
- K. L. McMillan. Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits. In CAV, pages 164– 177. Springer, 1993. Google ScholarDigital Library
- T. Murata. Petri nets: Properties, analysis and applications. Proceedings of the IEEE, 77(4):541–580, 1989.Google ScholarCross Ref
- L. R. Nielsen, K. A. Andersen, and D. Pretolani. Finding the K shortest hyperpaths. Computers & OR, 32:1477–1497, 2005. Google ScholarDigital Library
- S. Ogata, T. Tsuchiya, and T. Kikuno. SAT-based verification of safe petri nets. In ATVA, pages 79–92. Springer, 2004.Google Scholar
- P.-M. Osera and S. Zdancewic. Type-and-example-directed program synthesis. In PLDI, pages 619–630, 2015. Google ScholarDigital Library
- D. Peled. Ten years of partial order reduction. In CAV, pages 17–28. Springer, 1998. Google ScholarDigital Library
- D. Perelman, S. Gulwani, T. Ball, and D. Grossman. Type-directed completion of partial expressions. In PLDI, pages 275–286. ACM, 2012. Google ScholarDigital Library
- D. Perelman, S. Gulwani, D. Grossman, and P. Provost. Test-driven synthesis. In PLDI, page 43. ACM, 2014. Google ScholarDigital Library
- V. Raychev, M. T. Vechev, and E. Yahav. Code completion with statistical language models. In PLDI, page 44. ACM, 2014. Google ScholarDigital Library
- A. Reinking and R. Piskac. A type-directed approach to program repair. In CAV, pages 511–517, 2015.Google Scholar
- N. Sahavechaphan and K. Claypool. Xsnippet: Mining for sample code. In OOPSLA, pages 413–430. ACM, 2006. Google ScholarDigital Library
- R. Singh and S. Gulwani. Learning semantic string transformations from examples. PVLDB, pages 740–751, 2012. Google ScholarDigital Library
- R. Singh and S. Gulwani. Synthesizing number transformations from input-output examples. In CAV, pages 634–651. ACM, 2012. Google ScholarDigital Library
- A. Solar-Lezama. Program Synthesis By Sketching. PhD thesis, EECS Department, University of California, Berkeley, 2008. Google ScholarDigital Library
- A. Solar-Lezama, R. M. Rabbah, R. Bod´ık, and K. Ebcioglu. Programming by sketching for bit-streaming programs. In PLDI, pages 281–294. ACM, 2005. Google ScholarDigital Library
- A. Solar-Lezama, L. Tancau, R. Bodik, S. Seshia, and V. Saraswat. Combinatorial sketching for finite programs. In ASPLOS, pages 404– 415. ACM, 2006. Google ScholarDigital Library
- A. Solar-Lezama, G. Arnold, L. Tancau, R. Bod´ık, V. A. Saraswat, and S. A. Seshia. Sketching stencils. In PLDI, pages 167–178. ACM, 2007. Google ScholarDigital Library
- S. Thummalapenta and T. Xie. Parseweb: A programmer assistant for reusing open source code on the web. In ASE, pages 204–213. ACM, 2007. Google ScholarDigital Library
- R. Vallée-Rai, P. Co, E. Gagnon, L. J. Hendren, P. Lam, and V. Sundaresan. Soot - a Java bytecode optimization framework. In CASCON, page 13, 1999. Google ScholarDigital Library
- W. Vogler. Efficiency of asynchronous systems and read arcs in petri nets. In ICALP, pages 538–548. Springer, 1997. Google ScholarDigital Library
- Y. Wang, S. Lafortune, T. Kelly, M. Kudlur, and S. A. Mahlke. The theory of deadlock avoidance via discrete control. In POPL, pages 252–263. ACM, 2009. Google ScholarDigital Library
- K. Yessenov, Z. Xu, and A. Solar-Lezama. Data-driven synthesis for object-oriented frameworks. In OOPSLA, pages 65–82. ACM, 2011. Google ScholarDigital Library
- Component-based synthesis for complex APIs
Recommendations
FrAngel: component-based synthesis with control structures
In component-based program synthesis, the synthesizer generates a program given a library of components (functions). Existing component-based synthesizers have difficulty synthesizing loops and other control structures, and they often require formal ...
Component-based synthesis for complex APIs
POPL '17Component-based approaches to program synthesis assemble programs from a database of existing components, such as methods provided by an API. In this paper, we present a novel type-directed algorithm for component-based synthesis. The key novelty of ...
Can reactive synthesis and syntax-guided synthesis be friends?
SPLASH Companion 2021: Companion Proceedings of the 2021 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for HumanityWhile reactive synthesis and syntax-guided synthesis (SyGuS) have seen enormous progress in recent years, combining the two approaches has remained a challenge. In this work, we present the synthesis of reactive programs from Temporal Stream Logic ...
Comments