Concolic testing engine

[rmonat]

trafficstars

This contains the work of @pierregoutagny done during his internship. I spent a few hours merging with master, I'm opening a PR to track upcoming breaking changes.

[rmonat]

Thank you for your comments @AltGr! I'll see what I can process and let Pierre handle the rest when he's back on the project.

[AltGr]

Ah I see you've added if Global.options.debug then Message.debug <xxx>; everywhere... I am curious with what you observed about the costs: without those,

• when %a is used the cost of the corresponding string conversion won't be paid when debug is off
• you still always pay the costs for %s, obviously. I can see in particular a Solver.string_of_model which looks coslty
• I think you will also always pay the cost of parsing the format-string (for % chars), even with debug off, because that is needed to know the arity of the function to apply (even if they are going to be ignored by ifprintf)

Because of the last item indeed there should be a gain even if the debug is a pure string... but I wouldn't have expected that to be significant ?

(* TODO QU RAPHAEL: turns out del_genericerror is pretty costly (~2x), so I decided to remove it because I think it is a safety/debugging check now *)

Yes, it will require a whole traversal and reconstruction of the term :/ Indeed, if you don't mind having the GenericError case still existing in your result type, you shouldn't bother. In the case of the "normal" interpreter it's not really a problem because the returned value is'nt expected to be so big (although at some point it got called on an intermediate closure and the cost was horrible). Also be careful with timings and bindlib, anything done with Bindlib.box_apply and consorts is actually delayed until you unbind/unbox.

[AltGr]

Ah my bad, after re-examining the code we don't actually use ifprintf but only a void ppf in debug mode, which means that indeed the full price of conversion is always paid. That will be easy to work around !