Reference. Generating Well-Typed Terms That Are Not “Useless”
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. We implement our algorithm demonstrating that it’s much closer to real programs in terms of argument usage rate, and we replicate a case study from the literature that finds bugs in the strictness analyzer of GHC, with our approach finding bugs four times faster than the current state-of-the-art local approach.
Cite
Cites 38 works (1 here)
With notes (1)
Finding and Understanding Bugs in C Compilers yangFindingUnderstandingBugs
Compilers should be correct. To improve the quality of C compilers, we created Csmith, a randomized test-case generation tool, and spent three years using it to find compiler bugs. During this period we reported more than 325 previously unknown bugs to compiler developers. Every compiler we tested was found to crash and also to silently generate wrong code when presented with valid input. In this paper we present our compiler-testing tool and the results of our bug-hunting study. Our first contribution is to advance the state of the art in compiler testing. Unlike previous tools, Csmith generates programs that cover a large subset of C while avoiding the undefined and unspecified behaviors that would destroy its ability to automatically find wrong-code bugs. Our second contribution is a collection of qualitative and quantitative results about the bugs we have found in open-source C compilers.
External (37)
- Reproduction Package for Article `Generating Well-Typed Terms That Are Not "Useless"` (2024)
- Random Testing of a Higher-Order Blockchain Language (Experience Report) (2022)
- A Formal Model of Checked C (2022)
- Analyzing binding extent in 3CPS (2022)
- Do Judge a Test by its Cover: Combining Combinatorial and Property-Based Testing (2021)
- Ray Tracing in One Weekend (2020)
- Generating Random Well-Typed Featherweight Java Programs Using QuickCheck (2019)
- Testing of OCaml exceptions by effect-driven generation of programs (2019)
- Achieving Safety Incrementally with Checked C (2019)
- Liveness-Driven Random Program Generation (2018)
- Program Synthesis (2017)
- Beginner's luck: a language for property-based generators (2017)
- Ode on a random urn (functional pearl) (2017)
- Effect-driven QuickChecking of compilers (2017)
- Boltzmann Samplers for Closed Simply-Typed Lambda Terms (2016)
- Program synthesis from polymorphic refinement types (2016)
- Generating constrained random data with uniform distribution (2015)
- Synthesizing data structure transformations from input-output examples (2015)
- Making Random Judgments: Automatically Generating Well-Typed Terms from the Definition of a Type-System (2015)
- Type-and-example-directed program synthesis (2015)
- On Type-directed Generation of Lambda Terms (2015)
- Boltzmann samplers for random generation of lambda terms (2014)
- Random Structured Test Data Generation for Black-Box Testing (2014)
- Finding test data with specific properties via metaheuristic search (2013)
- Advances in Lazy SmallCheck (2013)
- Feat (2012)
- Counting and generating lambda terms (2012)
- Every bit counts: The binary representation of typed data and programs (2012)
- Testing an optimising compiler by generating random lambda terms (2011)
- Smallcheck and lazy smallcheck (2008)
- Boltzmann Samplers for the Random Generation of Combinatorial Structures (2004)
- Featherweight Java (2001)
- Efficient and safe-for-space closure conversion (2000)
- Benchmarking implementations of functional languages with ‘Pseudoknot’, a float-intensive benchmark (1996)
- A calculus for the random generation of labelled combinatorial structures (1994)
- Representing Control: a Study of the CPS Transformation (1992)
- On a Test of Whether one of Two Random Variables is Stochastically Larger than the Other (1947)