Effect-driven QuickChecking of compilers

Research output: Research - peer-reviewArticle in proceedings – Annual report year: 2017



View graph of relations

How does one test a language implementation with QuickCheck (aka. property-based testing)? One approach is to generate programs following the grammar of the language. But in a statically-typed language such as OCaml too many of these candidate programs will be rejected as ill-typed by the type checker. As a refinement Pałka et al. propose to generate programs in a goal-directed, bottom-up reading up of the typing relation. We have written such a generator. However many of the generated programs has output that depend on the evaluation order, which is commonly under-specified in languages such as OCaml, Scheme, C, C++, etc. In this paper we develop a type and effect system for conservatively detecting evaluation-order dependence and propose its goal-directed reading as a generator of programs that are independent of evaluation order. We illustrate the approach by generating programs to test OCaml's two compiler backends against each other and report on a number of bugs we have found doing so.
Original languageEnglish
Title of host publicationProceedings of the Acm on Programming Languages
Number of pages23
PublisherAssociation for Computing Machinery
Publication date2017
StatePublished - 2017
SeriesProceedings of the Acm on Programming Languages
CitationsWeb of Science® Times Cited: No match on DOI

    Research areas

  • QuickCheck, compiler testing, type and effect system
Download as:
Download as PDF
Select render style:
Download as HTML
Select render style:
Download as Word
Select render style:

ID: 140633580