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

Cite as @frank-2024-generating (helia, typst) · \cite{frank-2024-generating} (LaTeX)
BibTeX
bibtex · 1 line
@article{frank-2024-generating, title={Generating Well-Typed Terms That Are Not “Useless”}, volume={8}, ISSN={2475-1421}, url={http://dx.doi.org/10.1145/3632919}, DOI={10.1145/3632919}, number={POPL}, journal={Proceedings of the ACM on Programming Languages}, publisher={Association for Computing Machinery (ACM)}, author={Frank, Justine and Quiring, Benjamin and Lampropoulos, Leonidas}, year={2024}, month=Jan, pages={2318–2339} }
hayagriva YAML (typst)
yaml · 19 lines
frank-2024-generating:
  type: article
  title: Generating Well-Typed Terms That Are Not “Useless”
  author:
  - Frank, Justine
  - Quiring, Benjamin
  - Lampropoulos, Leonidas
  date: 2024-01
  page-range: 2318-2339
  url: http://dx.doi.org/10.1145/3632919
  serial-number:
    doi: 10.1145/3632919
    issn: 2475-1421
  parent:
    type: periodical
    title: Proceedings of the ACM on Programming Languages
    publisher: Association for Computing Machinery (ACM)
    issue: POPL
    volume: 8
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.
PDF · DOI · pldb
External (37)
frank-2024-generating reference entries/refs/frank-2024-generating/frank-2024-generating.hel