Thanks for finding all those bugs! I see the BI / SI / LI invariances you define are looking for program states that aren't present in the unoptimised program, while PI is looking for the absence of information that is in the unoptimised code. Do you think it will be possible to define and search for invariants that involve program states that are in the unoptimised program, but are presented in in the wrong way in the optimised program? For example variable values being presented at the wrong time, or stepping behaviour that misleads developers.
It'd be great to hunt those kinds of bugs, however it's hard to define what the "right" behaviour would be in those circumstances.
We are able to identify some kind of mis-stepping behaviour (look at Section 7-6). However, as you can imagine, we cannot catch all cases.
As you pointed out, a real problem is that there is no clear definition of what should be the semantic of debug information in the optimized binary (e.g., the compiler is free to squish several lines of source code into a smaller snippet of assembly language).
We are working to have more refined results in the near future .
What are your future plans for your framework? Will you spin it out into a startup? Will it only be used for writing future papers? Will it be released under an open source license?
We plan to use the framework to investigate more the correctness of debug information. Personally, I am not interested in startup and commercial opportunities.
Releasing the software is a step we are discussing.
We are not working on DWARF. However, we hope that the paper will spur a public discussion on these problems. Helping the entire community to have a more expressive standard.
It'd be great to hunt those kinds of bugs, however it's hard to define what the "right" behaviour would be in those circumstances.