Hi Maxime et al.,Thanks for mailing, your project sounds very interesting! I'd be happy to read over a draft of a paper on this topic if that would be useful to you.
I have added Xuejun Yang to this mail, he is the best one to decide whether or not Csmith can trigger your CompCert mutant.
The CompCert bugs that Csmith did trigger had a different character, they were most often in the frontend and also in the area of integer promotions, where Xavier had admitted a few innocuous-looking properties that turned out to be wrong, if I remember correctly.
The unfortunately situation is that if you insist that Csmith catches a particular bug -- even a very nasty one -- you will often be disappointed. The development of Csmith was a years-long process of eliminating classes of bugs that it could not find. However, there appears to be a nearly limitless supply of categories of compiler bugs. As you might imagine, this is very dissatisfying to us. On the other hand, it serves as a strong motivation to do research on testcase generation and on proved systems. There is a lot of work still to do.
This link is to the preliminary version of a paper that has been accepted to PLDI this year, it may be interesting for you:
http://mehrdadafshari.com/emi/paper.pdf John On 02/20/2014 12:57 AM, Maxime Dénès wrote:
Hello, I am working in Benjamin Pierce's group at UPenn. We have recently been designing a methodology based on mutation to evaluate testing frameworks. As an experiment, we took compcert and tried to insert some "plausible" bugs, to see if CSmith would find them. We were surprised that removing a precondition for tail call optimizations does not seem to be caught by CSmith. I attach a patch for Compcert 2.1 which makes it do this optimization incorrectly in some cases, and a program witnessing the bug. What do you think of this? Would you expect CSmith to be able to find it? Best, Maxime.