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

[in progress] working on integrating UseImmediate optimization into Pipeline.v #340

Closed 0adb closed 1 year ago

0adb commented 1 year ago

FlatImp currently has an SOp variant in its statement datatype that could be used to compile to RISC-V immediate instructions in certain cases. Optimization to do this has been written in UseImmediate.v but proof of correctness not yet integrated into main pipeline. Example has been made in end2end/src/end2end/End2EndLightbulb.v in module PrintProgram' . Difference between RISC-V assembly produced without UseImmediate and with UseImmediate at https://www.diffchecker.com/KarK1dqd/.