jmid/ocaml-efftester repository overview

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

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.