Generating Well-Typed Terms That Are Not “Useless”
Article No.: 77, Pages 2318 - 2339
Abstract
Random generation of well-typed terms lies at the core of effective random testing of compilers for functional languages. Existing techniques have had success following a top-down type-oriented approach to generation that makes choices locally, which suffers from an inherent limitation: the type of an expression is often generated independently from the expression itself. Such generation frequently yields functions with argument types that cannot be used to produce a result in a meaningful way, leaving those arguments unused. Such "use-less" functions can hinder both performance, as the argument generation code is dead but still needs to be compiled, and effectiveness, as a lot of interesting optimizations are tested less frequently.
In this paper, we introduce a novel algorithm that is significantly more effective at generating functions that use their arguments. We formalize both the "local" and the "nonlocal" algorithms as step-relations in an extension of the simply-typed lambda calculus with type and arguments holes, showing how delaying the generation of types for subexpressions by allowing nonlocal generation steps leads to "useful" functions.
References
[1]
Gergö Barany. 2018. Liveness-Driven Random Program Generation. In Logic-Based Program Synthesis and Transformation, Fabio Fioravanti and John P. Gallagher (Eds.). Springer International Publishing, Cham. 112–127. isbn:978-3-319-94460-9
[2]
Maciej Bendkowski, Katarzyna Grygiel, and Paul Tarau. 2017. Boltzmann Samplers for Closed Simply-Typed Lambda Terms. In Practical Aspects of Declarative Languages, Yuliya Lierler and Walid Taha (Eds.). Springer International Publishing, Cham. 120–135. isbn:978-3-319-51676-9
[3]
Koen Claessen, Jonas Duregård, and Michal H. Palka. 2015. Generating constrained random data with uniform distribution. J. Funct. Program., 25 (2015), https://doi.org/10.1017/S0956796815000143
[4]
Samuel da Silva Feitosa, Rodrigo Geraldo Ribeiro, and Andre Rauber Du Bois. 2019. Generating Random Well-Typed Featherweight Java Programs Using QuickCheck. Electronic Notes in Theoretical Computer Science, 342 (2019), 3–20. issn:1571-0661 https://doi.org/10.1016/j.entcs.2019.04.002 The proceedings of CLEI 2018, the XLIV Latin American Computing Conference
[5]
Olivier Danvy and Andrzej Filinski. 1992. Representing Control: A study of the CPS transformation. Mathematical Structures in Computer Science, 2, 4 (1992), Dec., 361–391. https://doi.org/10.1017/S0960129500001535
[6]
Philippe Duchon, Philippe Flajolet, Guy Louchard, and Gilles Schaeffer. 2004. Boltzmann Samplers for the Random Generation of Combinatorial Structures. Combinatorics, Probability & Computing, 13, 4-5 (2004), 577–625. https://doi.org/10.1017/S0963548304006315
[7]
Jonas Duregård, Patrik Jansson, and Meng Wang. 2012. Feat: Functional Enumeration of Algebraic Types. In Proceedings of the 2012 Haskell Symposium (Haskell ’12). ACM, New York, NY, USA. 61–72. isbn:978-1-4503-1574-6 https://doi.org/10.1145/2364506.2364515
[8]
Robert Feldt and Simon M. Poulding. 2013. Finding test data with specific properties via metaheuristic search. In 24th International Symposium on Software Reliability Engineering. IEEE, 350–359. http://robertfeldt.net/publications/feldt_poulding_2013_finding_test_data_with_specific_properties.pdf
[9]
John K. Feser, Swarat Chaudhuri, and Isil Dillig. 2015. Synthesizing Data Structure Transformations from Input-output Examples. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’15). ACM, New York, NY, USA. 229–239. isbn:978-1-4503-3468-6 https://doi.org/10.1145/2737924.2737977
[10]
Burke Fetscher, Koen Claessen, Michal H. Palka, John Hughes, and Robert Bruce Findler. 2015. Making Random Judgments: Automatically Generating Well-Typed Terms from the Definition of a Type-System. In 24th European Symposium on Programming (Lecture Notes in Computer Science, Vol. 9032). Springer, 383–405. isbn:978-3-662-46668-1 http://users.eecs.northwestern.edu/~baf111/random-judgments/
[11]
Philippe Flajolet, Paul Zimmermann, and Bernard Van Cutsem. 1994. A Calculus for the Random Generation of Labelled Combinatorial Structures. Theor. Comput. Sci., 132, 2 (1994), 1–35. https://doi.org/10.1016/0304-3975(94)90226-7
[12]
Justin Frank, Benjamin Quiring, and Leonidas Lampropoulos. 2023. Reproduction Package for Article ‘Generating Well- Typed Terms That Are Not "Useless„. https://doi.org/10.5281/zenodo.8423782
[13]
Harrison Goldstein, John Hughes, Leonidas Lampropoulos, and Benjamin C. Pierce. 2021. Do Judge a Test by its Cover: Combining Combinatorial and Property-Based Testing.
[14]
Katarzyna Grygiel and Pierre Lescanne. 2012. Counting and generating lambda terms. CoRR, abs/1210.2610 (2012), arxiv:1210.2610. arxiv:1210.2610
[15]
Sumit Gulwani, Alex Polozov, and Rishabh Singh. 2017. Program Synthesis. 4, NOW.
[16]
Pieter H. Hartel, Marc Feeley, Martin Alt, Lennart Augustsson, and et al. 1996. Benchmarking implementations of functional languages with ‘Pseudoknot’, a float-intensive benchmark. Journal of Functional Programming, 6, 4 (1996), 621–655. https://doi.org/10.1017/S0956796800001891
[17]
Tram Hoang, Anton Trunov, Leonidas Lampropoulos, and Ilya Sergey. 2022. Random Testing of a Higher-Order Blockchain Language (Experience Report). In Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP).
[18]
Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. 2001. Featherweight Java: A Minimal Core Calculus for Java and GJ. ACM Trans. Program. Lang. Syst., 23, 3 (2001), may, 396–450. issn:0164-0925 https://doi.org/10.1145/503502.503505
[19]
Andrew J. Kennedy and Dimitrios Vytiniotis. 2012. Every bit counts: The binary representation of typed data and programs. Journal of Functional Programming, 22, 4-5 (2012), 529–573. https://research.microsoft.com/en-us/people/dimitris/jfpcoding.pdf
[20]
Leonidas Lampropoulos, Diane Gallois-Wong, Catalin Hritcu, John Hughes, Benjamin C. Pierce, and Li-yao Xia. 2017. Beginner’s Luck: a language for property-based generators. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017. 114–129. http://dl.acm.org/citation.cfm?id=3009868
[21]
Leonidas Lampropoulos, Antal Spector-Zabusky, and Kenneth Foner. 2017. Ode on a Random Urn (Functional Pearl). In Proceedings of the 10th ACM SIGPLAN International Symposium on Haskell (Haskell 2017). ACM, New York, NY, USA. 26–37. isbn:978-1-4503-5182-9 https://doi.org/10.1145/3122955.3122959
[22]
Pierre Lescanne. 2014. Boltzmann samplers for random generation of lambda terms. CoRR, abs/1404.3875 (2014), arxiv:1404.3875
[23]
Liyi Li, Yiyun Liu, Deena L. Postol, Leonidas Lampropoulos, David Van Horn, and Michael Hicks. 2022. A Formal Model of Checked C. In Proceedings of the Computer Security Foundations Symposium (CSF).
[24]
H. B. Mann and D. R. Whitney. 1947. On a Test of Whether one of Two Random Variables is Stochastically Larger than the Other. The Annals of Mathematical Statistics, 18, 1 (1947), 50 – 60. https://doi.org/10.1214/aoms/1177730491
[25]
Jan Midtgaard, Mathias Nygaard Justesen, Patrick Kasting, Flemming Nielson, and Hanne Riis Nielson. 2017. Effect-Driven QuickChecking of Compilers. Proc. ACM Program. Lang., 1, ICFP (2017), Article 15, aug, 23 pages. https://doi.org/10.1145/3110259
[26]
Peter-Michael Osera and Steve Zdancewic. 2015. Type-and-example-directed Program Synthesis. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’15). ACM, New York, NY, USA. 619–630. isbn:978-1-4503-3468-6 https://doi.org/10.1145/2737924.2738007
[27]
Michał H. Pał ka. 2014. Random Structured Test Data Generation for Black-Box Testing. Department of Computer Science and Engineering, Software Technology (Chalmers), Chalmers University of Technology,. isbn:978-91-7385-996-7 http://publications.lib.chalmers.se/records/fulltext/195849/195849.pdf 168
[28]
Michał H. Pał ka, Koen Claessen, Alejandro Russo, and John Hughes. 2011. Testing an Optimising Compiler by Generating Random Lambda Terms. In Proceedings of the 6th International Workshop on Automation of Software Test (AST ’11). ACM, New York, NY, USA. 91–97. isbn:978-1-4503-0592-1 https://doi.org/10.1145/1982595.1982615
[29]
Nadia Polikarpova, Ivan Kuraj, and Armando Solar-Lezama. 2016. Program Synthesis from Polymorphic Refinement Types. SIGPLAN Not., 51, 6 (2016), June, 522–538. issn:0362-1340 https://doi.org/10.1145/2980983.2908093
[30]
Benjamin Quiring, John Reppy, and Olin Shivers. 2022. Analyzing Binding Extent in 3CPS. Proc. ACM Program. Lang., 6, ICFP (2022), Article 114, aug, 29 pages. https://doi.org/10.1145/3547645
[31]
Jason S. Reich, Matthew Naylor, and Colin Runciman. 2012. Advances in Lazy SmallCheck. Presented at the 24th Symposium on Implementation and Application of Functional Languages. http://www.cs.york.ac.uk/fp/jason-docs/ReichNaylorRunciman2013.pdf
[32]
Murilo Giacometti Rocha. 2019. Testing of OCaml exceptions by effect-driven generation of programs. Master’s thesis. University of Edinburgh. https://project-archive.inf.ed.ac.uk/msc/20193481/msc_proj.pdf
[33]
Andrew Ruef, Leonidas Lampropoulos, Ian Sweet, David Tarditi, and Michael Hicks. 2019. Achieving Safety Incrementally with Checked C. In Proceedings of the Symposium on Principles of Security and Trust (POST).
[34]
Colin Runciman, Matthew Naylor, and Fredrik Lindblad. 2008. SmallCheck and Lazy SmallCheck: automatic exhaustive testing for small values. In 1st ACM SIGPLAN Symposium on Haskell. ACM, 37–48. isbn:978-1-60558-064-7 http://www.cs.york.ac.uk/fp/smallcheck/smallcheck.pdf
[35]
Zhong Shao and Andrew W. Appel. 2000. Efficient and Safe-for-Space Closure Conversion. ACM Transactions on Programming Languages and Systems, 22, 1 (2000), Jan., 129–161. issn:0164-0925 https://doi.org/10.1145/345099.345125
[36]
Peter Shirley. 2020. Ray Tracing in One Weekend. https://raytracing.github.io
[37]
Paul Tarau. 2015. On Type-directed Generation of Lambda Terms. In Proceedings of the Technical Communications of the 31st International Conference on Logic Programming (ICLP 2015), Cork, Ireland, August 31 - September 4, 2015. http://ceur-ws.org/Vol-1433/tc_12.pdf
[38]
Xuejun Yang, Yang Chen, Eric Eide, and John Regehr. 2011. Finding and understanding bugs in C compilers. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, June 4-8, 2011. 283–294. https://doi.org/10.1145/1993498.1993532
Index Terms
- Generating Well-Typed Terms That Are Not “Useless”
Recommendations
Generating Random Well-Typed Featherweight Java Programs Using QuickCheck
AbstractCurrently, Java is one of the most used programming language, being adopted in many large projects, where applications reach a level of complexity for which manual testing and human inspection are not enough to guarantee quality in software ...
Automatically generating the dynamic semantics of gradually typed languages
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming LanguagesMany language designers have adopted gradual typing. However, there remains open questions regarding how to gradualize languages. Cimini and Siek (2016) created a methodology and algorithm to automatically generate the type system of a gradually typed ...
Generating tests to analyse dynamically-typed programs
ASE '19: Proceedings of the 34th IEEE/ACM International Conference on Automated Software EngineeringThe increasing popularity of dynamically-typed programming languages, such as JavaScript or Python, requires specific support methods for developers to avoid pitfalls arising from the dynamic nature of these languages. Static analyses are frequently ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
January 2024
2820 pages
Copyright © 2024 Owner/Author.
This work is licensed under a Creative Commons Attribution 4.0 International License.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 05 January 2024
Published in PACMPL Volume 8, Issue POPL
Check for updates
Badges
Author Tags
Qualifiers
- Research-article
Funding Sources
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 587Total Downloads
- Downloads (Last 12 months)587
- Downloads (Last 6 weeks)44
Reflects downloads up to 09 Jan 2025
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in