Global deadcode elimination for wordLang

[myreen]

The data_to_word compilation pass introduces various helper functions. Some of these are never needed because the compiled program might never use the operations that need these helpers.

A deadcode elimination pass that deletes unused code in wordLang would consist of three parts:

1. an algorithm proof for a search of all reachable function names given a next-names function (as an sptree) and start name (type :num)
2. a function that extracts the next-names sptree from a whole wordLang program
3. a proof that one can delete all unreachable function names from the code

This pass would probably be best to attach to word_to_stack. It makes sense to have this pass before stackLang so that the GC bitmaps aren't populated with unused entires.

This project could serve as a starter project for a new student.

[hrutvik]

This was largely completed some time ago (2ba5cb6355c357ce3af56dfdcb857571c9e69b8b), and then cleaned up (https://github.com/CakeML/cakeml/pull/553).

However, the optimisation is not used in the compiler. This is because:

• The proof relies on some properties of the GC (see gc_no_new_locs_def in word_elimProofScript) which were not proved at the time of completion.
• The optimisation is unlikely to have a significant impact on code quality in the CakeML compiler.

The optimisation might instead be useful for the Pancake compiler.

[hrutvik]

The optimisation could also be improved. It currently does not deal with Install functions well - if a program contains any, the elimination pass will leave it unchanged. A better way of handling this would be:

• Determine if any Install functions are reachable using the analysis pass.
• Proceed with deadcode elimination only when none can be reached.
• Otherwise leave the program unchanged.