jasmin icon indicating copy to clipboard operation
jasmin copied to clipboard

Release with ARM support

Open vbgl opened this issue 2 years ago • 1 comments

This gathers things to happen before a release of Jasmin with ARM support can happen.

Required

  • [ ] Extraction to EasyCrypt (#366)
    • Started: #417
    • Continued: #460
  • [ ] Fix known bugs
  • [ ] Fix add sp & sub sp.
  • [ ] Support for flags with ?{ … } syntax
    • Done: #594
  • [ ] Support for global variables
    • Started: #428
  • [ ] Ensure stack-frame allocation emits valid code
    • Started: #677

Maybe

  • [ ] Safety checker

Nice to have

  • [ ] EasyCrypt model of the ARM platform
  • [ ] Fix other issues

Out of scope

  • LibJade for ARM
  • Fancy instructions (LDM etc.)

vbgl avatar Mar 02 '23 10:03 vbgl

I tried to understand the add r, sp, #imm and sub r, sp #imm problem a bit better. It is simpler than what I explained earlier. The restriction is the following: If the output register r is sp, then imm needs to be a multiple of four. Since we need to do further computation with the value of sp, in Jasmin we don't use this case. So I believe that there is nothing to fix here. I will test more thoroughly now.

sarranz avatar May 12 '23 16:05 sarranz