mit-plv / bedrock2

A work-in-progress language and compiler for verified low-level programming
http://adam.chlipala.net/papers/LightbulbPLDI21/
MIT License
297 stars 45 forks source link

[do not merge] work-in-progress dead code elimination #348

Open 0adb opened 1 year ago

0adb commented 1 year ago

Work on implementing a compiler phase for replacing SSet's, SLit's and SOp's that target variables that are unread later in the function (or not live) with SSkip. Currently first pass of implementation is done, still need to work on proof of correctness. Attached are screenshots of diffs of assembly code in compilerExamples/deadAssExample.v img1 img2 img3