jasmin
jasmin copied to clipboard
Release with ARM support
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 (
LDMetc.)
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.