RISC-V backlifting and examples

kth-step / HolBA

Binary analysis in HOL

Other

33 stars 20 forks source link

Closed palmskog closed 4 months ago

palmskog commented 4 months ago

This PR contains:

backlifting results for RISC-V, following those for ARMv8
fixes to the backlifting proof generation for ARMv8 (and proper name for the theory)
more RISC-V examples and results for those examples (testing backlifting)

Currently a draft because a final cheat in a test case needs to be addressed.

palmskog commented 4 months ago

No cheat anymore, can we please merge this before #173 @didriklundberg?