Effect-driven QuickChecking of compilers

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

DOI

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
Volume1
PublisherAssociation for Computing Machinery
Publication date2017
Pages1-23
DOIs
StatePublished - 2017
SeriesProceedings of the Acm on Programming Languages
ISSN2475-1421
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:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
PDF
Download as HTML
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
HTML
Download as Word
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
Word

ID: 140633580