Dead code elimination transformation #850
Description
Since we know where dead code is and can output C programs via CIL, we could have a transformation that removes all the dead code from the program.
It wouldn't be super practical on real-world code as CIL also changes all the formatting, but it might be useful for debugging unsoundness on huge programs. For example, the program from #750 has both branches dead in a massive function where Graphviz gives up on the CFG:
If instead we could transform the program, it would be much easier to see, which parts of the program we consider live at all and thus where we go wrong.
Such elimination could apply to many things:
- Remove dead statements
- Remove dead functions altogether
- Remove dead (i.e. unreferenced) globals
- Remove dead (i.e. unused) types, like typedefs, struct declarations, etc.
The latter should be determined after the first two, such that dead functions wouldn't keep otherwise unused globals/types around. Cilled LDV programs in sv-benchmarks are notorious for containing large amounts of environment modeling code, which the particular benchmark doesn't actually use.