Hello folks, we wrote up a quick blog post about a thing we’re doing to look for opt bugs:
https://blog.regehr.org/archives/2148
If this seems interesting to the community, I’ll likely ask Yuyou to give a short talk about this stuff at the next dev meeting.
John
3 Likes
Awesome results!
I’d definitely encourage you to give a talk at the dev meeting. I think this type of compiler correctness work which mixes formal methods and pragmatism is very very high impact and interesting.
One comment on the blog post itself… I think the example you chose to describe is a poor one for demonstrating the value of the approach. It brings up the whole topic of pointer provenience where we don’t really have agreement on what correct means. This requires either a bunch of context, or runs the risk of misleading readers into believing that the tool is only finding cases where the spec is ambiguous. I would suggest leading with a different example (where there’s no debate on the semantics), and moving the example you currently use to a footnote.
Thanks for the feedback Philip. I’m OK with this example but if a better one pops up, I’ll replace it!
John
IIRC, mutating regression tests came up in a discussion about correctness with fast-math-flags in IR.
I’m a bit afraid of what you’ll uncover if you steer the work in that direction, but I look forward to a presentation and more bug reports either way. 
Yeah we’ve seen some potentially interesting stuff come up that way for sure, but haven’t reported that much of it since the details are so fiddly. I’ll maybe move towards reporting more of those next time I do a fuzzing run. I find them exhausting to triage!!