Cleanup reporting of dead code

[michael-schwarz]

This addresses the shortcomings identified in #94:

• For dead branches, insert a message that the dead branch may have been inserted by CIL if the synthetic attribute of the location is set.
• Add new option alldeadcode that also reports on dead code in branches over constants that are not taken. Include hint that this option exists when print_dead_code is on, but alldeadcode is off.

TODO:

• Wait for Add option removeBranchingOnConstants cil#103 to be merged

Closes #94.

[sim642]

I'm not sure if loc.synthetic is the appropriate thing to base this output on, because the location being synthetic doesn't necessarily correspond to an If that CIL created. In some cases it does, e.g. in a && b, when b has a constant value, then there's a dead branch in that CIL-created If and its location is synthetic because there's no program point in the original source code between the evaluation of a and b, which is why the location is synthetic.

I haven't checked with this PR, but I'm suspicious about cases like the following:

• Again in a && b, when a has a constant value and there's a dead branch in that CIL-created If, then there is a program point (right before the whole expression) where an invariant assert (which the synthetic locations are for) about a could be inserted. So that location needn't be synthetic, it might currently be since synthetic locations are probably assigned more crudely than necessary, but if that is ever improved, then the output about a dead branch would actually become more wrong.
• When for loops are transformed by CIL, the branching node (for which the branching expression literally exists in the original source code!) has a synthetic location, because an (assert) statement cannot be inserted between the for initializer and condition.

Maybe it's something we should address separately in the future, for example by adding synthetic fields to CIL statements (such that it's explicit which Ifs were added by CIL) and variables (such that it's explicit which temporaries, etc it came up with) instead of semi-heuristics for these.

[michael-schwarz]

Yes, that sounds like a good idea. However, I'd think that we should do this in an new issue & PR.

[sim642]

Just as a post-merge note: the renaming of dbg.print_dead_code and dbg.uncalled will probably require a bunch of renaming in the bench repo as well.

[michael-schwarz]

True!

[sim642]

One last remark since this is supposed to close #94. That issue has an example program. We should check that this PR indeed fixes the problems on that example and possibly add it as a test with some // WARN.

[michael-schwarz]

It does indeed solve the issues with that example program, but currently our regression test annotations can not currently express the needed properties, so we'll have to do without automatic tests for now.