Release 2024.07.0 of the Jasmin compiler

A new major version of the Jasmin compiler has just been released. It contains some big changes, together with fixes and additions whose details can be found in the CHANGELOG. Below are a few highlights.

Arrays in the arguments and results of functions

A long-awaited feature has landed! Export functions can have reg ptr arrays as arguments and results.

Another improvement has been made regarding functions and arrays. Local functions can have reg arrays and sub-arrays as arguments and results.

Selective Speculative Load Hardening support

The compiler supports SLH operators, and a speculative constant-time checker is available. It can be called with jasmin-ct --sct.

Easy spills and unspills

Spilling and unspilling of reg and reg ptr can now be done without introducing stack variables, thanks to the #spill and #unspill operators.

More flexible parameters

The definition of parameters can now use arbitrary expressions and depend on other parameters.

Stack zeroization support

The compiler can introduce code that zeroizes the stack at the end of export functions. The user can enable the feature with an annotation or a compiler flag.

Help for debugging

Option -g adds source-code positions in the generated assembly files, which can help for debugging.

Enhancements to the support of the ARMv7 architecture

The support for the ARMv7 instruction set has been polished. In particular, some issues with large immediates have been fixed. The support for ARMv7 is still marked as experimental, but this is expected to change in the next releases.

Other noteworthy changes

Extraction to EasyCrypt for safety verification is deprecated.

The deprecated legacy interface to the CT checker has been removed.