Public Repository

Last pushed: a month ago
Short Description
An effect-driven compiler tester for OCaml
Full Description

This image contains a prototype implementation of the effect-driven compiler tester described in the paper

Effect-Driven QuickChecking of Compilers
Jan Midtgaard, Mathias Nygaard Justesen, Patrick Kasting, Flemming Nielson, Hanne Riis Nielson
ICFP'17
http://janmidtgaard.dk/papers/Midtgaard-al:ICFP17-full.pdf (full version)

The source code of the prototype is also available here: https://github.com/jmid/efftester/

It is precompiled on top of a Debian 8 Linux distribution, with ocaml 4.04.1, opam, and the qcheck library (v.0.5.2).

Getting started:

  • Download and install Docker as described here: https://docs.docker.com/
  • Make sure that you can run docker run hello-world before proceeding.
  • You can run an instance of this Docker hub image as follows:
       $ docker run -ti jmid/ocaml-efftester bash
    
    This will start a bash shell within the virtual Linux box, in the directory of the precompiled build.

Step-by-step:

Run the effect-tester with ./effmain.native -v. This should produce output along
the lines of the following:

   $ ./effmain.native -v
  random seed: 379229741
  .........................................................................................x.....x.....x.....x.....x......law bytecode/native backends agree: 90 relevant cases (90 total)
    test `bytecode/native backends agree`
    failed on ≥ 1 cases:
    Some ((mod) 0 (let m = print_int in 0)) (after 13 shrink steps)

  failure (1 tests failed, ran 1 tests)
   $

The above is an example of reproducing a known bug (GPR#954)
mentioned in the included README.md.

You can confirm the difference in the behaviour of the code produced
by the two backends as follows:

  $ ocamlc -o mod.byte mod.ml 
  File "mod.ml", line 1, characters 13-14:
  Warning 26: unused variable m.
  $ ocamlopt -o mod.native mod.ml 
  File "mod.ml", line 1, characters 13-14:
  Warning 26: unused variable m.
  $ ./mod.byte 
  Fatal error: exception Division_by_zero
  $ ./mod.native 
  $

Different reruns should result in different mismatch-bugs being found.

We suggest to try multiple runs and compare the outputs. Sometimes the
produced counterexamples represent different issues and sometimes they
are different syntactic variations of the same underlying problem.

Docker Pull Command
Owner
jmid

Comments (0)