Extend signature DSL with a program printer

[jmid]

Each generated test input represents a program of a certain, stylistic form. Upon failure, it would be handy to be able to print the corresponding program

• without the interpretive overhead
• without a dependency on Lin

Bonus points for printing the program to a file.

Overall, this will make it easier to recreate and share any discovered issues.

[n-osborne]

I have recently given some though about this issue.

I was wondering whether we need (or would it be nice to have) a similar printer for STM? I believe this can be easily done with shared code.

I would suggest that we use PPrint, my experience with it is that it is really easy to use and build a nice representation for programs.

I'm happy to give it a try.

[jmid]

I gave this a shot for Lin in #115 and then paused. Here is a recap of my understanding (if I recall correctly):

It is relatively easy to run over the internal cmd structure and printf an OCaml representation of a counterexample. This is what #115 currently offers.

• To get a nice push-button user experience of "I generated a standalone counterexample for you in /tmp/test.ml" we need to include the code for init in such an extracted test, which is harder. I think one needs to walk the OCaml AST of the test to extract that and doing so means adding compilerlibs (unstable) or ppxlib (still not working for the 5.1 branch) as a dependency.
• More importantly: The bug I tried to extract a printed program for simply did not trigger when I just printed a program that would run the cmds! :shrug: So for this feature to be useful we also need to generate the interleaving search.

How can we solve the latter?

• We can emit direct code for all possible interleavings - which means the printed program will be exponentially larger.. :grimacing:
• Or we could keep a cmd representation and emit a much shorter search function that then spends exponential time searching like Lin and STM
• A third option could be to calculate the output of all interleavings at generation-time and emit an exponentially long list of acceptable outputs, that the generated program just has to search through.
• A fourth variant could be to collect acceptable outputs at generation time and generate an assert checking the output of each generated parallel cmd

Overall, I expect that we will meet the same challenges when trying to generate a parallel STM interleaving search. For this reason I think it makes sense to focus on solving these issues in #115 for Lin first rather than to start a parallel effort for STM.

The above focuses on the problem with a printer for a parallel Lin or STM mode (the init issue remains). A less ambitious project would be to implement a program printer for STM_sequential. Such a printer could potentially be useful to some STM users - but not so much for multicore testing.

As to using PPrint, as long as we are generating small stylistic programs I'd probably prefer to just use printf and keep our dependencies minimal. We are battling to install dependencies when testing any recent PRs on ocaml/ocaml trunk. I can see that it is useful when generating larger programs though.