PLDI 23 Supplementary Material

Results

The Coq formalization of our core language and its soundness theorem are included in the "proof" subdirectory.

Details about the 14 benchmarks used in our evaluation are given in individual folders with the same name as the benchmark; these folders are all located under "benchmarks". Each benchmark has a file prog.ml that presents the source code of the input test generator and a file ty.ml that defines the coverage type coverage type we want to check the generator implementation against and the coverage types of various library functions (notated with [@library]) used by the implementation. For example, there are three coverage types in RedBlackTree\ty.ml: two types that have name int_gen and bool_gen which are the types of primitive generators used by the implementation, and one type named rbtree_gen which is the type we want to check with the rbtree_gen program in RedBlackTree\prog.ml.
The directory synthesizer_input contains the input specification files for the 5 benchmarks for which we synthesized generators (shown in Figure 9). For E.g. the file synthesizer_input\sizedBST.spec is passed to the synthesizer as input.
The outputs generated by the synthesizer (containing multiple generators) are present in the formatted directories _synth_<benchmark_name>\prog.ml. E.g. the file \benchmarks\_synth_sizedbst\prog.ml contains the output of running the synthesizer on the file synthesizer_input\sizedBST.spec