Release 2023.06.0 of the Jasmin compiler

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

Local functions use CALL and RET instructions

Calls to local functions that expect a return address on the stack are now compiled using the standard CALL instruction rather than a direct jump. Therefore, returns from such functions are compiled using the RET instruction rather than a computed jump.

Moreover, it is now the default that local functions expect their return address on the stack. This is a breaking change: the old behavior (return address in a register; call using a direct jump; return using a computed jump) is still available using the #[returnaddress=reg] annotation.

Enhancements to the automated safety checker

The Jasmin language is rather strict regarding memory alignment. The safety checker requires user code (as opposed to code introduced by the compiler) to comply with requirements that are stricter than what microprocessors actually enforce. There is now a command-line flag to weaken these checks.

While loops may now be annotated in two ways to fine-tune the safety analysis. Loops tagged as #[bounded] will be fully unrolled at analysis time: this may improve the precision. This can prove particularly useful when loops initialize arrays. Beware that the analyzer blindly follows this hint: if no constant upper bound to the number of iteration can be found, analysis will loop forever.

The second annotation is #[no_termination_check]: to be used when the termination proof is out of reach of the automated tool.

Note that these annotations are ignored by the compiler and other tools.

Experimental support of the ARMv7 architecture

The compiler is now able to emit assembly from the ARMv7 instruction set, meaning that Jasmin programs can now be run, for instance, on Cortex-M4 microprocessors. This feature is still experimental: do not hesitate to contribute bug reports.

Changes to the semantics of shift and rotation operators

Shift and rotation operators used to truncate their second operand (the shift amount) to the word size. This behavior matches the semantics of the x86 instructions but differs from the semantics of the arm instructions.

In this version, this implicit truncation is no longer present. It is still possible to explicitly ask for the old behavior (in particular this might be required when compiling to x86) and add a bitwise AND, e.g., x <<= c & 63. Beware of the relative priorities of the shift and AND operators: parentheses are needed in instructions such as x = y << (c & 63).

Other noteworthy changes

The build system uses dune instead of ocamlbuild; this is only relevant when manually building from sources (as opposed to installing using a package manager).

The EasyCrypt library that supports verification of Jasmin programs is now distributed with the compiler.

The latex pretty-printer is now available as a separate jazz2tex binary.