Jasmin
Language reference
Syntax reference
Semantics reference
Compiler
Compilation passes
Replace word-sized integers with machine words
Array Copy
Array Init
Lowering of spills
Function Inlining
Removal of unused functions
Constant Propagation
Dead-code Elimination
Loop unrolling
Liverange splitting
Make ref arguments
Removes array-init
Expansion of register arrays
Remove global
Load constants in conditions (RISC-V)
Instruction selection
Propagate Inline
Lowering of SLH instructions
Stack allocation
Lowering of complex addressing modes (RISC-V)
Remove unused returned values
Register allocation
Merge varmaps
Linearization
Stack zeroization
Tunelling
ASM generation
Advanced details
Tools
How to compile a Jasmin program to assembly
Easycrypt extraction
Safety checker
Constant-time programming
Selective Speculative Load Hardening
How to execute the formal semantics
How to pretty-print a Jasmin program
Miscellaneous
FAQ
Emacs mode
Jasmin
Compilation passes
Linearization
Edit on GitHub
Linearization
TODO